From b945d946f185cac112a77c1383953a8a2b5b1eb3 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 10 Feb 2022 17:24:56 +0100
Subject: [PATCH] [tests] restore ./src/plugin/wp/tests from master
---
.../tests/wp/oracle/wp_call_pre.4.res.oracle | 9 -
src/plugins/wp/tests/wp_plugin/combined.c | 4 +-
.../tests/wp_plugin/oracle/dynamic.res.oracle | 394 ------------------
.../wp/tests/wp_plugin/oracle/stmt.res.oracle | 141 -------
.../wp_plugin/oracle/unsigned.res.oracle | 18 -
.../wp_plugin/oracle_qualif/bool.0.res.oracle | 25 --
.../wp/tests/wp_plugin/oracle_qualif/stmt.log | 21 -
.../wp_plugin/oracle_qualif/stmt.res.oracle | 114 -----
src/plugins/wp/tests/wp_plugin/stmt.c | 63 ---
.../oracle_qualif/user_init.res.oracle | 22 -
.../tests/wp_usage/oracle/core.0.res.oracle | 54 ---
.../tests/wp_usage/oracle/core.1.res.oracle | 46 --
.../tests/wp_usage/oracle/save_load.sav.err | 0
13 files changed, 2 insertions(+), 909 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle/unsigned.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/stmt.c
delete mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle
create mode 100644 src/plugins/wp/tests/wp_usage/oracle/save_load.sav.err
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle
deleted file mode 100644
index 9f092860709..00000000000
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-# frama-c -wp -wp-model 'Hoare' [...]
-[kernel] Parsing wp_call_pre.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-
-Goal Pre-condition 'qed_ok,Rstmt' at instruction (file wp_call_pre.c, line 47):
-Prove: true.
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/combined.c b/src/plugins/wp/tests/wp_plugin/combined.c
index 8850cc07bd8..33a5d1e193a 100644
--- a/src/plugins/wp/tests/wp_plugin/combined.c
+++ b/src/plugins/wp/tests/wp_plugin/combined.c
@@ -3,8 +3,8 @@
*/
/* run.config_qualif
- MODULE: @PTEST_NAME@
- OPT: -wp-par 1
+ EXECNOW: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -wp-par 1 -load-module @PTEST_DIR@/@PTEST_NAME@
*/
/* ZD : this should not be here such as it cannot be tested by all frama-c
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
deleted file mode 100644
index cd32ffa297b..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ /dev/null
@@ -1,394 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing dynamic.i (no preprocessing)
-[wp] Running WP plugin...
-[wp:calls] Computing dynamic calls.
-[wp] dynamic.i:30: Calls f1 f2
-[wp] dynamic.i:44: Calls g
-[wp] dynamic.i:65: Calls h1 h2
-[wp] dynamic.i:78: Calls (for bhv1) h1 h2 h0
-[wp] dynamic.i:78: Calls (for bhv0) h1 h2 h0
-[wp] dynamic.i:87: Calls h1
-[wp] dynamic.i:100: Calls unreachable_g
-[wp:calls] Dynamic call(s): 6.
-[wp] dynamic.i:78: Warning: Missing 'calls' for default behavior
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function behavior with behavior bhv1
-------------------------------------------------------------
-
-Goal Call point h1 h2 in 'behavior' at instruction (file dynamic.i, line 65):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition for 'bhv1' (file dynamic.i, line 62) in 'behavior' (1/2):
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition for 'bhv1' (file dynamic.i, line 62) in 'behavior' (2/2):
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 61) in 'behavior' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 61) in 'behavior' (2/2):
-Call Effect at line 65
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 61) in 'behavior' (1/4):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 61) in 'behavior' (2/4):
-Call Effect at line 65
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 61) in 'behavior' (3/4):
-Call Result at line 65
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 61) in 'behavior' (4/4):
-Call Result at line 65
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function call
-------------------------------------------------------------
-
-Goal Call point f1 f2 in 'call' at instruction (file dynamic.i, line 30):
-Let a = Mptr_0[shiftfield_F1_S_f(closure_0)].
-Let a_1 = global(G_f2_30).
-Let a_2 = global(G_f1_22).
-Let x = Mint_0[shiftfield_F1_S_param(closure_0)].
-Assume {
- Type: is_sint32(x).
- (* Heap *)
- Type: (region(closure_0.base) <= 0) /\ framed(Mptr_0).
- (* Pre-condition *)
- Have: (a = a_1) \/ ((a = a_2) /\ (abs_int(x) <= 5)).
-}
-Prove: (a = a_2) \/ (a = a_1).
-
-------------------------------------------------------------
-
-Goal Post-condition (file dynamic.i, line 26) in 'call' (1/2):
-Tags: Call f1.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file dynamic.i, line 26) in 'call' (2/2):
-Tags: Call f2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Instance of 'Pre-condition (file dynamic.i, line 10) in 'f1'' in 'call' at instruction (file dynamic.i, line 30)
-:
-Tags: Call f1.
-Let x = Mint_0[shiftfield_F1_S_param(closure_0)].
-Assume {
- Type: is_sint32(x).
- (* Heap *)
- Type: (region(closure_0.base) <= 0) /\ framed(Mptr_0).
- (* Pre-condition *)
- Have: abs_int(x) <= 5.
- (* Instance of 'f1' *)
- (* Call point f1 f2 *)
- Have: Mptr_0[shiftfield_F1_S_f(closure_0)] = global(G_f1_22).
-}
-Prove: ((-10) <= x) /\ (x <= 10).
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function guarded_call
-------------------------------------------------------------
-
-Goal Call point g in 'guarded_call' at instruction (file dynamic.i, line 44):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file dynamic.i, line 38) in 'guarded_call' (1/2):
-Assume {
- Type: is_sint32(X).
- (* Heap *)
- Type: (region(p.base) <= 0) /\ framed(Mptr_0).
- (* Goal *)
- When: Mptr_0[shiftfield_F1_S_f(p)] = global(0).
- (* Else *)
- Have: G_g_48 = 0.
-}
-Prove: X = 1.
-
-------------------------------------------------------------
-
-Goal Post-condition (file dynamic.i, line 38) in 'guarded_call' (2/2):
-Tags: Call g.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file dynamic.i, line 39) in 'guarded_call' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file dynamic.i, line 39) in 'guarded_call' (2/2):
-Tags: Call g.
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function missing_context
-------------------------------------------------------------
-
-Goal Call point h1 in 'missing_context' at instruction (file dynamic.i, line 87):
-Assume { (* Heap *) Type: region(p.base) <= 0. }
-Prove: global(G_h1_61) = p.
-
-------------------------------------------------------------
-
-Goal Post-condition (file dynamic.i, line 82) in 'missing_context':
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file dynamic.i, line 83) in 'missing_context':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file dynamic.i, line 83) in 'missing_context' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file dynamic.i, line 83) in 'missing_context' (2/2):
-Call Result at line 87
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function no_call
-------------------------------------------------------------
-
-Goal Call point unreachable_g in 'no_call' at instruction (file dynamic.i, line 100):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file dynamic.i, line 94) in 'no_call' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file dynamic.i, line 94) in 'no_call' (2/2):
-Tags: Call unreachable_g.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Instance of 'Pre-condition (file dynamic.i, line 91) in 'unreachable_g'' in 'no_call' at instruction (file dynamic.i, line 100)
-:
-Tags: Call unreachable_g.
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function some_behaviors with behavior bhv0
-------------------------------------------------------------
-
-Goal Call point h1 h2 h0 for bhv0 in 'some_behaviors' at instruction (file dynamic.i, line 78):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition for 'bhv0' (file dynamic.i, line 75) in 'some_behaviors' (1/3):
-Tags: Call h0.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition for 'bhv0' (file dynamic.i, line 75) in 'some_behaviors' (2/3):
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition for 'bhv0' (file dynamic.i, line 75) in 'some_behaviors' (3/3):
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv0' nothing in 'some_behaviors' (1/3):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv0' nothing in 'some_behaviors' (2/3):
-Call Effect at line 78
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv0' nothing in 'some_behaviors' (3/3):
-Call Effect at line 78
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv0' nothing in 'some_behaviors' (1/6):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv0' nothing in 'some_behaviors' (2/6):
-Call Effect at line 78
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv0' nothing in 'some_behaviors' (3/6):
-Call Effect at line 78
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv0' nothing in 'some_behaviors' (4/6):
-Call Result at line 78
-Tags: Call h0.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv0' nothing in 'some_behaviors' (5/6):
-Call Result at line 78
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv0' nothing in 'some_behaviors' (6/6):
-Call Result at line 78
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function some_behaviors with behavior bhv1
-------------------------------------------------------------
-
-Goal Call point h1 h2 h0 for bhv1 in 'some_behaviors' at instruction (file dynamic.i, line 78):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition for 'bhv1' (file dynamic.i, line 71) in 'some_behaviors' (1/3):
-Tags: Call h0.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition for 'bhv1' (file dynamic.i, line 71) in 'some_behaviors' (2/3):
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition for 'bhv1' (file dynamic.i, line 71) in 'some_behaviors' (3/3):
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 70) in 'some_behaviors' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 70) in 'some_behaviors' (2/2):
-Call Effect at line 78
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 70) in 'some_behaviors' (1/5):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 70) in 'some_behaviors' (2/5):
-Call Effect at line 78
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 70) in 'some_behaviors' (3/5):
-Call Result at line 78
-Tags: Call h0.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 70) in 'some_behaviors' (4/5):
-Call Result at line 78
-Tags: Call h2.
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'bhv1' (file dynamic.i, line 70) in 'some_behaviors' (5/5):
-Call Result at line 78
-Tags: Call h1.
-Prove: true.
-
-------------------------------------------------------------
-[wp] dynamic.i:41: Warning:
- Memory model hypotheses for function 'guarded_call':
- /*@ behavior wp_typed:
- requires \separated(p, &X); */
- void guarded_call(struct S *p);
-[wp] dynamic.i:63: Warning:
- Memory model hypotheses for function 'behavior':
- /*@ behavior wp_typed:
- requires \separated(p + (..), &X1); */
- int behavior(int (*p)(void));
-[wp] dynamic.i:76: Warning:
- Memory model hypotheses for function 'some_behaviors':
- /*@ behavior wp_typed:
- requires \separated(p + (..), &X1); */
- int some_behaviors(int (*p)(void));
-[wp] dynamic.i:85: Warning:
- Memory model hypotheses for function 'missing_context':
- /*@ behavior wp_typed:
- requires \separated(p, &X1); */
- int missing_context(int (*p)(void));
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle
deleted file mode 100644
index a369ec0fabc..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle
+++ /dev/null
@@ -1,141 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing stmt.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] [CFG] Goal f_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_assigns : Valid (Unreachable)
-[wp] [CFG] Goal g_ensures : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_assigns : Valid (Unreachable)
-[wp] [CFG] Goal h_ensures : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function f
-------------------------------------------------------------
-
-Goal Post-condition (file stmt.c, line 18) in 'f':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file stmt.c, line 19) in 'f':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (file stmt.c, line 24):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f with behavior default_for_stmt_2
-------------------------------------------------------------
-
-Goal Post-condition (file stmt.c, line 25) at block:
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file stmt.c, line 29) at block:
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function g
-------------------------------------------------------------
-
-Goal Post-condition (file stmt.c, line 35) in 'g':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (file stmt.c, line 40):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function h
-------------------------------------------------------------
-
-Goal Post-condition (file stmt.c, line 48) in 'h':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (generated):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (generated):
-Prove: true.
-
-------------------------------------------------------------
-[report] Computing properties status...
-
---------------------------------------------------------------------------------
---- Properties of Function 'f'
---------------------------------------------------------------------------------
-
-[ Valid ] Exit-condition (file stmt.c, line 23) at block
- by Unreachable Annotations.
-[ Partial ] Return-condition (file stmt.c, line 24) at block
- By Frama-C kernel, with pending:
- - Assertion (file stmt.c, line 24)
-[ - ] Default behavior at block
- tried with Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'g'
---------------------------------------------------------------------------------
-
-[ Valid ] Exit-condition (file stmt.c, line 39) at block
- by Unreachable Annotations.
-[ Valid ] Return-condition (file stmt.c, line 40) at block
- by Unreachable Annotations.
-[ Valid ] Post-condition (file stmt.c, line 41) at block
- by Unreachable Annotations.
-[ Valid ] Assigns (file stmt.c, line 44) at block
- by Unreachable Annotations.
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'h'
---------------------------------------------------------------------------------
-
-[ Valid ] Exit-condition (file stmt.c, line 51) at block
- by Unreachable Annotations.
-[ Valid ] Post-condition (file stmt.c, line 52) at block
- by Unreachable Annotations.
-[ Partial ] Return-condition for 'POS' (file stmt.c, line 56) at block
- By Frama-C kernel, with pending:
- - Assertion (generated)
- - Assertion (generated)
-[ Partial ] Return-condition for 'NEG' (file stmt.c, line 59) at block
- By Frama-C kernel, with pending:
- - Assertion (generated)
- - Assertion (generated)
-[ Valid ] Assigns (file stmt.c, line 61) at block
- by Unreachable Annotations.
-[ Partial ] Behavior 'NEG' at block
- By Frama-C kernel, with pending:
- - Assertion (generated)
- - Assertion (generated)
-[ Partial ] Behavior 'POS' at block
- By Frama-C kernel, with pending:
- - Assertion (generated)
- - Assertion (generated)
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Status Report Summary
---------------------------------------------------------------------------------
- 10 Completely validated
- 5 Locally validated
- 1 To be validated
- 16 Total
---------------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unsigned.res.oracle
deleted file mode 100644
index 914550152f5..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle/unsigned.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing unsigned.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] 1 goal scheduled
-[wp] [Tactical] Goal typed_lemma_U32 : Valid
-[wp] Proved goals: 1 / 1
- Qed: 0
- Script: 1
-------------------------------------------------------------
- Global
-------------------------------------------------------------
-
-Lemma U32:
-Prove: (is_uint32 x_0) -> ((land 4294967295 x_0)=x_0)
-Prover Tactical returns Valid
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
deleted file mode 100644
index 38370a03818..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
+++ /dev/null
@@ -1,25 +0,0 @@
-# frama-c -wp -wp-no-let -wp-timeout 45 -wp-steps 1500 [...]
-[kernel] Parsing bool.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] Warning: Missing RTE guards
-[wp] 7 goals scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_band_bool_false_ensures : Unsuccess
-[wp] [Qed] Goal typed_band_bool_true_ensures : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_bor_bool_false_ensures : Unsuccess
-[wp] [Alt-Ergo 2.0.0] Goal typed_bor_bool_true_ensures : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_bxor_bool_false_ensures : Unsuccess
-[wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_job_ensures : Unsuccess
-[wp] Proved goals: 3 / 7
- Qed: 2
- Alt-Ergo 2.0.0: 1 (unsuccess: 4)
-[wp] Report in: 'oracle_qualif/bool.0.report.json'
-[wp] Report out: 'result_qualif/bool.0.report.json'
--------------------------------------------------------------
-Functions WP Alt-Ergo Total Success
-job - - 1 0.0%
-bor_bool - 1 (4..16) 2 50.0%
-band_bool 1 - 2 50.0%
-bxor_bool 1 - 2 50.0%
--------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
deleted file mode 100644
index 54cef061daa..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+++ /dev/null
@@ -1,21 +0,0 @@
-# frama-c -wp -wp-model 'Dump' [...]
-[kernel] Parsing stmt.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] [CFG] Goal f_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_assigns : Valid (Unreachable)
-[wp] [CFG] Goal g_ensures : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_assigns : Valid (Unreachable)
-[wp] [CFG] Goal h_ensures : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] CFG h -> h
-[wp] CFG h -> h_NEG_stmt_15
-[wp] CFG h -> h_POS_stmt_15
-[wp] CFG h -> h_default_for_stmt_15
-[wp] CFG g -> g
-[wp] CFG g -> g_default_for_stmt_11
-[wp] CFG f -> f
-[wp] CFG f -> f_default_for_stmt_2
-[wp] Warning: No goal generated
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
deleted file mode 100644
index 97195231fdf..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
+++ /dev/null
@@ -1,114 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing stmt.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] [CFG] Goal f_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_assigns : Valid (Unreachable)
-[wp] [CFG] Goal g_ensures : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_assigns : Valid (Unreachable)
-[wp] [CFG] Goal h_ensures : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] Warning: Missing RTE guards
-[wp] 10 goals scheduled
-[wp] [Qed] Goal typed_f_ensures : Valid
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Qed] Goal typed_f_ensures_2 : Valid
-[wp] [Qed] Goal typed_f_ensures_3 : Valid
-[wp] [Qed] Goal typed_f_assert : Valid
-[wp] [Qed] Goal typed_g_ensures_2 : Valid
-[wp] [Qed] Goal typed_g_assert : Valid
-[wp] [Qed] Goal typed_h_ensures_2 : Valid
-[wp] [Qed] Goal typed_h_assert : Valid
-[wp] [Qed] Goal typed_h_assert_2 : Valid
-[wp] Proved goals: 10 / 10
- Qed: 10
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- f 5 - 5 100%
- g 2 - 2 100%
- h 3 - 3 100%
-------------------------------------------------------------
-[report] Computing properties status...
-
---------------------------------------------------------------------------------
---- Properties of Function 'f'
---------------------------------------------------------------------------------
-
-[ Valid ] Post-condition (file stmt.c, line 10)
- by Wp.typed.
-[ Valid ] Post-condition (file stmt.c, line 11)
- by Wp.typed.
-[ Valid ] Exit-condition (file stmt.c, line 15) at block
- by Unreachable Annotations.
-[ Valid ] Return-condition (file stmt.c, line 16) at block
- by Frama-C kernel.
-[ Valid ] Post-condition (file stmt.c, line 17) at block
- by Wp.typed.
-[ Valid ] Assigns (file stmt.c, line 21) at block
- by Wp.typed.
-[ Valid ] Assertion (file stmt.c, line 16)
- by Wp.typed.
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-[ Valid ] Default behavior
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'g'
---------------------------------------------------------------------------------
-
-[ Valid ] Post-condition (file stmt.c, line 27)
- by Wp.typed.
-[ Valid ] Exit-condition (file stmt.c, line 31) at block
- by Unreachable Annotations.
-[ Valid ] Return-condition (file stmt.c, line 32) at block
- by Frama-C kernel.
- by Unreachable Annotations.
-[ Valid ] Post-condition (file stmt.c, line 33) at block
- by Unreachable Annotations.
-[ Valid ] Assigns (file stmt.c, line 36) at block
- by Unreachable Annotations.
-[ Valid ] Assertion (file stmt.c, line 32)
- by Wp.typed.
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-[ Valid ] Default behavior
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'h'
---------------------------------------------------------------------------------
-
-[ Valid ] Post-condition (file stmt.c, line 40)
- by Wp.typed.
-[ Valid ] Exit-condition (file stmt.c, line 43) at block
- by Unreachable Annotations.
-[ Valid ] Post-condition (file stmt.c, line 44) at block
- by Unreachable Annotations.
-[ Valid ] Return-condition for 'POS' (file stmt.c, line 48) at block
- by Frama-C kernel.
-[ Valid ] Return-condition for 'NEG' (file stmt.c, line 51) at block
- by Frama-C kernel.
-[ Valid ] Assigns (file stmt.c, line 53) at block
- by Unreachable Annotations.
-[ Valid ] Assertion (generated)
- by Wp.typed.
-[ Valid ] Assertion (generated)
- by Wp.typed.
-[ Valid ] Behavior 'NEG' at block
- by Frama-C kernel.
-[ Valid ] Behavior 'POS' at block
- by Frama-C kernel.
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-[ Valid ] Default behavior
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Status Report Summary
---------------------------------------------------------------------------------
- 29 Completely validated
- 29 Total
---------------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/stmt.c b/src/plugins/wp/tests/wp_plugin/stmt.c
deleted file mode 100644
index 6bb4cc685fc..00000000000
--- a/src/plugins/wp/tests/wp_plugin/stmt.c
+++ /dev/null
@@ -1,63 +0,0 @@
-/* run.config
- PLUGIN: @PTEST_PLUGIN@ report
- OPT: -then -report
-*/
-/* run.config_qualif
-<<<<<<< HEAD
- PLUGIN: @PTEST_PLUGIN@ report
- OPT: -then -report
- EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -wp-precond-weakening -wp -wp-warn-key pedantic-assigns=inactive -wp-model Dump -wp-out . -wp-msg-key shell 1> stmt.log
-||||||| ac7807782d
- OPT: -load-module report -then -report
- EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
-=======
- OPT: -load-module report -then -report
- EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-warn-key pedantic-assigns=inactive -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
->>>>>>> origin/master
-*/
-/*@ ensures a > 0 ==> \result == a + b;
- @ ensures a <= 0 ==> \result == -1;
-*/
-int f(int a, int b) {
-
- /*@ exits \false;
- @ returns \result == a + b;
- @ ensures a <= 0;
- @ assigns \nothing;
- */
- if (a > 0)
- return a + b;
-
- return -1;
-}
-
-
-/*@ ensures \result == a + b;
-*/
-int g(int a, int b) {
-
- /*@ exits \false;
- @ returns \result == a + b;
- @ ensures \false;
- @ assigns \nothing;
- */
- return a + b;
-
-}
-
-/*@ ensures \result == (e ? a : b) ; */
-int h(int e,int a,int b) {
-
- /*@ exits \false;
- @ ensures \false;
- @ assigns \nothing;
- @ behavior POS:
- @ assumes e ;
- @ returns \result == a;
- @ behavior NEG:
- @ assumes !e ;
- @ returns \result == b;
- */
- if (e) return a; else return b;
-
-}
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
deleted file mode 100644
index 58ae426289c..00000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
+++ /dev/null
@@ -1,22 +0,0 @@
-# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
-[kernel] Parsing user_init.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] Warning: Missing RTE guards
-[wp] 8 goals scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_init_ensures : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_init_loop_invariant_Partial_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_init_loop_invariant_Range_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_Range_established : Valid
-[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_init_loop_assigns_part2 : Valid
-[wp] [Qed] Goal typed_init_assigns : Valid
-[wp] Proved goals: 8 / 8
- Qed: 4
- Alt-Ergo 2.0.0: 4
-[wp] Report 'user_init.i.0.report.json'
--------------------------------------------------------------
-Functions WP Alt-Ergo Total Success
-init 4 4 (48..60) 8 100%
--------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle
deleted file mode 100644
index 59bb37ee9ae..00000000000
--- a/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle
+++ /dev/null
@@ -1,54 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing core.i (no preprocessing)
-[kernel] core.i:11: Warning:
- parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] core.i:24: Warning: Missing assigns clause (assigns 'everything' instead)
-[wp] core.i:20: Warning: Missing assigns clause (assigns 'everything' instead)
-[wp] core.i:17: Warning: Missing assigns clause (assigns 'everything' instead)
-------------------------------------------------------------
- Function f
-------------------------------------------------------------
-
-Goal Post-condition (file core.i, line 12) in 'f':
-Assume {
- Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(x) /\
- is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3).
- If a != 0
- Then { Have: x_3 = x. }
- Else { Have: x_3 = x. }
- If b != 0
- Then { Have: x_3 = x_2. }
- Else { Have: x_3 = x_2. }
- If c != 0
- Then { Have: (1 + x_2) = x_1. }
- Else { Have: (1 + x_2) = x_1. }
-}
-Prove: P_OBS(x, x_1).
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f with behavior default_for_stmt_15
-------------------------------------------------------------
-
-Goal Post-condition (file core.i, line 23) at instruction (file core.i, line 24):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f with behavior default_for_stmt_4
-------------------------------------------------------------
-
-Goal Post-condition (file core.i, line 16) at instruction (file core.i, line 17):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f with behavior default_for_stmt_9
-------------------------------------------------------------
-
-Goal Post-condition (file core.i, line 19) at instruction (file core.i, line 20):
-Prove: true.
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle
deleted file mode 100644
index 772b9e4940c..00000000000
--- a/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle
+++ /dev/null
@@ -1,46 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing core.i (no preprocessing)
-[kernel] core.i:11: Warning:
- parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] core.i:24: Warning: Missing assigns clause (assigns 'everything' instead)
-[wp] core.i:20: Warning: Missing assigns clause (assigns 'everything' instead)
-[wp] core.i:17: Warning: Missing assigns clause (assigns 'everything' instead)
-------------------------------------------------------------
- Function f
-------------------------------------------------------------
-
-Goal Post-condition (file core.i, line 12) in 'f':
-Let x_1 = 1 + x.
-Assume {
- Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(x) /\
- is_sint32(x_1).
-}
-Prove: P_OBS(x, x_1).
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f with behavior default_for_stmt_15
-------------------------------------------------------------
-
-Goal Post-condition (file core.i, line 23) at instruction (file core.i, line 24):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f with behavior default_for_stmt_4
-------------------------------------------------------------
-
-Goal Post-condition (file core.i, line 16) at instruction (file core.i, line 17):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f with behavior default_for_stmt_9
-------------------------------------------------------------
-
-Goal Post-condition (file core.i, line 19) at instruction (file core.i, line 20):
-Prove: true.
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.err b/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.err
new file mode 100644
index 00000000000..e69de29bb2d
--
GitLab