--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2011 ---
[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--