Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000440Frama-CPlug-in > jessiepublic2010-04-04 01:062014-02-12 16:55
Reportergava 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000440: Pb with annot.c in
DescriptionIf you use

frama-c -jessie annot.c
where annot.c (from /test/cil.) ==

int fact(int n) {
  int r = 1 ;
  while ( n > 0 ) {
    //@ assert n > 0 ;
  before:
    r *= n-- ;
    //@ assert r == \at(r*n,before) ;
  }
  return r ;
}


Computation of VCs...
File "why/annot.why", line 410, characters 74-82:
Unbound label 'before'

(which is true when looking the file)
Additional InformationThe bug does not show up if the first assert is removed. So it seems the first assert "enclosed" the statement "before: r *= n-- ;"

Which means that the problem might come from the Frama-C parser itself, which might have built a wrong AST.

Virgile, any thoughts ?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000821)
monate (reporter)
2010-05-10 16:47

 This is a bug of the AST elaboration. "frama-c -print -debug 1" outputs incorrectly imbricated blocks.

int fact(int n )
{
  int r ;
  int tmp ;
  /*sid:1*/
  r = 1;
  /*sid:2*/
  while (1) {
    /*sid:4*/
    if (n > 0) { }
    else { /*sid:5*/ break; }
    /*sid:6*/
    /*@ assert (n > 0); */ ;
    /*sid:7*/
    {
      /* */
      before: /*sid:8*/
      { /*undefined sequence*/
        /*sid:9*/
        /*block:begin*/ {
                          /* */
                          /*sid:10*/ tmp = n;
                          /*sid:11*/ n -= 1; }
          
        /*block:end*/
        /*effects: n <- */
        /*sid:12*/
        r *= tmp;
        /*effects: r <- tmp*/
      }
    }
    
    /*sid:13*/
    /*@ assert (r ? \at(r*n,before)); */ ;
  }
  /*sid:14*/
  return (r);
}
(0000829)
virgile (developer)
2010-05-11 16:12

 It's not incorrect. The annotation is tied to the next statement, which happens to be split by CIL, and is thus enclosed in a block to preserve its semantics (not a problem for assert, but with an ensures you definitely do not want it to be tied to tmp = n;)
(0000831)
monate (reporter)
2010-05-12 00:45

 I think you may have lissed the point. Annotation in sid 13 refers to a label "before" in sid 8. But the scoping rule of logic label prevents sid 13 from mentioning a label _inside_ sid 7. By the way the output is not parsable: this really seems to be a bug.
(0000893)
virgile (developer)
2010-06-02 11:18

 A fix is about to be commited, but this slightly changes how annotations are handled wrt labels. See http://bts.frama-c.com/wiki.php?id=440 [^] for more information/discussion

- Issue History
Date Modified Username Field Change
2010-04-04 01:06 gava New Issue
2010-04-04 01:06 gava Status new => assigned
2010-04-04 01:06 gava Assigned To => cmarche
2010-04-06 10:27 cmarche Additional Information Updated
2010-05-10 16:45 monate Assigned To cmarche => virgile
2010-05-10 16:47 monate Note Added: 0000821
2010-05-11 16:12 virgile Note Added: 0000829
2010-05-12 00:45 monate Note Added: 0000831
2010-06-02 11:18 virgile Note Added: 0000893
2010-06-02 11:45 svn Checkin
2010-06-02 11:45 svn Status assigned => resolved
2010-06-02 11:45 svn Resolution open => fixed
2010-12-10 15:47 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-10 15:47 signoles Additional Information Updated
2010-12-17 19:35 signoles Status resolved => closed

Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker