--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on February 2011 ---
In the following code, I use a ghost variable foo_result to express a specification on the return value of function foo. If I don't specify assigns foo_result; in the contract of foo, the code verifies. //@ ghost int foo_result; //@ ensures foo_result == \result; int foo(); void bar() { int k = foo(); int l = foo(); //@ assert k == foo_result; } Since foo may be impure, the assertion in bar doesn't have to hold. However, shouldn't Jessie automatically deduce from foo's postcondition that foo may modify foo_result? In the code below, foo is annotated with assigns foo_result; and a function foobar is called after foo is called in bar. //@ ghost int foo_result; /*@ assigns foo_result; ensures foo_result == \result; */ int foo(); int foobar(); void bar() { int k = foo(); int l = foobar(); //@ assert k == foo_result; } Again, the assertion in bar doesn't have to hold as foobar may call foo. Indeed, this code doesn't verify: //@ ghost int foo_result; /*@ assigns foo_result; ensures foo_result == \result; */ int foo(); int foobar() { return foo(); } void bar() { int k = foo(); int l = foobar(); //@ assert k == foo_result; } However, the definition of a function is not visible if the code is organized in source and header files. Is this a source of unsoundness? -- Regards, Boris