--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plugin development >> Going through loops twice.



Hello everyone,

I still am working on the CerCo plugin, and while treating loops, something odd happens.

Trying to add a simple annotation (e.g assert true)? on top of every loop, the assertion is doubled.

?i = (unsigned char )0;
? /*@ assert \true; */
? /*@ assert \true; */
? while ((int )i < 17) {...

I can't figure out where it comes from, so here's what the program does:

Override vspec.