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
Assigned Tocorrenson 
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
correnson (manager)
2015-08-19 10:38

Fixed normalization of `Here` in assumes when prepended to ensures.
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker