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