Frama-C Bug Tracking System - Frama-C
View Issue Details
0000039Frama-CPlug-in > jessiepublic2009-04-07 15:332009-11-24 14:14
Frama-C Lithium-20081201 
0000039: Frama-C/Jessie: memory set problem
[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/", line 716, characters 7-7: Uncaught exception: File "jc/", line 716, characters 7-13: Assertion failed Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jc
No tags attached.
has duplicate 0000106closed  Jessie: memory in memeory set 
has duplicate 0000080closed cmarche Assertion failed in 
has duplicate 0000303closed cmarche assign makes Jessie crash 
Issue History
2009-04-07 15:33virgileNew Issue
2009-04-07 15:41signolesStatusnew => acknowledged
2009-04-10 10:16signolesStatusacknowledged => assigned
2009-04-10 10:16signolesAssigned To => cmarche
2009-05-28 21:40signolesRelationship addedhas duplicate 0000106
2009-11-24 12:15signolesRelationship addedhas duplicate 0000080
2009-11-24 14:14signolesNote Added: 0000575
2009-11-24 14:14signolesStatusassigned => confirmed
2009-11-24 14:15signolesRelationship addedhas duplicate 0000303

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).