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.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information