--- layout: fc_discuss_archives title: Message 63 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie: Local variables leading to



Am Sonntag, 17. Oktober 2010, 18:04:06 schrieb Pascal Cuoq:
> On 10/17/10, Norbert M?ller <mueller at uni-trier.de> wrote:
> > I try to verify a C program with local variables that are passed
> > to
> > subroutines using the address operator.
> 
> Another way to nudge the Why file generation into working is
> apparently to use the following line at the top of your file:
> 
> #pragma SeparationPolicy(none)
> 
> This has the same effect as the previous, now obsolete option
> -jessie-no-regions documented in the online manual, chapter 5:
> http://frama-c.com/jessie/jessie-tutorial.pdf
> 
> (by the way there is an updated version of this manual, we just have
> to think to upload it someday)
> 
> Like removing the assigns clauses, this changes the assumptions made
> by Jessie, and may make your reduced example, or indeed your real
> target program, unprovable. I am not quite competent enough to tell if
> this is the case on the reduced example.
> 
> I do recommend that you upgrade to Why 2.27; there were a number of
> bugfixes and improvements since Why 2.24.

Thank you for pointing me to "SeparationPolicy(none)", this worked (at least 
for the example)! The example provalbe via COQ is as now as follows:

-----------------------------------------------------------
#pragma SeparationPolicy(none)
typedef struct _my_type {int i; int j;} my_type;

/*@
  requires \valid(s);
  assigns (*s);
  ensures s->i == \old(s->j);
*/
void my_changes (my_type* s){s->i = s->j;};

/*@
  assigns \result;
  ensures \result == \old(n);
*/
int my_main (int n){
  my_type t;
  t.j=n;
  my_changes(&t);
  return t.i;
}
-----------------------------------------------------------

Using Why 2.27 does not help, so I really think there still might be a bug in 
the jessie for local variables.



Verifying my own program is still on the way, and I do not know yet whether 
that will be possible. In fact, my source is a program in C++ and I do a 
manual rewrite to C first (for the main components).

One important feature of C++ are constructors/destructors. For a translation 
to C I would certainly need features like \fresh(p) and \freed(p), that are 
marked as "experimental" even in the ACSL-specification. 

Do you perhaps know whether they might be supported by jessie in the nearer 
future? 

Until then,  I will try to use axiomatic definitions like in chapter 2.6.3 of 
the ACSL-specification to define something similar to what \fresh and \freed 
should perhaps do.

Regards, and thanks for helping me,

Norbert