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] Jessie: Local variables leading to

> Like removing the assigns clauses, this changes the assumptions made
> by Jessie, and may make your reduced example, or indeed your real
> target program, unprovable. I am not quite competent enough to tell if
> this is the case on the reduced example.

Continuing to look at your reduced example, I added "requires
\valid(s);" as precondition of function my_changes. This is an
important part of its contract.

Writing "\old(n)" is correct in the post-condition of function
my_main, but you can also simply write "n". Even if n was modified
inside my_main, this would still, because it is in a post-condition,
designate the original value that was passed as an argument. Since
post-conditions often relate outputs of the function with the values
of the arguments that were passed to the function, this convention was
chosen for a lighter syntax.

Then, the only difficulty left is to prove that function my_main()
does not assign anything. Alt-ergo failed to prove two obligations
that were related to that property. Because the reasoning should be
rather direct (my_main only calls a function that only modifies a
pointed location, and the address passed to that function is a local
variable that does not need to appear in my_main's assigns), I am
afraid this means that some hypotheses are missing.

The file I ended up with is below.

Pascal

___


#pragma SeparationPolicy(none)

typedef struct _my_type {int i; int j;} my_type;

/*@
 requires \valid(s);
 assigns (*s);
 ensures s->i == \old(s->j);
*/
void my_changes (my_type* s){s->i = s->j;};

/*@
 assigns \result;
 ensures \result == n;
*/
int my_main (int n){
 my_type t;
 t.j=n;
 my_changes(&t);
 return t.i;
}