--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2019 ---
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>