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