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: 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