precondition isn't proved
ID0001109: This issue was created automatically from Mantis Issue 1109. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001109 | Frama-C | Plug-in > jessie | public | 2012-02-29 | 2012-03-01 |
| Reporter | krvladislav | Assigned To | cmarche | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
There is a line: while (cur != NULL && next != NULL && cur != list->tail)
Jessie makes precondtions for these 3 conditions. The fact is all preconditions for "cur != NULL" and "next != NULL" and none of precondtions for "cur != list->tail" are proved automatically. But if I replace "cur != list->tail" by "cur != list->head" then all precondtions for it are proved too.
Additional Information :
Check attach