2020-12-05 00:56 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001740Frama-CPlug-in > E-ACSLpublic2017-05-31 19:05
Reportersignoles 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C 15-Phosphorus 
Summary0001740: Incorrectness when early exiting a block
DescriptionLocal variables of a block are de-allocated at the end of the block. However, they are not de-allocated when exiting a block earlier (e.g. by a goto or a break). That may lead to incorrectness as in the attached example.

$ frama-c -e-acsl a.i -then-on e-acsl -print -ocode b.i
$ ./gcc.sh b.i
compiling b.i
executing b.i
Assertion failed at line 13 in function main.
The failing predicate is:
!\valid(p).

No error should be detected.
TagsNo tags attached.
Attached Files
  • ? file icon a.i (156 bytes) 2014-04-07 13:57 -
    int main(void) {
    
      int *p;
      
      {
        int a = 0;
        p = &a;
        /*@ assert \valid(p); */
        goto L;
      }
    
     L:
      /*@ assert ! \valid(p); */
    
      return 0;
    }
    
    ? file icon a.i (156 bytes) 2014-04-07 13:57 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2014-04-07 13:57 signoles New Issue
2014-04-07 13:57 signoles Status new => assigned
2014-04-07 13:57 signoles Assigned To => signoles
2014-04-07 13:57 signoles File Added: a.i
2014-04-07 13:57 signoles Status assigned => confirmed
2017-03-02 15:18 kvorobyov Status confirmed => resolved
2017-03-02 15:18 kvorobyov Resolution open => fixed
2017-05-31 19:04 signoles Fixed in Version => Frama-C 15-Phosphorus
2017-05-31 19:05 signoles Status resolved => closed
+Issue History