Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000102Frama-CPlug-in > jessiepublic2009-05-27 16:342010-07-13 14:01
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0000102: Jessie: struct field's validity
Description(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.) The following annotated code can not be proved by ATPs. Function f() needs an invariant on global var v : //@ global invariant aa: \valid(&v.c); that should normally be generated automatically. Function f2() needs a type invariant : //@ type invariant Tt(las* l) = \valid(&(l->c)); but this type invariant is visibly not taken into account in the Why generated file (predicate Tt does exist but is not axiomatized). Source code: typedef struct { int c; } las; las v; //@ requires \valid(p); void g(int * p); void f(){ g(&v.c); } //@ requires \valid(x); void f2(las * x){ g(&(x->c)); } Commande line: frama-c -jessie-analysis -jessie-gui file.c
TagsNo tags attached.
Attached Files

- Relationships
related to 0000369closedcmarche Decreases clause 

-  Notes
(0001004)
boris (reporter)
2010-07-13 14:01

The same problem occurs in this code. In function bar, Jessie is unable to verify to validity of the this-pointer to object a. typedef struct _A { int x; }A; typedef struct _B { A a; }B; //@ requires \valid(this); void foo(A* this) { this->x = 0; } //@ requires \valid(this); void bar(B* this) { foo(&this->a); }

- Issue History
Date Modified Username Field Change
2009-05-27 16:34 dpariente New Issue
2009-06-05 12:31 cmarche Assigned To => cmarche
2009-06-05 12:31 cmarche Status new => acknowledged
2009-10-15 10:49 cmarche Status acknowledged => confirmed
2010-01-14 08:40 signoles Relationship added related to 0000369
2010-07-13 14:01 boris Note Added: 0001004


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker