From a551f7d0145a9e1f4f4fa50966428deb38601345 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 10 Dec 2020 16:19:34 +0100
Subject: [PATCH] [wp] Update tests for new default machdep

---
 .../wp_plugin/oracle/overflow2.res.oracle     |  20 ++-
 .../wp_plugin/oracle/string_c.res.oracle      |  70 +++++------
 .../wp_region/oracle/fb_ADD/region/job.dot    |  18 +--
 .../wp_region/oracle/fb_SORT/region/job.dot   |  10 +-
 .../oracle/multi_matrix_types.res.oracle      | 118 +++++++++++-------
 .../wp_typed/oracle/unit_bitwise.res.oracle   |   2 +-
 .../wp_typed/oracle/user_string.0.res.oracle  |  26 +++-
 .../wp_typed/oracle/user_string.1.res.oracle  |  26 +++-
 8 files changed, 190 insertions(+), 100 deletions(-)

diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
index d2b0d3de19a..bbd22a05eec 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
@@ -63,7 +63,13 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Assertion 'a06' (file tests/wp_plugin/overflow2.c, line 39):
-Prove: true.
+Let x = p1_off_alt_0 + to_uint16(distance_0).
+Assume {
+  Type: is_sint16(distance_0) /\ is_uint64(p1_off_alt_0).
+  (* Pre-condition *)
+  Have: p1_off_alt_0 <= 10.
+}
+Prove: to_uint64(x) = to_uint32(x).
 
 ------------------------------------------------------------
 
@@ -78,25 +84,29 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Assertion 'a09' (file tests/wp_plugin/overflow2.c, line 42):
+Let x = p1_off_alt_0 + to_uint16(distance_0).
 Assume {
-  Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
+  Type: is_sint16(distance_0) /\ is_uint64(p1_off_alt_0).
   (* Pre-condition *)
   Have: p1_off_alt_0 <= 10.
+  Have: to_uint64(x) = to_uint32(x).
 }
-Prove: (p1_off_alt_0 + to_uint16(distance_0)) <= 65545.
+Prove: x <= 65545.
 
 ------------------------------------------------------------
 
 Goal Assertion 'a10' (file tests/wp_plugin/overflow2.c, line 43):
 Let x = p1_off_alt_0 + to_uint16(distance_0).
+Let x_1 = to_uint32(x).
 Assume {
-  Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
+  Type: is_sint16(distance_0) /\ is_uint64(p1_off_alt_0).
   (* Pre-condition *)
   Have: p1_off_alt_0 <= 10.
+  Have: to_uint64(x) = x_1.
   (* Assertion 'a09' *)
   Have: x <= 65545.
 }
-Prove: x = to_uint32(x).
+Prove: x = x_1.
 
 ------------------------------------------------------------
 
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 aa233aaddc7..1774140d9e3 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).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n).
+  Type: is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -37,7 +37,7 @@ Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 3
 Let a = shift_sint8(dest_0, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n).
+  Type: is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -53,13 +53,13 @@ Assume {
   (* Then *)
   Have: i < n.
 }
-Prove: to_uint32(1 + i) <= n.
+Prove: to_uint64(1 + i) <= n.
 
 ------------------------------------------------------------
 
 Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 33):
 Assume {
-  Type: is_uint32(n).
+  Type: is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0).
@@ -77,12 +77,12 @@ Let a = shift_sint8(dest_0, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = a_1[shift_sint8(dest_0, i) <- a_1[shift_sint8(src_0, i)]].
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n).
+  Type: is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
-  When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+  When: (0 <= i_1) /\ (i_1 < to_uint64(1 + i)).
   (* Pre-condition *)
   Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
       P_valid_read_or_empty(Malloc_0, src_0, n) /\
@@ -121,7 +121,7 @@ Let a = shift_sint8(dest_0, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(dest_0, i).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n).
+  Type: is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -153,7 +153,7 @@ Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 3
 Let a = shift_sint8(dest_0, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n).
+  Type: is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -169,7 +169,7 @@ Assume {
   (* Then *)
   Have: i < n.
 }
-Prove: i < to_uint32(1 + i).
+Prove: i < to_uint64(1 + i).
 
 ------------------------------------------------------------
 
@@ -180,8 +180,8 @@ Prove: true.
 
 Goal Post-condition 'copied_contents' in 'memmove':
 Assume {
-  Type: is_uint32(i) /\ is_uint32(i_1) /\ is_uint32(n) /\
-      is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(i_1) /\
+      is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -252,7 +252,7 @@ Let a = shift_sint8(dest_0, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(src_0, 0).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -280,7 +280,7 @@ Assume {
   (* Then *)
   Have: i < n.
 }
-Prove: to_uint32(1 + i) <= n.
+Prove: to_uint64(1 + i) <= n.
 
 ------------------------------------------------------------
 
@@ -288,7 +288,7 @@ Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line
 Let a = shift_sint8(d, 0).
 Let a_1 = shift_sint8(s, 0).
 Assume {
-  Type: is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
   (* Pre-condition *)
@@ -314,12 +314,12 @@ Let a = shift_sint8(d, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(s, 0).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0) /\
       sconst(Mchar_0).
   (* Goal *)
-  When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+  When: (0 <= i_1) /\ (i_1 < to_uint64(1 + i)).
   (* Pre-condition *)
   Have: P_valid_or_empty(Malloc_0, d, n) /\
       P_valid_read_or_empty(Malloc_0, s, n).
@@ -360,12 +360,12 @@ Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(s, 0).
 Let a_3 = shift_sint8(s, i_1).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0) /\
       sconst(Mchar_0).
   (* Goal *)
-  When: (i_1 < n) /\ (to_uint32(1 + i) <= i_1).
+  When: (i_1 < n) /\ (to_uint64(1 + i) <= i_1).
   (* Pre-condition *)
   Have: P_valid_or_empty(Malloc_0, d, n) /\
       P_valid_read_or_empty(Malloc_0, s, n).
@@ -404,7 +404,7 @@ Let a = shift_sint8(dest_0, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(src_0, 0).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -432,7 +432,7 @@ Assume {
   (* Then *)
   Have: 0 < i.
 }
-Prove: to_uint32(i - 1) < n.
+Prove: to_uint64(i - 1) < n.
 
 ------------------------------------------------------------
 
@@ -440,7 +440,7 @@ Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line
 Let a = shift_sint8(d, 0).
 Let a_1 = shift_sint8(s, 0).
 Assume {
-  Type: is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
   (* Pre-condition *)
@@ -457,7 +457,7 @@ Assume {
   (* Else *)
   Have: 0 < memoverlap_0.
 }
-Prove: to_uint32(n - 1) < n.
+Prove: to_uint64(n - 1) < n.
 
 ------------------------------------------------------------
 
@@ -466,12 +466,12 @@ Let a = shift_sint8(d, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(s, 0).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0) /\
       sconst(Mchar_0).
   (* Goal *)
-  When: (i_1 < n) /\ (to_uint32(i - 1) < i_1).
+  When: (i_1 < n) /\ (to_uint64(i - 1) < i_1).
   (* Pre-condition *)
   Have: P_valid_or_empty(Malloc_0, d, n) /\
       P_valid_read_or_empty(Malloc_0, s, n).
@@ -505,12 +505,12 @@ Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line
 Let a = shift_sint8(dest_0, 0).
 Let a_1 = shift_sint8(src_0, 0).
 Assume {
-  Type: is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
-  When: (i < n) /\ (to_uint32(n - 1) < i).
+  When: (i < n) /\ (to_uint64(n - 1) < i).
   (* Pre-condition *)
   Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
       P_valid_read_or_empty(Malloc_0, src_0, n).
@@ -535,12 +535,12 @@ Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(s, 0).
 Let a_3 = shift_sint8(s, i_1).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0) /\
       sconst(Mchar_0).
   (* Goal *)
-  When: (0 <= i_1) /\ (i_1 <= to_uint32(i - 1)).
+  When: (0 <= i_1) /\ (i_1 <= to_uint64(i - 1)).
   (* Pre-condition *)
   Have: P_valid_or_empty(Malloc_0, d, n) /\
       P_valid_read_or_empty(Malloc_0, s, n).
@@ -592,7 +592,7 @@ Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(src_0, 0).
 Let a_3 = shift_sint8(d, i).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -644,7 +644,7 @@ Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(src_0, 0).
 Let a_3 = shift_sint8(d, i).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -718,7 +718,7 @@ Let a = shift_sint8(d, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(src_0, 0).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -763,7 +763,7 @@ Let a = shift_sint8(dest_0, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(src_0, 0).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -791,7 +791,7 @@ Assume {
   (* Then *)
   Have: i < n.
 }
-Prove: i < to_uint32(1 + i).
+Prove: i < to_uint64(1 + i).
 
 ------------------------------------------------------------
 
@@ -805,7 +805,7 @@ Let a = shift_sint8(dest_0, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
 Let a_2 = shift_sint8(src_0, 0).
 Assume {
-  Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
@@ -833,7 +833,7 @@ Assume {
   (* Then *)
   Have: 0 < i.
 }
-Prove: to_uint32(i - 1) < i.
+Prove: to_uint64(i - 1) < i.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot
index eb1fa949b61..c6648e78e8f 100644
--- a/src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot
+++ b/src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot
@@ -15,12 +15,12 @@ digraph "job" {
   _003 [ label="roots:&fb", style="filled", color="lightblue", shape="box" ];
   { rank=same; A001; _003; }
   _003 -> A001 [ arrowhead="tee" ];
-  _004 [ shape="record", label="<_p1> 128..159: D32|<_p2> 160..191: D32" ];
+  _004 [ shape="record", label="<_p1> 256..319: D64|<_p2> 320..383: D64" ];
   _004:_p2 -> A003 [ style="dotted" ];
   _004:_p1 -> A002 [ style="dotted" ];
   A001 -> _004:w [ arrowhead="tee" ];
   A002 [ label="D", shape="oval" ];
-  _005 [ label="roots:&fb+128", style="filled", color="lightblue",
+  _005 [ label="roots:&fb+256", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A002; _005; }
@@ -29,7 +29,7 @@ digraph "job" {
   _006:_p1 -> A004:w [ taillabel="*", labelangle="+30", color="red" ];
   A002 -> _006:w [ arrowhead="tee" ];
   A003 [ label="D", shape="oval" ];
-  _007 [ label="roots:&fb+160", style="filled", color="lightblue",
+  _007 [ label="roots:&fb+320", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A003; _007; }
@@ -38,7 +38,7 @@ digraph "job" {
   _008:_p1 -> A005:w [ taillabel="*", labelangle="+30", color="red" ];
   A003 -> _008:w [ arrowhead="tee" ];
   A004 [ label="", shape="oval" ];
-  _009 [ label="roots:&fb+128", style="filled", color="lightblue",
+  _009 [ label="roots:&fb+256", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A004; _009; }
@@ -48,7 +48,7 @@ digraph "job" {
   _010:_p1 -> A006 [ style="dotted" ];
   A004 -> _010:w [ arrowhead="tee" ];
   A005 [ label="", shape="oval" ];
-  _011 [ label="roots:&fb+160", style="filled", color="lightblue",
+  _011 [ label="roots:&fb+320", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A005; _011; }
@@ -58,7 +58,7 @@ digraph "job" {
   _012:_p1 -> A008 [ style="dotted" ];
   A005 -> _012:w [ arrowhead="tee" ];
   A006 [ label="RW", shape="oval", fillcolor="green", style="filled" ];
-  _013 [ label="roots:&fb+128", style="filled", color="lightblue",
+  _013 [ label="roots:&fb+256", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A006; _013; }
@@ -66,7 +66,7 @@ digraph "job" {
   _014 [ shape="record", label="Var float64" ];
   A006 -> _014:w [ arrowhead="tee" ];
   A007 [ label="RW", shape="oval", fillcolor="green", style="filled" ];
-  _015 [ label="roots:&fb+192", style="filled", color="lightblue",
+  _015 [ label="roots:&fb+320", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A007; _015; }
@@ -74,7 +74,7 @@ digraph "job" {
   _016 [ shape="record", label="Var sint32" ];
   A007 -> _016:w [ arrowhead="tee" ];
   A008 [ label="R", shape="oval", fillcolor="green", style="filled" ];
-  _017 [ label="roots:&fb+160", style="filled", color="lightblue",
+  _017 [ label="roots:&fb+320", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A008; _017; }
@@ -82,7 +82,7 @@ digraph "job" {
   _018 [ shape="record", label="Var float64" ];
   A008 -> _018:w [ arrowhead="tee" ];
   A009 [ label="R", shape="oval", fillcolor="green", style="filled" ];
-  _019 [ label="roots:&fb+224", style="filled", color="lightblue",
+  _019 [ label="roots:&fb+384", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A009; _019; }
diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot
index 4cbd5b27d23..c278bffd209 100644
--- a/src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot
+++ b/src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot
@@ -45,7 +45,7 @@ digraph "job" {
   { rank=same; A005; _011; }
   _011 -> A005 [ arrowhead="tee" ];
   _012 [ shape="record",
-    label="<_p1> 0..31: D32|<_p2> 32..127: D32[3]|<_p3> 128..223: D32[3]|<_p4> 224..319: D32[3]|<_p5> 320..351: D32"
+    label="<_p1> 0..63: D64|<_p2> 64..255: D64[3]|<_p3> 256..447: D64[3]|<_p4> 448..639: D64[3]|<_p5> 640..703: D64"
   ];
   _012:_p5 -> A010 [ style="dotted" ];
   _012:_p4 -> A008 [ style="dotted" ];
@@ -82,7 +82,7 @@ digraph "job" {
   _020:_p1 -> A014:w [ taillabel="*", labelangle="+30", color="red" ];
   A009 -> _020:w [ arrowhead="tee" ];
   A010 [ label="D", shape="oval" ];
-  _021 [ label="roots:&fb+320", style="filled", color="lightblue",
+  _021 [ label="roots:&fb+640", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A010; _021; }
@@ -122,7 +122,7 @@ digraph "job" {
   _030:_p1 -> A022 [ style="dotted" ];
   A014 -> _030:w [ arrowhead="tee" ];
   A015 [ label="", shape="oval" ];
-  _031 [ label="roots:&fb+320", style="filled", color="lightblue",
+  _031 [ label="roots:&fb+640", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A015; _031; }
@@ -174,7 +174,7 @@ digraph "job" {
   _046 [ shape="record", label="Var float64" ];
   A022 -> _046:w [ arrowhead="tee" ];
   A023 [ label="W", shape="oval", fillcolor="green", style="filled" ];
-  _047 [ label="roots:&fb+320", style="filled", color="lightblue",
+  _047 [ label="roots:&fb+640", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A023; _047; }
@@ -182,7 +182,7 @@ digraph "job" {
   _048 [ shape="record", label="Var float64" ];
   A023 -> _048:w [ arrowhead="tee" ];
   A024 [ label="W", shape="oval", fillcolor="green", style="filled" ];
-  _049 [ label="roots:&fb+384", style="filled", color="lightblue",
+  _049 [ label="roots:&fb+704", style="filled", color="lightblue",
     shape="box"
   ];
   { rank=same; A024; _049; }
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 227396b81fc..81c5c6cc27c 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
@@ -25,7 +25,7 @@ theory Matrix
   
   predicate IsArray_uint32 (t:int -> int) = forall i:int. is_uint32 (get t i)
   
-  predicate IsArray_sint32 (t:int -> int) = forall i:int. is_sint32 (get t i)
+  predicate IsArray_sint64 (t:int -> int) = forall i:int. is_sint64 (get t i)
   
   predicate EqArray_int (n:int) (t:int -> int) (t1:int -> int) =
     forall i:int. 0 <= i -> i < n -> get t1 i = get t i
@@ -54,7 +54,7 @@ theory S1_S
   (* use Matrix *)
   
   predicate IsS1_S (s:S1_S) =
-    (IsArray_sint32 (F1_S_b s) /\ IsArray_uint32 (F1_S_a s)) /\
+    (IsArray_sint64 (F1_S_b s) /\ IsArray_uint32 (F1_S_a s)) /\
     is_sint32 (F1_S_f s)
   
   predicate EqS1_S (s:S1_S) (s1:S1_S) =
@@ -91,16 +91,17 @@ theory Compound
   
   function shiftfield_F1_S_b (p:addr) : addr = shift p 6
   
-  function shift_sint32 (p:addr) (k:int) : addr = shift p k
+  function shift_sint64 (p:addr) (k:int) : addr = shift p k
   
-  function Array_sint32 addr int (addr -> int) : int -> int
+  function Array_sint64 addr int (addr -> int) : int -> int
   
   (* use S1_S *)
   
-  function Load_S1_S (p:addr) (mint:addr -> int) (mint1:addr -> int) : S1_S =
+  function Load_S1_S (p:addr) (mint:addr -> int) (mint1:addr -> int) (mint2:
+    addr -> int) : S1_S =
     S1_S1 (get mint1 (shiftfield_F1_S_f p))
     (Array_uint32 (shiftfield_F1_S_a p) 5 mint)
-    (Array_sint32 (shiftfield_F1_S_b p) 5 mint1)
+    (Array_sint64 (shiftfield_F1_S_b p) 5 mint2)
   
   Q_Array_uint32_access :
     forall mint:addr -> int, i:int, n:int, p:addr
@@ -126,67 +127,98 @@ theory Compound
      separated p 1 q n1 ->
      Array_uint32 p n (havoc mint1 mint q n1) = Array_uint32 p n mint
   
-  Q_Array_sint32_access :
+  Q_Array_sint64_access :
     forall mint:addr -> int, i:int, n:int, p:addr
-     [get (Array_sint32 p n mint) i].
+     [get (Array_sint64 p n mint) i].
      0 <= i ->
-     i < n -> get (Array_sint32 p n mint) i = get mint (shift_sint32 p i)
+     i < n -> get (Array_sint64 p n mint) i = get mint (shift_sint64 p i)
   
-  Q_Array_sint32_update_Mint0 :
+  Q_Array_sint64_update_Mint0 :
     forall mint:addr -> int, n:int, p:addr, q:addr, v:int
-     [Array_sint32 p n (set mint q v)].
-     not q = p -> Array_sint32 p n (set mint q v) = Array_sint32 p n mint
+     [Array_sint64 p n (set mint q v)].
+     not q = p -> Array_sint64 p n (set mint q v) = Array_sint64 p n mint
   
-  Q_Array_sint32_eqmem_Mint0 :
+  Q_Array_sint64_eqmem_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
-     [Array_sint32 p n mint, eqmem mint mint1 q n1| Array_sint32 p n mint1,
+     [Array_sint64 p n mint, eqmem mint mint1 q n1| Array_sint64 p n mint1,
      eqmem mint mint1 q n1].
      included p 1 q n1 ->
-     eqmem mint mint1 q n1 -> Array_sint32 p n mint1 = Array_sint32 p n mint
+     eqmem mint mint1 q n1 -> Array_sint64 p n mint1 = Array_sint64 p n mint
   
-  Q_Array_sint32_havoc_Mint0 :
+  Q_Array_sint64_havoc_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
-     [Array_sint32 p n (havoc mint1 mint q n1)].
+     [Array_sint64 p n (havoc mint1 mint q n1)].
      separated p 1 q n1 ->
-     Array_sint32 p n (havoc mint1 mint q n1) = Array_sint32 p n mint
+     Array_sint64 p n (havoc mint1 mint q n1) = Array_sint64 p n mint
   
   Q_Load_S1_S_update_Mint0 :
-    forall mint:addr -> int, mint1:addr -> int, p:addr, q:addr, v:int
-     [Load_S1_S p (set mint q v) mint1].
+    forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
+     addr, v:int [Load_S1_S p (set mint q v) mint1 mint2].
      separated p 11 q 1 ->
-     Load_S1_S p (set mint q v) mint1 = Load_S1_S p mint mint1
+     Load_S1_S p (set mint q v) mint1 mint2 = Load_S1_S p mint mint1 mint2
   
   Q_Load_S1_S_eqmem_Mint0 :
-    forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
-     addr, q:addr [Load_S1_S p mint mint2, eqmem mint mint1 q n|
-     Load_S1_S p mint1 mint2, eqmem mint mint1 q n].
+    forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
+     -> int, n:int, p:addr, q:addr [Load_S1_S p mint mint2 mint3,
+     eqmem mint mint1 q n| Load_S1_S p mint1 mint2 mint3,
+     eqmem mint mint1 q n].
      included p 11 q n ->
-     eqmem mint mint1 q n -> Load_S1_S p mint1 mint2 = Load_S1_S p mint mint2
+     eqmem mint mint1 q n ->
+     Load_S1_S p mint1 mint2 mint3 = Load_S1_S p mint mint2 mint3
   
   Q_Load_S1_S_havoc_Mint0 :
-    forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
-     addr, q:addr [Load_S1_S p (havoc mint1 mint q n) mint2].
+    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].
      separated p 11 q n ->
-     Load_S1_S p (havoc mint1 mint q n) mint2 = Load_S1_S p mint mint2
+     Load_S1_S p (havoc mint1 mint q n) mint2 mint3
+     = Load_S1_S p mint mint2 mint3
   
   Q_Load_S1_S_update_Mint1 :
-    forall mint:addr -> int, mint1:addr -> int, p:addr, q:addr, v:int
-     [Load_S1_S p mint1 (set mint q v)].
+    forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
+     addr, v:int [Load_S1_S p mint2 (set mint1 q v) mint].
      separated p 11 q 1 ->
-     Load_S1_S p mint1 (set mint q v) = Load_S1_S p mint1 mint
+     Load_S1_S p mint2 (set mint1 q v) mint = Load_S1_S p mint2 mint1 mint
   
   Q_Load_S1_S_eqmem_Mint1 :
-    forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
-     addr, q:addr [Load_S1_S p mint2 mint, eqmem mint mint1 q n|
-     Load_S1_S p mint2 mint1, eqmem mint mint1 q n].
+    forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
+     -> int, n:int, p:addr, q:addr [Load_S1_S p mint3 mint1 mint,
+     eqmem mint1 mint2 q n| Load_S1_S p mint3 mint2 mint,
+     eqmem mint1 mint2 q n].
      included p 11 q n ->
-     eqmem mint mint1 q n -> Load_S1_S p mint2 mint1 = Load_S1_S p mint2 mint
+     eqmem mint1 mint2 q n ->
+     Load_S1_S p mint3 mint2 mint = Load_S1_S p mint3 mint1 mint
   
   Q_Load_S1_S_havoc_Mint1 :
-    forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
-     addr, q:addr [Load_S1_S p mint2 (havoc mint1 mint q n)].
+    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].
      separated p 11 q n ->
-     Load_S1_S p mint2 (havoc mint1 mint q n) = Load_S1_S p mint2 mint
+     Load_S1_S p mint3 (havoc mint2 mint1 q n) mint
+     = Load_S1_S p mint3 mint1 mint
+  
+  Q_Load_S1_S_update_Mint2 :
+    forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
+     addr, v:int [Load_S1_S p mint1 mint (set mint2 q v)].
+     separated p 11 q 1 ->
+     Load_S1_S p mint1 mint (set mint2 q v) = Load_S1_S p mint1 mint mint2
+  
+  Q_Load_S1_S_eqmem_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 mint2,
+     eqmem mint2 mint3 q n| Load_S1_S p mint1 mint mint3,
+     eqmem mint2 mint3 q n].
+     included p 11 q n ->
+     eqmem mint2 mint3 q n ->
+     Load_S1_S p mint1 mint mint3 = Load_S1_S p mint1 mint mint2
+  
+  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)].
+     separated p 11 q n ->
+     Load_S1_S p mint1 mint (havoc mint3 mint2 q n)
+     = Load_S1_S p mint1 mint mint2
 end
 [wp:print-generated] 
   theory WP
@@ -211,9 +243,9 @@ end
     (* use Compound *)
     
     goal wp_goal :
-      forall t:addr -> int, t1:addr -> int, a:addr, i:int.
-       let a1 = Load_S1_S a t t1 in
-       let a2 = Load_S1_S a t (set t1 (shiftfield_F1_S_f a) i) in
+      forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, i:int.
+       let a1 = Load_S1_S a t t2 t1 in
+       let a2 = Load_S1_S a t (set t2 (shiftfield_F1_S_f a) i) t1 in
        region (base a) <= 0 -> IsS1_S a1 -> IsS1_S a2 -> EqS1_S a2 a1
   end
 [wp] 1 goal generated
@@ -222,8 +254,8 @@ end
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_typed/multi_matrix_types.i, line 10) in 'job':
-Let a = Load_S1_S(p, Mint_0, Mint_1).
-Let a_1 = Load_S1_S(p, Mint_0, Mint_1[shiftfield_F1_S_f(p) <- v]).
+Let a = Load_S1_S(p, Mint_0, Mint_1, Mint_2).
+Let a_1 = Load_S1_S(p, Mint_0, Mint_1[shiftfield_F1_S_f(p) <- v], Mint_2).
 Assume {
   Type: IsS1_S(a) /\ IsS1_S(a_1).
   (* Heap *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
index 6bddd899e5d..80bd40ad07f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
@@ -175,7 +175,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Assertion 'ok' (file tests/wp_typed/unit_bitwise.c, line 170):
-Let x = land(1, a). Assume { Type: is_uint32(a) /\ is_uint32(x). }
+Let x = land(1, a). Assume { Type: is_uint64(a) /\ is_uint64(x). }
 Prove: 0 <= x.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle
index f6ac9a650ae..2da8a610645 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle
@@ -7,7 +7,31 @@
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_typed/user_string.i, line 23) in 'strlen':
-Prove: true.
+Let x = ss_0.offset.
+Let x_1 = s.offset.
+Let x_2 = x - x_1.
+Let x_3 = s.base.
+Assume {
+  (* Heap *)
+  Type: (region(x_3) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, i).
+  (* Pre-condition *)
+  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, i_1).
+  (* Invariant 'ZERO' *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> (((i_2 + x_1) < x) ->
+      (Mchar_0[shift_sint8(s, i_2)] != 0))).
+  (* Invariant 'RANGE' *)
+  Have: addr_le(s, ss_0) /\
+      addr_le(ss_0, shift_sint8(s, L_Length(Mchar_0, s))).
+  (* Invariant 'BASE' *)
+  Have: ss_0.base = x_3.
+  (* Else *)
+  Have: Mchar_0[ss_0] = 0.
+  (* Assertion 'END' *)
+  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, x_2).
+}
+Prove: P_Length_of_str_is(Malloc_0, Mchar_0, s, to_sint32(x_2)).
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle
index b0256f00b0c..ed81e6ce070 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle
@@ -7,7 +7,31 @@
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_typed/user_string.i, line 23) in 'strlen':
-Prove: true.
+Let x = ss_0.offset.
+Let x_1 = s.offset.
+Let x_2 = x - x_1.
+Let x_3 = s.base.
+Assume {
+  (* Heap *)
+  Type: (region(x_3) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, i).
+  (* Pre-condition *)
+  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, i_1).
+  (* Invariant 'ZERO' *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> (((i_2 + x_1) < x) ->
+      (Mchar_0[shift_sint8(s, i_2)] != 0))).
+  (* Invariant 'RANGE' *)
+  Have: addr_le(s, ss_0) /\
+      addr_le(ss_0, shift_sint8(s, L_Length(Mchar_0, s))).
+  (* Invariant 'BASE' *)
+  Have: ss_0.base = x_3.
+  (* Else *)
+  Have: Mchar_0[ss_0] = 0.
+  (* Assertion 'END' *)
+  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, x_2).
+}
+Prove: P_Length_of_str_is(Malloc_0, Mchar_0, s, to_sint32(x_2)).
 
 ------------------------------------------------------------
 
-- 
GitLab