--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on October 2010 ---
Hi Vergile, A 2010/10/25, ?s 09:20, Virgile Prevosto escreveu: > 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. >> } >> @*/ It worked ;-) I'm sorry, but I completely forgot the labels. > > 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. The PO are not provable now! Thank you very much for your help. Best regards, B?rbara > > Best regards, > -- > E tutto per oggi, a la prossima volta. > Virgile > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss