From c718cf07bb19475193a34faff3a851b55d827384 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 16 Mar 2021 18:35:18 +0100
Subject: [PATCH] [wp] updated oracles for complex init cases
# Conflicts:
# src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
---
.../wp_acsl/assigned_initialized_memvar.i | 10 +-
.../assigned_initialized_memvar.res.oracle | 123 ++++++++++++++----
.../assigned_initialized_memvar.res.oracle | 20 +--
3 files changed, 121 insertions(+), 32 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
index c320c1273b9..7fc06531a4a 100644
--- a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
@@ -31,7 +31,10 @@ void range(void){
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
- /*@ loop assigns CHECK: i, s.a[1 .. 4]; */
+ /*@
+ loop invariant CHECK: \initialized(&s);
+ loop assigns CHECK: i, s.a[1 .. 4];
+ */
for(int i = 0; i < 10; ++i){
if(1 <= i && i <= 4) s.a[i] = 1 ;
}
@@ -98,7 +101,10 @@ void descr(void){
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
- /*@ loop assigns CHECK: i, { s.a[i] | integer i ; i \in { 0, 2, 4 } }; */
+ /*@
+ loop invariant CHECK: \initialized(&s);
+ loop assigns CHECK: i, { s.a[i] | integer i ; i \in { 0, 2, 4 } };
+ */
for(int i = 0; i < 10; ++i){
if(i == 0 || i == 2 || i == 4) s.a[i] = 1 ;
}
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 a095737754b..846c0324155 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
@@ -6,7 +6,7 @@
Function array
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 73):
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 76):
Assume {
Have: 0 <= i.
Have: i <= 9.
@@ -37,7 +37,7 @@ Prove: true.
Function comp
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 125):
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 131):
Let a = Init_s_0.Init_F1_S_a.
Assume {
Have: 0 <= i.
@@ -70,7 +70,7 @@ Prove: true.
Function descr
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
+Goal Preservation of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
@@ -83,8 +83,38 @@ Assume {
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_1.
+ (* Invariant 'CHECK' *)
+ Have: ((Init_s_1.Init_F1_S_i)=true) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((Init_s_1.Init_F1_S_a)[i_2]=true)))).
+ (* Then *)
+ Have: i_1 <= 9.
+ If i_1 = 0
+ Then {
+ Have: Init_s_1 = Init_s_2.
+ Have: ({ Init_s_2 with Init_F1_S_a = (Init_s_2.Init_F1_S_a)[0 <- true] }) =
+ Init_s_0.
+ }
+ Else {
+ Have: (Init_s_1 = Init_s_3) /\ (s = s_1).
+ If i_1 = 2
+ Then {
+ Have: (Init_s_3 = Init_s_4) /\ (s_1 = s_2).
+ Have: ({ Init_s_4 with Init_F1_S_a = (Init_s_4.Init_F1_S_a)[2 <- true]
+ }) = Init_s_0.
+ }
+ Else {
+ Have: (Init_s_3 = Init_s_5) /\ (s_1 = s_3).
+ If i_1 = 4
+ Then {
+ Have: Init_s_5 = Init_s_6.
+ Have: ({ Init_s_6 with
+ Init_F1_S_a = (Init_s_6.Init_F1_S_a)[4 <- true] }) =
+ Init_s_0.
+ }
+ Else { Have: Init_s_5 = Init_s_0. }
+ }
+ }
}
Prove: ((Init_s_0.Init_F1_S_i)=true) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
@@ -92,13 +122,34 @@ Prove: ((Init_s_0.Init_F1_S_i)=true) /\
------------------------------------------------------------
+Goal Establishment of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
+Assume {
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_sint32(i_1).
+ (* Invariant *)
+ Have: (0 <= i_1) /\ (i_1 <= 10) /\
+ (((0 < i_1) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true)))))).
+ (* Else *)
+ Have: 10 <= i_1.
+}
+Prove: (v[i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 111):
+Prove: true.
+
+------------------------------------------------------------
+
Goal Loop assigns 'CHECK' (1/5):
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (2/5):
-Effect at line 102
+Effect at line 108
Assume {
Type: is_sint32(i_2) /\ is_sint32(i_3).
(* Goal *)
@@ -124,19 +175,19 @@ Prove: ((i != 0) /\ (i != 2) /\ (i != 4)) \/
------------------------------------------------------------
Goal Loop assigns 'CHECK' (3/5):
-Effect at line 103
+Effect at line 109
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (4/5):
-Effect at line 103
+Effect at line 109
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (5/5):
-Effect at line 103
+Effect at line 109
Prove: true.
------------------------------------------------------------
@@ -144,7 +195,7 @@ Prove: true.
Function field
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 54):
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 57):
Assume {
Have: 0 <= i.
Have: i <= 9.
@@ -170,7 +221,7 @@ Prove: true.
Function index
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 89):
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 92):
Assume {
Have: 0 <= i.
Have: i <= 9.
@@ -196,7 +247,7 @@ Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (2/2):
-Effect at line 87
+Effect at line 90
Prove: true.
------------------------------------------------------------
@@ -249,25 +300,53 @@ Prove: true.
Function range
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 38):
+Goal Preservation of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 35):
+Let a = Init_s_0.Init_F1_S_a.
Assume {
- Type: is_sint32(i) /\ is_sint32(i_1).
+ Type: is_sint32(i_1) /\ is_sint32(i).
+ (* Residual *)
+ When: i <= 4.
+ (* Residual *)
+ When: 0 < i.
(* Invariant *)
- Have: (0 <= i) /\ (i <= 10) /\
- (((0 < i) ->
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
+ Have: (0 <= i_1) /\ (i_1 <= 10) /\
+ (((0 < i_1) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true)))))).
(* Else *)
- Have: 10 <= i.
+ Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
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]))))).
+ (* Invariant 'CHECK' *)
+ Have: ((Init_s_0.Init_F1_S_i)=true) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) -> (a[i_2]=true)))).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ (a[i <- true][i_2]=true))).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 35):
+Assume {
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_sint32(i_1).
+ (* Invariant *)
+ Have: (0 <= i_1) /\ (i_1 <= 10) /\
+ (((0 < i_1) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true)))))).
(* Else *)
Have: 10 <= i_1.
}
-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)))).
+Prove: (v[i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 41):
+Prove: true.
------------------------------------------------------------
@@ -277,7 +356,7 @@ Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (2/2):
-Effect at line 36
+Effect at line 39
Prove: 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 de07c211f1c..756f8f52f89 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
@@ -2,12 +2,14 @@
[kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 22 goals scheduled
+[wp] 26 goals scheduled
[wp] [Alt-Ergo] Goal typed_initialize_loop_invariant_CHECK_preserved : Valid
[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 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_range_loop_invariant_CHECK_preserved : Valid
+[wp] [Alt-Ergo] Goal typed_range_loop_invariant_CHECK_established : Valid
+[wp] [Qed] Goal typed_range_check_CHECK : Valid
[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 +19,9 @@
[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 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_descr_loop_invariant_CHECK_preserved : Valid
+[wp] [Alt-Ergo] Goal typed_descr_loop_invariant_CHECK_established : Valid
+[wp] [Qed] Goal typed_descr_check_CHECK : Valid
[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 +29,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: 20 / 22
- Qed: 13
- Alt-Ergo: 7 (unsuccess: 2)
+[wp] Proved goals: 26 / 26
+ Qed: 15
+ Alt-Ergo: 11
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 2 2 4 100%
- range 2 - 3 66.7%
+ range 3 2 5 100%
field 1 1 2 100%
array 1 1 2 100%
index 2 1 3 100%
- descr 4 1 6 83.3%
+ descr 5 3 8 100%
comp 1 1 2 100%
------------------------------------------------------------
--
GitLab