--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2011 ---
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) on top of every lo= op, the assertion is doubled.<br><br> i =3D (unsigned char )0;<br>&nbs= p; /*@ assert \true; */<br> /*@ assert \true; */<br> while ((in= t )i < 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--