--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RTE plugin with Frama-c: “-rte-unsigned-ov” is not recognized



Hi,

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 the 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 in 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190713/b0912437/attachment-0001.html>