--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie and local variable addresses



Hi everybody,

I am currently using Jessie (with Nitrogen and Oxygen versions of Frama-C) 
to prove some stuff.
I got a problem for proving an assign clause when calling a function with 
the address of a local variable.

More precisely, I have a function comp that compares arrays of integers.
It returns an error code thus the result has to be obtained through a 
poiter parameter:
The prototype is (I removed some of the contract annotations that do not 
interfer).

//@ assigns *res
error_t comp ( const unsigned a[2], const unsigned b[2], char *res);

Then I want to use this function in another one say f and want to prove 
that f does not modify any memory location excepted the one used to call 
comp.

//@ assigns \nothing
int f(const unsigned a[2], const unsigned b[2])
{
  unsigned res = 0;
  char tmp;
  comp( a, b, &tmp);
 
 // some code here

  return res;
}

I put assigns \nothing since tmp is not visible from postconditions but 
when launching Jessie and Why3, I obtain an error:
"Unbound variable charP_tmp_8_alloc_table"

This variable is not allocated in the stack since it is a local variable 
and I assume this is the reason why there is not such variable.
Neverthelesss this variable actually appears in the VCs corresponding to 
the assigns postcondition.

Am I doing something wrong or is it something that obviously will never be 
proved and that requires some trick to get rid of?

Best,

Beno?t GERARD

[ENVOYE PAR INTERNET] 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130530/27d77c4a/attachment.html>