WP ignores some goals when 'initialized' is used in hypotheses
ID0001670: This issue was created automatically from Mantis Issue 1670. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001670 | Frama-C | Plug-in > wp | public | 2014-03-04 | 2015-03-17 |
| Reporter | Anne | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Sodium |
Description :
The 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 Reproduce :
Example: /*@ 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