Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Logic types and Ghost code
  • From: barbaraisabelvieira at gmail.com (Barbara Vieira)
  • Date: Fri, 22 Oct 2010 14:32:03 +0100
  • In-reply-to: <20101020133658.5c576e56@is010235>
  • References: <C03171CB-38E5-4D5B-87AA-CEC1FC9A1001@gmail.com> <20101020133658.5c576e56@is010235>
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>