| Anonymous | Login | Signup for a new account | This BTS is being migrated to Gitlab, consider using those issues instead |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| 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 | ||||||||||
| Platform | OS | OS Version | |||||||||||
| 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 | |||||||||||||
 Relationships |
||||||
|
||||||
 Relationships |
|
Notes |
|
|
(0004012) 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. |
|
(0004013) correnson (manager) 2013-07-30 09:51 |
Feature wish: infer workaround. |
|
(0004499) correnson (manager) 2014-02-05 14:30 |
Feature wish |
|
Notes |
|
Issue History |
|||
| 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 |
|
Issue History |
| Copyright © 2000 - 2020 MantisBT Team |
|