Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2357

Closed
Open
Created May 27, 2009 by Dillon Pariente@dillon

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking