Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002040Frama-CPlug-in > wppublic2014-12-27 17:482016-01-26 08:52
Reporterjens 
Assigned Tocorrenson 
PriorityhighSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002040: assumes clause and labels
DescriptionMy 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 InformationConcerns 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.
TagsNo tags attached.
Attached Filesc file icon assumes_label.c [^] (1,548 bytes) 2014-12-27 17:48 [Show Content]

- Relationships

-  Notes
(0006007)
correnson (manager)
2015-08-19 10:38

Fixed normalization of `Here` in assumes when prepended to ensures.
(0006008)
correnson (manager)
2015-08-19 10:39

@Jens : this bug was never fixed before ; probably Kim found a workaround when working with Fluorine...

- Issue History
Date Modified Username Field Change
2014-12-27 17:48 jens New Issue
2014-12-27 17:48 jens Status new => assigned
2014-12-27 17:48 jens Assigned To => correnson
2014-12-27 17:48 jens File Added: assumes_label.c
2015-06-29 17:46 correnson Status assigned => acknowledged
2015-08-19 10:38 correnson Note Added: 0006007
2015-08-19 10:38 correnson Status acknowledged => resolved
2015-08-19 10:38 correnson Resolution open => fixed
2015-08-19 10:39 correnson Note Added: 0006008
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker