Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

  • Subject: [Frama-c-discuss] RTE plugin with Frama-c: “-rte-unsigned-ov” is not recognized
  • From: syadus.sefat at gmail.com (Md. Syadus Sefat)
  • Date: Sat, 13 Jul 2019 12:23:02 -0400
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>