--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on October 2010 ---
Hello B?rbara, Le ven. 22 oct. 2010 14:32:03 CEST, Barbara Vieira <barbaraisabelvieira at gmail.com> a ?crit : > > I did as you suggested above. The problem is when I want to do some proofs with the successive changes of logical variable (I need a variable with state) I'm not able to do it. The provers are always able to prove the assertions that I include in the code even when the things to prove are wrong. Well, I warned you that this was not thoroughly tested ;-). However, I'd say that the declaration of your logic variable does not completely match what I suggested, and your issue might well lie therein: > > - Declaration of the logical and ghost variables > //@ ghost int var_1; > /*@ axiomatic logic_var_1{ > logic list logic_var_1 reads var_1; ^^^ There is an {L} missing to inform the tool that you want logic_var_1 to depend on the memory state where it is applied. > } > @*/ > > //@ ghost int var_2; > /*@ axiomatic logic_var_2{ > logic list logic_var_2 reads var_2; ^^^ Same thing with logic_var_2 of course. > } > @*/ I haven't checked whether this is sufficient to make the generated PO unprovable, but it should be a step in the good direction. Feel free to tell me if there are still some problems. Best regards, -- E tutto per oggi, a la prossima volta. Virgile