0000426: Jessie internal error - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Tags

No tags attached.

Attached Files

crash.c [^] (303 bytes) 2010-03-12 10:44 [Show Content] [Hide Content]

typedef struct {
	int index;
    char b;
} T_S;

//@ predicate P0{L}(T_S s) = (s.b==1) ;

/*@ axiomatic Index {

logic integer f_index{L}(integer old, T_S new);

// XXX ceci fait crasher Jessie

axiom Index1{L}:
    \forall integer old, T_S new;
        P0{L}(new) ==> f_index{L}(old, new) == old;
}*/

Relationships

Notes
(0000729) signoles (manager) 2010-03-12 11:49	See this message for a workaround: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-March/001848.html

(0001323) cmarche (developer) 2010-12-16 17:37	structs as parameters to fucntions are explicitly disallowed now. the workaorund mentionned earlier should be used

Issue History
Date Modified	Username	Field	Change
2010-03-12 10:44	ddelmas	New Issue
2010-03-12 10:44	ddelmas	Status	new => assigned
2010-03-12 10:44	ddelmas	Assigned To	=> cmarche
2010-03-12 10:44	ddelmas	File Added: crash.c
2010-03-12 10:59	signoles	Relationship added	related to 0000424
2010-03-12 11:46	signoles	Relationship deleted	related to 0000424
2010-03-12 11:49	signoles	Note Added: 0000729
2010-12-16 17:37	cmarche	Note Added: 0001323
2010-12-16 17:37	cmarche	Status	assigned => resolved
2010-12-16 17:37	cmarche	Resolution	open => fixed
2010-12-18 11:18	signoles	Fixed in Version	=> Frama-C Carbon-20101202-beta2
2010-12-18 11:19	signoles	Status	resolved => closed