2021-02-27 10:20 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000426Frama-CPlug-in > jessiepublic2010-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)

See this message for a workaround:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-March/001848.html

~0001323

cmarche (developer)


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