precondition isn't proved
ID0001109: This issue was created automatically from Mantis Issue 1109. Further discussion may take place here.
|ID0001109||Frama-C||Plug-in > jessie||public||2012-02-29||2012-03-01|
|Reporter||krvladislav||Assigned To||cmarche||Resolution||no change required|
|Product Version||Frama-C Boron-20100401||Target Version||-||Fixed in Version||-|
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 :