--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on October 2010 ---
Hello Vergile, Thank you very much for your answer. It helped to clarify some concepts but I don't know if it does really work properly or not! > Then you can use (ghost) calls to the relevant functions in places where > you'd have modified the ghost variable. 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. As you suggested I have the following code (notice that this code is a small example that abstracts a bigger one): - axiomatic definition /*@ axiomatic list{ @ type list; @ logic list null; @ logic list cons(int n, list s); @ } @*/ - Declaration of the logical and ghost variables //@ ghost int var_1; /*@ axiomatic logic_var_1{ logic list logic_var_1 reads var_1; } @*/ //@ ghost int var_2; /*@ axiomatic logic_var_2{ logic list logic_var_2 reads var_2; } @*/ - C functions to map the cons operation /*@ assigns var_1; ensures logic_var_1 == cons(offset,logic_var_1); */ void append_2(int offset); /*@ assigns var_2; ensures logic_var_2 == cons(offset,logic_var_2); */ void append_2(int offset); - the C function I want to prove /*@ requires logic_var_1 == null && logic_var_2==null; */ void func(int a1, int a2){ //@ ghost append_1(1); //@ ghost append_2(1); //@ assert logic_var_1 == logic_var_2; } The provers are able to prove the property written in the assert statement. The problem is when the function code is the following (the second ghost statement adds a number 2 to the list, instead of 1) /*@ requires logic_var_1 == null && logic_var_2==null; */ void func(int a1, int a2){ //@ ghost append_1(1); //@ ghost append_2(2); //@ assert logic_var_1 == logic_var_2; } The provers are still able to prove it (notice that the second ghost statement is different from the first one). Probably I introduced some inconsistency in the code but I don't know where it is. Thank you again. Best regards, B?rbara -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101022/d8f86f8d/attachment.htm>