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