From 29c20694715593de06936b43cfecf26c8a66ae21 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Tue, 17 Dec 2024 11:33:35 +0100
Subject: [PATCH] [wp] havoc->memcpy: non-qualif oracles
---
.../assigned_initialized_memtyped.res.oracle | 122 ++++----
...signed_not_initialized_memtyped.res.oracle | 43 +--
.../wp/tests/wp_acsl/oracle/axioms.res.oracle | 12 +-
.../wp_acsl/oracle/chunk_typing.res.oracle | 294 +++++++++---------
.../wp_acsl/oracle/looplabels.res.oracle | 4 +-
.../wp_acsl/oracle/opaque_struct.res.oracle | 36 +--
.../wp_acsl/oracle/simpl_is_type.res.oracle | 40 +--
.../wp_acsl/oracle/struct_fields.res.oracle | 16 +-
.../wp/tests/wp_acsl/oracle/zero.0.res.oracle | 7 +-
.../wp/tests/wp_acsl/oracle/zero.1.res.oracle | 6 +-
.../tests/wp_bts/oracle/bts_2110.res.oracle | 6 +-
.../wp_bytes/oracle/assigns_sep.res.oracle | 15 +-
.../tests/wp_bytes/oracle/structs.res.oracle | 2 +-
.../wp/tests/wp_bytes/oracle/union.res.oracle | 8 +-
.../oracle/reference_and_struct.res.oracle | 2 +-
.../oracle/reference_array.res.oracle | 2 +-
.../wp_plugin/oracle/combined.res.oracle | 30 +-
.../wp/tests/wp_plugin/oracle/copy.res.oracle | 12 +-
.../wp/tests/wp_plugin/oracle/loop.res.oracle | 9 +-
.../wp_plugin/oracle/string_c.res.oracle | 38 +--
.../oracle/unfold_assigns.0.res.oracle | 4 +-
.../oracle/unfold_assigns.1.res.oracle | 4 +-
.../oracle/unfold_assigns.2.res.oracle | 4 +-
.../oracle/unfold_assigns.3.res.oracle | 4 +-
.../wp_region/oracle/copy_array.res.oracle | 12 +-
.../oracle/multi_matrix_types.res.oracle | 20 +-
.../wp_typed/oracle/user_init.0.res.oracle | 46 +--
.../wp_typed/oracle/user_init.1.res.oracle | 46 +--
.../wp_usage/oracle/caveat_range.res.oracle | 42 +--
.../oracle/issue-189-bis.0.res.oracle | 20 +-
.../oracle/issue-189-bis.1.res.oracle | 35 ++-
31 files changed, 489 insertions(+), 452 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
index 27be73e9aa2..677ad375262 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
@@ -10,8 +10,8 @@ Goal Check 'FAILS' (file assigned_initialized_memtyped.i, line 69):
Let m = Init_0[shiftfield_F1_S_i(s) <- true].
Let a = shiftfield_F1_S_a(s).
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Init_undef_0, m, a_1, 10).
-Let a_3 = havoc(Init_undef_1, m, a_1, 10).
+Let a_2 = memcpy(m, Init_undef_0, a_1, a_1, 10).
+Let a_3 = memcpy(m, Init_undef_1, a_1, a_1, 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
@@ -63,25 +63,26 @@ Prove: IsInit_S1_S(global(G_glob_82), Init_0).
Goal Preservation of Invariant 'CHECK' (file assigned_initialized_memtyped.i, line 129):
Let a = shiftfield_F1_S_a(pg_0).
-Let a_1 = havoc(Init_undef_0, Init_0[shiftfield_F1_S_i(pg_0) <- true],
- shift_sint32(a, 0), 10).
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = memcpy(Init_0[shiftfield_F1_S_i(pg_0) <- true], Init_undef_0, a_1,
+ a_1, 10).
Assume {
Type: is_sint32(i) /\ is_sint32(1 + i).
(* Heap *)
Type: (region(G_glob_82) <= 0) /\ (region(pg_0.base) <= 0) /\
cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: cinits(a_1).
+ Have: cinits(a_2).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_1[shift_sint32(a, i_1)]=true)))).
+ (a_2[shift_sint32(a, i_1)]=true)))).
(* Then *)
Have: i <= 9.
}
Prove: ((-1) <= i) /\
(forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
- (a_1[shift_sint32(a, i) <- true][shift_sint32(a, i_1)]=true)))).
+ (a_2[shift_sint32(a, i) <- true][shift_sint32(a, i_1)]=true)))).
------------------------------------------------------------
@@ -92,20 +93,21 @@ Prove: true.
Goal Check 'FAILS' (file assigned_initialized_memtyped.i, line 142):
Let m = Init_0[shiftfield_F1_S_i(pg_0) <- true].
-Let a = havoc(Init_undef_0, m, pg_0, 11).
+Let a = memcpy(m, Init_undef_0, pg_0, pg_0, 11).
Let a_1 = shiftfield_F1_S_a(pg_0).
-Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
+Let a_2 = shift_sint32(a_1, 0).
+Let a_3 = memcpy(m, Init_undef_1, a_2, a_2, 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(G_glob_82) <= 0) /\ (region(pg_0.base) <= 0) /\
cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: cinits(a_2).
+ Have: cinits(a_3).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_2[shift_sint32(a_1, i_2)]=true)))).
+ (a_3[shift_sint32(a_1, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
@@ -121,20 +123,21 @@ Prove: IsInit_S1_S(pg_0, a).
Goal Check 'FAILS' (file assigned_initialized_memtyped.i, line 143):
Let m = Init_0[shiftfield_F1_S_i(pg_0) <- true].
-Let a = havoc(Init_undef_0, m, pg_0, 11).
+Let a = memcpy(m, Init_undef_0, pg_0, pg_0, 11).
Let a_1 = shiftfield_F1_S_a(pg_0).
-Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
+Let a_2 = shift_sint32(a_1, 0).
+Let a_3 = memcpy(m, Init_undef_1, a_2, a_2, 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(G_glob_82) <= 0) /\ (region(pg_0.base) <= 0) /\
cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: cinits(a_2).
+ Have: cinits(a_3).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_2[shift_sint32(a_1, i_2)]=true)))).
+ (a_3[shift_sint32(a_1, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
@@ -187,19 +190,20 @@ Prove: true.
Goal Check 'FAILS' (file assigned_initialized_memtyped.i, line 118):
Let m = Init_0[shiftfield_F1_S_i(s) <- true].
-Let a = havoc(Init_undef_0, m, s, 11).
+Let a = memcpy(m, Init_undef_0, s, s, 11).
Let a_1 = shiftfield_F1_S_a(s).
-Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
+Let a_2 = shift_sint32(a_1, 0).
+Let a_3 = memcpy(m, Init_undef_1, a_2, a_2, 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: cinits(a_2).
+ Have: cinits(a_3).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_2[shift_sint32(a_1, i_2)]=true)))).
+ (a_3[shift_sint32(a_1, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
@@ -237,7 +241,7 @@ Goal Check 'FAILS' (file assigned_initialized_memtyped.i, line 99):
Let a = shiftfield_F1_S_a(s).
Let a_1 = shiftfield_F1_S_i(s).
Let a_2 = shift_sint32(a, 0).
-Let a_3 = havoc(Init_undef_0, Init_1[a_1 <- true], a_2, 10).
+Let a_3 = memcpy(Init_1[a_1 <- true], Init_undef_0, a_2, a_2, 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
@@ -259,7 +263,8 @@ Assume {
(forall a_4 : addr.
((forall i_2 : Z. (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) ->
(shift_sint32(a, i_2) != a_4))) ->
- (havoc(Mint_undef_0, Mint_0[a_1 <- 0], a_2, 10)[a_4] = Mint_1[a_4]))).
+ (memcpy(Mint_0[a_1 <- 0], Mint_undef_0, a_2, a_2, 10)[a_4] =
+ Mint_1[a_4]))).
(* Else *)
Have: 10 <= i_1.
}
@@ -275,6 +280,7 @@ Prove: true.
Goal Loop assigns 'CHECK' (2/5):
Effect at line 96
Let a = shiftfield_F1_S_a(s).
+Let a_1 = shift_sint32(a, 0).
Assume {
Type: is_sint32(i_2) /\ is_sint32(i_3).
(* Heap *)
@@ -288,11 +294,11 @@ Assume {
(* Else *)
Have: 10 <= i_2.
(* Loop assigns 'CHECK' *)
- Have: forall a_1 : addr.
+ Have: forall a_2 : addr.
((forall i_5 : Z. (((i_5 = 0) \/ (i_5 = 2) \/ (i_5 = 4)) ->
- (shift_sint32(a, i_5) != a_1))) ->
- (havoc(Mint_undef_0, Mint_0[shiftfield_F1_S_i(s) <- 0],
- shift_sint32(a, 0), 10)[a_1] = Mint_1[a_1])).
+ (shift_sint32(a, i_5) != a_2))) ->
+ (memcpy(Mint_0[shiftfield_F1_S_i(s) <- 0], Mint_undef_0, a_1, a_1, 10)
+ [a_2] = Mint_1[a_2])).
(* Then *)
Have: i_3 <= 9.
}
@@ -325,26 +331,27 @@ Prove: true.
Goal Check 'FAILS' (file assigned_initialized_memtyped.i, line 51):
Let a = shiftfield_F1_S_i(s).
Let a_1 = shiftfield_F1_S_a(s).
-Let a_2 = havoc(Init_undef_0, Init_0[a <- true], shift_sint32(a_1, 0), 10).
-Let a_3 = a_2[a <- i].
+Let a_2 = shift_sint32(a_1, 0).
+Let a_3 = memcpy(Init_0[a <- true], Init_undef_0, a_2, a_2, 10).
+Let a_4 = a_3[a <- i].
Assume {
Type: is_sint32(i_1) /\ is_sint32(i_2).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: cinits(a_2).
+ Have: cinits(a_3).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10) /\
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
- (a_2[shift_sint32(a_1, i_3)]=true)))).
+ (a_3[shift_sint32(a_1, i_3)]=true)))).
(* Else *)
Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
- Have: cinits(a_3).
+ Have: cinits(a_4).
(* Else *)
Have: 10 <= i_2.
}
-Prove: IsInit_S1_S(s, a_3).
+Prove: IsInit_S1_S(s, a_4).
------------------------------------------------------------
@@ -364,27 +371,28 @@ Prove: true.
Goal Check 'FAILS' (file assigned_initialized_memtyped.i, line 84):
Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_0, Init_0[shiftfield_F1_S_i(s) <- true],
- shift_sint32(a, 0), 10).
-Let a_2 = a_1[shift_sint32(a, 4) <- i].
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = memcpy(Init_0[shiftfield_F1_S_i(s) <- true], Init_undef_0, a_1,
+ a_1, 10).
+Let a_3 = a_2[shift_sint32(a, 4) <- i].
Assume {
Type: is_sint32(i_1) /\ is_sint32(i_2).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: cinits(a_1).
+ Have: cinits(a_2).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10) /\
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
- (a_1[shift_sint32(a, i_3)]=true)))).
+ (a_2[shift_sint32(a, i_3)]=true)))).
(* Else *)
Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
- Have: cinits(a_2).
+ Have: cinits(a_3).
(* Else *)
Have: 10 <= i_2.
}
-Prove: IsInit_S1_S(s, a_2).
+Prove: IsInit_S1_S(s, a_3).
------------------------------------------------------------
@@ -410,24 +418,25 @@ Prove: true.
Goal Preservation of Invariant 'CHECK' (file assigned_initialized_memtyped.i, line 16):
Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_0, Init_0[shiftfield_F1_S_i(s) <- true],
- shift_sint32(a, 0), 10).
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = memcpy(Init_0[shiftfield_F1_S_i(s) <- true], Init_undef_0, a_1,
+ a_1, 10).
Assume {
Type: is_sint32(i) /\ is_sint32(1 + i).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: cinits(a_1).
+ Have: cinits(a_2).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_1[shift_sint32(a, i_1)]=true)))).
+ (a_2[shift_sint32(a, i_1)]=true)))).
(* Then *)
Have: i <= 9.
}
Prove: ((-1) <= i) /\
(forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
- (a_1[shift_sint32(a, i) <- true][shift_sint32(a, i_1)]=true)))).
+ (a_2[shift_sint32(a, i) <- true][shift_sint32(a, i_1)]=true)))).
------------------------------------------------------------
@@ -438,22 +447,23 @@ Prove: true.
Goal Check 'CHECK' (file assigned_initialized_memtyped.i, line 21):
Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_0, Init_0[shiftfield_F1_S_i(s) <- true],
- shift_sint32(a, 0), 10).
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = memcpy(Init_0[shiftfield_F1_S_i(s) <- true], Init_undef_0, a_1,
+ a_1, 10).
Assume {
Type: is_sint32(i).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: cinits(a_1).
+ Have: cinits(a_2).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_1[shift_sint32(a, i_1)]=true)))).
+ (a_2[shift_sint32(a, i_1)]=true)))).
(* Else *)
Have: 10 <= i.
}
-Prove: IsInit_S1_S(s, a_1).
+Prove: IsInit_S1_S(s, a_2).
------------------------------------------------------------
@@ -479,27 +489,29 @@ Prove: true.
Goal Check 'FAILS' (file assigned_initialized_memtyped.i, line 36):
Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_1, Init_0[shiftfield_F1_S_i(s) <- true],
- shift_sint32(a, 0), 10).
-Let a_2 = havoc(Init_undef_0, a_1, shift_sint32(a, 1), 4).
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = memcpy(Init_0[shiftfield_F1_S_i(s) <- true], Init_undef_0, a_1,
+ a_1, 10).
+Let a_3 = shift_sint32(a, 1).
+Let a_4 = memcpy(a_2, Init_undef_1, a_3, a_3, 4).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: cinits(a_1).
+ Have: cinits(a_2).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shift_sint32(a, i_2)]=true)))).
+ (a_2[shift_sint32(a, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: cinits(a_2).
+ Have: cinits(a_4).
(* Else *)
Have: 10 <= i_1.
}
-Prove: IsInit_S1_S(s, a_2).
+Prove: IsInit_S1_S(s, a_4).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
index cc9ab803f2d..15eea06fe87 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
@@ -7,17 +7,18 @@
------------------------------------------------------------
Goal Check 'FAIL' (file assigned_not_initialized_memtyped.i, line 28):
-Let a = havoc(Init_undef_0, Init_0, shift_sint32(array_0, 0), 10).
+Let a = shift_sint32(array_0, 0).
+Let a_1 = memcpy(Init_0, Init_undef_0, a, a, 10).
Assume {
Type: is_sint32(i).
(* Heap *)
Type: (region(array_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: cinits(a).
+ Have: cinits(a_1).
(* Else *)
Have: 10 <= i.
}
-Prove: IsInitArray_sint32(array_0, 10, a).
+Prove: IsInitArray_sint32(array_0, 10, a_1).
------------------------------------------------------------
------------------------------------------------------------
@@ -25,38 +26,41 @@ Prove: IsInitArray_sint32(array_0, 10, a).
------------------------------------------------------------
Goal Check 'FAIL' (file assigned_not_initialized_memtyped.i, line 60):
-Let a = havoc(Init_undef_1, Init_0, shift_sint32(global(G_glob_array_51), 0),
- 10).
-Let a_1 = havoc(Init_undef_0, a, shift_sint32(pg_array_0, 0), 10).
+Let a = shift_sint32(global(G_glob_array_51), 0).
+Let a_1 = memcpy(Init_0, Init_undef_0, a, a, 10).
+Let a_2 = shift_sint32(pg_array_0, 0).
+Let a_3 = memcpy(a_1, Init_undef_1, a_2, a_2, 10).
Assume {
Type: is_sint32(i).
(* Heap *)
Type: (region(G_glob_array_51) <= 0) /\ (region(pg_array_0.base) <= 0) /\
cinits(Init_0).
(* Loop assigns ... *)
- Have: cinits(a) /\ cinits(a_1).
+ Have: cinits(a_1) /\ cinits(a_3).
(* Else *)
Have: 10 <= i.
}
-Prove: IsInitArray_sint32(pg_array_0, 10, a_1).
+Prove: IsInitArray_sint32(pg_array_0, 10, a_3).
------------------------------------------------------------
Goal Check 'OK' (file assigned_not_initialized_memtyped.i, line 61):
Let a = global(G_glob_array_51).
-Let a_1 = havoc(Init_undef_1, Init_0, shift_sint32(a, 0), 10).
-Let a_2 = havoc(Init_undef_0, a_1, shift_sint32(pg_array_0, 0), 10).
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = memcpy(Init_0, Init_undef_0, a_1, a_1, 10).
+Let a_3 = shift_sint32(pg_array_0, 0).
+Let a_4 = memcpy(a_2, Init_undef_1, a_3, a_3, 10).
Assume {
Type: is_sint32(i).
(* Heap *)
Type: (region(G_glob_array_51) <= 0) /\ (region(pg_array_0.base) <= 0) /\
cinits(Init_0).
(* Loop assigns ... *)
- Have: cinits(a_1) /\ cinits(a_2).
+ Have: cinits(a_2) /\ cinits(a_4).
(* Else *)
Have: 10 <= i.
}
-Prove: IsInitArray_sint32(a, 10, a_2).
+Prove: IsInitArray_sint32(a, 10, a_4).
------------------------------------------------------------
------------------------------------------------------------
@@ -97,26 +101,27 @@ Prove: (m_1[a]=true).
------------------------------------------------------------
Goal Check 'FAIL' (file assigned_not_initialized_memtyped.i, line 49):
-Let a = havoc(Init_undef_1, Init_0, global(G_glob_comp_45), 11).
-Let a_1 = havoc(Init_undef_0, a, pg_comp_0, 11).
+Let a = global(G_glob_comp_45).
+Let a_1 = memcpy(Init_0, Init_undef_0, a, a, 11).
+Let a_2 = memcpy(a_1, Init_undef_1, pg_comp_0, pg_comp_0, 11).
Assume {
Type: is_sint32(i).
(* Heap *)
Type: (region(G_glob_comp_45) <= 0) /\ (region(pg_comp_0.base) <= 0) /\
cinits(Init_0).
(* Loop assigns ... *)
- Have: cinits(a) /\ cinits(a_1).
+ Have: cinits(a_1) /\ cinits(a_2).
(* Else *)
Have: 10 <= i.
}
-Prove: IsInit_S1_S(pg_comp_0, a_1).
+Prove: IsInit_S1_S(pg_comp_0, a_2).
------------------------------------------------------------
Goal Check 'FAIL' (file assigned_not_initialized_memtyped.i, line 50):
Let a = global(G_glob_comp_45).
-Let a_1 = havoc(Init_undef_1, Init_0, a, 11).
-Let a_2 = havoc(Init_undef_0, a_1, pg_comp_0, 11).
+Let a_1 = memcpy(Init_0, Init_undef_0, a, a, 11).
+Let a_2 = memcpy(a_1, Init_undef_1, pg_comp_0, pg_comp_0, 11).
Assume {
Type: is_sint32(i).
(* Heap *)
@@ -144,7 +149,7 @@ Prove: (i=true).
------------------------------------------------------------
Goal Check 'FAIL' (file assigned_not_initialized_memtyped.i, line 22):
-Let a = havoc(Init_undef_0, Init_0, s, 11).
+Let a = memcpy(Init_0, Init_undef_0, s, s, 11).
Assume {
Type: is_sint32(i).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
index 4cd6d14f461..ef6d4421d9d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
@@ -11,7 +11,7 @@
Goal Post-condition 'P,todo' in 'f':
Let a_1 = shift_sint32(t, a).
Let x = -a.
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, i - a).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, i - a).
Let x_1 = 1 + b.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(i).
@@ -38,7 +38,7 @@ Prove: P_P(a_2, t, a, b).
Goal Post-condition 'Q' in 'f':
Let a_1 = shift_sint32(t, a).
Let x = -a.
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, i - a).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, i - a).
Let x_1 = 1 + b.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(i).
@@ -81,7 +81,9 @@ Assume {
Have: (a <= i) /\ (i <= x_1).
(* Invariant 'Positive' *)
Have: forall i_1 : Z. ((a <= i_1) -> ((i_1 < i) ->
- (0 < havoc(Mint_undef_0, Mint_0, a_1, i - a)[shift_sint32(t, i_1)]))).
+ (0
+ < memcpy(Mint_0, Mint_undef_0, a_1, a_1, i - a)
+ [shift_sint32(t, i_1)]))).
(* Then *)
Have: i <= b.
}
@@ -107,7 +109,7 @@ Goal Preservation of Invariant 'Positive' (file axioms.i, line 31):
Let x = 1 + i.
Let a_1 = shift_sint32(t, a).
Let x_1 = -a.
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, i - a).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, i - a).
Let x_2 = 1 + b.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(i) /\ is_sint32(x).
@@ -155,7 +157,7 @@ Goal Loop assigns (file axioms.i, line 32) (3/3):
Effect at line 35
Let a_1 = shift_sint32(t, a).
Let x = -a.
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, i - a).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, i - a).
Let a_3 = shift_sint32(t, i).
Let x_1 = 1 + i.
Let x_2 = 1 + b.
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index cd9646ce0fd..1ebf1e9f5c9 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -10,33 +10,33 @@
Goal Post-condition (file chunk_typing.i, line 15) in 'function':
Let a = shift_uint64(u64_0, 0).
-Let a_1 = havoc(Mint_undef_6, Mint_6, a, 10).
+Let a_1 = memcpy(Mint_5, Mint_undef_5, a, a, 10).
Let a_2 = shift_sint64(i64_0, 0).
-Let a_3 = havoc(Mint_undef_5, Mint_5, a_2, 10).
+Let a_3 = memcpy(Mint_6, Mint_undef_6, a_2, a_2, 10).
Let a_4 = shift_uint32(u32_0, 0).
-Let a_5 = havoc(Mint_undef_4, Mint_4, a_4, 10).
+Let a_5 = memcpy(Mint_3, Mint_undef_3, a_4, a_4, 10).
Let a_6 = shift_sint32(i32_0, 0).
-Let a_7 = havoc(Mint_undef_3, Mint_3, a_6, 10).
+Let a_7 = memcpy(Mint_4, Mint_undef_4, a_6, a_6, 10).
Let a_8 = shift_uint16(u16_0, 0).
-Let a_9 = havoc(Mint_undef_2, Mint_2, a_8, 10).
+Let a_9 = memcpy(Mint_1, Mint_undef_1, a_8, a_8, 10).
Let a_10 = shift_sint16(i16_0, 0).
-Let a_11 = havoc(Mint_undef_1, Mint_1, a_10, 10).
+Let a_11 = memcpy(Mint_2, Mint_undef_2, a_10, a_10, 10).
Let a_12 = shift_uint8(u8_0, 0).
-Let a_13 = havoc(Mint_undef_0, Mint_0, a_12, 10).
+Let a_13 = memcpy(Mint_0, Mint_undef_0, a_12, a_12, 10).
Let a_14 = shift_sint8(i8_0, 0).
-Let a_15 = havoc(Mchar_undef_0, Mchar_0, a_14, 10).
+Let a_15 = memcpy(Mchar_0, Mchar_undef_0, a_14, a_14, 10).
Let a_16 = a_15[shift_sint8(i8_0, i)].
Let a_17 = a_13[shift_uint8(u8_0, i)].
-Let a_18 = a_11[shift_sint16(i16_0, i)].
-Let a_19 = a_9[shift_uint16(u16_0, i)].
-Let a_20 = a_7[shift_sint32(i32_0, i)].
-Let a_21 = a_5[shift_uint32(u32_0, i)].
+Let a_18 = a_9[shift_uint16(u16_0, i)].
+Let a_19 = a_11[shift_sint16(i16_0, i)].
+Let a_20 = a_5[shift_uint32(u32_0, i)].
+Let a_21 = a_7[shift_sint32(i32_0, i)].
Let a_22 = a_3[shift_sint64(i64_0, i)].
Assume {
- Type: IsArray_sint8(x) /\ is_sint16_chunk(Mint_1) /\
- is_sint32_chunk(Mint_3) /\ is_sint64_chunk(Mint_5) /\
- is_sint8_chunk(Mchar_0) /\ is_uint16_chunk(Mint_2) /\
- is_uint32_chunk(Mint_4) /\ is_uint64_chunk(Mint_6) /\
+ Type: IsArray_sint8(x) /\ is_sint16_chunk(Mint_2) /\
+ is_sint32_chunk(Mint_4) /\ is_sint64_chunk(Mint_6) /\
+ is_sint8_chunk(Mchar_0) /\ is_uint16_chunk(Mint_1) /\
+ is_uint32_chunk(Mint_3) /\ is_uint64_chunk(Mint_5) /\
is_uint8_chunk(Mint_0) /\ is_sint32(i_1) /\ is_sint16_chunk(a_11) /\
is_sint32_chunk(a_7) /\ is_sint64_chunk(a_3) /\ is_sint8_chunk(a_15) /\
is_uint16_chunk(a_9) /\ is_uint32_chunk(a_5) /\ is_uint64_chunk(a_1) /\
@@ -85,9 +85,9 @@ Assume {
(* Else *)
Have: 10 <= i_1.
}
-Prove: (a_16 = (1 + x[i])) /\ (a_17 = (1 + a_16)) /\ (a_18 = (1 + a_17)) /\
- (a_19 = (1 + a_18)) /\ (a_20 = (1 + a_19)) /\ (a_21 = (1 + a_20)) /\
- (a_22 = (1 + a_21)) /\ (a_1[shift_uint64(u64_0, i)] = (1 + a_22)).
+Prove: (a_16 = (1 + x[i])) /\ (a_17 = (1 + a_16)) /\ (a_18 = (1 + a_19)) /\
+ (a_19 = (1 + a_17)) /\ (a_20 = (1 + a_21)) /\ (a_21 = (1 + a_18)) /\
+ (a_1[shift_uint64(u64_0, i)] = (1 + a_22)) /\ (a_22 = (1 + a_20)).
------------------------------------------------------------
@@ -111,21 +111,21 @@ Let a_5 = shift_sint16(i16_0, i).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = shift_sint8(i8_0, i).
Let a_8 = shift_uint64(u64_0, 0).
-Let a_9 = havoc(Mint_undef_5, Mint_5, a_8, 10).
+Let a_9 = memcpy(Mint_5, Mint_undef_5, a_8, a_8, 10).
Let a_10 = shift_sint64(i64_0, 0).
-Let a_11 = havoc(Mint_undef_2, Mint_2, a_10, 10).
+Let a_11 = memcpy(Mint_2, Mint_undef_2, a_10, a_10, 10).
Let a_12 = shift_uint32(u32_0, 0).
-Let a_13 = havoc(Mint_undef_4, Mint_4, a_12, 10).
+Let a_13 = memcpy(Mint_4, Mint_undef_4, a_12, a_12, 10).
Let a_14 = shift_sint32(i32_0, 0).
-Let a_15 = havoc(Mint_undef_1, Mint_1, a_14, 10).
+Let a_15 = memcpy(Mint_1, Mint_undef_1, a_14, a_14, 10).
Let a_16 = shift_uint16(u16_0, 0).
-Let a_17 = havoc(Mint_undef_3, Mint_3, a_16, 10).
+Let a_17 = memcpy(Mint_3, Mint_undef_3, a_16, a_16, 10).
Let a_18 = shift_sint16(i16_0, 0).
-Let a_19 = havoc(Mint_undef_0, Mint_0, a_18, 10).
+Let a_19 = memcpy(Mint_0, Mint_undef_0, a_18, a_18, 10).
Let a_20 = shift_uint8(u8_0, 0).
-Let a_21 = havoc(Mint_undef_6, Mint_6, a_20, 10).
+Let a_21 = memcpy(Mint_6, Mint_undef_6, a_20, a_20, 10).
Let a_22 = shift_sint8(i8_0, 0).
-Let a_23 = havoc(Mchar_undef_0, Mchar_0, a_22, 10).
+Let a_23 = memcpy(Mchar_0, Mchar_undef_0, a_22, a_22, 10).
Let a_24 = a_23[a_7 <- 1].
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
@@ -213,7 +213,7 @@ Prove: true.
Goal Preservation of Invariant (file chunk_typing.i, line 33):
Let a = shift_sint8(i8_0, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, 10).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, 10).
Let a_2 = shift_sint8(i8_0, i).
Let a_3 = a_1[a_2 <- 1].
Let a_4 = shift_uint64(u64_0, i).
@@ -224,19 +224,19 @@ Let a_8 = shift_uint16(u16_0, i).
Let a_9 = shift_sint16(i16_0, i).
Let a_10 = shift_uint8(u8_0, i).
Let a_11 = shift_uint64(u64_0, 0).
-Let a_12 = havoc(Mint_undef_6, Mint_6, a_11, 10).
+Let a_12 = memcpy(Mint_6, Mint_undef_6, a_11, a_11, 10).
Let a_13 = shift_sint64(i64_0, 0).
-Let a_14 = havoc(Mint_undef_3, Mint_3, a_13, 10).
+Let a_14 = memcpy(Mint_3, Mint_undef_3, a_13, a_13, 10).
Let a_15 = shift_uint32(u32_0, 0).
-Let a_16 = havoc(Mint_undef_5, Mint_5, a_15, 10).
+Let a_16 = memcpy(Mint_5, Mint_undef_5, a_15, a_15, 10).
Let a_17 = shift_sint32(i32_0, 0).
-Let a_18 = havoc(Mint_undef_2, Mint_2, a_17, 10).
+Let a_18 = memcpy(Mint_2, Mint_undef_2, a_17, a_17, 10).
Let a_19 = shift_uint16(u16_0, 0).
-Let a_20 = havoc(Mint_undef_4, Mint_4, a_19, 10).
+Let a_20 = memcpy(Mint_4, Mint_undef_4, a_19, a_19, 10).
Let a_21 = shift_sint16(i16_0, 0).
-Let a_22 = havoc(Mint_undef_1, Mint_1, a_21, 10).
+Let a_22 = memcpy(Mint_1, Mint_undef_1, a_21, a_21, 10).
Let a_23 = shift_uint8(u8_0, 0).
-Let a_24 = havoc(Mint_undef_0, Mint_0, a_23, 10).
+Let a_24 = memcpy(Mint_0, Mint_undef_0, a_23, a_23, 10).
Let a_25 = a_24[a_10 <- 2].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
@@ -327,11 +327,11 @@ Prove: true.
Goal Preservation of Invariant (file chunk_typing.i, line 34):
Let a = shift_uint8(u8_0, 0).
-Let a_1 = havoc(Mint_undef_6, Mint_6, a, 10).
+Let a_1 = memcpy(Mint_6, Mint_undef_6, a, a, 10).
Let a_2 = shift_uint8(u8_0, i).
Let a_3 = a_1[a_2 <- 2].
Let a_4 = shift_sint8(i8_0, 0).
-Let a_5 = havoc(Mchar_undef_0, Mchar_0, a_4, 10).
+Let a_5 = memcpy(Mchar_0, Mchar_undef_0, a_4, a_4, 10).
Let a_6 = shift_sint8(i8_0, i).
Let a_7 = a_5[a_6 <- 1].
Let a_8 = shift_uint64(u64_0, i).
@@ -341,17 +341,17 @@ Let a_11 = shift_sint32(i32_0, i).
Let a_12 = shift_uint16(u16_0, i).
Let a_13 = shift_sint16(i16_0, i).
Let a_14 = shift_uint64(u64_0, 0).
-Let a_15 = havoc(Mint_undef_5, Mint_5, a_14, 10).
+Let a_15 = memcpy(Mint_5, Mint_undef_5, a_14, a_14, 10).
Let a_16 = shift_sint64(i64_0, 0).
-Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
+Let a_17 = memcpy(Mint_2, Mint_undef_2, a_16, a_16, 10).
Let a_18 = shift_uint32(u32_0, 0).
-Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
+Let a_19 = memcpy(Mint_4, Mint_undef_4, a_18, a_18, 10).
Let a_20 = shift_sint32(i32_0, 0).
-Let a_21 = havoc(Mint_undef_1, Mint_1, a_20, 10).
+Let a_21 = memcpy(Mint_1, Mint_undef_1, a_20, a_20, 10).
Let a_22 = shift_uint16(u16_0, 0).
-Let a_23 = havoc(Mint_undef_3, Mint_3, a_22, 10).
+Let a_23 = memcpy(Mint_3, Mint_undef_3, a_22, a_22, 10).
Let a_24 = shift_sint16(i16_0, 0).
-Let a_25 = havoc(Mint_undef_0, Mint_0, a_24, 10).
+Let a_25 = memcpy(Mint_0, Mint_undef_0, a_24, a_24, 10).
Let a_26 = a_25[a_13 <- 3].
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
@@ -445,15 +445,15 @@ Prove: true.
Goal Preservation of Invariant (file chunk_typing.i, line 35):
Let a = shift_sint16(i16_0, 0).
-Let a_1 = havoc(Mint_undef_1, Mint_1, a, 10).
+Let a_1 = memcpy(Mint_1, Mint_undef_1, a, a, 10).
Let a_2 = shift_sint16(i16_0, i).
Let a_3 = a_1[a_2 <- 3].
Let a_4 = shift_uint8(u8_0, 0).
-Let a_5 = havoc(Mint_undef_6, Mint_6, a_4, 10).
+Let a_5 = memcpy(Mint_6, Mint_undef_6, a_4, a_4, 10).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = a_5[a_6 <- 2].
Let a_8 = shift_sint8(i8_0, 0).
-Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_9 = memcpy(Mchar_0, Mchar_undef_0, a_8, a_8, 10).
Let a_10 = shift_sint8(i8_0, i).
Let a_11 = a_9[a_10 <- 1].
Let a_12 = shift_uint64(u64_0, i).
@@ -462,15 +462,15 @@ Let a_14 = shift_uint32(u32_0, i).
Let a_15 = shift_sint32(i32_0, i).
Let a_16 = shift_uint16(u16_0, i).
Let a_17 = shift_uint64(u64_0, 0).
-Let a_18 = havoc(Mint_undef_5, Mint_5, a_17, 10).
+Let a_18 = memcpy(Mint_5, Mint_undef_5, a_17, a_17, 10).
Let a_19 = shift_sint64(i64_0, 0).
-Let a_20 = havoc(Mint_undef_3, Mint_3, a_19, 10).
+Let a_20 = memcpy(Mint_3, Mint_undef_3, a_19, a_19, 10).
Let a_21 = shift_uint32(u32_0, 0).
-Let a_22 = havoc(Mint_undef_4, Mint_4, a_21, 10).
+Let a_22 = memcpy(Mint_4, Mint_undef_4, a_21, a_21, 10).
Let a_23 = shift_sint32(i32_0, 0).
-Let a_24 = havoc(Mint_undef_2, Mint_2, a_23, 10).
+Let a_24 = memcpy(Mint_2, Mint_undef_2, a_23, a_23, 10).
Let a_25 = shift_uint16(u16_0, 0).
-Let a_26 = havoc(Mint_undef_0, Mint_0, a_25, 10).
+Let a_26 = memcpy(Mint_0, Mint_undef_0, a_25, a_25, 10).
Let a_27 = a_26[a_16 <- 4].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
@@ -567,19 +567,19 @@ Prove: true.
Goal Preservation of Invariant (file chunk_typing.i, line 36):
Let a = shift_uint16(u16_0, 0).
-Let a_1 = havoc(Mint_undef_3, Mint_3, a, 10).
+Let a_1 = memcpy(Mint_3, Mint_undef_3, a, a, 10).
Let a_2 = shift_uint16(u16_0, i).
Let a_3 = a_1[a_2 <- 4].
Let a_4 = shift_sint16(i16_0, 0).
-Let a_5 = havoc(Mint_undef_1, Mint_1, a_4, 10).
+Let a_5 = memcpy(Mint_1, Mint_undef_1, a_4, a_4, 10).
Let a_6 = shift_sint16(i16_0, i).
Let a_7 = a_5[a_6 <- 3].
Let a_8 = shift_uint8(u8_0, 0).
-Let a_9 = havoc(Mint_undef_6, Mint_6, a_8, 10).
+Let a_9 = memcpy(Mint_6, Mint_undef_6, a_8, a_8, 10).
Let a_10 = shift_uint8(u8_0, i).
Let a_11 = a_9[a_10 <- 2].
Let a_12 = shift_sint8(i8_0, 0).
-Let a_13 = havoc(Mchar_undef_0, Mchar_0, a_12, 10).
+Let a_13 = memcpy(Mchar_0, Mchar_undef_0, a_12, a_12, 10).
Let a_14 = shift_sint8(i8_0, i).
Let a_15 = a_13[a_14 <- 1].
Let a_16 = shift_uint64(u64_0, i).
@@ -587,13 +587,13 @@ Let a_17 = shift_sint64(i64_0, i).
Let a_18 = shift_uint32(u32_0, i).
Let a_19 = shift_sint32(i32_0, i).
Let a_20 = shift_uint64(u64_0, 0).
-Let a_21 = havoc(Mint_undef_5, Mint_5, a_20, 10).
+Let a_21 = memcpy(Mint_5, Mint_undef_5, a_20, a_20, 10).
Let a_22 = shift_sint64(i64_0, 0).
-Let a_23 = havoc(Mint_undef_2, Mint_2, a_22, 10).
+Let a_23 = memcpy(Mint_2, Mint_undef_2, a_22, a_22, 10).
Let a_24 = shift_uint32(u32_0, 0).
-Let a_25 = havoc(Mint_undef_4, Mint_4, a_24, 10).
+Let a_25 = memcpy(Mint_4, Mint_undef_4, a_24, a_24, 10).
Let a_26 = shift_sint32(i32_0, 0).
-Let a_27 = havoc(Mint_undef_0, Mint_0, a_26, 10).
+Let a_27 = memcpy(Mint_0, Mint_undef_0, a_26, a_26, 10).
Let a_28 = a_27[a_19 <- 5].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_0) /\
@@ -693,34 +693,34 @@ Prove: true.
Goal Preservation of Invariant (file chunk_typing.i, line 37):
Let a = shift_sint32(i32_0, 0).
-Let a_1 = havoc(Mint_undef_2, Mint_2, a, 10).
+Let a_1 = memcpy(Mint_2, Mint_undef_2, a, a, 10).
Let a_2 = shift_sint32(i32_0, i).
Let a_3 = a_1[a_2 <- 5].
Let a_4 = shift_uint16(u16_0, 0).
-Let a_5 = havoc(Mint_undef_4, Mint_4, a_4, 10).
+Let a_5 = memcpy(Mint_4, Mint_undef_4, a_4, a_4, 10).
Let a_6 = shift_uint16(u16_0, i).
Let a_7 = a_5[a_6 <- 4].
Let a_8 = shift_sint16(i16_0, 0).
-Let a_9 = havoc(Mint_undef_1, Mint_1, a_8, 10).
+Let a_9 = memcpy(Mint_1, Mint_undef_1, a_8, a_8, 10).
Let a_10 = shift_sint16(i16_0, i).
Let a_11 = a_9[a_10 <- 3].
Let a_12 = shift_uint8(u8_0, 0).
-Let a_13 = havoc(Mint_undef_6, Mint_6, a_12, 10).
+Let a_13 = memcpy(Mint_6, Mint_undef_6, a_12, a_12, 10).
Let a_14 = shift_uint8(u8_0, i).
Let a_15 = a_13[a_14 <- 2].
Let a_16 = shift_sint8(i8_0, 0).
-Let a_17 = havoc(Mchar_undef_0, Mchar_0, a_16, 10).
+Let a_17 = memcpy(Mchar_0, Mchar_undef_0, a_16, a_16, 10).
Let a_18 = shift_sint8(i8_0, i).
Let a_19 = a_17[a_18 <- 1].
Let a_20 = shift_uint64(u64_0, i).
Let a_21 = shift_sint64(i64_0, i).
Let a_22 = shift_uint32(u32_0, i).
Let a_23 = shift_uint64(u64_0, 0).
-Let a_24 = havoc(Mint_undef_5, Mint_5, a_23, 10).
+Let a_24 = memcpy(Mint_5, Mint_undef_5, a_23, a_23, 10).
Let a_25 = shift_sint64(i64_0, 0).
-Let a_26 = havoc(Mint_undef_3, Mint_3, a_25, 10).
+Let a_26 = memcpy(Mint_3, Mint_undef_3, a_25, a_25, 10).
Let a_27 = shift_uint32(u32_0, 0).
-Let a_28 = havoc(Mint_undef_0, Mint_0, a_27, 10).
+Let a_28 = memcpy(Mint_0, Mint_undef_0, a_27, a_27, 10).
Let a_29 = a_28[a_22 <- 6].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
@@ -823,35 +823,35 @@ Prove: true.
Goal Preservation of Invariant (file chunk_typing.i, line 38):
Let a = shift_uint32(u32_0, 0).
-Let a_1 = havoc(Mint_undef_4, Mint_4, a, 10).
+Let a_1 = memcpy(Mint_4, Mint_undef_4, a, a, 10).
Let a_2 = shift_uint32(u32_0, i).
Let a_3 = a_1[a_2 <- 6].
Let a_4 = shift_sint32(i32_0, 0).
-Let a_5 = havoc(Mint_undef_2, Mint_2, a_4, 10).
+Let a_5 = memcpy(Mint_2, Mint_undef_2, a_4, a_4, 10).
Let a_6 = shift_sint32(i32_0, i).
Let a_7 = a_5[a_6 <- 5].
Let a_8 = shift_uint16(u16_0, 0).
-Let a_9 = havoc(Mint_undef_3, Mint_3, a_8, 10).
+Let a_9 = memcpy(Mint_3, Mint_undef_3, a_8, a_8, 10).
Let a_10 = shift_uint16(u16_0, i).
Let a_11 = a_9[a_10 <- 4].
Let a_12 = shift_sint16(i16_0, 0).
-Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
+Let a_13 = memcpy(Mint_1, Mint_undef_1, a_12, a_12, 10).
Let a_14 = shift_sint16(i16_0, i).
Let a_15 = a_13[a_14 <- 3].
Let a_16 = shift_uint8(u8_0, 0).
-Let a_17 = havoc(Mint_undef_6, Mint_6, a_16, 10).
+Let a_17 = memcpy(Mint_6, Mint_undef_6, a_16, a_16, 10).
Let a_18 = shift_uint8(u8_0, i).
Let a_19 = a_17[a_18 <- 2].
Let a_20 = shift_sint8(i8_0, 0).
-Let a_21 = havoc(Mchar_undef_0, Mchar_0, a_20, 10).
+Let a_21 = memcpy(Mchar_0, Mchar_undef_0, a_20, a_20, 10).
Let a_22 = shift_sint8(i8_0, i).
Let a_23 = a_21[a_22 <- 1].
Let a_24 = shift_uint64(u64_0, i).
Let a_25 = shift_sint64(i64_0, i).
Let a_26 = shift_uint64(u64_0, 0).
-Let a_27 = havoc(Mint_undef_5, Mint_5, a_26, 10).
+Let a_27 = memcpy(Mint_5, Mint_undef_5, a_26, a_26, 10).
Let a_28 = shift_sint64(i64_0, 0).
-Let a_29 = havoc(Mint_undef_0, Mint_0, a_28, 10).
+Let a_29 = memcpy(Mint_0, Mint_undef_0, a_28, a_28, 10).
Let a_30 = a_29[a_25 <- 7].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
@@ -957,36 +957,36 @@ Prove: true.
Goal Preservation of Invariant (file chunk_typing.i, line 39):
Let a = shift_sint64(i64_0, 0).
-Let a_1 = havoc(Mint_undef_3, Mint_3, a, 10).
+Let a_1 = memcpy(Mint_3, Mint_undef_3, a, a, 10).
Let a_2 = shift_sint64(i64_0, i).
Let a_3 = a_1[a_2 <- 7].
Let a_4 = shift_uint32(u32_0, 0).
-Let a_5 = havoc(Mint_undef_5, Mint_5, a_4, 10).
+Let a_5 = memcpy(Mint_5, Mint_undef_5, a_4, a_4, 10).
Let a_6 = shift_uint32(u32_0, i).
Let a_7 = a_5[a_6 <- 6].
Let a_8 = shift_sint32(i32_0, 0).
-Let a_9 = havoc(Mint_undef_2, Mint_2, a_8, 10).
+Let a_9 = memcpy(Mint_2, Mint_undef_2, a_8, a_8, 10).
Let a_10 = shift_sint32(i32_0, i).
Let a_11 = a_9[a_10 <- 5].
Let a_12 = shift_uint16(u16_0, 0).
-Let a_13 = havoc(Mint_undef_4, Mint_4, a_12, 10).
+Let a_13 = memcpy(Mint_4, Mint_undef_4, a_12, a_12, 10).
Let a_14 = shift_uint16(u16_0, i).
Let a_15 = a_13[a_14 <- 4].
Let a_16 = shift_sint16(i16_0, 0).
-Let a_17 = havoc(Mint_undef_1, Mint_1, a_16, 10).
+Let a_17 = memcpy(Mint_1, Mint_undef_1, a_16, a_16, 10).
Let a_18 = shift_sint16(i16_0, i).
Let a_19 = a_17[a_18 <- 3].
Let a_20 = shift_uint8(u8_0, 0).
-Let a_21 = havoc(Mint_undef_6, Mint_6, a_20, 10).
+Let a_21 = memcpy(Mint_6, Mint_undef_6, a_20, a_20, 10).
Let a_22 = shift_uint8(u8_0, i).
Let a_23 = a_21[a_22 <- 2].
Let a_24 = shift_sint8(i8_0, 0).
-Let a_25 = havoc(Mchar_undef_0, Mchar_0, a_24, 10).
+Let a_25 = memcpy(Mchar_0, Mchar_undef_0, a_24, a_24, 10).
Let a_26 = shift_sint8(i8_0, i).
Let a_27 = a_25[a_26 <- 1].
Let a_28 = shift_uint64(u64_0, i).
Let a_29 = shift_uint64(u64_0, 0).
-Let a_30 = havoc(Mint_undef_0, Mint_0, a_29, 10).
+Let a_30 = memcpy(Mint_0, Mint_undef_0, a_29, a_29, 10).
Let a_31 = a_30[a_28 <- 8].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
@@ -1095,21 +1095,21 @@ Prove: true.
Goal Assertion 'rte,mem_access' (file chunk_typing.i, line 45):
Let a = shift_uint64(u64_0, 0).
-Let a_1 = havoc(Mint_undef_5, Mint_5, a, 10).
+Let a_1 = memcpy(Mint_5, Mint_undef_5, a, a, 10).
Let a_2 = shift_sint64(i64_0, 0).
-Let a_3 = havoc(Mint_undef_2, Mint_2, a_2, 10).
+Let a_3 = memcpy(Mint_2, Mint_undef_2, a_2, a_2, 10).
Let a_4 = shift_uint32(u32_0, 0).
-Let a_5 = havoc(Mint_undef_4, Mint_4, a_4, 10).
+Let a_5 = memcpy(Mint_4, Mint_undef_4, a_4, a_4, 10).
Let a_6 = shift_sint32(i32_0, 0).
-Let a_7 = havoc(Mint_undef_1, Mint_1, a_6, 10).
+Let a_7 = memcpy(Mint_1, Mint_undef_1, a_6, a_6, 10).
Let a_8 = shift_uint16(u16_0, 0).
-Let a_9 = havoc(Mint_undef_3, Mint_3, a_8, 10).
+Let a_9 = memcpy(Mint_3, Mint_undef_3, a_8, a_8, 10).
Let a_10 = shift_sint16(i16_0, 0).
-Let a_11 = havoc(Mint_undef_0, Mint_0, a_10, 10).
+Let a_11 = memcpy(Mint_0, Mint_undef_0, a_10, a_10, 10).
Let a_12 = shift_uint8(u8_0, 0).
-Let a_13 = havoc(Mint_undef_6, Mint_6, a_12, 10).
+Let a_13 = memcpy(Mint_6, Mint_undef_6, a_12, a_12, 10).
Let a_14 = shift_sint8(i8_0, 0).
-Let a_15 = havoc(Mchar_undef_0, Mchar_0, a_14, 10).
+Let a_15 = memcpy(Mchar_0, Mchar_undef_0, a_14, a_14, 10).
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
@@ -1165,21 +1165,21 @@ Prove: valid_rw(Malloc_0, shift_sint8(i8_0, i), 1).
Goal Assertion 'rte,mem_access' (file chunk_typing.i, line 46):
Let a = shift_sint8(i8_0, i).
Let a_1 = shift_uint64(u64_0, 0).
-Let a_2 = havoc(Mint_undef_5, Mint_5, a_1, 10).
+Let a_2 = memcpy(Mint_5, Mint_undef_5, a_1, a_1, 10).
Let a_3 = shift_sint64(i64_0, 0).
-Let a_4 = havoc(Mint_undef_2, Mint_2, a_3, 10).
+Let a_4 = memcpy(Mint_2, Mint_undef_2, a_3, a_3, 10).
Let a_5 = shift_uint32(u32_0, 0).
-Let a_6 = havoc(Mint_undef_4, Mint_4, a_5, 10).
+Let a_6 = memcpy(Mint_4, Mint_undef_4, a_5, a_5, 10).
Let a_7 = shift_sint32(i32_0, 0).
-Let a_8 = havoc(Mint_undef_1, Mint_1, a_7, 10).
+Let a_8 = memcpy(Mint_1, Mint_undef_1, a_7, a_7, 10).
Let a_9 = shift_uint16(u16_0, 0).
-Let a_10 = havoc(Mint_undef_3, Mint_3, a_9, 10).
+Let a_10 = memcpy(Mint_3, Mint_undef_3, a_9, a_9, 10).
Let a_11 = shift_sint16(i16_0, 0).
-Let a_12 = havoc(Mint_undef_0, Mint_0, a_11, 10).
+Let a_12 = memcpy(Mint_0, Mint_undef_0, a_11, a_11, 10).
Let a_13 = shift_uint8(u8_0, 0).
-Let a_14 = havoc(Mint_undef_6, Mint_6, a_13, 10).
+Let a_14 = memcpy(Mint_6, Mint_undef_6, a_13, a_13, 10).
Let a_15 = shift_sint8(i8_0, 0).
-Let a_16 = havoc(Mchar_undef_0, Mchar_0, a_15, 10).
+Let a_16 = memcpy(Mchar_0, Mchar_undef_0, a_15, a_15, 10).
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
@@ -1240,21 +1240,21 @@ Goal Assertion 'rte,mem_access' (file chunk_typing.i, line 47):
Let a = shift_uint8(u8_0, i).
Let a_1 = shift_sint8(i8_0, i).
Let a_2 = shift_uint64(u64_0, 0).
-Let a_3 = havoc(Mint_undef_5, Mint_5, a_2, 10).
+Let a_3 = memcpy(Mint_5, Mint_undef_5, a_2, a_2, 10).
Let a_4 = shift_sint64(i64_0, 0).
-Let a_5 = havoc(Mint_undef_2, Mint_2, a_4, 10).
+Let a_5 = memcpy(Mint_2, Mint_undef_2, a_4, a_4, 10).
Let a_6 = shift_uint32(u32_0, 0).
-Let a_7 = havoc(Mint_undef_4, Mint_4, a_6, 10).
+Let a_7 = memcpy(Mint_4, Mint_undef_4, a_6, a_6, 10).
Let a_8 = shift_sint32(i32_0, 0).
-Let a_9 = havoc(Mint_undef_1, Mint_1, a_8, 10).
+Let a_9 = memcpy(Mint_1, Mint_undef_1, a_8, a_8, 10).
Let a_10 = shift_uint16(u16_0, 0).
-Let a_11 = havoc(Mint_undef_3, Mint_3, a_10, 10).
+Let a_11 = memcpy(Mint_3, Mint_undef_3, a_10, a_10, 10).
Let a_12 = shift_sint16(i16_0, 0).
-Let a_13 = havoc(Mint_undef_0, Mint_0, a_12, 10).
+Let a_13 = memcpy(Mint_0, Mint_undef_0, a_12, a_12, 10).
Let a_14 = shift_uint8(u8_0, 0).
-Let a_15 = havoc(Mint_undef_6, Mint_6, a_14, 10).
+Let a_15 = memcpy(Mint_6, Mint_undef_6, a_14, a_14, 10).
Let a_16 = shift_sint8(i8_0, 0).
-Let a_17 = havoc(Mchar_undef_0, Mchar_0, a_16, 10).
+Let a_17 = memcpy(Mchar_0, Mchar_undef_0, a_16, a_16, 10).
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
@@ -1318,21 +1318,21 @@ Let a = shift_sint16(i16_0, i).
Let a_1 = shift_uint8(u8_0, i).
Let a_2 = shift_sint8(i8_0, i).
Let a_3 = shift_uint64(u64_0, 0).
-Let a_4 = havoc(Mint_undef_5, Mint_5, a_3, 10).
+Let a_4 = memcpy(Mint_5, Mint_undef_5, a_3, a_3, 10).
Let a_5 = shift_sint64(i64_0, 0).
-Let a_6 = havoc(Mint_undef_2, Mint_2, a_5, 10).
+Let a_6 = memcpy(Mint_2, Mint_undef_2, a_5, a_5, 10).
Let a_7 = shift_uint32(u32_0, 0).
-Let a_8 = havoc(Mint_undef_4, Mint_4, a_7, 10).
+Let a_8 = memcpy(Mint_4, Mint_undef_4, a_7, a_7, 10).
Let a_9 = shift_sint32(i32_0, 0).
-Let a_10 = havoc(Mint_undef_1, Mint_1, a_9, 10).
+Let a_10 = memcpy(Mint_1, Mint_undef_1, a_9, a_9, 10).
Let a_11 = shift_uint16(u16_0, 0).
-Let a_12 = havoc(Mint_undef_3, Mint_3, a_11, 10).
+Let a_12 = memcpy(Mint_3, Mint_undef_3, a_11, a_11, 10).
Let a_13 = shift_sint16(i16_0, 0).
-Let a_14 = havoc(Mint_undef_0, Mint_0, a_13, 10).
+Let a_14 = memcpy(Mint_0, Mint_undef_0, a_13, a_13, 10).
Let a_15 = shift_uint8(u8_0, 0).
-Let a_16 = havoc(Mint_undef_6, Mint_6, a_15, 10).
+Let a_16 = memcpy(Mint_6, Mint_undef_6, a_15, a_15, 10).
Let a_17 = shift_sint8(i8_0, 0).
-Let a_18 = havoc(Mchar_undef_0, Mchar_0, a_17, 10).
+Let a_18 = memcpy(Mchar_0, Mchar_undef_0, a_17, a_17, 10).
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
@@ -1400,21 +1400,21 @@ Let a_1 = shift_sint16(i16_0, i).
Let a_2 = shift_uint8(u8_0, i).
Let a_3 = shift_sint8(i8_0, i).
Let a_4 = shift_uint64(u64_0, 0).
-Let a_5 = havoc(Mint_undef_5, Mint_5, a_4, 10).
+Let a_5 = memcpy(Mint_5, Mint_undef_5, a_4, a_4, 10).
Let a_6 = shift_sint64(i64_0, 0).
-Let a_7 = havoc(Mint_undef_2, Mint_2, a_6, 10).
+Let a_7 = memcpy(Mint_2, Mint_undef_2, a_6, a_6, 10).
Let a_8 = shift_uint32(u32_0, 0).
-Let a_9 = havoc(Mint_undef_4, Mint_4, a_8, 10).
+Let a_9 = memcpy(Mint_4, Mint_undef_4, a_8, a_8, 10).
Let a_10 = shift_sint32(i32_0, 0).
-Let a_11 = havoc(Mint_undef_1, Mint_1, a_10, 10).
+Let a_11 = memcpy(Mint_1, Mint_undef_1, a_10, a_10, 10).
Let a_12 = shift_uint16(u16_0, 0).
-Let a_13 = havoc(Mint_undef_3, Mint_3, a_12, 10).
+Let a_13 = memcpy(Mint_3, Mint_undef_3, a_12, a_12, 10).
Let a_14 = shift_sint16(i16_0, 0).
-Let a_15 = havoc(Mint_undef_0, Mint_0, a_14, 10).
+Let a_15 = memcpy(Mint_0, Mint_undef_0, a_14, a_14, 10).
Let a_16 = shift_uint8(u8_0, 0).
-Let a_17 = havoc(Mint_undef_6, Mint_6, a_16, 10).
+Let a_17 = memcpy(Mint_6, Mint_undef_6, a_16, a_16, 10).
Let a_18 = shift_sint8(i8_0, 0).
-Let a_19 = havoc(Mchar_undef_0, Mchar_0, a_18, 10).
+Let a_19 = memcpy(Mchar_0, Mchar_undef_0, a_18, a_18, 10).
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
@@ -1485,21 +1485,21 @@ Let a_2 = shift_sint16(i16_0, i).
Let a_3 = shift_uint8(u8_0, i).
Let a_4 = shift_sint8(i8_0, i).
Let a_5 = shift_uint64(u64_0, 0).
-Let a_6 = havoc(Mint_undef_5, Mint_5, a_5, 10).
+Let a_6 = memcpy(Mint_5, Mint_undef_5, a_5, a_5, 10).
Let a_7 = shift_sint64(i64_0, 0).
-Let a_8 = havoc(Mint_undef_2, Mint_2, a_7, 10).
+Let a_8 = memcpy(Mint_2, Mint_undef_2, a_7, a_7, 10).
Let a_9 = shift_uint32(u32_0, 0).
-Let a_10 = havoc(Mint_undef_4, Mint_4, a_9, 10).
+Let a_10 = memcpy(Mint_4, Mint_undef_4, a_9, a_9, 10).
Let a_11 = shift_sint32(i32_0, 0).
-Let a_12 = havoc(Mint_undef_1, Mint_1, a_11, 10).
+Let a_12 = memcpy(Mint_1, Mint_undef_1, a_11, a_11, 10).
Let a_13 = shift_uint16(u16_0, 0).
-Let a_14 = havoc(Mint_undef_3, Mint_3, a_13, 10).
+Let a_14 = memcpy(Mint_3, Mint_undef_3, a_13, a_13, 10).
Let a_15 = shift_sint16(i16_0, 0).
-Let a_16 = havoc(Mint_undef_0, Mint_0, a_15, 10).
+Let a_16 = memcpy(Mint_0, Mint_undef_0, a_15, a_15, 10).
Let a_17 = shift_uint8(u8_0, 0).
-Let a_18 = havoc(Mint_undef_6, Mint_6, a_17, 10).
+Let a_18 = memcpy(Mint_6, Mint_undef_6, a_17, a_17, 10).
Let a_19 = shift_sint8(i8_0, 0).
-Let a_20 = havoc(Mchar_undef_0, Mchar_0, a_19, 10).
+Let a_20 = memcpy(Mchar_0, Mchar_undef_0, a_19, a_19, 10).
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
@@ -1574,21 +1574,21 @@ Let a_3 = shift_sint16(i16_0, i).
Let a_4 = shift_uint8(u8_0, i).
Let a_5 = shift_sint8(i8_0, i).
Let a_6 = shift_uint64(u64_0, 0).
-Let a_7 = havoc(Mint_undef_5, Mint_5, a_6, 10).
+Let a_7 = memcpy(Mint_5, Mint_undef_5, a_6, a_6, 10).
Let a_8 = shift_sint64(i64_0, 0).
-Let a_9 = havoc(Mint_undef_2, Mint_2, a_8, 10).
+Let a_9 = memcpy(Mint_2, Mint_undef_2, a_8, a_8, 10).
Let a_10 = shift_uint32(u32_0, 0).
-Let a_11 = havoc(Mint_undef_4, Mint_4, a_10, 10).
+Let a_11 = memcpy(Mint_4, Mint_undef_4, a_10, a_10, 10).
Let a_12 = shift_sint32(i32_0, 0).
-Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
+Let a_13 = memcpy(Mint_1, Mint_undef_1, a_12, a_12, 10).
Let a_14 = shift_uint16(u16_0, 0).
-Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
+Let a_15 = memcpy(Mint_3, Mint_undef_3, a_14, a_14, 10).
Let a_16 = shift_sint16(i16_0, 0).
-Let a_17 = havoc(Mint_undef_0, Mint_0, a_16, 10).
+Let a_17 = memcpy(Mint_0, Mint_undef_0, a_16, a_16, 10).
Let a_18 = shift_uint8(u8_0, 0).
-Let a_19 = havoc(Mint_undef_6, Mint_6, a_18, 10).
+Let a_19 = memcpy(Mint_6, Mint_undef_6, a_18, a_18, 10).
Let a_20 = shift_sint8(i8_0, 0).
-Let a_21 = havoc(Mchar_undef_0, Mchar_0, a_20, 10).
+Let a_21 = memcpy(Mchar_0, Mchar_undef_0, a_20, a_20, 10).
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
@@ -1666,21 +1666,21 @@ Let a_4 = shift_sint16(i16_0, i).
Let a_5 = shift_uint8(u8_0, i).
Let a_6 = shift_sint8(i8_0, i).
Let a_7 = shift_uint64(u64_0, 0).
-Let a_8 = havoc(Mint_undef_5, Mint_5, a_7, 10).
+Let a_8 = memcpy(Mint_5, Mint_undef_5, a_7, a_7, 10).
Let a_9 = shift_sint64(i64_0, 0).
-Let a_10 = havoc(Mint_undef_2, Mint_2, a_9, 10).
+Let a_10 = memcpy(Mint_2, Mint_undef_2, a_9, a_9, 10).
Let a_11 = shift_uint32(u32_0, 0).
-Let a_12 = havoc(Mint_undef_4, Mint_4, a_11, 10).
+Let a_12 = memcpy(Mint_4, Mint_undef_4, a_11, a_11, 10).
Let a_13 = shift_sint32(i32_0, 0).
-Let a_14 = havoc(Mint_undef_1, Mint_1, a_13, 10).
+Let a_14 = memcpy(Mint_1, Mint_undef_1, a_13, a_13, 10).
Let a_15 = shift_uint16(u16_0, 0).
-Let a_16 = havoc(Mint_undef_3, Mint_3, a_15, 10).
+Let a_16 = memcpy(Mint_3, Mint_undef_3, a_15, a_15, 10).
Let a_17 = shift_sint16(i16_0, 0).
-Let a_18 = havoc(Mint_undef_0, Mint_0, a_17, 10).
+Let a_18 = memcpy(Mint_0, Mint_undef_0, a_17, a_17, 10).
Let a_19 = shift_uint8(u8_0, 0).
-Let a_20 = havoc(Mint_undef_6, Mint_6, a_19, 10).
+Let a_20 = memcpy(Mint_6, Mint_undef_6, a_19, a_19, 10).
Let a_21 = shift_sint8(i8_0, 0).
-Let a_22 = havoc(Mchar_undef_0, Mchar_0, a_21, 10).
+Let a_22 = memcpy(Mchar_0, Mchar_undef_0, a_21, a_21, 10).
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
index 3658aa0a248..1ca8b3a8e79 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
@@ -25,7 +25,7 @@ Prove: true.
Goal Preservation of Invariant (file looplabels.i, line 19):
Let a_1 = shift_sint32(b, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Let a_3 = shift_sint32(a, 0).
Let x = 1 + i.
Assume {
@@ -89,7 +89,7 @@ Prove: true.
Goal Loop assigns (file looplabels.i, line 20) (3/3):
Effect at line 24
Let a_1 = shift_sint32(b, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Let x = i - 1.
Let a_3 = shift_sint32(b, x).
Let a_4 = shift_sint32(a, 0).
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
index bbcfeeaf580..a2bb4e09129 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
@@ -52,15 +52,15 @@ Prove: true.
------------------------------------------------------------
Goal Check 'fail' (file opaque_struct.i, line 60):
-Let a = havoc(Mint_undef_0, Mint_0, p, Length_of_S1_S).
-Let a_1 = havoc(Mint_undef_3, Mint_3, p, Length_of_S1_S).
-Let a_2 = havoc(Mint_undef_5, Mint_5, p, Length_of_S1_S).
-Let a_3 = havoc(Mint_undef_7, Mint_7, p, Length_of_S1_S).
-Let a_4 = havoc(Mchar_undef_0, Mchar_0, p, Length_of_S1_S).
-Let a_5 = havoc(Mint_undef_2, Mint_2, p, Length_of_S1_S).
-Let a_6 = havoc(Mint_undef_4, Mint_4, p, Length_of_S1_S).
-Let a_7 = havoc(Mint_undef_6, Mint_6, p, Length_of_S1_S).
-Let a_8 = havoc(Mint_undef_1, Mint_1, p, Length_of_S1_S).
+Let a = memcpy(Mint_0, Mint_undef_0, p, p, Length_of_S1_S).
+Let a_1 = memcpy(Mint_3, Mint_undef_3, p, p, Length_of_S1_S).
+Let a_2 = memcpy(Mint_5, Mint_undef_5, p, p, Length_of_S1_S).
+Let a_3 = memcpy(Mint_7, Mint_undef_7, p, p, Length_of_S1_S).
+Let a_4 = memcpy(Mchar_0, Mchar_undef_0, p, p, Length_of_S1_S).
+Let a_5 = memcpy(Mint_2, Mint_undef_2, p, p, Length_of_S1_S).
+Let a_6 = memcpy(Mint_4, Mint_undef_4, p, p, Length_of_S1_S).
+Let a_7 = memcpy(Mint_6, Mint_undef_6, p, p, Length_of_S1_S).
+Let a_8 = memcpy(Mint_1, Mint_undef_1, p, p, Length_of_S1_S).
Assume {
Type: is_bool_chunk(Mint_0) /\ is_sint16_chunk(Mint_3) /\
is_sint32_chunk(Mint_5) /\ is_sint64_chunk(Mint_7) /\
@@ -74,9 +74,9 @@ Assume {
Type: (region(p.base) <= 0) /\ framed(Mptr_0) /\ sconst(Mchar_0).
}
Prove: EqS1_S(Load_S1_S(p, a, a_8, a_4, a_5, a_1, a_6, a_2, a_7, a_3,
- havoc(Mf32_undef_0, Mf32_0, p, Length_of_S1_S),
- havoc(Mf64_undef_0, Mf64_0, p, Length_of_S1_S),
- havoc(Mptr_undef_0, Mptr_0, p, Length_of_S1_S)),
+ memcpy(Mf32_0, Mf32_undef_0, p, p, Length_of_S1_S),
+ memcpy(Mf64_0, Mf64_undef_0, p, p, Length_of_S1_S),
+ memcpy(Mptr_0, Mptr_undef_0, p, p, Length_of_S1_S)),
Load_S1_S(p, Mint_0, Mint_1, Mchar_0, Mint_2, Mint_3, Mint_4,
Mint_5, Mint_6, Mint_7, Mf32_0, Mf64_0, Mptr_0)).
@@ -120,7 +120,7 @@ Prove: true.
Goal Check 'fail' (file opaque_struct.i, line 69):
Let x = Mint_0[p].
-Let a_1 = havoc(Mint_undef_0, Mint_0, a, Length_of_S1_S).
+Let a_1 = memcpy(Mint_0, Mint_undef_0, a, a, Length_of_S1_S).
Let a_2 = a_1[p].
Assume {
Type: is_sint32_chunk(Mint_0) /\ is_sint32(x) /\ is_sint32_chunk(a_1) /\
@@ -143,14 +143,14 @@ Assume {
(* Pre-condition *)
Have: separated(a, Length_of_S1_S, c, 1).
}
-Prove: of_f32(havoc(Mf32_undef_0, Mf32_0, a, Length_of_S1_S)[q])
+Prove: of_f32(memcpy(Mf32_0, Mf32_undef_0, a, a, Length_of_S1_S)[q])
= of_f32(Mf32_0[q]).
------------------------------------------------------------
Goal Check 'succeed' (file opaque_struct.i, line 71):
Let x = Mchar_0[c].
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, Length_of_S1_S).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, Length_of_S1_S).
Let a_2 = a_1[c].
Assume {
Type: is_sint8_chunk(Mchar_0) /\ is_sint8(x) /\ is_sint8_chunk(a_1) /\
@@ -201,7 +201,7 @@ Prove: true.
------------------------------------------------------------
Goal Check 'fails' (file opaque_struct.i, line 38):
-Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
+Let a = memcpy(Init_0, Init_undef_0, p, p, Length_of_S1_S).
Assume {
(* Heap *)
Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ cinits(Init_0).
@@ -242,7 +242,7 @@ Prove: true.
------------------------------------------------------------
Goal Check 'fail' (file opaque_struct.i, line 54):
-Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
+Let a = memcpy(Init_0, Init_undef_0, p, p, Length_of_S1_S).
Assume {
(* Heap *)
Type: (region(p.base) <= 0) /\ cinits(Init_0).
@@ -256,7 +256,7 @@ Prove: !IsInit_S1_S(p, a).
------------------------------------------------------------
Goal Check 'fail' (file opaque_struct.i, line 55):
-Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
+Let a = memcpy(Init_0, Init_undef_0, p, p, Length_of_S1_S).
Assume {
(* Heap *)
Type: (region(p.base) <= 0) /\ cinits(Init_0).
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
index 08d574c3187..18a691c67f3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
@@ -207,7 +207,7 @@ Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
Goal Post-condition (file simpl_is_type.i, line 17) in 'f':
Let a = shift_sint32(t, 0).
-Let a_1 = havoc(Mint_undef_0, Mint_0, a, size_0).
+Let a_1 = memcpy(Mint_0, Mint_undef_0, a, a, size_0).
Assume {
Type: is_sint32(i) /\ is_sint32(size_0).
(* Heap *)
@@ -230,7 +230,7 @@ Assume {
(* Else *)
Have: size_0 <= i.
}
-Prove: 0 < havoc(Mint_undef_0, Mint_0, a, i)[shift_sint32(t, i_1)].
+Prove: 0 < memcpy(Mint_0, Mint_undef_0, a, a, i)[shift_sint32(t, i_1)].
------------------------------------------------------------
@@ -245,12 +245,13 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file simpl_is_type.i, line 23):
-Let a = havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), size_0).
-Let a_1 = shift_sint32(t, i).
-Let a_2 = a[a_1].
+Let a = shift_sint32(t, 0).
+Let a_1 = memcpy(Mint_0, Mint_undef_0, a, a, size_0).
+Let a_2 = shift_sint32(t, i).
+Let a_3 = a_1[a_2].
Assume {
Type: is_sint32(i) /\ is_sint32(size_0) /\ is_sint32(1 + i) /\
- is_sint32(a_2).
+ is_sint32(a_3).
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
@@ -264,16 +265,16 @@ Assume {
Have: (0 <= i) /\ (i <= size_0).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (0 < a[shift_sint32(t, i_2)]))).
+ (0 < a_1[shift_sint32(t, i_2)]))).
(* Invariant *)
Have: forall i_2 : Z. ((i <= i_2) -> ((i_2 < size_0) ->
- (a[shift_sint32(t, i_2)] < 0))).
+ (a_1[shift_sint32(t, i_2)] < 0))).
(* Then *)
Have: i < size_0.
(* Invariant *)
Have: (-1) <= i.
}
-Prove: 0 < a[a_1 <- -a_2][shift_sint32(t, i_1)].
+Prove: 0 < a_1[a_2 <- -a_3][shift_sint32(t, i_1)].
------------------------------------------------------------
@@ -283,13 +284,14 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file simpl_is_type.i, line 24):
-Let a = havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), size_0).
-Let a_1 = shift_sint32(t, i).
-Let a_2 = a[a_1].
-Let a_3 = a[a_1 <- -a_2].
+Let a = shift_sint32(t, 0).
+Let a_1 = memcpy(Mint_0, Mint_undef_0, a, a, size_0).
+Let a_2 = shift_sint32(t, i).
+Let a_3 = a_1[a_2].
+Let a_4 = a_1[a_2 <- -a_3].
Assume {
Type: is_sint32(i) /\ is_sint32(size_0) /\ is_sint32(1 + i) /\
- is_sint32(a_2).
+ is_sint32(a_3).
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
@@ -303,19 +305,19 @@ Assume {
Have: (0 <= i) /\ (i <= size_0).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (0 < a[shift_sint32(t, i_2)]))).
+ (0 < a_1[shift_sint32(t, i_2)]))).
(* Invariant *)
Have: forall i_2 : Z. ((i <= i_2) -> ((i_2 < size_0) ->
- (a[shift_sint32(t, i_2)] < 0))).
+ (a_1[shift_sint32(t, i_2)] < 0))).
(* Then *)
Have: i < size_0.
(* Invariant *)
Have: (-1) <= i.
(* Invariant *)
Have: forall i_2 : Z. ((i_2 <= i) -> ((0 <= i_2) ->
- (0 < a_3[shift_sint32(t, i_2)]))).
+ (0 < a_4[shift_sint32(t, i_2)]))).
}
-Prove: a_3[shift_sint32(t, i_1)] < 0.
+Prove: a_4[shift_sint32(t, i_1)] < 0.
------------------------------------------------------------
@@ -350,7 +352,7 @@ Prove: true.
Goal Loop assigns (file simpl_is_type.i, line 25) (3/3):
Effect at line 29
Let a = shift_sint32(t, 0).
-Let a_1 = havoc(Mint_undef_0, Mint_0, a, size_0).
+Let a_1 = memcpy(Mint_0, Mint_undef_0, a, a, size_0).
Let x = i - 1.
Let a_2 = shift_sint32(t, x).
Let a_3 = a_1[a_2].
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index f43f3e075ee..3488a9b01fa 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -149,9 +149,9 @@ theory Compound
axiom Q_Load_S1_X_havoc_Mchar0 :
forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
addr -> int, n:int, p:addr, q:addr
- [Load_S1_X p (havoc mchar1 mchar q n) mint mint1].
+ [Load_S1_X p (memcpy mchar mchar1 q q n) mint mint1].
separated p 3 q n ->
- Load_S1_X p (havoc mchar1 mchar q n) mint mint1 =
+ Load_S1_X p (memcpy mchar mchar1 q q n) mint mint1 =
Load_S1_X p mchar mint mint1
axiom Q_Load_S1_X_update_Mint1 :
@@ -172,9 +172,9 @@ theory Compound
axiom Q_Load_S1_X_havoc_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr
- [Load_S1_X p mchar (havoc mint2 mint1 q n) mint].
+ [Load_S1_X p mchar (memcpy mint1 mint2 q q n) mint].
separated p 3 q n ->
- Load_S1_X p mchar (havoc mint2 mint1 q n) mint =
+ Load_S1_X p mchar (memcpy mint1 mint2 q q n) mint =
Load_S1_X p mchar mint1 mint
axiom Q_Load_S1_X_update_Mint2 :
@@ -195,9 +195,9 @@ theory Compound
axiom Q_Load_S1_X_havoc_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr
- [Load_S1_X p mchar mint (havoc mint2 mint1 q n)].
+ [Load_S1_X p mchar mint (memcpy mint1 mint2 q q n)].
separated p 3 q n ->
- Load_S1_X p mchar mint (havoc mint2 mint1 q n) =
+ Load_S1_X p mchar mint (memcpy mint1 mint2 q q n) =
Load_S1_X p mchar mint mint1
axiom Q_Load_Init_S1_X_update_Init0 :
@@ -215,9 +215,9 @@ theory Compound
axiom Q_Load_Init_S1_X_havoc_Init0 :
forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
- [Load_Init_S1_X p (havoc init1 init q n)].
+ [Load_Init_S1_X p (memcpy init init1 q q n)].
separated p 3 q n ->
- Load_Init_S1_X p (havoc init1 init q n) = Load_Init_S1_X p init
+ Load_Init_S1_X p (memcpy init init1 q q n) = Load_Init_S1_X p init
end
[wp:print-generated]
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle
index 9ba39839927..71e9a2acf38 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle
@@ -30,7 +30,8 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Invariant 'is_zero' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (of_f64(havoc(Mf64_undef_0, Mf64_0, a, 10)[shift_float64(s, i_1)]) = .0))).
+ (of_f64(memcpy(Mf64_0, Mf64_undef_0, a, a, 10)[shift_float64(s, i_1)])
+ = .0))).
(* Then *)
Have: i <= 9.
}
@@ -46,7 +47,7 @@ Prove: true.
Goal Preservation of Invariant 'is_zero' (file zero.i, line 25):
Let x = to_uint32(1 + i).
Let a = shift_float64(s, 0).
-Let a_1 = havoc(Mf64_undef_0, Mf64_0, a, 10).
+Let a_1 = memcpy(Mf64_0, Mf64_undef_0, a, a, 10).
Assume {
Type: is_uint32(i).
(* Heap *)
@@ -101,7 +102,7 @@ Prove: true.
Goal Decreasing of Loop variant at loop (file zero.i, line 29):
Let x = to_uint32(1 + i).
Let a = shift_float64(s, 0).
-Let a_1 = havoc(Mf64_undef_0, Mf64_0, a, 10).
+Let a_1 = memcpy(Mf64_0, Mf64_undef_0, a, a, 10).
Assume {
Type: is_uint32(i).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle
index 8d825e04288..313b9ed702f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle
@@ -30,7 +30,7 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Invariant 'is_zero' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (havoc(Mf64_undef_0, Mf64_0, a, 10)[shift_float64(s, i_1)] = 0))).
+ (memcpy(Mf64_0, Mf64_undef_0, a, a, 10)[shift_float64(s, i_1)] = 0))).
(* Then *)
Have: i <= 9.
}
@@ -46,7 +46,7 @@ Prove: true.
Goal Preservation of Invariant 'is_zero' (file zero.i, line 25):
Let x = to_uint32(1 + i).
Let a = shift_float64(s, 0).
-Let a_1 = havoc(Mf64_undef_0, Mf64_0, a, 10).
+Let a_1 = memcpy(Mf64_0, Mf64_undef_0, a, a, 10).
Assume {
Type: is_uint32(i).
(* Heap *)
@@ -100,7 +100,7 @@ Prove: true.
Goal Decreasing of Loop variant at loop (file zero.i, line 29):
Let x = to_uint32(1 + i).
Let a = shift_float64(s, 0).
-Let a_1 = havoc(Mf64_undef_0, Mf64_0, a, 10).
+Let a_1 = memcpy(Mf64_0, Mf64_undef_0, a, a, 10).
Assume {
Type: is_uint32(i).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index 710eb5bae2e..2befafc093e 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -82,9 +82,9 @@ theory Compound
axiom Q_Load_S2_A_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
- [Load_S2_A p (havoc mint1 mint q n)].
+ [Load_S2_A p (memcpy mint mint1 q q n)].
separated p 1 q n ->
- Load_S2_A p (havoc mint1 mint q n) = Load_S2_A p mint
+ Load_S2_A p (memcpy mint mint1 q q n) = Load_S2_A p mint
end
[wp:print-generated]
@@ -113,7 +113,7 @@ end
let a2 = shiftfield_F1_FD_pos a1 in
let x = get t a2 in
let a3 = Load_S2_A a t in
- let a4 = Load_S2_A a (set (havoc t1 t a 1) a2 i) in
+ let a4 = Load_S2_A a (set (memcpy t t1 a a 1) a2 i) in
not x = i ->
region (a1.base) <= 0 ->
region (a.base) <= 0 ->
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle
index c2ac0df24d1..0df97f15cf9 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle
@@ -47,8 +47,8 @@ Goal Check (file assigns_sep.i, line 27):
Let x = read_uint32(mem_0, array_0).
Let m = write_uint8(mem_0, shift_uint8(array_0, 7), v).
Let x_1 = read_uint32(m, array_0).
-Let x_2 = read_uint32(havoc(mem_undef_0, m, shift_uint8(array_0, 4), 4),
- array_0).
+Let a = shift_uint8(array_0, 4).
+Let x_2 = read_uint32(memcpy(m, mem_undef_0, a, a, 4), array_0).
Assume {
Type: is_uint32(x) /\ is_uint32(x_1) /\ is_uint32(x_2).
(* Heap *)
@@ -60,19 +60,20 @@ Prove: (x_1 = x) /\ (x_2 = x_1).
Goal Check (file assigns_sep.i, line 30):
Let m = write_uint8(mem_0, shift_uint8(array_0, 7), v).
-Let a = havoc(mem_undef_0, m, shift_uint8(array_0, 4), 4).
+Let a = shift_uint8(array_0, 4).
+Let a_1 = memcpy(m, mem_undef_0, a, a, 4).
Let x = read_uint32(mem_1, array_0).
-Let x_1 = read_uint32(a, array_0).
+Let x_1 = read_uint32(a_1, array_0).
Assume {
Type: is_uint32(x) /\ is_uint32(read_uint32(mem_0, array_0)) /\
is_uint32(read_uint32(m, array_0)) /\ is_uint32(x_1).
(* Heap *)
Type: (region(array_0.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
(* Call Effects *)
- Have: forall a_1 : addr.
+ Have: forall a_2 : addr.
((forall i : Z. (((i = 4) \/ (i = 6)) ->
- (shift_uint8(array_0, i) != a_1))) ->
- (raw_get(a, a_1) = raw_get(mem_1, a_1))).
+ (shift_uint8(array_0, i) != a_2))) ->
+ (raw_get(a_1, a_2) = raw_get(mem_1, a_2))).
}
Prove: x_1 = x.
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle
index 898225de015..31b9b8eebe1 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle
@@ -16,7 +16,7 @@ Prove: true.
Goal Post-condition (file structs.i, line 18) in 'caller':
Let a = Load_S2_Y(u, mem_0).
-Let a_1 = Load_S2_Y(u, havoc(mem_undef_0, mem_0, y, 32)).
+Let a_1 = Load_S2_Y(u, memcpy(mem_0, mem_undef_0, y, y, 32)).
Assume {
Type: IsS2_Y(a) /\ IsS2_Y(a_1).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
index 23b86bc3588..a5aa25272a0 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
@@ -341,7 +341,7 @@ Prove: read_uint8(m, shift_uint8(shiftfield_F2_U_a(u), i)) = 0.
Goal Check (file union.i, line 70):
Let a = shiftfield_F2_U_x(u).
-Let a_1 = havoc(mem_undef_0, mem_0, a, 8).
+Let a_1 = memcpy(mem_0, mem_undef_0, a, a, 8).
Let x = read_uint64(a_1, shiftfield_F2_U_u(u)).
Assume {
Type: is_uint32(read_uint32(a_1, shiftfield_F2_U_s(u))) /\ is_uint64(x).
@@ -361,7 +361,7 @@ Prove: x = 4294967295.
Goal Check (file union.i, line 72):
Let a = shiftfield_F2_U_x(u).
-Let a_1 = havoc(mem_undef_0, mem_0, a, 8).
+Let a_1 = memcpy(mem_0, mem_undef_0, a, a, 8).
Assume {
Type: is_uint32(read_uint32(a_1, shiftfield_F2_U_s(u))) /\
is_uint64(read_uint64(a_1, shiftfield_F2_U_u(u))).
@@ -383,7 +383,7 @@ Prove: read_uint8(a_1, shift_uint8(shiftfield_F2_U_a(u), i)) = 255.
Goal Check (file union.i, line 73):
Let a = shiftfield_F2_U_x(u).
-Let a_1 = havoc(mem_undef_0, mem_0, a, 8).
+Let a_1 = memcpy(mem_0, mem_undef_0, a, a, 8).
Assume {
Type: is_uint32(read_uint32(a_1, shiftfield_F2_U_s(u))) /\
is_uint64(read_uint64(a_1, shiftfield_F2_U_u(u))).
@@ -405,7 +405,7 @@ Prove: read_uint8(a_1, shift_uint8(shiftfield_F2_U_a(u), i)) = 0.
Goal Check (file union.i, line 75):
Let a = shiftfield_F2_U_x(u).
-Let a_1 = havoc(mem_undef_0, mem_0, a, 8).
+Let a_1 = memcpy(mem_0, mem_undef_0, a, a, 8).
Let x = read_uint32(a_1, shiftfield_F2_U_s(u)).
Assume {
Type: is_uint32(x) /\ is_uint64(read_uint64(a_1, shiftfield_F2_U_u(u))).
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index 997835abf96..cd4f15d440d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -281,7 +281,7 @@ Prove: true.
Goal Post-condition 'Preset_5_tps' in 'call_reset_5_tps':
Let a = tps_0[9].
Let a_1 = shift_S1_T(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, 10).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, 10).
Assume {
(* Heap *)
Type: linked(Malloc_0) /\ (forall i_1 : Z. region(tps_0[i_1].base) <= 0).
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
index 66fd41e2399..b819acb5658 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
@@ -432,7 +432,7 @@ Prove: true.
Goal Post-condition (file reference_array.i, line 36) in 'reset_1_5':
Let a = shift_A5_sint32(rp_0, 0).
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, 5).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, 5).
Assume {
(* Heap *)
Type: (region(rp_0.base) <= 0) /\ linked(Malloc_0).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
index e3f4ccc6a7f..0e23fe0de0b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
@@ -39,7 +39,8 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file combined.c, line 30):
-Let a = havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), 50).
+Let a = shift_sint32(t, 0).
+Let a_1 = memcpy(Mint_0, Mint_undef_0, a, a, 50).
Assume {
Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(v) /\ is_sint32(1 + i).
(* Heap *)
@@ -52,7 +53,7 @@ Assume {
Have: (0 <= i) /\ (i <= 50).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- P_P(a[shift_sint32(t, i_2)]))).
+ P_P(a_1[shift_sint32(t, i_2)]))).
(* Then *)
Have: i <= 49.
(* Call 'f' *)
@@ -60,7 +61,7 @@ Assume {
(* Invariant *)
Have: (-1) <= i.
}
-Prove: P_P(a[shift_sint32(t, i) <- v][shift_sint32(t, i_1)]).
+Prove: P_P(a_1[shift_sint32(t, i) <- v][shift_sint32(t, i_1)]).
------------------------------------------------------------
@@ -70,6 +71,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file combined.c, line 36):
+Let a = shift_sint32(t, 0).
Let x = 1 + j.
Assume {
Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(j) /\ is_sint32(x).
@@ -81,8 +83,7 @@ Assume {
Have: (0 <= i) /\ (i <= 50).
(* Invariant *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- P_P(havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), 50)
- [shift_sint32(t, i_1)]))).
+ P_P(memcpy(Mint_0, Mint_undef_0, a, a, 50)[shift_sint32(t, i_1)]))).
(* Else *)
Have: 50 <= i.
(* Invariant *)
@@ -100,7 +101,9 @@ Prove: true.
------------------------------------------------------------
Goal Assertion (file combined.c, line 42):
-Let a = havoc(Mint_undef_1, Mint_0, shift_sint32(t, 0), 50).
+Let a = shift_sint32(t, 0).
+Let a_1 = memcpy(Mint_0, Mint_undef_0, a, a, 50).
+Let a_2 = shift_sint32(t, A).
Assume {
Type: is_sint32(A) /\ is_sint32(i_1) /\ is_sint32(j).
(* Heap *)
@@ -113,7 +116,7 @@ Assume {
Have: (0 <= i_1) /\ (i_1 <= 50).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
- P_P(a[shift_sint32(t, i_2)]))).
+ P_P(a_1[shift_sint32(t, i_2)]))).
(* Else *)
Have: 50 <= i_1.
(* Invariant *)
@@ -121,8 +124,7 @@ Assume {
(* Else *)
Have: 100 <= j.
}
-Prove: P_P(havoc(Mint_undef_0, a, shift_sint32(t, A), 100 - A)
- [shift_sint32(t, i)]).
+Prove: P_P(memcpy(a_1, Mint_undef_1, a_2, a_2, 100 - A)[shift_sint32(t, i)]).
------------------------------------------------------------
@@ -156,22 +158,22 @@ Prove: true.
Goal Loop assigns (file combined.c, line 37) (3/3):
Call Result at line 40
+Let a = shift_sint32(t, 0).
Let x = j - 1.
-Let a = shift_sint32(t, x).
+Let a_1 = shift_sint32(t, x).
Assume {
Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(j) /\ is_sint32(x).
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: !invalid(Malloc_0, a, 1).
+ When: !invalid(Malloc_0, a_1, 1).
(* Assertion *)
Have: (50 <= A) /\ (A <= 100).
(* Invariant *)
Have: (0 <= i) /\ (i <= 50).
(* Invariant *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- P_P(havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), 50)
- [shift_sint32(t, i_1)]))).
+ P_P(memcpy(Mint_0, Mint_undef_0, a, a, 50)[shift_sint32(t, i_1)]))).
(* Else *)
Have: 50 <= i.
(* Invariant *)
@@ -179,7 +181,7 @@ Assume {
(* Then *)
Have: j <= 100.
}
-Prove: included(a, 1, shift_sint32(t, A), 100 - A).
+Prove: included(a_1, 1, shift_sint32(t, A), 100 - A).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
index ed016013308..c3d598aa21a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
@@ -10,8 +10,8 @@
Goal Post-condition (file copy.i, line 5) in 'copy':
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
-Let a_3 = havoc(Mint_undef_0, Mint_0, a_1, i).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
+Let a_3 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, i).
Assume {
Type: is_sint32(i) /\ is_sint32(n).
(* Heap *)
@@ -36,7 +36,7 @@ Prove: a_3[shift_sint32(b, i_1)] = a_3[shift_sint32(a, i_1)].
Goal Preservation of Invariant 'Copy' (file copy.i, line 11):
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
@@ -85,7 +85,7 @@ Prove: true.
Goal Assertion 'A' (file copy.i, line 18):
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Let a_3 = shift_sint32(a, i_1).
Assume {
Type: is_sint32(i) /\ is_sint32(n).
@@ -111,7 +111,7 @@ Prove: a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]][a_3] = a_2[a_3].
Goal Assertion 'B' (file copy.i, line 19):
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
Let a_4 = shift_sint32(b, i_1).
Assume {
@@ -153,7 +153,7 @@ Prove: true.
Goal Loop assigns (file copy.i, line 12) (3/3):
Effect at line 17
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Let x = i - 1.
Let a_3 = shift_sint32(a, x).
Let a_4 = a_2[a_3 <- a_2[shift_sint32(b, x)]].
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
index d43b32da852..1a0f184dade 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
@@ -11,7 +11,7 @@
Goal Post-condition 'qed_ok' in 'init':
Let a_1 = shift_sint32(t, a).
Let x = -a.
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, i - a).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, i - a).
Let x_1 = 1 + b.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(i).
@@ -56,7 +56,8 @@ Assume {
Have: (a <= i) /\ (i <= x_1).
(* Invariant 'qed_ok' *)
Have: forall i_1 : Z. ((a <= i_1) -> ((i_1 < i) ->
- (havoc(Mint_undef_0, Mint_0, a_1, i - a)[shift_sint32(t, i_1)] = e))).
+ (memcpy(Mint_0, Mint_undef_0, a_1, a_1, i - a)[shift_sint32(t, i_1)] =
+ e))).
(* Then *)
Have: i <= b.
}
@@ -82,7 +83,7 @@ Goal Preservation of Invariant 'qed_ok' (file loop.i, line 13):
Let x = 1 + i.
Let a_1 = shift_sint32(t, a).
Let x_1 = -a.
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, i - a).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, i - a).
Let x_2 = 1 + b.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(i) /\ is_sint32(x).
@@ -130,7 +131,7 @@ Goal Loop assigns 'qed_ok' (3/3):
Effect at line 18
Let a_1 = shift_sint32(t, a).
Let x = -a.
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, i - a).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, i - a).
Let a_3 = shift_sint32(t, i).
Let x_1 = 1 + i.
Let x_2 = 1 + b.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
index f48b3ded682..e9fcd31a9e0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
@@ -7,7 +7,7 @@
Goal Post-condition 'copied_contents' in 'memcpy':
Let a = shift_sint8(dest_0, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Assume {
Type: is_uint64(i) /\ is_uint64(n).
(* Heap *)
@@ -29,8 +29,8 @@ Assume {
(* Else *)
Have: n <= i.
}
-Prove: L_memcmp(Mchar_0, havoc(Mchar_undef_0, Mchar_0, a, i), dest_0, src_0,
- i) = 0.
+Prove: L_memcmp(Mchar_0, memcpy(Mchar_0, Mchar_undef_0, a, a, i), dest_0,
+ src_0, i) = 0.
------------------------------------------------------------
@@ -41,7 +41,7 @@ Prove: true.
Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 33):
Let a = shift_sint8(dest_0, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Assume {
Type: is_uint64(i) /\ is_uint64(n).
(* Heap *)
@@ -75,7 +75,7 @@ Prove: true.
Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 34):
Let x = to_uint64(1 + i).
Let a = shift_sint8(dest_0, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = a_1[shift_sint8(dest_0, i) <- a_1[shift_sint8(src_0, i)]].
Assume {
Type: is_uint64(i) /\ is_uint64(n).
@@ -126,7 +126,7 @@ Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 35) (3/3):
Effect at line 39
Let x = to_uint64(1 + i).
Let a = shift_sint8(dest_0, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = shift_sint8(dest_0, i).
Let a_3 = a_1[a_2 <- a_1[shift_sint8(src_0, i)]].
Assume {
@@ -170,7 +170,7 @@ Prove: true.
Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 38):
Let x = to_uint64(1 + i).
Let a = shift_sint8(dest_0, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = a_1[shift_sint8(dest_0, i) <- a_1[shift_sint8(src_0, i)]].
Assume {
Type: is_uint64(i) /\ is_uint64(n).
@@ -242,7 +242,7 @@ Assume {
(* Invariant 'no_eva' *)
Have: 0 <= n.
(* Loop assigns ... *)
- Have: havoc(Mchar_undef_0, Mchar_0, a, n) = Mchar_1.
+ Have: memcpy(Mchar_0, Mchar_undef_0, a, a, n) = Mchar_1.
(* Invariant 'no_eva' *)
Have: (0 <= i) /\ (i <= n).
(* Invariant 'no_eva' *)
@@ -267,7 +267,7 @@ Assume {
(Mchar_0[shift_sint8(src_0, i_3)]
= Mchar_0[shift_sint8(dest_0, i_3)]))).
(* Loop assigns ... *)
- Have: havoc(Mchar_undef_1, Mchar_0, a, n) = Mchar_2.
+ Have: memcpy(Mchar_0, Mchar_undef_1, a, a, n) = Mchar_2.
(* Invariant 'no_eva' *)
Have: (0 <= i_1) /\ (i_1 < n).
(* Invariant 'no_eva' *)
@@ -299,7 +299,7 @@ Prove: true.
Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 95):
Let a = shift_sint8(dest_0, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = shift_sint8(src_0, 0).
Assume {
Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
@@ -345,7 +345,7 @@ Prove: true.
Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 96):
Let x = to_uint64(1 + i).
Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = shift_sint8(s, 0).
Assume {
Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
@@ -396,7 +396,7 @@ Prove: true.
Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 97):
Let x = to_uint64(1 + i).
Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = a_1[shift_sint8(d, i) <- a_1[shift_sint8(s, i)]].
Let a_3 = shift_sint8(s, 0).
Let a_4 = shift_sint8(s, i_1).
@@ -450,7 +450,7 @@ Prove: true.
Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 107):
Let a = shift_sint8(dest_0, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let x = to_uint64(n - 1).
Let a_2 = shift_sint8(src_0, 0).
Assume {
@@ -521,7 +521,7 @@ Prove: to_uint64(n - 1) < n.
Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 108):
Let x = to_uint64(i - 1).
Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let x_1 = to_uint64(n - 1).
Let a_2 = shift_sint8(s, 0).
Assume {
@@ -603,7 +603,7 @@ Prove: Mchar_0[shift_sint8(src_0, i)] = Mchar_0[shift_sint8(dest_0, i)].
Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 109):
Let x = to_uint64(i - 1).
Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = a_1[shift_sint8(d, i) <- a_1[shift_sint8(s, i)]].
Let x_1 = to_uint64(n - 1).
Let a_3 = shift_sint8(s, 0).
@@ -674,7 +674,7 @@ Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 98) (3/3):
Effect at line 102
Let x = to_uint64(1 + i).
Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = shift_sint8(d, i).
Let a_3 = a_1[a_2 <- a_1[shift_sint8(s, i)]].
Let a_4 = shift_sint8(s, 0).
@@ -739,7 +739,7 @@ Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 110) (3/3):
Effect at line 114
Let x = to_uint64(i - 1).
Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = shift_sint8(d, i).
Let a_3 = a_1[a_2 <- a_1[shift_sint8(s, i)]].
Let x_1 = to_uint64(n - 1).
@@ -842,7 +842,7 @@ Prove: true.
Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 101):
Let x = to_uint64(1 + i).
Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = a_1[shift_sint8(d, i) <- a_1[shift_sint8(s, i)]].
Let a_3 = shift_sint8(s, 0).
Assume {
@@ -897,7 +897,7 @@ Prove: true.
Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 113):
Let x = to_uint64(i - 1).
Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
+Let a_1 = memcpy(Mchar_0, Mchar_undef_0, a, a, n).
Let a_2 = a_1[shift_sint8(d, i) <- a_1[shift_sint8(s, i)]].
Let x_1 = to_uint64(n - 1).
Let a_3 = shift_sint8(s, 0).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
index f93ab5d670e..b9bb077fb31 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
@@ -370,7 +370,7 @@ Prove: true.
Goal Post-condition (file unfold_assigns.i, line 52) in 'USE_ASSIGN_UNFOLD_KO':
Let a = Load_S1_S(q, Mint_0).
-Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Let a_1 = Load_S1_S(q, memcpy(Mint_0, Mint_undef_0, p, p, 2)).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
@@ -415,7 +415,7 @@ Prove: true.
Goal Post-condition (file unfold_assigns.i, line 43) in 'USE_ASSIGN_UNFOLD_OK':
Let a = Load_S1_S(q, Mint_0).
-Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Let a_1 = Load_S1_S(q, memcpy(Mint_0, Mint_undef_0, p, p, 2)).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
index 012860dfab7..e1451269a58 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
@@ -386,7 +386,7 @@ Prove: true.
Goal Post-condition (file unfold_assigns.i, line 52) in 'USE_ASSIGN_UNFOLD_KO':
Let a = Load_S1_S(q, Mint_0).
-Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Let a_1 = Load_S1_S(q, memcpy(Mint_0, Mint_undef_0, p, p, 2)).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
@@ -425,7 +425,7 @@ Prove: true.
Goal Post-condition (file unfold_assigns.i, line 43) in 'USE_ASSIGN_UNFOLD_OK':
Let a = Load_S1_S(q, Mint_0).
-Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Let a_1 = Load_S1_S(q, memcpy(Mint_0, Mint_undef_0, p, p, 2)).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.2.res.oracle
index 2a09b8ccd3d..d5264fbf8ce 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.2.res.oracle
@@ -374,7 +374,7 @@ Prove: true.
Goal Post-condition (file unfold_assigns.i, line 52) in 'USE_ASSIGN_UNFOLD_KO':
Let a = Load_S1_S(q, Mint_0).
-Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Let a_1 = Load_S1_S(q, memcpy(Mint_0, Mint_undef_0, p, p, 2)).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
@@ -413,7 +413,7 @@ Prove: true.
Goal Post-condition (file unfold_assigns.i, line 43) in 'USE_ASSIGN_UNFOLD_OK':
Let a = Load_S1_S(q, Mint_0).
-Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Let a_1 = Load_S1_S(q, memcpy(Mint_0, Mint_undef_0, p, p, 2)).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.3.res.oracle
index 28a5ec81a80..d47dda21e78 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.3.res.oracle
@@ -370,7 +370,7 @@ Prove: true.
Goal Post-condition (file unfold_assigns.i, line 52) in 'USE_ASSIGN_UNFOLD_KO':
Let a = Load_S1_S(q, Mint_0).
-Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Let a_1 = Load_S1_S(q, memcpy(Mint_0, Mint_undef_0, p, p, 2)).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
@@ -409,7 +409,7 @@ Prove: true.
Goal Post-condition (file unfold_assigns.i, line 43) in 'USE_ASSIGN_UNFOLD_OK':
Let a = Load_S1_S(q, Mint_0).
-Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Let a_1 = Load_S1_S(q, memcpy(Mint_0, Mint_undef_0, p, p, 2)).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
index 75bce10e980..d0453d1612a 100644
--- a/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
@@ -13,9 +13,9 @@
Goal Post-condition (file copy_array.c, line 4) in 'copy':
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let a_2 = memcpy(Msint32_0, Msint32_undef_0, a_1, a_1, n).
Let x = 4 * n.
-Let a_3 = havoc(Msint32_undef_0, Msint32_0, a_1, i).
+Let a_3 = memcpy(Msint32_0, Msint32_undef_0, a_1, a_1, i).
Assume {
Type: is_sint32(i) /\ is_sint32(n).
(* Heap *)
@@ -40,7 +40,7 @@ Prove: a_3[shift_sint32(b, i_1)] = a_3[shift_sint32(a, i_1)].
Goal Preservation of Invariant 'Copy' (file copy_array.c, line 11):
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let a_2 = memcpy(Msint32_0, Msint32_undef_0, a_1, a_1, n).
Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
Let x = 4 * n.
Assume {
@@ -90,7 +90,7 @@ Prove: true.
Goal Assertion 'A' (file copy_array.c, line 18):
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let a_2 = memcpy(Msint32_0, Msint32_undef_0, a_1, a_1, n).
Let x = 4 * n.
Let a_3 = shift_sint32(a, i_1).
Assume {
@@ -117,7 +117,7 @@ Prove: a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]][a_3] = a_2[a_3].
Goal Assertion 'B' (file copy_array.c, line 19):
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let a_2 = memcpy(Msint32_0, Msint32_undef_0, a_1, a_1, n).
Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
Let x = 4 * n.
Let a_4 = shift_sint32(b, i_1).
@@ -160,7 +160,7 @@ Prove: true.
Goal Loop assigns (file copy_array.c, line 12) (3/3):
Effect at line 17
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let a_2 = memcpy(Msint32_0, Msint32_undef_0, a_1, a_1, n).
Let x = i - 1.
Let a_3 = shift_sint32(a, x).
Let a_4 = a_2[a_3 <- a_2[shift_sint32(b, x)]].
diff --git a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
index ffdcf75c1ce..ba812dcdc33 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
@@ -132,9 +132,9 @@ theory Compound
axiom Q_Array_uint32_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
- [Array_uint32 p n (havoc mint1 mint q n1)].
+ [Array_uint32 p n (memcpy mint mint1 q q n1)].
separated p 1 q n1 ->
- Array_uint32 p n (havoc mint1 mint q n1) = Array_uint32 p n mint
+ Array_uint32 p n (memcpy mint mint1 q q n1) = Array_uint32 p n mint
axiom Q_Array_sint64_access :
forall mint:addr -> int, i:int, n:int, p:addr
@@ -156,9 +156,9 @@ theory Compound
axiom Q_Array_sint64_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
- [Array_sint64 p n (havoc mint1 mint q n1)].
+ [Array_sint64 p n (memcpy mint mint1 q q n1)].
separated p 1 q n1 ->
- Array_sint64 p n (havoc mint1 mint q n1) = Array_sint64 p n mint
+ Array_sint64 p n (memcpy mint mint1 q q n1) = Array_sint64 p n mint
axiom Q_Load_S1_S_update_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
@@ -178,9 +178,9 @@ theory Compound
axiom Q_Load_S1_S_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr
- [Load_S1_S p (havoc mint1 mint q n) mint2 mint3].
+ [Load_S1_S p (memcpy mint mint1 q q n) mint2 mint3].
separated p 11 q n ->
- Load_S1_S p (havoc mint1 mint q n) mint2 mint3 =
+ Load_S1_S p (memcpy mint mint1 q q n) mint2 mint3 =
Load_S1_S p mint mint2 mint3
axiom Q_Load_S1_S_update_Mint1 :
@@ -201,9 +201,9 @@ theory Compound
axiom Q_Load_S1_S_havoc_Mint1 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr
- [Load_S1_S p mint3 (havoc mint2 mint1 q n) mint].
+ [Load_S1_S p mint3 (memcpy mint1 mint2 q q n) mint].
separated p 11 q n ->
- Load_S1_S p mint3 (havoc mint2 mint1 q n) mint =
+ Load_S1_S p mint3 (memcpy mint1 mint2 q q n) mint =
Load_S1_S p mint3 mint1 mint
axiom Q_Load_S1_S_update_Mint2 :
@@ -224,9 +224,9 @@ theory Compound
axiom Q_Load_S1_S_havoc_Mint2 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr
- [Load_S1_S p mint1 mint (havoc mint3 mint2 q n)].
+ [Load_S1_S p mint1 mint (memcpy mint2 mint3 q q n)].
separated p 11 q n ->
- Load_S1_S p mint1 mint (havoc mint3 mint2 q n) =
+ Load_S1_S p mint1 mint (memcpy mint2 mint3 q q n) =
Load_S1_S p mint1 mint mint2
end
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 64c2f4fe312..6e39bf3db96 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -32,17 +32,17 @@ Assume {
Have: (0 <= i) /\ (i <= n).
(* Invariant 'Partial' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (havoc(Mint_undef_0, Mint_0, a_1, n)[shift_sint32(a, i_2)] = v))).
+ (memcpy(Mint_0, Mint_undef_0, a_1, a_1, n)[shift_sint32(a, i_2)] = v))).
(* Else *)
Have: n <= i.
}
-Prove: havoc(Mint_undef_0, Mint_0, a_1, i)[shift_sint32(a, i_1)] = v.
+Prove: memcpy(Mint_0, Mint_undef_0, a_1, a_1, i)[shift_sint32(a, i_1)] = v.
------------------------------------------------------------
Goal Preservation of Invariant 'Partial' (file user_init.i, line 17):
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
(* Heap *)
@@ -96,7 +96,7 @@ Prove: true.
Goal Loop assigns 'Zone' (3/3):
Effect at line 20
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Let x = i - 1.
Let a_3 = shift_sint32(a, x).
Assume {
@@ -287,7 +287,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
+Let a_3 = memcpy(Mint_0, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Goal *)
@@ -324,14 +324,15 @@ Prove: true.
Goal Preservation of Invariant 'Range' (file user_init.i, line 135):
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
+Let a_2 = shift_sint32(a_1, 0).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Loop assigns 'lack,Zone' *)
- Have: forall a_2 : addr.
+ Have: forall a_3 : addr.
((forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
- (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))))) ->
- (Mint_0[a_2] = Mint_1[a_2])).
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_3)))))) ->
+ (Mint_0[a_3] = Mint_1[a_3])).
(* Invariant 'Range' *)
Have: (0 <= i) /\ (i <= 10).
(* Invariant 'Partial' *)
@@ -342,8 +343,8 @@ Assume {
Have: i <= 9.
(* Call 'init' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
- [shift_sint32(a_1, i_1)] = v))).
+ (memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20)[shift_sint32(a_1, i_1)] =
+ v))).
}
Prove: to_uint32(1 + i) <= 10.
@@ -370,7 +371,7 @@ Let x = to_uint32(1 + i_2).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i_2).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
@@ -412,7 +413,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Goal *)
@@ -515,7 +516,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Loop assigns 'lack,Zone' *)
@@ -605,7 +606,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
+Let a_3 = memcpy(Mint_0, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Goal *)
@@ -641,13 +642,14 @@ Prove: true.
Goal Preservation of Invariant 'Range' (file user_init.i, line 153):
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
+Let a_2 = shift_sint32(a_1, 0).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Loop assigns 'tactic,Zone' *)
- Have: forall a_2 : addr.
+ Have: forall a_3 : addr.
((forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
- (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))) ->
- (Mint_0[a_2] = Mint_1[a_2])).
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_3)))) ->
+ (Mint_0[a_3] = Mint_1[a_3])).
(* Invariant 'Range' *)
Have: (0 <= i) /\ (i <= 10).
(* Invariant 'Partial' *)
@@ -658,8 +660,8 @@ Assume {
Have: i <= 9.
(* Call 'init' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
- [shift_sint32(a_1, i_1)] = v))).
+ (memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20)[shift_sint32(a_1, i_1)] =
+ v))).
}
Prove: to_uint32(1 + i) <= 10.
@@ -686,7 +688,7 @@ Let x = to_uint32(1 + i_2).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i_2).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
@@ -726,7 +728,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Goal *)
@@ -822,7 +824,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Loop assigns 'tactic,Zone' *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index 76eef451c02..5c0b0175dda 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -32,17 +32,17 @@ Assume {
Have: (0 <= i) /\ (i <= n).
(* Invariant 'Partial' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (havoc(Mint_undef_0, Mint_0, a_1, n)[shift_sint32(a, i_2)] = v))).
+ (memcpy(Mint_0, Mint_undef_0, a_1, a_1, n)[shift_sint32(a, i_2)] = v))).
(* Else *)
Have: n <= i.
}
-Prove: havoc(Mint_undef_0, Mint_0, a_1, i)[shift_sint32(a, i_1)] = v.
+Prove: memcpy(Mint_0, Mint_undef_0, a_1, a_1, i)[shift_sint32(a, i_1)] = v.
------------------------------------------------------------
Goal Preservation of Invariant 'Partial' (file user_init.i, line 17):
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
(* Heap *)
@@ -96,7 +96,7 @@ Prove: true.
Goal Loop assigns 'Zone' (3/3):
Effect at line 20
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, n).
Let x = i - 1.
Let a_3 = shift_sint32(a, x).
Assume {
@@ -287,7 +287,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
+Let a_3 = memcpy(Mint_0, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Goal *)
@@ -324,14 +324,15 @@ Prove: true.
Goal Preservation of Invariant 'Range' (file user_init.i, line 135):
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
+Let a_2 = shift_sint32(a_1, 0).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Loop assigns 'lack,Zone' *)
- Have: forall a_2 : addr.
+ Have: forall a_3 : addr.
((forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
- (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))))) ->
- (Mint_0[a_2] = Mint_1[a_2])).
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_3)))))) ->
+ (Mint_0[a_3] = Mint_1[a_3])).
(* Invariant 'Range' *)
Have: (0 <= i) /\ (i <= 10).
(* Invariant 'Partial' *)
@@ -342,8 +343,8 @@ Assume {
Have: i <= 9.
(* Call 'init' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
- [shift_sint32(a_1, i_1)] = v))).
+ (memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20)[shift_sint32(a_1, i_1)] =
+ v))).
}
Prove: to_uint32(1 + i) <= 10.
@@ -370,7 +371,7 @@ Let x = to_uint32(1 + i_2).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i_2).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
@@ -412,7 +413,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Goal *)
@@ -515,7 +516,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Loop assigns 'lack,Zone' *)
@@ -605,7 +606,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
+Let a_3 = memcpy(Mint_0, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Goal *)
@@ -641,13 +642,14 @@ Prove: true.
Goal Preservation of Invariant 'Range' (file user_init.i, line 153):
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
+Let a_2 = shift_sint32(a_1, 0).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Loop assigns 'tactic,Zone' *)
- Have: forall a_2 : addr.
+ Have: forall a_3 : addr.
((forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
- (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))) ->
- (Mint_0[a_2] = Mint_1[a_2])).
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_3)))) ->
+ (Mint_0[a_3] = Mint_1[a_3])).
(* Invariant 'Range' *)
Have: (0 <= i) /\ (i <= 10).
(* Invariant 'Partial' *)
@@ -658,8 +660,8 @@ Assume {
Have: i <= 9.
(* Call 'init' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
- [shift_sint32(a_1, i_1)] = v))).
+ (memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20)[shift_sint32(a_1, i_1)] =
+ v))).
}
Prove: to_uint32(1 + i) <= 10.
@@ -686,7 +688,7 @@ Let x = to_uint32(1 + i_2).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i_2).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
@@ -726,7 +728,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Goal *)
@@ -822,7 +824,7 @@ Let x = to_uint32(1 + i).
Let a = global(G_t2_52).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_1, a_2, 20).
+Let a_3 = memcpy(Mint_1, Mint_undef_0, a_2, a_2, 20).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
(* Loop assigns 'tactic,Zone' *)
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
index f8d4fe69e12..5f9dfd94dc8 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
@@ -10,7 +10,8 @@
Goal Post-condition (file caveat_range.i, line 12) in 'reset':
Let a = global(G_p_22).
-Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
+Let a_1 = shift_S1_S(a, 0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, 20).
Assume {
Type: is_sint32(i_1).
(* Goal *)
@@ -19,20 +20,21 @@ Assume {
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
- (a_1[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
+ (a_2[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
- (a_1[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
+ (a_2[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
(* Else *)
Have: 10 <= i_1.
}
-Prove: a_1[shiftfield_F1_S_f(shift_S1_S(a, i))] = 1.
+Prove: a_2[shiftfield_F1_S_f(shift_S1_S(a, i))] = 1.
------------------------------------------------------------
Goal Post-condition (file caveat_range.i, line 13) in 'reset':
Let a = global(G_p_22).
-Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
+Let a_1 = shift_S1_S(a, 0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, 20).
Assume {
Type: is_sint32(i_1).
(* Goal *)
@@ -41,14 +43,14 @@ Assume {
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
- (a_1[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
+ (a_2[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
- (a_1[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
+ (a_2[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
(* Else *)
Have: 10 <= i_1.
}
-Prove: a_1[shiftfield_F1_S_g(shift_S1_S(a, i))] = 2.
+Prove: a_2[shiftfield_F1_S_g(shift_S1_S(a, i))] = 2.
------------------------------------------------------------
@@ -64,7 +66,8 @@ Prove: true.
Goal Preservation of Invariant (file caveat_range.i, line 20):
Let a = global(G_p_22).
-Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
+Let a_1 = shift_S1_S(a, 0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, 20).
Assume {
Type: is_sint32(i) /\ is_sint32(1 + i).
(* Goal *)
@@ -73,16 +76,16 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
+ (a_2[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
+ (a_2[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
(* Then *)
Have: i <= 9.
(* Invariant *)
Have: (-1) <= i.
}
-Prove: a_1[shiftfield_F1_S_f(shift_S1_S(a, i)) <- 1]
+Prove: a_2[shiftfield_F1_S_f(shift_S1_S(a, i)) <- 1]
[shiftfield_F1_S_f(shift_S1_S(a, i_1))] = 1.
------------------------------------------------------------
@@ -94,9 +97,10 @@ Prove: true.
Goal Preservation of Invariant (file caveat_range.i, line 21):
Let a = global(G_p_22).
-Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
-Let a_2 = shift_S1_S(a, i).
-Let a_3 = a_1[shiftfield_F1_S_f(a_2) <- 1].
+Let a_1 = shift_S1_S(a, 0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, 20).
+Let a_3 = shift_S1_S(a, i).
+Let a_4 = a_2[shiftfield_F1_S_f(a_3) <- 1].
Assume {
Type: is_sint32(i) /\ is_sint32(1 + i).
(* Goal *)
@@ -105,19 +109,19 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
+ (a_2[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
+ (a_2[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
(* Then *)
Have: i <= 9.
(* Invariant *)
Have: (-1) <= i.
(* Invariant *)
Have: forall i_2 : Z. ((i_2 <= i) -> ((0 <= i_2) ->
- (a_3[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
+ (a_4[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
}
-Prove: a_3[shiftfield_F1_S_g(a_2) <- 2]
+Prove: a_4[shiftfield_F1_S_g(a_3) <- 2]
[shiftfield_F1_S_g(shift_S1_S(a, i_1))] = 2.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
index 78be9b03031..793bf4c678c 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
@@ -13,7 +13,7 @@
Goal Post-condition 'memcpy' in 'memcpy_alias_vars':
Let a = Mptr_0[global(P_dst_25)].
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
Let a_3 = Mptr_0[global(P_src_24)].
Let a_4 = shift_uint8(a_3, 0).
Assume {
@@ -47,7 +47,7 @@ Prove: a_2[shift_uint8(a, i)] = Mint_0[shift_uint8(a_3, i)].
Goal Post-condition 'unmodified' in 'memcpy_alias_vars':
Let a = Mptr_0[global(P_dst_25)].
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
Let a_3 = Mptr_0[global(P_src_24)].
Let a_4 = shift_uint8(a_3, 0).
Let a_5 = shift_uint8(a_3, i).
@@ -82,7 +82,7 @@ Prove: a_2[a_5] = Mint_0[a_5].
Goal Preservation of Invariant 'cpy' (file issue-189-bis.i, line 27):
Let a = Mptr_0[global(P_dst_25)].
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
Let a_3 = Mptr_0[global(P_src_24)].
Let a_4 = shift_uint8(a_3, 0).
Let a_5 = a_2[v <- a_2[v_1]].
@@ -134,7 +134,7 @@ Prove: true.
Goal Preservation of Invariant 'len' (file issue-189-bis.i, line 23):
Let a = Mptr_0[global(P_dst_25)].
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_1).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_1).
Let a_3 = Mptr_0[global(P_src_24)].
Let a_4 = shift_uint8(a_3, 0).
Assume {
@@ -200,7 +200,7 @@ Effect at line 33
Let a = global(P_dst_25).
Let a_1 = Mptr_0[a].
Let a_2 = shift_uint8(a_1, 0).
-Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, len_0).
+Let a_3 = memcpy(Mint_0, Mint_undef_0, a_2, a_2, len_0).
Let a_4 = a_3[v <- a_3[v_1]].
Let a_5 = global(P_src_24).
Let a_6 = Mptr_0[a_5].
@@ -260,7 +260,7 @@ Prove: true.
Goal Post-condition 'memcpy,ok' in 'memcpy_context_vars':
Let a = Mptr_0[global(P_dst_48)].
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
Let a_3 = Mptr_0[global(P_src_47)].
Let a_4 = shift_uint8(a_3, 0).
Assume {
@@ -294,7 +294,7 @@ Prove: a_2[shift_uint8(a, i)] = Mint_0[shift_uint8(a_3, i)].
Goal Post-condition 'unmodified,ok' in 'memcpy_context_vars':
Let a = Mptr_0[global(P_dst_48)].
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
Let a_3 = Mptr_0[global(P_src_47)].
Let a_4 = shift_uint8(a_3, 0).
Let a_5 = shift_uint8(a_3, i).
@@ -329,7 +329,7 @@ Prove: a_2[a_5] = Mint_0[a_5].
Goal Preservation of Invariant 'ok,cpy' (file issue-189-bis.i, line 56):
Let a = Mptr_0[global(P_dst_48)].
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
Let a_3 = Mptr_0[global(P_src_47)].
Let a_4 = shift_uint8(a_3, 0).
Let a_5 = a_2[dst2_0 <- a_2[src2_0]].
@@ -381,7 +381,7 @@ Prove: true.
Goal Preservation of Invariant 'ok,len' (file issue-189-bis.i, line 52):
Let a = Mptr_0[global(P_dst_48)].
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_1).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_1).
Let a_3 = Mptr_0[global(P_src_47)].
Let a_4 = shift_uint8(a_3, 0).
Assume {
@@ -446,7 +446,7 @@ Goal Loop assigns (file issue-189-bis.i, line 55) (4/4):
Effect at line 62
Let a = Mptr_0[global(P_dst_48)].
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
Let a_3 = a_2[tmp_0 <- a_2[src2_0]].
Let a_4 = Mptr_0[global(P_src_47)].
Let a_5 = shift_uint8(a_4, 0).
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
index 9478cae317a..b65c788fa08 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
@@ -7,8 +7,9 @@
Goal Post-condition 'memcpy,ok' in 'memcpy_context_vars':
Let a = global(G_dst_48).
-Let a_1 = havoc(Mint_undef_0, Mint_0, shift_uint8(a, 0), len_0).
-Let a_2 = global(G_src_47).
+Let a_1 = shift_uint8(a, 0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
+Let a_3 = global(G_src_47).
Assume {
Type: is_sint32(len_0) /\ is_sint32(len_1).
(* Goal *)
@@ -18,16 +19,16 @@ Assume {
(* Invariant 'ok,len' *)
Have: len_1 <= len_0.
(* Invariant 'ok,src' *)
- Have: shift_uint8(a_2, len_0) = shift_uint8(src2_0, len_1).
+ Have: shift_uint8(a_3, len_0) = shift_uint8(src2_0, len_1).
(* Invariant 'ok,dst' *)
Have: shift_uint8(a, len_0) = shift_uint8(dst2_0, len_1).
(* Invariant 'ok,cpy' *)
Have: forall i_1 : Z. ((0 <= i_1) -> (((len_1 + i_1) < len_0) ->
- (a_1[shift_uint8(a, i_1)] = Mint_0[shift_uint8(a_2, i_1)]))).
+ (a_2[shift_uint8(a, i_1)] = Mint_0[shift_uint8(a_3, i_1)]))).
(* Else *)
Have: len_1 <= 0.
}
-Prove: a_1[shift_uint8(a, i)] = Mint_0[shift_uint8(a_2, i)].
+Prove: a_2[shift_uint8(a, i)] = Mint_0[shift_uint8(a_3, i)].
------------------------------------------------------------
@@ -38,9 +39,10 @@ Prove: true.
Goal Preservation of Invariant 'ok,cpy' (file issue-189-bis.i, line 56):
Let a = global(G_dst_48).
-Let a_1 = havoc(Mint_undef_0, Mint_0, shift_uint8(a, 0), len_0).
-Let a_2 = global(G_src_47).
-Let a_3 = a_1[dst2_0 <- a_1[src2_0]].
+Let a_1 = shift_uint8(a, 0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
+Let a_3 = global(G_src_47).
+Let a_4 = a_2[dst2_0 <- a_2[src2_0]].
Assume {
Type: is_sint32(len_0) /\ is_sint32(len_1) /\ is_sint32(len_1 - 1).
(* Goal *)
@@ -50,18 +52,18 @@ Assume {
(* Invariant 'ok,len' *)
Have: len_1 <= len_0.
(* Invariant 'ok,src' *)
- Have: shift_uint8(a_2, len_0) = shift_uint8(src2_0, len_1).
+ Have: shift_uint8(a_3, len_0) = shift_uint8(src2_0, len_1).
(* Invariant 'ok,dst' *)
Have: shift_uint8(a, len_0) = shift_uint8(dst2_0, len_1).
(* Invariant 'ok,cpy' *)
Have: forall i_1 : Z. ((0 <= i_1) -> (((len_1 + i_1) < len_0) ->
- (a_1[shift_uint8(a, i_1)] = Mint_0[shift_uint8(a_2, i_1)]))).
+ (a_2[shift_uint8(a, i_1)] = Mint_0[shift_uint8(a_3, i_1)]))).
(* Then *)
Have: 0 < len_1.
(* Invariant 'ok,len' *)
Have: len_1 <= (1 + len_0).
}
-Prove: a_3[shift_uint8(a_2, i)] = a_3[shift_uint8(a, i)].
+Prove: a_4[shift_uint8(a_3, i)] = a_4[shift_uint8(a, i)].
------------------------------------------------------------
@@ -82,7 +84,8 @@ Prove: true.
Goal Preservation of Invariant 'ok,len' (file issue-189-bis.i, line 52):
Let a = global(G_dst_48).
-Let a_1 = global(G_src_47).
+Let a_1 = shift_uint8(a, 0).
+Let a_2 = global(G_src_47).
Assume {
Type: is_sint32(len_1) /\ is_sint32(len_0) /\ is_sint32(len_0 - 1).
(* Pre-condition 'write_access' *)
@@ -90,13 +93,13 @@ Assume {
(* Invariant 'ok,len' *)
Have: len_0 <= len_1.
(* Invariant 'ok,src' *)
- Have: shift_uint8(a_1, len_1) = shift_uint8(src2_0, len_0).
+ Have: shift_uint8(a_2, len_1) = shift_uint8(src2_0, len_0).
(* Invariant 'ok,dst' *)
Have: shift_uint8(a, len_1) = shift_uint8(dst2_0, len_0).
(* Invariant 'ok,cpy' *)
Have: forall i : Z. ((0 <= i) -> (((len_0 + i) < len_1) ->
- (havoc(Mint_undef_0, Mint_0, shift_uint8(a, 0), len_1)
- [shift_uint8(a, i)] = Mint_0[shift_uint8(a_1, i)]))).
+ (memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_1)[shift_uint8(a, i)] =
+ Mint_0[shift_uint8(a_2, i)]))).
(* Then *)
Have: 0 < len_0.
}
@@ -140,7 +143,7 @@ Goal Loop assigns (file issue-189-bis.i, line 55) (4/4):
Effect at line 62
Let a = global(G_dst_48).
Let a_1 = shift_uint8(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, len_0).
+Let a_2 = memcpy(Mint_0, Mint_undef_0, a_1, a_1, len_0).
Let a_3 = a_2[tmp_0 <- a_2[src2_0]].
Let a_4 = global(G_src_47).
Assume {
--
GitLab