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 - 2018 MantisBT Team
Powered by Mantis Bugtracker