--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on June 2011 ---
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.