diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unsupported_init.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unsupported_init.res.oracle deleted file mode 100644 index de62939814872ec39bd54585f6d53d134a7c622f..0000000000000000000000000000000000000000 --- a/src/plugins/wp/tests/wp_plugin/oracle/unsupported_init.res.oracle +++ /dev/null @@ -1,30 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing tests/wp_plugin/unsupported_init.i (no preprocessing) -[wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' -[wp] Warning: Missing RTE guards -[wp] tests/wp_plugin/unsupported_init.i:1: Warning: - Allocation, initialization and danglingness not yet implemented - (r1: \initialized(Y + (0 .. 99))) ------------------------------------------------------------- - Function f ------------------------------------------------------------- - -Goal Assertion 'a1' (file tests/wp_plugin/unsupported_init.i, line 9): -tests/wp_plugin/unsupported_init.i:1: warning from wp: - - Warning: Ignored Hypothesis - Reason: Allocation, initialization and danglingness not yet implemented -(r1: \initialized(Y + (0 .. 99))) -Prove: true. - ------------------------------------------------------------- - -Goal Instance of 'Pre-condition 'r1' in 'cp'' in 'f' at call 'cp' (file tests/wp_plugin/unsupported_init.i, line 8) -: -tests/wp_plugin/unsupported_init.i:1: warning from wp: - - Warning: Target turned to False, looking for context inconsistency - Reason: Allocation, initialization and danglingness not yet implemented -(r1: \initialized(Y + (0 .. 99))) -Prove: false. - ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle deleted file mode 100644 index 4e54eed5659c716e2ab3d4c01bfe13539b9c5543..0000000000000000000000000000000000000000 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle +++ /dev/null @@ -1,18 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing tests/wp_plugin/unsupported_init.i (no preprocessing) -[wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' -[wp] Warning: Missing RTE guards -[wp] tests/wp_plugin/unsupported_init.i:1: Warning: - Allocation, initialization and danglingness not yet implemented - (r1: \initialized(Y + (0 .. 99))) -[wp] 2 goals scheduled -[wp] [Qed] Goal typed_f_assert_a1 : Valid -[wp] [Alt-Ergo] Goal typed_f_call_cp_requires_r1 : Unsuccess (Degenerated) -[wp] Proved goals: 1 / 2 - Qed: 1 - Alt-Ergo: 0 (unsuccess: 1) ------------------------------------------------------------- - Functions WP Alt-Ergo Total Success - f 1 - 2 50.0% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_plugin/unsupported_init.i b/src/plugins/wp/tests/wp_plugin/unsupported_init.i deleted file mode 100644 index 7d8a068e0a1bf7ebcdfcdab0f3189533d1e6b3fb..0000000000000000000000000000000000000000 --- a/src/plugins/wp/tests/wp_plugin/unsupported_init.i +++ /dev/null @@ -1,11 +0,0 @@ -/*@ 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]; */ -} -