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

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



Hello, I'm getting answers of questions asked after mine, so I suppose my mail got lost in a spam filter or something.

Here is my initial message : 


Thank you.

Chihani Hichem Zakaria.


----- Mail transf?r? -----
De?: zakaria chihani <uaz11 at yahoo.fr>
??: "frama-c-discuss-request at lists.gforge.inria.fr" <frama-c-discuss at lists.gforge.inria.fr>
Envoy? le : Mercredi 8 Juin 2011 2h48
Objet?: 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.