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] Jessie and local variable addresses

  • Subject: [Frama-c-discuss] Jessie and local variable addresses
  • From: benoit.gerard at dga.defense.gouv.fr (benoit.gerard at dga.defense.gouv.fr)
  • Date: Thu, 30 May 2013 14:49:54 +0200
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>