Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • 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 209
    • Issues 209
    • 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
  • #2540

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

Jessie: memory in memeory set

ID0000106: This issue was created automatically from Mantis Issue 106. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000106 Frama-C Plug-in > jessie public 2009-05-27 2009-05-28
Reporter dpariente Assigned To - Resolution duplicate
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.)

An uncaugth exception is generated on the followin code:

typedef struct {int i;int j;} las;

/*@ requires \valid(a) && \valid(b); assigns *a, *b; */ void g (int *a,int *b){ *a=11; *b=15; }

/*@ requires \valid(p) ; assigns p->i,p->j; */ void f (las *p) { g (&(p->i), &(p->j)); }

Command line: frama-c.exe -jessie-analysis -jessie-gui foo.c

Error message: memory (mem-field(int_M),b_2) in memory set (mem-field(int_M),a_1), (mem-field(int_M),b_2) File "jc/jc_interp_misc.ml", line 714, characters 7-7: Uncaught exception: File "jc/jc_interp_misc.ml", line 714, characters 7-13: Assertion failed

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