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 - [assumes_label.c](/uploads/c4f41bff0222c51c966f982647981368/assumes_label.c)