--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Ghost variables and function prototypes



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