2021-03-02 03:17 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000404Frama-CPlug-in > jessiepublic2014-02-12 16:56
Reporterddelmas 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000404: Jessie translation unexpected failure
DescriptionWith WHY 2.21 or 2.23, "frama-c -jessie test.c" crashes on the attached test.c source file.
Additional InformationThe command-line output is :

[kernel] preprocessing with "gcc -C -E -I. -dD test.c"
[jessie] Starting Jessie translation
test.c:3:[jessie] failure: Unexpected failure.
                  Please submit bug report (Ref. "norm.ml:465:31").
[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 test.c (366 bytes) 2010-02-11 17:24 -
    typedef struct abstract_seq_call {int bidon;} SEQ_CALL;
    
    /*@ axiomatic Seq_call {
      @     logic SEQ_CALL nocall ;
      @     logic SEQ_CALL callto(integer call_id) ;
      @     logic SEQ_CALL addcallto(SEQ_CALL seq, integer call_id) ;
      @
      @     axiom A: 
      @       \forall integer id ;
      @       callto(id)==addcallto(nocall,id);
      @ }
      @*/
    
    int main(void) {return 0;}
    
    c file icon test.c (366 bytes) 2010-02-11 17:24 +

-Relationships
+Relationships

-Notes

~0001324

cmarche (developer)


structs should be passed as struct*
+Notes

-Issue History
Date Modified Username Field Change
2010-02-11 17:24 ddelmas New Issue
2010-02-11 17:24 ddelmas Status new => assigned
2010-02-11 17:24 ddelmas Assigned To => cmarche
2010-02-11 17:24 ddelmas File Added: test.c
2010-12-16 17:38 cmarche Note Added: 0001324
2010-12-16 17:38 cmarche Status assigned => resolved
2010-12-16 17:38 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
2013-12-19 01:14 Source_changeset_attached => framac master 61c9f390
2014-02-12 16:56 Source_changeset_attached => framac stable/neon 61c9f390
+Issue History