| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000440 | Frama-C | Plug-in > jessie | public | 2010-04-04 01:06 | 2014-02-12 16:55 | ||||
| Reporter | gava | ||||||||
| Assigned To | virgile | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Beryllium-20090902 | ||||||||
| Target Version | Fixed in Version | Frama-C Carbon-20101201-beta1 | |||||||
| Summary | 0000440: Pb with annot.c in | ||||||||
| Description | If 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 Information | The 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 ? | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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); } |
|
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;) |
|
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. |
|
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 |
| 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 |