From 51c9d57fae6493ba142a5620e594d0706b553c24 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 8 Oct 2020 18:23:14 +0200
Subject: [PATCH] [wp] MemVar: normalize offset on initialized array
---
src/plugins/wp/MemVar.ml | 7 +
.../tests/wp_acsl/initialized_shift_array.i | 56 ++++++++
.../oracle/initialized_shift_array.res.oracle | 134 ++++++++++++++++++
.../initialized_shift_array.res.oracle | 35 +++++
4 files changed, 232 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_acsl/initialized_shift_array.i
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 530280d0b20..87b4b38c114 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1103,6 +1103,13 @@ struct
let l = mloc_of_loc l in
M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
else
+ let rec normalize obj = function
+ | [] -> [], Extlib.id
+ | [Shift(elt, i)] when Ctypes.equal obj elt -> [], F.e_add i
+ | f :: ofs -> let l, fn = normalize obj ofs in f :: l, fn
+ in
+ let p, shift = normalize elt p in
+ let a = shift a and b = shift b in
let in_array = valid_range RW (vobject m x) p (elt, a, b) in
let initialized =
if x.vformal || x.vglob then p_true
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_shift_array.i b/src/plugins/wp/tests/wp_acsl/initialized_shift_array.i
new file mode 100644
index 00000000000..9fd5ed15b2f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/initialized_shift_array.i
@@ -0,0 +1,56 @@
+/*@
+ requires \initialized(buf + (0 .. count - 1));
+*/
+int test(char *buf, int count);
+
+// Success:
+
+void succ_full_first_cell(void){
+ char buf[3] = {0};
+ test(buf , 1);
+}
+void succ_full_full(void){
+ char buf[3] = {0};
+ test(&buf[0], 3);
+}
+void succ_full_from_1(void){
+ char buf[3] = {0};
+ test(buf+1 , 2);
+}
+void succ_from_1_from_1(void){
+ char buf[3];
+ buf[1] = buf[2] = 1 ;
+ test(buf+1 , 2);
+}
+void succ_full_from_2(void){
+ char buf[3] = {0};
+ test(&buf[2], 1);
+}
+
+// Failure:
+
+void fail_cell_before(void){
+ char buf[3] = {0};
+ test(buf-1 , 1);
+}
+void fail_too_long(void){
+ char buf[3] = {0};
+ test(buf , 4);
+}
+void fail_too_long_from_1(void){
+ char buf[3] = {0};
+ test(&buf[1], 3);
+}
+void fail_too_long_from_2(void){
+ char buf[3] = {0};
+ test(buf+2 , 2);
+}
+void fail_cell_after_end(void){
+ char buf[3] = {0};
+ test(buf+3 , 1);
+}
+void fail_partial_not_full(void){
+ char buf[3];
+ buf[0] = buf[1] = 0;
+ test(&buf[0], 3);
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
new file mode 100644
index 00000000000..7a9d25eed75
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
@@ -0,0 +1,134 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_shift_array.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel] tests/wp_acsl/initialized_shift_array.i:52: Warning:
+ No code nor implicit assigns clause for function test, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function fail_cell_after_end
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_cell_after_end' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 50)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_cell_before
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_cell_before' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 34)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_partial_not_full
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_partial_not_full' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 55)
+:
+Assume { (* Goal *) When: (0 <= i) /\ (i <= 2). }
+Prove: (([false..])[1 <- true][0 <- true][i]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_too_long
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 38)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_too_long_from_1
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 42)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_too_long_from_2
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long_from_2' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 46)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_from_1_from_1
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_from_1_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 23)
+:
+Assume { (* Goal *) When: (0 < i) /\ (i <= 2). }
+Prove: (([false..])[2 <- true][1 <- true][i]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_full_first_cell
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_first_cell' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 10)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_full_from_1
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 18)
+:
+Assume {
+ (* Goal *)
+ When: (0 < i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_buf_0[0]=true).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+ (Init_buf_0[i_1]=true))).
+}
+Prove: (Init_buf_0[i]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_full_from_2
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_from_2' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 27)
+:
+Assume {
+ (* Goal *)
+ When: (2 <= i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_buf_0[0]=true).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+ (Init_buf_0[i_1]=true))).
+}
+Prove: (Init_buf_0[2]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_full_full
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_full' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 14)
+:
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_buf_0[0]=true).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+ (Init_buf_0[i_1]=true))).
+}
+Prove: (Init_buf_0[i]=true).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
new file mode 100644
index 00000000000..ca01bf0f44a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
@@ -0,0 +1,35 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_shift_array.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel] tests/wp_acsl/initialized_shift_array.i:52: Warning:
+ No code nor implicit assigns clause for function test, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 11 goals scheduled
+[wp] [Qed] Goal typed_succ_full_first_cell_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_full_full_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_full_from_1_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_from_1_from_1_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_full_from_2_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_fail_cell_before_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_too_long_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_too_long_from_1_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_too_long_from_2_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_cell_after_end_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_partial_not_full_call_test_requires : Unsuccess
+[wp] Proved goals: 5 / 11
+ Qed: 1
+ Alt-Ergo: 4 (unsuccess: 6)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ succ_full_first_cell 1 - 1 100%
+ succ_full_full - 1 1 100%
+ succ_full_from_1 - 1 1 100%
+ succ_from_1_from_1 - 1 1 100%
+ succ_full_from_2 - 1 1 100%
+ fail_cell_before - - 1 0.0%
+ fail_too_long - - 1 0.0%
+ fail_too_long_from_1 - - 1 0.0%
+ fail_too_long_from_2 - - 1 0.0%
+ fail_cell_after_end - - 1 0.0%
+ fail_partial_not_full - - 1 0.0%
+------------------------------------------------------------
--
GitLab