assumes clause and labels
ID0002040: This issue was created automatically from Mantis Issue 2040. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002040 | Frama-C | Plug-in > wp | public | 2014-12-27 | 2016-01-26 |
| Reporter | jens | Assigned To | correnson | Resolution | fixed |
| Priority | high | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | Frama-C Magnesium |
Description :
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.