Jessie: struct field's validity
ID0000102: This issue was created automatically from Mantis Issue 102. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000102 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2010-07-13 |
| Reporter | dpariente | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
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