Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001670Frama-CPlug-in > wppublic2014-03-04 09:362015-03-17 22:17
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001670: WP ignores some goals when 'initialized' is used in hypotheses
DescriptionThe message: [wp] warning: Allocable, Freeable, Valid_read, Fresh and Initialized not yet implemented is perfectly clear, but I would have expected that annotations using these predicates would have been ignored. Instead of that, proof obligations of other annotations simply disappear.
Steps To ReproduceExample: /*@ requires r1: \initialized(Y+(0 .. 99)); assigns X[0..99]; ensures X[0] == Y[0]; */ void cp( int *X, int *Y ); void f (int *A, int *B) { cp(B, A); /*@ assert a1: A[0] == B[0]; */ } Without the 'requires' property, the assertion is proved: $ frama-c -wp test.c -wp-prop a1 ... [wp] 1 goal scheduled [wp] [Qed] Goal typed_f_assert_a1 : Valid [wp] Proved goals: 1 / 1 Qed: 1 With the 'requires' property, the assertion is not even scheduled as a goal: $ frama-c -wp test.c -wp-prop a1 ... [wp] 0 goal scheduled [wp] Proved goals: 0 / 0
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005180)
correnson (manager)
2014-06-02 15:38

Fix committed to master branch.

- Issue History
Date Modified Username Field Change
2014-03-04 09:36 Anne New Issue
2014-03-04 09:36 Anne Status new => assigned
2014-03-04 09:36 Anne Assigned To => correnson
2014-06-02 15:38 correnson Note Added: 0005180
2014-06-02 15:38 correnson Status assigned => resolved
2014-06-02 15:38 correnson Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:17 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker