Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000106Frama-CPlug-in > jessiepublic2009-05-27 16:372009-05-28 21:40
Reporterdpariente 
Assigned To 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionduplicate 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0000106: Jessie: memory in memeory set
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
TagsNo tags attached.
Attached Files

- Relationships
duplicate of 0000039confirmedcmarche Frama-C/Jessie: memory set problem 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-05-27 16:37 dpariente New Issue
2009-05-28 21:40 signoles Relationship added duplicate of 0000039
2009-05-28 21:40 signoles Status new => closed
2009-05-28 21:40 signoles Resolution open => duplicate


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker