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: Claude.Marche at inria.fr (Claude Marché)
  • Date: Tue, 04 Jun 2013 14:06:46 +0200
  • In-reply-to: <OFAC6BDFDF.A039F7DE-ONC1257B7B.004674B7-C1257B7B.00467C4C@dga.defense.gouv.fr>
  • References: <OFAC6BDFDF.A039F7DE-ONC1257B7B.004674B7-C1257B7B.00467C4C@dga.defense.gouv.fr>
Hi,

You did not make anything wrong, but you face some bug in the handling
of local variables whose adress is taken in the separation analysis
performed by Jessie.

One workaround is to disable this analysis, using

#pragma SeparationPolicy(none)

The drawback is that it may complicate other VCs, but in that particular
case it would allow proving the code you gave.

Hope this helps,


- Claude


Le 30/05/2013 14:49, benoit.gerard at dga.defense.gouv.fr a ?crit :
> 
> 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]
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> 

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |