View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0001461 | Frama-C | Plug-in > wp | public | 2013-07-24 18:36 | 2014-06-17 15:02 | ||||||||
Reporter | virgile | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | acknowledged | Resolution | open | ||||||||||
Product Version | Frama-C GIT, precise the release id | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0001461: assigns, loop assigns and loop invariant | ||||||||||||
Description | In the following (admittedly contrived) example, the assigns of g is not proved by WP (in fact it is reduced to false by Qed), although it is correct from ACSL semantics: as long as the loop invariant states that x still has its old value, the fact that it is mentioned in the loop assigns should not impede its absence in the assigns. --- test.c int x; /*@ assigns \nothing; */ int g() { /*@ loop assigns i,x; loop invariant x == \at(x,Pre); */ for (int i = 0; i<2; i++); return x; } | ||||||||||||
Steps To Reproduce | frama-c -wp test.c | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
||||||
|
![]() |
|
correnson (manager) 2013-07-30 09:50 |
This is known limitation of the WP. Assigns are verified with a stronger method than necessary: WP checks that all effects are included in the assigns specified, which is sufficient but not necessary. The workaround is to modify the contract with: /*@ assigns x; ensures x ==\old(x); */ int g() { /*@ loop assigns i,x; loop invariant x == \at(x,Pre); */ for (int i = 0; i<2; i++); return x; } An evolution of the WP may infer automatically this workaround. |
correnson (manager) 2013-07-30 09:51 |
Feature wish: infer workaround. |
correnson (manager) 2014-02-05 14:30 |
Feature wish |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2013-07-24 18:36 | virgile | New Issue | |
2013-07-24 18:36 | virgile | Status | new => assigned |
2013-07-24 18:36 | virgile | Assigned To | => correnson |
2013-07-30 09:50 | correnson | Note Added: 0004012 | |
2013-07-30 09:51 | correnson | Note Added: 0004013 | |
2013-07-30 09:51 | correnson | Status | assigned => confirmed |
2014-02-05 14:30 | correnson | Note Added: 0004499 | |
2014-02-05 14:30 | correnson | Status | confirmed => acknowledged |
2014-06-17 11:02 | correnson | Relationship added | related to 0001812 |