| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000998 | Frama-C | Plug-in > Eva | public | 2011-10-23 18:50 | 2011-11-02 12:54 | ||||
| Reporter | yakobowski | ||||||||
| Assigned To | yakobowski | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | no change required | ||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||
| Target Version | Fixed in Version | ||||||||
| Summary | 0000998: Invariant used only in absence of precondition | ||||||||
| Description | In the code below, analyzed using frama-c -val, the access *adr is proven valid only in the absence of requires. /*@ requires count > 0; */ void bla(char * adr, int count) { //@ loop invariant \at(adr,Pre) <= adr < \at(adr,Pre)+\at(count,Pre); do { int v = *adr; adr++; } while (--count); } char t[42]; void main () { bla(t+28, 14); } | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
 Notes |
|
|
yakobowski (manager) 2011-11-02 12:54 Last edited: 2011-11-02 12:54 |
Cannot reproduce as is. Adding behaviors exhibits the bug: /*@ behavior pos: assumes count > 0; */ void bla(char * adr, int count) { //@ for pos: loop invariant \at(adr,Pre) <= adr < \at(adr,Pre)+\at(count,Pre); do { Frama_C_show_each(adr); int v = *adr; adr++; } while (--count); } char t[42]; void main () { bla(t+28, 14); } However, this is the expected behavior. Since pos is not necessarily the only possible behavior, we cannot reduce by it on the loop invariant. With a "complete behaviors pos;" clause, the loop invariant is used as intended. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-10-23 18:50 | yakobowski | New Issue | |
| 2011-10-23 18:50 | yakobowski | Status | new => assigned |
| 2011-10-23 18:50 | yakobowski | Assigned To | => pascal |
| 2011-10-23 18:50 | yakobowski | Assigned To | pascal => yakobowski |
| 2011-11-02 12:54 | yakobowski | Note Added: 0002440 | |
| 2011-11-02 12:54 | yakobowski | Note Edited: 0002440 | |
| 2011-11-02 12:54 | yakobowski | Status | assigned => closed |
| 2011-11-02 12:54 | yakobowski | Resolution | open => no change required |
| 2011-11-02 13:09 | yakobowski | Relationship added | related to 0001006 |
| 2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |
| Issue History |