2021-02-27 10:20 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000426Frama-CPlug-in > jessiepublic2010-03-12 10:442010-12-18 11:19
Reporterddelmas 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000426: Jessie internal error
DescriptionRunning 'frama-c -jessie crash.c' on the attached source file (with either Why 2.21 or 2.23) crashes Jessie :

[kernel] preprocessing with "gcc -C -E -I. -dD crash.c"
[jessie] Starting Jessie translation
crash.c:8:[jessie] failure: Unexpected failure.
                  Please submit bug report (Ref. "norm.ml:1122:50").
[kernel] Plugin jessie aborted because of an internal error.
         Please report with 'crash' at http://bts.frama-c.com
TagsNo tags attached.
Attached Files
  • c file icon crash.c (303 bytes) 2010-03-12 10:44 - 
    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;
}*/
    c file icon crash.c (303 bytes) 2010-03-12 10:44 +

-Relationships
+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
+Notes

-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
+Issue History