Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000039Frama-CPlug-in > jessiepublic2009-04-07 15:332009-11-24 14:14
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000039: Frama-C/Jessie: memory set problem
Description[bug 7548 from old bts, reported by Dillon Pariente]
Hello,

(Issue already sent to discussion-list, and now registred into the BTS! Sorry for this "duplication".)

Launching:
    frama-c.byte.exe -jessie-analysis -jessie-gen-goals foo.c

with foo.c containing:

//*****************************************
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)); }
//*****************************************

returns the following error (Jessie/Why version is 2.18):

memory (mem-field(int_M),b_21)
in memory set (mem-field(int_M),a_20),
(mem-field(int_M),b_21)
File "jc/jc_interp_misc.ml", line 716, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 716, characters 7-13: Assertion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jc

TagsNo tags attached.
Attached Files

- Relationships
has duplicate 0000106closed Jessie: memory in memeory set 
has duplicate 0000080closedcmarche Assertion failed in jc_interp_misc.ml 
has duplicate 0000303closedcmarche assign makes Jessie crash 

-  Notes
(0000575)
signoles (manager)
2009-11-24 14:14

With Frama-C Beryllium 2, use the following command line:
$ frama-c.byte.exe -jessie foo.c

In Why 2.22, it will now pass the jessie phase but yields an invalid Why file
(application creates an alias).

- Issue History
Date Modified Username Field Change
2009-04-07 15:33 virgile New Issue
2009-04-07 15:41 signoles Status new => acknowledged
2009-04-10 10:16 signoles Status acknowledged => assigned
2009-04-10 10:16 signoles Assigned To => cmarche
2009-05-28 21:40 signoles Relationship added has duplicate 0000106
2009-11-24 12:15 signoles Relationship added has duplicate 0000080
2009-11-24 14:14 signoles Note Added: 0000575
2009-11-24 14:14 signoles Status assigned => confirmed
2009-11-24 14:15 signoles Relationship added has duplicate 0000303


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker