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] Ghost variables and function prototypes

  • Subject: [Frama-c-discuss] Ghost variables and function prototypes
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Fri, 18 Feb 2011 15:07:08 +0100 (CET)
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