--- layout: fc_discuss_archives title: Message 63 from Frama-C-discuss on October 2010 ---
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