From 1d0cf28595661a5a19c9aaf5d43a633cec95c473 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 26 Apr 2019 14:41:51 +0200
Subject: [PATCH] [wp] update qualif tests
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Since -wp-bool-range is activated by default…
---
.../wp_acsl/oracle_qualif/bitwise.res.oracle | 16 +--
src/plugins/wp/tests/wp_plugin/bool.i | 8 +-
.../tests/wp_plugin/oracle/bool.1.res.oracle | 127 ------------------
.../{bool.0.res.oracle => bool.res.oracle} | 14 +-
.../wp_plugin/oracle_qualif/bool.0.res.oracle | 25 ----
.../{bool.1.res.oracle => bool.res.oracle} | 4 +-
.../oracle_qualif/removed.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/rte.res.oracle | 12 +-
8 files changed, 25 insertions(+), 183 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle/bool.1.res.oracle
rename src/plugins/wp/tests/wp_plugin/oracle/{bool.0.res.oracle => bool.res.oracle} (95%)
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
rename src/plugins/wp/tests/wp_plugin/oracle_qualif/{bool.1.res.oracle => bool.res.oracle} (89%)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
index 8cc292011a2..226cd7c529a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
@@ -12,7 +12,7 @@
[wp] [Qed] Goal typed_band_bit2_ensures_band4 : Valid
[wp] [Qed] Goal typed_band_bit3_ensures_band5 : Valid
[wp] [Qed] Goal typed_band_bit4_ensures_band6 : Valid
-[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Unsuccess
+[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Valid
[wp] [Qed] Goal typed_band_bool_true_ensures : Valid
[wp] [Qed] Goal typed_bnot_ensures : Valid
[wp] [Qed] Goal typed_bor_ensures : Valid
@@ -20,12 +20,12 @@
[wp] [Qed] Goal typed_bor_bit1_ensures_bor1 : Valid
[wp] [Qed] Goal typed_bor_bit2_ensures_bor2 : Valid
[wp] [Qed] Goal typed_bor_bit3_ensures_bor3 : Valid
-[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Valid
[wp] [Alt-Ergo] Goal typed_bor_bool_true_ensures : Valid
[wp] [Qed] Goal typed_bxor_ensures : Valid
[wp] [Qed] Goal typed_bxor_bit1_ensures : Valid
[wp] [Qed] Goal typed_bxor_bit2_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Valid
[wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
[wp] [Qed] Goal typed_lshift_ensures : Valid
[wp] [Qed] Goal typed_lshift_shift1_ensures_lsl1 : Valid
@@ -33,9 +33,9 @@
[wp] [Qed] Goal typed_lshift_shift2_ensures_lsl3 : Valid
[wp] [Qed] Goal typed_rshift_ensures : Valid
[wp] [Qed] Goal typed_rshift_shift1_ensures_lsr1 : Valid
-[wp] Proved goals: 26 / 29
+[wp] Proved goals: 29 / 29
Qed: 25
- Alt-Ergo: 1 (unsuccess: 3)
+ Alt-Ergo: 4
[wp] Report in: 'tests/wp_acsl/oracle_qualif/bitwise.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/bitwise.0.report.json'
-------------------------------------------------------------
@@ -46,7 +46,7 @@ bxor 3 - 3 100%
bnot 1 - 1 100%
lshift 4 - 4 100%
rshift 2 - 2 100%
-bor_bool - 1 (4..16) 2 50.0%
-band_bool 1 - 2 50.0%
-bxor_bool 1 - 2 50.0%
+bor_bool - 2 (8..20) 2 100%
+band_bool 1 1 (20..32) 2 100%
+bxor_bool 1 1 (8..20) 2 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/bool.i b/src/plugins/wp/tests/wp_plugin/bool.i
index 0b90b861d07..3c38f396a1c 100644
--- a/src/plugins/wp/tests/wp_plugin/bool.i
+++ b/src/plugins/wp/tests/wp_plugin/bool.i
@@ -1,11 +1,9 @@
/* run.config
OPT: -wp-no-let
- OPT: -wp-no-let
*/
/* run.config_qualif
OPT: -wp-no-let
- OPT: -wp-no-let
*/
@@ -15,7 +13,7 @@ int job(_Bool a, _Bool b) { return a+b; }
/*@ behavior true:
@ assumes a == 1 || b == 1;
@ ensures \result == 1;
- @ behavior false:
+ @ behavior false:
@ assumes !(a == 1 || b == 1);
@ ensures \result == 0;
*/
@@ -25,7 +23,7 @@ _Bool bor_bool(_Bool a, _Bool b) { return (_Bool)(((int)a | (int)b) != 0); }
/*@ behavior true:
@ assumes a == 1 && b == 1;
@ ensures \result == 1;
- @ behavior false:
+ @ behavior false:
@ assumes !(a == 1 && b == 1);
@ ensures \result == 0;
*/
@@ -34,7 +32,7 @@ _Bool band_bool(_Bool a, _Bool b) { return (_Bool)(((int)a & (int)b) != 0); }
/*@ behavior true:
@ assumes (a == 1 && b == 0) || (a == 0 && b == 1);
@ ensures \result == 1;
- @ behavior false:
+ @ behavior false:
@ assumes !((a == 1 && b == 0) || (a == 0 && b == 1)) ;
@ ensures \result == 0;
*/
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bool.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bool.1.res.oracle
deleted file mode 100644
index feb6965058e..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle/bool.1.res.oracle
+++ /dev/null
@@ -1,127 +0,0 @@
-# frama-c -wp -wp-no-let [...]
-[kernel] Parsing tests/wp_plugin/bool.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function band_bool with behavior false
-------------------------------------------------------------
-
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 30) in 'band_bool':
-Assume {
- Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
- is_bool(band_bool_0) /\ is_bool(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'false' *)
- Have: (a_1 != 1) \/ (b_1 != 1).
- Have: (if (land(a, b) = 0) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = band_bool_0.
-}
-Prove: band_bool_0 = 0.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function band_bool with behavior true
-------------------------------------------------------------
-
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 27) in 'band_bool':
-Assume {
- Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
- is_bool(band_bool_0) /\ is_bool(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'true' *)
- Have: (a_1 = 1) /\ (b_1 = 1).
- Have: (if (land(a, b) = 0) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = band_bool_0.
-}
-Prove: band_bool_0 = 1.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function bor_bool with behavior false
-------------------------------------------------------------
-
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 20) in 'bor_bool':
-Assume {
- Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
- is_bool(bor_bool_0) /\ is_bool(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'false' *)
- Have: (a_1 != 1) /\ (b_1 != 1).
- Have: (if ((a = 0) & (b = 0)) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = bor_bool_0.
-}
-Prove: bor_bool_0 = 0.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function bor_bool with behavior true
-------------------------------------------------------------
-
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 17) in 'bor_bool':
-Assume {
- Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
- is_bool(bor_bool_0) /\ is_bool(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'true' *)
- Have: (a_1 = 1) \/ (b_1 = 1).
- Have: (if ((a = 0) & (b = 0)) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = bor_bool_0.
-}
-Prove: bor_bool_0 = 1.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function bxor_bool with behavior false
-------------------------------------------------------------
-
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 39) in 'bxor_bool':
-Assume {
- Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
- is_bool(bxor_bool_0) /\ is_bool(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'false' *)
- Have: ((a_1 != 0) \/ (b_1 != 1)) /\ ((a_1 != 1) \/ (b_1 != 0)).
- Have: (if (b = a) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = bxor_bool_0.
-}
-Prove: bxor_bool_0 = 0.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function bxor_bool with behavior true
-------------------------------------------------------------
-
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 36) in 'bxor_bool':
-Assume {
- Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
- is_bool(bxor_bool_0) /\ is_bool(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'true' *)
- Have: ((a_1 = 0) /\ (b_1 = 1)) \/ ((a_1 = 1) /\ (b_1 = 0)).
- Have: (if (b = a) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = bxor_bool_0.
-}
-Prove: bxor_bool_0 = 1.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function job
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_plugin/bool.i, line 12) in 'job':
-Assume {
- Type: is_bool(a) /\ is_bool(b) /\ is_sint32(job_0) /\ is_sint32(retres_0).
- Have: (a + b) = retres_0.
- (* Return *)
- Have: retres_0 = job_0.
-}
-Prove: (0 <= job_0) /\ (job_0 <= 2).
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle
similarity index 95%
rename from src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle
rename to src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle
index feb6965058e..c80bbdfdc62 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle
@@ -7,7 +7,7 @@
Function band_bool with behavior false
------------------------------------------------------------
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 30) in 'band_bool':
+Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 28) in 'band_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(band_bool_0) /\ is_bool(retres_0).
@@ -25,7 +25,7 @@ Prove: band_bool_0 = 0.
Function band_bool with behavior true
------------------------------------------------------------
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 27) in 'band_bool':
+Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 25) in 'band_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(band_bool_0) /\ is_bool(retres_0).
@@ -43,7 +43,7 @@ Prove: band_bool_0 = 1.
Function bor_bool with behavior false
------------------------------------------------------------
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 20) in 'bor_bool':
+Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 18) in 'bor_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(bor_bool_0) /\ is_bool(retres_0).
@@ -61,7 +61,7 @@ Prove: bor_bool_0 = 0.
Function bor_bool with behavior true
------------------------------------------------------------
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 17) in 'bor_bool':
+Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 15) in 'bor_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(bor_bool_0) /\ is_bool(retres_0).
@@ -79,7 +79,7 @@ Prove: bor_bool_0 = 1.
Function bxor_bool with behavior false
------------------------------------------------------------
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 39) in 'bxor_bool':
+Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 37) in 'bxor_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(bxor_bool_0) /\ is_bool(retres_0).
@@ -97,7 +97,7 @@ Prove: bxor_bool_0 = 0.
Function bxor_bool with behavior true
------------------------------------------------------------
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 36) in 'bxor_bool':
+Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 34) in 'bxor_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(bxor_bool_0) /\ is_bool(retres_0).
@@ -115,7 +115,7 @@ Prove: bxor_bool_0 = 1.
Function job
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/bool.i, line 12) in 'job':
+Goal Post-condition (file tests/wp_plugin/bool.i, line 10) in 'job':
Assume {
Type: is_bool(a) /\ is_bool(b) /\ is_sint32(job_0) /\ is_sint32(retres_0).
Have: (a + b) = retres_0.
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 8361dfbe06c..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 90 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_plugin/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] Goal typed_band_bool_false_ensures : Unsuccess
-[wp] [Qed] Goal typed_band_bool_true_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Unsuccess
-[wp] [Alt-Ergo] Goal typed_bor_bool_true_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Unsuccess
-[wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_job_ensures : Unsuccess
-[wp] Proved goals: 3 / 7
- Qed: 2
- Alt-Ergo: 1 (unsuccess: 4)
-[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.0.report.json'
-[wp] Report out: 'tests/wp_plugin/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/bool.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
similarity index 89%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle
rename to src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
index 04c1d1900f3..81ddac40fbc 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
@@ -14,8 +14,8 @@
[wp] Proved goals: 7 / 7
Qed: 2
Alt-Ergo: 5
-[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.1.report.json'
-[wp] Report out: 'tests/wp_plugin/result_qualif/bool.1.report.json'
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.0.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/bool.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job - 1 (12..24) 1 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
index c1ef69535ae..397e221edae 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
@@ -12,11 +12,11 @@
__retres ∈ [-2147483647..2147483647]
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_Eva_signed_overflow : Unsuccess
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
index 5bc109acf7a..2404c6c172d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
@@ -5,24 +5,20 @@
[rte] annotating function job
[rte] annotating function job2
[rte] annotating function job3
-[wp] tests/wp_plugin/rte.i:34: Warning:
- Option -wp-bool-range incompatiable with RTE (ignored)
-[wp] tests/wp_plugin/rte.i:34: Warning:
- Option -wp-bool-range incompatiable with RTE (ignored)
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow_2 : Unsuccess
[wp] [Qed] Goal typed_job_assert_rte_mem_access_3 : Valid
-[wp] [Alt-Ergo] Goal typed_job3_assert_rte_bool_value : Unsuccess
-[wp] Proved goals: 1 / 6
+[wp] [Alt-Ergo] Goal typed_job3_assert_rte_bool_value : Valid
+[wp] Proved goals: 2 / 6
Qed: 1
- Alt-Ergo: 0 (unsuccess: 5)
+ Alt-Ergo: 1 (unsuccess: 4)
[wp] Report in: 'tests/wp_plugin/oracle_qualif/rte.0.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/rte.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job 1 - 5 20.0%
-job3 - - 1 0.0%
+job3 - 1 (4..16) 1 100%
-------------------------------------------------------------
--
GitLab