RTE plugin with Frama-c: "-rte-unsigned-ov" is not recognized

Question

I am new to frama-c. I'm trying to generate annotation using rte plugin. By looking into the link [1], I tried generating annotation by using the command:

frama-c -rte -rte-unsigned-ov test.c

Where my test.c contains

int main(void){
  signed char cx, cy, cz;
  cz = cx + cy;
  return 0;
}

I have copied the code from [2] section 2.1.2. I was hoping that rte will generate the following annotations and modify my test.c file:

/*@ assert rte: signed_overflow: -2147483648 <= (int)cx+(int)cy; */
/*@ assert rte: signed_overflow: (int)cx+(int)cy <= 2147483647; */

But instead, it didn't generate any annotations (did not modify test.c) and furthermore, frama-c could not detect option "-rte-unsigned-ov". It shows me

[kernel] User Error: option `-rte-unsigned-ov' is unknown.

I also tried the command "frama-c -rte test.c" but didn't get the annotations generated. I have tried with both 19.0 and 18.0 versions of frama-c.

It would be really nice if somebody can help me find out what I am missing. Thanks.

[1] https://frama-c.com/rte.html

[2] https://frama-c.com/download/frama-c-rte-manual.pdf

byako byako · Accepted Answer · 2019-07-16T09:36:57

There are two problems here, one in your understanding of what Frama-C would do, and one in the documentation available at https://frama-c.com/rte.html.

Let's start by the second point: the documentation is outdated, and you should probably open an issue at https://github.com/Frama-C/Frama-C-snapshot/issues. The RTE manual gives you the new name of the option in Section 2.3, namely -warn-unsigned-overflow.

For the second point, Frama-C will never modify your input files. Instead, you can ask it to pretty-print back the code source it has parsed using option -print. You can furthermore redirect this result into one file using option -ocode <file>. You must do this after the RTE plugin has run, hence the need for the -then operator.

Thus, your full command-line should be

frama-c test.c -rte -warn-unsigned-overflow -then -print -ocode <yourfile>

RTE plugin with Frama-c: "-rte-unsigned-ov" is not recognized

1 Answers