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]

No subject

from the late, gets the body.
Gives the body to a private method (not overriding the vstmt_aux) and adds =
assertion to the loop.=20

Even if I try and print things, everything is doubled.
I tested with other stmts, and I get the same result.

Can you help me find out where it can possibly come from?

Thank you so much for your help.

Hichem Zakaria Chihani.

--0-601468404-1307494111=:7507
Content-Type: text/html; charset=iso-8859-1
Content-Transfer-Encoding: quoted-printable

<table cellspacing=3D"0" cellpadding=3D"0" border=3D"0" ><tr><td valign=3D"=
top" style=3D"font: inherit;">Hello everyone,<br><br>I still am working on =
the CerCo plugin, and while treating loops, something odd happens.<br><br>T=
rying to add a simple annotation (e.g assert true)&nbsp; on top of every lo=
op, the assertion is doubled.<br><br>&nbsp;i =3D (unsigned char )0;<br>&nbs=
p; /*@ assert \true; */<br>&nbsp; /*@ assert \true; */<br>&nbsp; while ((in=
t )i &lt; 17) {...<br><br>I can't figure out where it comes from, so here's=
 what the program does:<br><br>Override vspec.<br>From vspec, gets the curr=
ent kf.<br>from the late, gets the body.<br>Gives the body to a private met=
hod (not overriding the vstmt_aux) and adds assertion to the loop. <br><br>=
Even if I try and print things, everything is doubled.<br>I tested with oth=
er stmts, and I get the same result.<br><br>Can you help me find out where =
it can possibly come from?<br><br>Thank you so much for your help.<br><br>H=
ichem
 Zakaria Chihani.<br></td></tr></table>
--0-601468404-1307494111=:7507--