assumes clause and labels
ID0002040: This issue was created automatically from Mantis Issue 2040. Further discussion may take place here.
|ID0002040||Frama-C||Plug-in > wp||public||2014-12-27||2016-01-26|
|Product Version||Frama-C Neon-20140301||Target Version||-||Fixed in Version||Frama-C Magnesium|
My understanding of assumes clauses is that they refer to the pre-state of a function. The attached example, however, works differently. The function push_back has two disjoint behaviors that rely on the predicate "full".
The function push_back_twice is only verified if I add the label "Pre" to the predicate "full" in the assumes clauses of function push_back. I think this is a bug. It should not be necessary to add this explicit label.
Additional Information :
Concerns versions Neon-20140301 Neon-20140301+dev-stance
I remember that Kim Völlinger had observed the same(?) problem in Oxygen and that it was fixed in Fluorine.