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
- Subject: [Frama-c-discuss] Jessie: Local variables leading to
- From: mueller at uni-trier.de (Norbert Mueller)
- Date: Thu, 21 Oct 2010 13:55:42 +0200
- In-reply-to: <AANLkTimedC0EbbRomeYC9e3qPyF4WX3qckFRCEtKEXec@mail.gmail.com>
- References: <201010171700.49736.mueller@uni-trier.de> <AANLkTimedC0EbbRomeYC9e3qPyF4WX3qckFRCEtKEXec@mail.gmail.com>
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
- References:
- [Frama-c-discuss] Jessie: Local variables leading to
- From: mueller at uni-trier.de (Norbert Müller)
- [Frama-c-discuss] Jessie: Local variables leading to
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Jessie: Local variables leading to
- Prev by Date: [Frama-c-discuss] Logic types and Ghost code
- Next by Date: [Frama-c-discuss] Logic types and Ghost code
- Previous by thread: [Frama-c-discuss] Jessie: Local variables leading to
- Next by thread: [Frama-c-discuss] a value analysis case studie
- Index(es):