2021-03-02 03:35 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000434Frama-CPlug-in > jessiepublic2010-12-18 11:19
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000434: assertion at line 2772 of jc/jc_typing.ml fails
Description(Similar to report 432; Virgile encouraged me to resubmit:)

Calling the unix command
<<frama-c -jessie -jessie-no-regions -jessie-why-opt="-exp goal"
-jessie-atp simplify ftest.c>>
causes the assertion in the jessie source file jc/jc_typing.ml, line 2772:25-31 to fail.

The error vanishes if I delete the subformula
<<\base_addr(f) == \base_addr(b) &&>>
in line 12 of the attached file ftest.c.
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (338 bytes) 2010-03-25 14:34 -
    #define NULL		((void*)0)
    
    struct _cell { struct _cell *nxt; }; 
    
    // define linked-list property:
    /*@ axiomatic a1 {
        logic boolean isList{L}(struct _cell *b,struct _cell *f);
        axiom a2{L}:
    	\forall struct _cell *b, struct _cell *f; isList(b,f) <==>
    	    f == NULL || 
    	    \base_addr(f) == \base_addr(b) && isList(b,f->nxt);
    }
    */
    
    
    c file icon ftest.c (338 bytes) 2010-03-25 14:34 +

-Relationships
+Relationships

-Notes

~0001321

cmarche (developer)


Fixed in Why 2.28
+Notes

-Issue History
Date Modified Username Field Change
2010-03-25 14:34 Jochen New Issue
2010-03-25 14:34 Jochen Status new => assigned
2010-03-25 14:34 Jochen Assigned To => cmarche
2010-03-25 14:34 Jochen File Added: ftest.c
2010-12-16 17:28 cmarche Note Added: 0001321
2010-12-16 17:28 cmarche Status assigned => resolved
2010-12-16 17:28 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