--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on October 2010 ---
[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;
}