--- layout: fc_discuss_archives title: Message 113 from Frama-C-discuss on September 2013 ---
Hello, 2013/9/17 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>: > After inserting the two annotations below, there were some not proved VCs > (401/405): > assigns Gbl_Eventos[9].Gbl_Ativo; There is no "Gbl_Eventos" variable in the code you sent. You probably meant: assigns Eventos[9].Ativo; > ensures (pri == 1) && (ID == 1) && (\old(Eventos[9].Ativo) == 0) && > average > 12.0 ==> Eventos[9].Ativo == 1; I cannot test as I don't have Jessie installed so take my remarks with a grain of salt. Jessie loops are somewhat "opaque", so you need to state in loop invariants properties that are true when entering the loop, even if the loop does not modify this property, e.g. "loop invariant pri == 1". The best way to debug such cases is to add various assert in your code to check that properties you think are true at a given code point are indeed seen true by Jessie (or WP or Value analysis). You can for example try to add "assert pri == 1;" before and within the for loop. I hope it helps, Best regards, david