Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000361Frama-CPlug-in > jessiepublic2009-12-15 14:362010-04-19 16:14
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000361: "why" reports "unbound label"
Description"why" reports an "unbound label" if a C-label of a statement having more than one effect (e.g. "b[j++] = 3;") is referred to in an "\at(...)" within an acsl-assertion. See attached file "labelBug.c"; process it with and without the initial "#define showBug" uncommented.
TagsNo tags attached.
Attached Filesc file icon labelBug.c [^] (500 bytes) 2009-12-15 14:36 [Show Content]

- Relationships

-  Notes
(0000607)
cmarche (developer)
2009-12-15 14:52

In Beryllium, the CIL translation as rendered in framc-gui, is void ftest(void) { int j ; int b[10] ; int tmp ; j = 3; { /*undefined sequence*/ M: tmp = j; j ++; b[tmp] = 3; } /*@ assert (j ? \at(j,M)+1); */ ; return; } which is wrong because label is put inside a block. In current development version I get void ftest(void) { int j ; int b[10] ; int tmp ; j = 3; M: { /*undefined sequence*/ tmp = j; j ++; b[tmp] = 3; } /*@ assert (j ? \at(j,M)+1); */ ; return; } which is correct, and can be processed normally by Jessie/Why. It is definitively a Frama-C front-end bug, fortunately already fixed in development version
(0000784)
signoles (manager)
2010-04-19 16:14

Fix in Why 2.24 (require Frama-C Boron-20100401).

- Issue History
Date Modified Username Field Change
2009-12-15 14:36 Jochen New Issue
2009-12-15 14:36 Jochen Status new => assigned
2009-12-15 14:36 Jochen Assigned To => cmarche
2009-12-15 14:36 Jochen File Added: labelBug.c
2009-12-15 14:52 cmarche Note Added: 0000607
2009-12-15 14:52 cmarche Status assigned => resolved
2009-12-15 14:52 cmarche Resolution open => fixed
2010-04-19 16:13 signoles Status resolved => closed
2010-04-19 16:13 signoles Fixed in Version => Frama-C Boron
2010-04-19 16:14 signoles Note Added: 0000784


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker