From 0ac12d406813062af68b06ae79bfed55df219d3b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 24 Feb 2021 18:46:37 +0100
Subject: [PATCH] [wp] oracle updates
---
.../assigned_initialized_memvar.res.oracle | 58 ++++++++-----------
.../assigned_initialized_memvar.res.oracle | 12 ++--
2 files changed, 30 insertions(+), 40 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
index a4e3a95a841..a095737754b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
@@ -71,29 +71,24 @@ Prove: true.
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
-Let a = Init_s_0.Init_F1_S_a.
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (((0 < i_1) ->
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_3 : Z. ((i_3 != 0) -> ((i_3 != 2) -> ((i_3 != 4) ->
- ((0 <= i_3) -> ((i_3 <= 9) -> ((a[i_3]=true) <-> (v[i_3]=true)))))))) /\
- (forall i_3 : Z. ((i_3 != 0) -> ((i_3 != 2) -> ((i_3 != 4) ->
- ((0 <= i_3) -> ((i_3 <= 9) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))))) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((v[i_3]=true) ->
- (((i_3 = 0) \/ (i_3 = 2) \/ (i_3 = 4)) -> (a[i_3]=true)))))).
+ Have: ((s.F1_S_i) = 0) /\
+ (forall i_2 : Z. ((i_2 != 0) -> ((i_2 != 2) -> ((i_2 != 4) ->
+ ((0 <= i_2) -> ((i_2 <= 9) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))))).
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
}
-Prove: (a[i]=true).
+Prove: ((Init_s_0.Init_F1_S_i)=true) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((Init_s_0.Init_F1_S_a)[i_2]=true)))).
------------------------------------------------------------
@@ -255,29 +250,24 @@ Prove: true.
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 38):
-Let a = Init_s_0.Init_F1_S_a.
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (((0 < i_1) ->
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (((i_3 <= 0) \/ (5 <= i_3)) -> ((a[i_3]=true) <-> (v[i_3]=true)))))) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (((i_3 <= 0) \/ (5 <= i_3)) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))) /\
- (forall i_3 : Z. ((0 < i_3) -> ((0 <= i_3) -> ((i_3 <= 4) ->
- ((i_3 <= 9) -> ((v[i_3]=true) -> (a[i_3]=true))))))).
+ Have: ((s.F1_S_i) = 0) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ (((i_2 <= 0) \/ (5 <= i_2)) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))).
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
}
-Prove: (a[i]=true).
+Prove: ((Init_s_0.Init_F1_S_i)=true) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((Init_s_0.Init_F1_S_a)[i_2]=true)))).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
index bdd6cac2653..de07c211f1c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
@@ -7,7 +7,7 @@
[wp] [Qed] Goal typed_initialize_loop_invariant_CHECK_established : Valid
[wp] [Alt-Ergo] Goal typed_initialize_check_CHECK : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns : Valid
-[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Unsuccess
[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
@@ -17,7 +17,7 @@
[wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Unsuccess
[wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
@@ -25,16 +25,16 @@
[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
[wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
[wp] [Qed] Goal typed_comp_loop_assigns : Valid
-[wp] Proved goals: 22 / 22
+[wp] Proved goals: 20 / 22
Qed: 13
- Alt-Ergo: 9
+ Alt-Ergo: 7 (unsuccess: 2)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 2 2 4 100%
- range 2 1 3 100%
+ range 2 - 3 66.7%
field 1 1 2 100%
array 1 1 2 100%
index 2 1 3 100%
- descr 4 2 6 100%
+ descr 4 1 6 83.3%
comp 1 1 2 100%
------------------------------------------------------------
--
GitLab