|View Issue Details [ Jump to Notes ] ||[ Issue History ] [ Print ] |
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002040||Frama-C||Plug-in > wp||public||2014-12-27 17:48||2016-01-26 08:52|
|Assigned To||correnson|| |
|Product Version||Frama-C Neon-20140301|| |
|Target Version||Fixed in Version||Frama-C Magnesium|| |
|Summary||0002040: assumes clause and labels|
|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
I remember that Kim Völlinger had observed the same(?) problem in Oxygen and
that it was fixed in Fluorine.|
|Tags||No tags attached.|
|Attached Files|| assumes_label.c [^] (1,548 bytes) 2014-12-27 17:48 [Show Content]