From 885707e531a1e25318c84df2190e02a0cf1c4f5b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 8 Oct 2020 13:31:33 +0200
Subject: [PATCH] [wp] Make sure that init are dispatched to MemTyped when
needed
---
src/plugins/wp/MemVar.ml | 26 ++++++++++---------
.../wp/tests/wp_acsl/initialized_memtyped.i | 8 +++++-
.../oracle/initialized_memtyped.res.oracle | 20 ++++++++++++++
.../initialized_local_init.res.oracle | 4 +--
.../initialized_memtyped.res.oracle | 8 +++---
5 files changed, 48 insertions(+), 18 deletions(-)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index cff7c98d4b9..530280d0b20 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1085,11 +1085,11 @@ struct
| Ref _ -> p_true
| Loc l -> M.initialized sigma.mem (Rloc(obj,l))
| Val(m,x,p) ->
- if (x.vformal || x.vglob) then
+ if is_heap_allocated m then
+ M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
+ else if (x.vformal || x.vglob) then
try valid_offset RW (vobject m x) p
with ShiftMismatch -> shift_mismatch l
- else if is_heap_allocated m then
- M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
else
initialized_loc sigma obj x p
end
@@ -1099,17 +1099,18 @@ struct
| Loc l -> M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
| Val(m,x,p) ->
try
- let in_array = valid_range RW (vobject m x) p (elt, a, b) in
- let initialized =
- if x.vformal || x.vglob then p_true
- else initialized_range sigma (vobject m x) x p a b
- in
- F.p_imply (F.p_leq a b) (p_and in_array initialized)
- with ShiftMismatch ->
if is_heap_allocated m then
let l = mloc_of_loc l in
M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
- else shift_mismatch l
+ else
+ let in_array = valid_range RW (vobject m x) p (elt, a, b) in
+ let initialized =
+ if x.vformal || x.vglob then p_true
+ else initialized_range sigma (vobject m x) x p a b
+ in
+ F.p_imply (F.p_leq a b) (p_and in_array initialized)
+ with ShiftMismatch ->
+ shift_mismatch l
end
| Rrange(l, _,a,b) ->
Warning.error
@@ -1191,7 +1192,8 @@ struct
| Leave -> []
| Enter ->
let xs = List.filter
- (fun v -> not v.vformal && not v.vglob && not v.vdefined) xs
+ (fun v -> is_mvar_alloc v && not v.vformal &&
+ not v.vglob && not v.vdefined) xs
in
let uninitialized v =
let value = Cvalues.uninitialized_obj (Ctypes.object_of v.vtype) in
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
index b9a70c9c0fa..2968325323b 100644
--- a/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
+++ b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
@@ -81,4 +81,10 @@ void formal(int x)
{
int * p = &x ;
//@ assert provable: \initialized(p);
-}
\ No newline at end of file
+}
+
+void ptr_on_local(void){
+ int x[3] = {0} ;
+ int *p = x ;
+ //@ assert provable: \initialized(p + (0..2));
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
index 10608888723..1a01091dabd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
@@ -50,6 +50,26 @@ Goal Post-condition 'unknown' in 'glob_var':
Assume { (* Heap *) Type: (region(px_0.base) <= 0) /\ cinits(Init_0). }
Prove: (Init_0[px_0]=true).
+------------------------------------------------------------
+------------------------------------------------------------
+ Function ptr_on_local
+------------------------------------------------------------
+
+Goal Assertion 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 89):
+Let a = global(L_x_63).
+Assume {
+ (* Heap *)
+ Type: cinits(Init_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_0[shift_sint32(a, 0)]=true).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+ (Init_0[shift_sint32(a, i_1)]=true))).
+}
+Prove: (Init_0[shift_sint32(a, i)]=true).
+
------------------------------------------------------------
------------------------------------------------------------
Function test
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle
index 59f14e4c073..86800d74f72 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle
@@ -6,8 +6,8 @@
[wp] [Qed] Goal typed_l_int_assert_SUCCS : Valid
[wp] [Qed] Goal typed_l_int_assert_SUCCS_2 : Valid
[wp] [Alt-Ergo] Goal typed_l_int_check_FAILS : Unsuccess
-[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS : Valid (missing cache)
-[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS_2 : Valid (missing cache)
+[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS : Valid
+[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS_2 : Valid
[wp] [Alt-Ergo] Goal typed_l_array_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_l_struct_assert_SUCCS : Valid
[wp] [Qed] Goal typed_l_struct_assert_SUCCS_2 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
index 88684268b9c..3024322ab32 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_acsl/initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 28 goals scheduled
+[wp] 29 goals scheduled
[wp] [Alt-Ergo] Goal typed_test_check_unknown : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_3 : Unsuccess
@@ -31,13 +31,15 @@
[wp] [Alt-Ergo] Goal typed_glob_arr_ensures_provable : Valid
[wp] [Alt-Ergo] Goal typed_glob_arr_ensures_unknown : Unsuccess
[wp] [Alt-Ergo] Goal typed_formal_assert_provable : Valid
-[wp] Proved goals: 13 / 28
+[wp] [Alt-Ergo] Goal typed_ptr_on_local_assert_provable : Valid
+[wp] Proved goals: 14 / 29
Qed: 6
- Alt-Ergo: 7 (unsuccess: 15)
+ Alt-Ergo: 8 (unsuccess: 15)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
test 6 4 23 43.5%
glob_var - 1 2 50.0%
glob_arr - 1 2 50.0%
formal - 1 1 100%
+ ptr_on_local - 1 1 100%
------------------------------------------------------------
--
GitLab