Invariant used only in absence of precondition
ID0000998: This issue was created automatically from Mantis Issue 998. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000998 | Frama-C | Plug-in > Eva | public | 2011-10-23 | 2011-11-02 |
| Reporter | yakobowski | Assigned To | yakobowski | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
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); }