assumes clause and labels
ID0002040: This issue was created automatically from Mantis Issue 2040. Further discussion may take place here.
|Plug-in > wp
|Fixed in Version
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.