2021-03-01 04:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000440Frama-CPlug-in > jessiepublic2014-02-12 16:55
Reportergava 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0000821

monate (reporter)

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)

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)

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)

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
+Notes

-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
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
2013-12-19 01:13 Source_changeset_attached => framac master 8ed21ff3
2014-02-12 16:55 Source_changeset_attached => framac stable/neon 8ed21ff3
+Issue History