--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Logic types and Ghost code



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>