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.
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>