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 - 2018 MantisBT Team
Powered by Mantis Bugtracker