From 79464946c36902104a4899d012ef198bd57e5896 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 18 Sep 2024 10:56:38 +0200
Subject: [PATCH] [wp] adds tests for the MemBytes module
---
src/plugins/wp/tests/ptests_config | 4 +-
src/plugins/wp/tests/wp_bytes/assigns_sep.i | 31 +
src/plugins/wp/tests/wp_bytes/floats.i | 15 +
src/plugins/wp/tests/wp_bytes/integers.i | 182 ++
.../wp_bytes/oracle/assigns_sep.res.oracle | 79 +
.../tests/wp_bytes/oracle/floats.res.oracle | 44 +
.../tests/wp_bytes/oracle/integers.res.oracle | 2098 +++++++++++++++++
.../tests/wp_bytes/oracle/pointers.res.oracle | 120 +
.../tests/wp_bytes/oracle/structs.res.oracle | 46 +
.../wp/tests/wp_bytes/oracle/union.res.oracle | 424 ++++
.../oracle_qualif/assigns_sep.res.oracle | 32 +
.../wp_bytes/oracle_qualif/floats.res.oracle | 20 +
.../oracle_qualif/integers.res.oracle | 90 +
.../oracle_qualif/pointers.res.oracle | 33 +
.../wp_bytes/oracle_qualif/structs.res.oracle | 20 +
.../wp_bytes/oracle_qualif/union.res.oracle | 43 +
src/plugins/wp/tests/wp_bytes/pointers.i | 50 +
src/plugins/wp/tests/wp_bytes/structs.i | 22 +
src/plugins/wp/tests/wp_bytes/test_config | 1 +
.../wp/tests/wp_bytes/test_config_qualif | 1 +
src/plugins/wp/tests/wp_bytes/union.i | 76 +
21 files changed, 3429 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_bytes/assigns_sep.i
create mode 100644 src/plugins/wp/tests/wp_bytes/floats.i
create mode 100644 src/plugins/wp/tests/wp_bytes/integers.i
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle/floats.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle/integers.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle/pointers.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle_qualif/assigns_sep.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle_qualif/floats.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle_qualif/pointers.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle_qualif/structs.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/oracle_qualif/union.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bytes/pointers.i
create mode 100644 src/plugins/wp/tests/wp_bytes/structs.i
create mode 100644 src/plugins/wp/tests/wp_bytes/test_config
create mode 100644 src/plugins/wp/tests/wp_bytes/test_config_qualif
create mode 100644 src/plugins/wp/tests/wp_bytes/union.i
diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config
index d71d6024da0..9ea351239b8 100644
--- a/src/plugins/wp/tests/ptests_config
+++ b/src/plugins/wp/tests/ptests_config
@@ -1,8 +1,8 @@
DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare
-DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip
+DEFAULT_SUITES= wp_typed wp_bytes wp_usage wp_gallery wp_manual wp_tip
qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
-qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip
+qualif_SUITES= wp_typed wp_bytes wp_usage wp_gallery wp_manual wp_tip
qualif_SUITES= why3
ce_SUITES= wp_ce
diff --git a/src/plugins/wp/tests/wp_bytes/assigns_sep.i b/src/plugins/wp/tests/wp_bytes/assigns_sep.i
new file mode 100644
index 00000000000..8f2285630ce
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/assigns_sep.i
@@ -0,0 +1,31 @@
+typedef unsigned uint32 ;
+typedef unsigned char uint8 ;
+
+void assignment(uint8 * array){
+ uint32 u32_0a = * (uint32 *) array ;
+ array[7] = 0x00 ;
+ uint32 u32_0b = * (uint32 *) array ;
+
+ //@ check u32_0a == u32_0b ;
+}
+
+//@ assigns array[l] ;
+void assigns(uint8* array, uint8 l);
+
+//@ assigns array[b .. e] ;
+void assigns_r(uint8* array, uint8 b, uint8 e);
+
+//@ assigns { array[i] | integer i ; i == x || i == y } ;
+void assigns_l2(uint8* array, uint8 x, uint8 y);
+
+void assigns_clause(uint8 * array){
+ uint32 u32_0a = * (uint32 *) array ;
+ assigns (array, 7) ;
+ uint32 u32_0b = * (uint32 *) array ;
+ assigns_r (array, 4, 7) ;
+ uint32 u32_0c = * (uint32 *) array ;
+ //@ check u32_0a == u32_0b == u32_0c ;
+ assigns_l2 (array, 4, 6) ;
+ uint32 u32_0d = * (uint32 *) array ;
+ //@ check u32_0c == u32_0d ;
+}
diff --git a/src/plugins/wp/tests/wp_bytes/floats.i b/src/plugins/wp/tests/wp_bytes/floats.i
new file mode 100644
index 00000000000..0ea0cc1c8fb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/floats.i
@@ -0,0 +1,15 @@
+typedef unsigned char uint8 ;
+
+void float_(float f){
+ uint8 buffer[sizeof(float)] ;
+ *((float*) buffer) = f ;
+ float read = *((float*) buffer) ;
+ //@ assert read == f ;
+}
+
+void double_(double d){
+ uint8 buffer[sizeof(double)] ;
+ *((double*) buffer) = d ;
+ double read = *((double*) buffer) ;
+ //@ assert read == d ;
+}
diff --git a/src/plugins/wp/tests/wp_bytes/integers.i b/src/plugins/wp/tests/wp_bytes/integers.i
new file mode 100644
index 00000000000..b67a164c323
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/integers.i
@@ -0,0 +1,182 @@
+/* run.config*
+ STDOPT:+"-wp-model bytes+raw"
+*/
+
+typedef unsigned long long uint64 ;
+typedef unsigned uint32 ;
+typedef unsigned short uint16 ;
+typedef unsigned char uint8 ;
+
+typedef long long int64 ;
+typedef int int32 ;
+typedef short int int16 ;
+typedef signed char int8 ;
+
+void unsigned_(void){
+ uint64 u64 ;
+ uint32 u32 ;
+ uint16 u16 ;
+ uint8 u8 ;
+ unsigned write ;
+
+ u64 = 0x1122334455667788ULL ;
+ u32 = 0x11223344U ;
+ u16 = 0x1122 ;
+ u8 = 0x11 ;
+
+ write = 0 ;
+
+ //@ check \initialized(&u64) ;
+ //@ check \initialized(&u32) ;
+ //@ check \initialized(&u16) ;
+ //@ check \initialized(&u8) ;
+
+ //@ check u64 == 0x1122334455667788ULL ;
+ //@ check u32 == 0x11223344U ;
+ //@ check u16 == 0x1122 ;
+ //@ check u8 == 0x11 ;
+}
+
+void signed_pos(void){
+ int64 p64 ;
+ int32 p32 ;
+ int16 p16 ;
+ int8 p8 ;
+ unsigned write ;
+
+ p64 = 0x0122334455667788LL ;
+ p32 = 0x01223344 ;
+ p16 = 0x0122 ;
+ p8 = 0x01 ;
+
+ write = 0 ;
+
+ //@ check \initialized(&p64) ;
+ //@ check \initialized(&p32) ;
+ //@ check \initialized(&p16) ;
+ //@ check \initialized(&p8) ;
+
+ //@ check 0 < p64 == 0x0122334455667788LL ;
+ //@ check 0 < p32 == 0x01223344 ;
+ //@ check 0 < p16 == 0x0122 ;
+ //@ check 0 < p8 == 0x01 ;
+}
+
+void signed_neg(void){
+ int64 m64 ;
+ int32 m32 ;
+ int16 m16 ;
+ int8 m8 ;
+ unsigned write ;
+
+ m64 = -0x0122334455667788LL ;
+ m32 = -0x01223344 ;
+ m16 = -0x0122 ;
+ m8 = -0x01 ;
+
+ write = 0 ;
+
+ //@ check \initialized(&m64) ;
+ //@ check \initialized(&m32) ;
+ //@ check \initialized(&m16) ;
+ //@ check \initialized(&m8) ;
+
+ //@ check 0 > m64 == -0x0122334455667788LL ;
+ //@ check 0 > m32 == -0x01223344 ;
+ //@ check 0 > m16 == -0x0122 ;
+ //@ check 0 > m8 == -0x01 ;
+}
+
+void cast_unsigned_signed_pos(void){
+ uint64 u64 ;
+ uint16 u16 ;
+ unsigned write ;
+
+ u64 = 0x0122334455667788ULL ;
+ u16 = 0x0122 ;
+
+ //@ check 0 < *((int64*)&u64) == 0x0122334455667788LL ;
+ //@ check 0 < *(((int32*)&u64)+1) == 0x01223344 ;
+ //@ check 0 < *((int16*)&u16) == 0x0122 ;
+ //@ check 0 < *(((int8*) &u16)+1) == 0x01 ;
+}
+
+void cast_unsigned_signed_neg(void){
+ uint64 u64 ;
+ uint16 u16 ;
+ unsigned write ;
+
+ u64 = 0x8122334455667788ULL ;
+ u16 = 0x8182 ;
+
+ //@ check 0 > *((int64*)&u64) == -0x7EDDCCBBAA998878;
+ //@ check 0 > *(((int32*)&u64)+1) == -0x7EDDCCBC;
+ //@ check 0 > *((int16*)&u16) == -0x7E7E;
+ //@ check 0 > *(((int8*)&u16)+1) == -0x7F;
+}
+
+void cast_from_bytes_to_unsigned(void){
+ uint8 array[] = { 0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88 };
+
+ uint64 u64_0 = * (uint64 *) array ;
+
+ uint32 u32_0 = * (uint32 *) array ;
+ uint32 u32_1 = * (((uint32 *) array) + 1) ;
+
+ uint16 u16_0 = * (uint16 *) array ;
+ uint16 u16_1 = * (((uint16 *) array) + 1) ;
+ uint16 u16_2 = * (((uint16 *) array) + 2) ;
+ uint16 u16_3 = * (((uint16 *) array) + 3) ;
+
+ //@ check u64_0 == 0x8877665544332211ULL ;
+ //@ check u32_0 == 0x44332211UL ;
+ //@ check u32_1 == 0x88776655UL ;
+ //@ check u16_0 == 0x2211 ;
+ //@ check u16_1 == 0x4433 ;
+ //@ check u16_2 == 0x6655 ;
+ //@ check u16_3 == 0x8877 ;
+}
+
+void cast_from_bytes_to_signed_pos(void){
+ uint8 array[] = { 0x11, 0x02, 0x33, 0x04, 0x55, 0x06, 0x77, 0x08 };
+
+ int64 i64_0 = * (int64 *) array ;
+
+ int32 i32_0 = * (int32 *) array ;
+ int32 i32_1 = * (((int32 *) array) + 1) ;
+
+ int16 i16_0 = * (int16 *) array ;
+ int16 i16_1 = * (((int16 *) array) + 1) ;
+ int16 i16_2 = * (((int16 *) array) + 2) ;
+ int16 i16_3 = * (((int16 *) array) + 3) ;
+
+ //@ check i64_0 > 0 && i64_0 == 0x0877065504330211LL ;
+ //@ check i32_0 > 0 && i32_0 == 0x04330211L ;
+ //@ check i32_1 > 0 && i32_1 == 0x08770655L ;
+ //@ check i16_0 > 0 && i16_0 == 0x0211 ;
+ //@ check i16_1 > 0 && i16_1 == 0x0433 ;
+ //@ check i16_2 > 0 && i16_2 == 0x0655 ;
+ //@ check i16_3 > 0 && i16_3 == 0x0877 ;
+}
+
+void cast_from_bytes_to_signed_neg(void){
+ uint8 array[] = { 0x11, 0x82, 0x33, 0x84, 0x55, 0x86, 0x77, 0x88 };
+
+ int64 i64_0 = * (int64 *) array ;
+
+ int32 i32_0 = * (int32 *) array ;
+ int32 i32_1 = * (((int32 *) array) + 1) ;
+
+ int16 i16_0 = * (int16 *) array ;
+ int16 i16_1 = * (((int16 *) array) + 1) ;
+ int16 i16_2 = * (((int16 *) array) + 2) ;
+ int16 i16_3 = * (((int16 *) array) + 3) ;
+
+ //@ check i64_0 < 0 && i64_0 == -0x778879AA7BCC7DEFLL ;
+ //@ check i32_0 < 0 && i32_0 == -0x7BCC7DEFL ;
+ //@ check i32_1 < 0 && i32_1 == -0x778879ABL ;
+ //@ check i16_0 < 0 && i16_0 == -0x7DEF ;
+ //@ check i16_1 < 0 && i16_1 == -0x7BCD ;
+ //@ check i16_2 < 0 && i16_2 == -0x79AB ;
+ //@ check i16_3 < 0 && i16_3 == -0x7789 ;
+}
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
new file mode 100644
index 00000000000..db98c5be956
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle
@@ -0,0 +1,79 @@
+# frama-c -wp -wp-model 'Bytes' [...]
+[kernel] Parsing assigns_sep.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] assigns_sep.i:13: Warning:
+ Neither code nor explicit exits and terminates for function assigns,
+ generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] assigns_sep.i:16: Warning:
+ Neither code nor explicit exits and terminates for function assigns_r,
+ generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] assigns_sep.i:19: Warning:
+ Neither code nor explicit exits and terminates for function assigns_l2,
+ generating default clauses. See -generated-spec-* options for more info
+[wp] [Valid] Goal assignment_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal assignment_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function assignment
+------------------------------------------------------------
+
+Goal Check (file assigns_sep.i, line 9):
+Let x = read_uint32(mem_0, array_0).
+Let x_1 = read_uint32(write_uint8(mem_0, shift_uint8(array_0, 7), 0),
+ array_0).
+Assume {
+ Type: is_uint32(x) /\ is_uint32(x_1).
+ (* Heap *)
+ Type: (region(array_0.base) <= 0) /\ sconst(mem_0).
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function assigns_clause
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'assigns_clause':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Exit-condition (generated) in 'assigns_clause':
+Prove: true.
+
+------------------------------------------------------------
+
+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).
+Assume {
+ Type: is_uint32(x) /\ is_uint32(x_1) /\ is_uint32(x_2).
+ (* Heap *)
+ Type: (region(array_0.base) <= 0) /\ sconst(mem_0).
+}
+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 x = read_uint32(mem_1, array_0).
+Let x_1 = read_uint32(a, 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) /\ sconst(mem_0).
+ (* Call Effects *)
+ Have: forall a_1 : 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))).
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/floats.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/floats.res.oracle
new file mode 100644
index 00000000000..af3805ad36e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle/floats.res.oracle
@@ -0,0 +1,44 @@
+# frama-c -wp -wp-model 'Bytes' [...]
+[kernel] Parsing floats.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal double_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal double_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal float_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal float_terminates (Cfg) (Trivial)
+------------------------------------------------------------
+ Function double_
+------------------------------------------------------------
+
+Goal Assertion (file floats.i, line 14):
+Let a = shift_uint8(global(L_buffer_30), 0).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_buffer_30 <- 8]).
+}
+Prove: of_f64(int_to_float64(read_uint64(write_uint64(mem_0, a,
+ float64_to_int(d)), a)))
+ = of_f64(d).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function float_
+------------------------------------------------------------
+
+Goal Assertion (file floats.i, line 7):
+Let a = shift_uint8(global(L_buffer_23), 0).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_buffer_23 <- 4]).
+}
+Prove: of_f32(int_to_float32(read_uint32(write_uint32(mem_0, a,
+ float32_to_int(f)), a)))
+ = of_f32(f).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/integers.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/integers.res.oracle
new file mode 100644
index 00000000000..99ddd415285
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle/integers.res.oracle
@@ -0,0 +1,2098 @@
+# frama-c -wp -wp-model 'Bytes (Raw)' [...]
+[kernel] Parsing integers.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal cast_from_bytes_to_signed_neg_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_from_bytes_to_signed_neg_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal cast_from_bytes_to_signed_pos_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_from_bytes_to_signed_pos_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal cast_from_bytes_to_unsigned_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_from_bytes_to_unsigned_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal cast_unsigned_signed_neg_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_unsigned_signed_neg_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal cast_unsigned_signed_pos_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_unsigned_signed_pos_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal signed_neg_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal signed_neg_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal signed_pos_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal signed_pos_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal unsigned_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal unsigned_terminates (Cfg) (Trivial)
+------------------------------------------------------------
+ Function cast_from_bytes_to_signed_neg
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 175):
+Let a = global(L_array_75).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_82)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_81)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_80)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_79)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_78)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_77)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_76)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_75 <- 8][L_i64_0_76 <- 8][L_i32_0_77 <- 4]
+ [L_i32_1_78 <- 4][L_i16_0_79 <- 2][L_i16_1_80 <- 2]
+ [L_i16_2_81 <- 2][L_i16_3_82 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 130.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 132.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 134.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_13 = (-8613268060474473967)) /\ (x_13 < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 176):
+Let a = global(L_array_75).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_82)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_81)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_80)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_79)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_78)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_77)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_76)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_75 <- 8][L_i64_0_76 <- 8][L_i32_0_77 <- 4]
+ [L_i32_1_78 <- 4][L_i16_0_79 <- 2][L_i16_1_80 <- 2]
+ [L_i16_2_81 <- 2][L_i16_3_82 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 130.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 132.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 134.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_11 = (-2076999151)) /\ (x_11 < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 177):
+Let a = global(L_array_75).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_82)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_81)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_80)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_79)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_78)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_77)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_76)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_75 <- 8][L_i64_0_76 <- 8][L_i32_0_77 <- 4]
+ [L_i32_1_78 <- 4][L_i16_0_79 <- 2][L_i16_1_80 <- 2]
+ [L_i16_2_81 <- 2][L_i16_3_82 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 130.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 132.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 134.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_9 = (-2005432747)) /\ (x_9 < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 178):
+Let a = global(L_array_75).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_82)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_81)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_80)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_79)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_78)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_77)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_76)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_75 <- 8][L_i64_0_76 <- 8][L_i32_0_77 <- 4]
+ [L_i32_1_78 <- 4][L_i16_0_79 <- 2][L_i16_1_80 <- 2]
+ [L_i16_2_81 <- 2][L_i16_3_82 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 130.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 132.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 134.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_7 = (-32239)) /\ (x_7 < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 179):
+Let a = global(L_array_75).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_82)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_81)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_80)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_79)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_78)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_77)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_76)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_75 <- 8][L_i64_0_76 <- 8][L_i32_0_77 <- 4]
+ [L_i32_1_78 <- 4][L_i16_0_79 <- 2][L_i16_1_80 <- 2]
+ [L_i16_2_81 <- 2][L_i16_3_82 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 130.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 132.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 134.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_5 = (-31693)) /\ (x_5 < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 180):
+Let a = global(L_array_75).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_82)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_81)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_80)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_79)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_78)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_77)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_76)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_75 <- 8][L_i64_0_76 <- 8][L_i32_0_77 <- 4]
+ [L_i32_1_78 <- 4][L_i16_0_79 <- 2][L_i16_1_80 <- 2]
+ [L_i16_2_81 <- 2][L_i16_3_82 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 130.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 132.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 134.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_3 = (-31147)) /\ (x_3 < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 181):
+Let a = global(L_array_75).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_82)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_81)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_80)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_79)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_78)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_77)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_76)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_75 <- 8][L_i64_0_76 <- 8][L_i32_0_77 <- 4]
+ [L_i32_1_78 <- 4][L_i16_0_79 <- 2][L_i16_1_80 <- 2]
+ [L_i16_2_81 <- 2][L_i16_3_82 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 130.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 132.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 134.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_1 = (-30601)) /\ (x_1 < 0).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function cast_from_bytes_to_signed_pos
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 153):
+Let a = global(L_array_65).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_72)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_71)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_70)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_69)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_68)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_67)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_66)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_65 <- 8][L_i64_0_66 <- 8][L_i32_0_67 <- 4]
+ [L_i32_1_68 <- 4][L_i16_0_69 <- 2][L_i16_1_70 <- 2]
+ [L_i16_2_71 <- 2][L_i16_3_72 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 2.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 4.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 6.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 8.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_13 = 609963236744430097) /\ (0 < x_13).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 154):
+Let a = global(L_array_65).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_72)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_71)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_70)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_69)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_68)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_67)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_66)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_65 <- 8][L_i64_0_66 <- 8][L_i32_0_67 <- 4]
+ [L_i32_1_68 <- 4][L_i16_0_69 <- 2][L_i16_1_70 <- 2]
+ [L_i16_2_71 <- 2][L_i16_3_72 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 2.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 4.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 6.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 8.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_11 = 70451729) /\ (0 < x_11).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 155):
+Let a = global(L_array_65).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_72)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_71)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_70)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_69)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_68)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_67)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_66)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_65 <- 8][L_i64_0_66 <- 8][L_i32_0_67 <- 4]
+ [L_i32_1_68 <- 4][L_i16_0_69 <- 2][L_i16_1_70 <- 2]
+ [L_i16_2_71 <- 2][L_i16_3_72 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 2.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 4.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 6.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 8.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_9 = 142018133) /\ (0 < x_9).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 156):
+Let a = global(L_array_65).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_72)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_71)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_70)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_69)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_68)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_67)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_66)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_65 <- 8][L_i64_0_66 <- 8][L_i32_0_67 <- 4]
+ [L_i32_1_68 <- 4][L_i16_0_69 <- 2][L_i16_1_70 <- 2]
+ [L_i16_2_71 <- 2][L_i16_3_72 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 2.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 4.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 6.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 8.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_7 = 529) /\ (0 < x_7).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 157):
+Let a = global(L_array_65).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_72)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_71)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_70)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_69)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_68)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_67)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_66)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_65 <- 8][L_i64_0_66 <- 8][L_i32_0_67 <- 4]
+ [L_i32_1_68 <- 4][L_i16_0_69 <- 2][L_i16_1_70 <- 2]
+ [L_i16_2_71 <- 2][L_i16_3_72 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 2.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 4.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 6.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 8.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_5 = 1075) /\ (0 < x_5).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 158):
+Let a = global(L_array_65).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_72)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_71)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_70)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_69)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_68)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_67)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_66)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_65 <- 8][L_i64_0_66 <- 8][L_i32_0_67 <- 4]
+ [L_i32_1_68 <- 4][L_i16_0_69 <- 2][L_i16_1_70 <- 2]
+ [L_i16_2_71 <- 2][L_i16_3_72 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 2.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 4.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 6.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 8.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_3 = 1621) /\ (0 < x_3).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 159):
+Let a = global(L_array_65).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_sint16(mem_0, shift_sint16(a_1, 3)).
+Let x_1 = read_sint16(mem_0, global(L_i16_3_72)).
+Let x_2 = read_sint16(mem_0, shift_sint16(a_1, 2)).
+Let x_3 = read_sint16(mem_0, global(L_i16_2_71)).
+Let x_4 = read_sint16(mem_0, shift_sint16(a_1, 1)).
+Let x_5 = read_sint16(mem_0, global(L_i16_1_70)).
+Let x_6 = read_sint16(mem_0, a_1).
+Let x_7 = read_sint16(mem_0, global(L_i16_0_69)).
+Let x_8 = read_sint32(mem_0, shift_sint32(a_1, 1)).
+Let x_9 = read_sint32(mem_0, global(L_i32_1_68)).
+Let x_10 = read_sint32(mem_0, a_1).
+Let x_11 = read_sint32(mem_0, global(L_i32_0_67)).
+Let x_12 = read_sint64(mem_0, a_1).
+Let x_13 = read_sint64(mem_0, global(L_i64_0_66)).
+Assume {
+ Type: is_sint16(x_7) /\ is_sint16(x_5) /\ is_sint16(x_3) /\
+ is_sint16(x_1) /\ is_sint32(x_11) /\ is_sint32(x_9) /\
+ is_sint64(x_13) /\ is_sint16(x_6) /\ is_sint32(x_10) /\
+ is_sint64(x_12) /\ is_sint16(x_4) /\ is_sint16(x_2) /\ is_sint16(x) /\
+ is_sint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_65 <- 8][L_i64_0_66 <- 8][L_i32_0_67 <- 4]
+ [L_i32_1_68 <- 4][L_i16_0_69 <- 2][L_i16_1_70 <- 2]
+ [L_i16_2_71 <- 2][L_i16_3_72 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 2.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 4.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 6.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 8.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: (x_1 = 2167) /\ (0 < x_1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function cast_from_bytes_to_unsigned
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 131):
+Let a = global(L_array_55).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_uint16(mem_0, shift_uint16(a_1, 3)).
+Let x_1 = read_uint16(mem_0, global(L_u16_3_62)).
+Let x_2 = read_uint16(mem_0, shift_uint16(a_1, 2)).
+Let x_3 = read_uint16(mem_0, global(L_u16_2_61)).
+Let x_4 = read_uint16(mem_0, shift_uint16(a_1, 1)).
+Let x_5 = read_uint16(mem_0, global(L_u16_1_60)).
+Let x_6 = read_uint16(mem_0, a_1).
+Let x_7 = read_uint16(mem_0, global(L_u16_0_59)).
+Let x_8 = read_uint32(mem_0, shift_uint32(a_1, 1)).
+Let x_9 = read_uint32(mem_0, global(L_u32_1_58)).
+Let x_10 = read_uint32(mem_0, a_1).
+Let x_11 = read_uint32(mem_0, global(L_u32_0_57)).
+Let x_12 = read_uint64(mem_0, a_1).
+Let x_13 = read_uint64(mem_0, global(L_u64_0_56)).
+Assume {
+ Type: is_uint16(x_7) /\ is_uint16(x_5) /\ is_uint16(x_3) /\
+ is_uint16(x_1) /\ is_uint32(x_11) /\ is_uint32(x_9) /\
+ is_uint64(x_13) /\ is_uint16(x_6) /\ is_uint32(x_10) /\
+ is_uint64(x_12) /\ is_uint16(x_4) /\ is_uint16(x_2) /\ is_uint16(x) /\
+ is_uint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_55 <- 8][L_u64_0_56 <- 8][L_u32_0_57 <- 4]
+ [L_u32_1_58 <- 4][L_u16_0_59 <- 2][L_u16_1_60 <- 2]
+ [L_u16_2_61 <- 2][L_u16_3_62 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 34.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 68.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 102.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: x_13 = 9833440827789222417.
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 132):
+Let a = global(L_array_55).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_uint16(mem_0, shift_uint16(a_1, 3)).
+Let x_1 = read_uint16(mem_0, global(L_u16_3_62)).
+Let x_2 = read_uint16(mem_0, shift_uint16(a_1, 2)).
+Let x_3 = read_uint16(mem_0, global(L_u16_2_61)).
+Let x_4 = read_uint16(mem_0, shift_uint16(a_1, 1)).
+Let x_5 = read_uint16(mem_0, global(L_u16_1_60)).
+Let x_6 = read_uint16(mem_0, a_1).
+Let x_7 = read_uint16(mem_0, global(L_u16_0_59)).
+Let x_8 = read_uint32(mem_0, shift_uint32(a_1, 1)).
+Let x_9 = read_uint32(mem_0, global(L_u32_1_58)).
+Let x_10 = read_uint32(mem_0, a_1).
+Let x_11 = read_uint32(mem_0, global(L_u32_0_57)).
+Let x_12 = read_uint64(mem_0, a_1).
+Let x_13 = read_uint64(mem_0, global(L_u64_0_56)).
+Assume {
+ Type: is_uint16(x_7) /\ is_uint16(x_5) /\ is_uint16(x_3) /\
+ is_uint16(x_1) /\ is_uint32(x_11) /\ is_uint32(x_9) /\
+ is_uint64(x_13) /\ is_uint16(x_6) /\ is_uint32(x_10) /\
+ is_uint64(x_12) /\ is_uint16(x_4) /\ is_uint16(x_2) /\ is_uint16(x) /\
+ is_uint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_55 <- 8][L_u64_0_56 <- 8][L_u32_0_57 <- 4]
+ [L_u32_1_58 <- 4][L_u16_0_59 <- 2][L_u16_1_60 <- 2]
+ [L_u16_2_61 <- 2][L_u16_3_62 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 34.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 68.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 102.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: x_11 = 1144201745.
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 133):
+Let a = global(L_array_55).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_uint16(mem_0, shift_uint16(a_1, 3)).
+Let x_1 = read_uint16(mem_0, global(L_u16_3_62)).
+Let x_2 = read_uint16(mem_0, shift_uint16(a_1, 2)).
+Let x_3 = read_uint16(mem_0, global(L_u16_2_61)).
+Let x_4 = read_uint16(mem_0, shift_uint16(a_1, 1)).
+Let x_5 = read_uint16(mem_0, global(L_u16_1_60)).
+Let x_6 = read_uint16(mem_0, a_1).
+Let x_7 = read_uint16(mem_0, global(L_u16_0_59)).
+Let x_8 = read_uint32(mem_0, shift_uint32(a_1, 1)).
+Let x_9 = read_uint32(mem_0, global(L_u32_1_58)).
+Let x_10 = read_uint32(mem_0, a_1).
+Let x_11 = read_uint32(mem_0, global(L_u32_0_57)).
+Let x_12 = read_uint64(mem_0, a_1).
+Let x_13 = read_uint64(mem_0, global(L_u64_0_56)).
+Assume {
+ Type: is_uint16(x_7) /\ is_uint16(x_5) /\ is_uint16(x_3) /\
+ is_uint16(x_1) /\ is_uint32(x_11) /\ is_uint32(x_9) /\
+ is_uint64(x_13) /\ is_uint16(x_6) /\ is_uint32(x_10) /\
+ is_uint64(x_12) /\ is_uint16(x_4) /\ is_uint16(x_2) /\ is_uint16(x) /\
+ is_uint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_55 <- 8][L_u64_0_56 <- 8][L_u32_0_57 <- 4]
+ [L_u32_1_58 <- 4][L_u16_0_59 <- 2][L_u16_1_60 <- 2]
+ [L_u16_2_61 <- 2][L_u16_3_62 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 34.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 68.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 102.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: x_9 = 2289526357.
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 134):
+Let a = global(L_array_55).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_uint16(mem_0, shift_uint16(a_1, 3)).
+Let x_1 = read_uint16(mem_0, global(L_u16_3_62)).
+Let x_2 = read_uint16(mem_0, shift_uint16(a_1, 2)).
+Let x_3 = read_uint16(mem_0, global(L_u16_2_61)).
+Let x_4 = read_uint16(mem_0, shift_uint16(a_1, 1)).
+Let x_5 = read_uint16(mem_0, global(L_u16_1_60)).
+Let x_6 = read_uint16(mem_0, a_1).
+Let x_7 = read_uint16(mem_0, global(L_u16_0_59)).
+Let x_8 = read_uint32(mem_0, shift_uint32(a_1, 1)).
+Let x_9 = read_uint32(mem_0, global(L_u32_1_58)).
+Let x_10 = read_uint32(mem_0, a_1).
+Let x_11 = read_uint32(mem_0, global(L_u32_0_57)).
+Let x_12 = read_uint64(mem_0, a_1).
+Let x_13 = read_uint64(mem_0, global(L_u64_0_56)).
+Assume {
+ Type: is_uint16(x_7) /\ is_uint16(x_5) /\ is_uint16(x_3) /\
+ is_uint16(x_1) /\ is_uint32(x_11) /\ is_uint32(x_9) /\
+ is_uint64(x_13) /\ is_uint16(x_6) /\ is_uint32(x_10) /\
+ is_uint64(x_12) /\ is_uint16(x_4) /\ is_uint16(x_2) /\ is_uint16(x) /\
+ is_uint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_55 <- 8][L_u64_0_56 <- 8][L_u32_0_57 <- 4]
+ [L_u32_1_58 <- 4][L_u16_0_59 <- 2][L_u16_1_60 <- 2]
+ [L_u16_2_61 <- 2][L_u16_3_62 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 34.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 68.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 102.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: x_7 = 8721.
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 135):
+Let a = global(L_array_55).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_uint16(mem_0, shift_uint16(a_1, 3)).
+Let x_1 = read_uint16(mem_0, global(L_u16_3_62)).
+Let x_2 = read_uint16(mem_0, shift_uint16(a_1, 2)).
+Let x_3 = read_uint16(mem_0, global(L_u16_2_61)).
+Let x_4 = read_uint16(mem_0, shift_uint16(a_1, 1)).
+Let x_5 = read_uint16(mem_0, global(L_u16_1_60)).
+Let x_6 = read_uint16(mem_0, a_1).
+Let x_7 = read_uint16(mem_0, global(L_u16_0_59)).
+Let x_8 = read_uint32(mem_0, shift_uint32(a_1, 1)).
+Let x_9 = read_uint32(mem_0, global(L_u32_1_58)).
+Let x_10 = read_uint32(mem_0, a_1).
+Let x_11 = read_uint32(mem_0, global(L_u32_0_57)).
+Let x_12 = read_uint64(mem_0, a_1).
+Let x_13 = read_uint64(mem_0, global(L_u64_0_56)).
+Assume {
+ Type: is_uint16(x_7) /\ is_uint16(x_5) /\ is_uint16(x_3) /\
+ is_uint16(x_1) /\ is_uint32(x_11) /\ is_uint32(x_9) /\
+ is_uint64(x_13) /\ is_uint16(x_6) /\ is_uint32(x_10) /\
+ is_uint64(x_12) /\ is_uint16(x_4) /\ is_uint16(x_2) /\ is_uint16(x) /\
+ is_uint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_55 <- 8][L_u64_0_56 <- 8][L_u32_0_57 <- 4]
+ [L_u32_1_58 <- 4][L_u16_0_59 <- 2][L_u16_1_60 <- 2]
+ [L_u16_2_61 <- 2][L_u16_3_62 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 34.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 68.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 102.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: x_5 = 17459.
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 136):
+Let a = global(L_array_55).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_uint16(mem_0, shift_uint16(a_1, 3)).
+Let x_1 = read_uint16(mem_0, global(L_u16_3_62)).
+Let x_2 = read_uint16(mem_0, shift_uint16(a_1, 2)).
+Let x_3 = read_uint16(mem_0, global(L_u16_2_61)).
+Let x_4 = read_uint16(mem_0, shift_uint16(a_1, 1)).
+Let x_5 = read_uint16(mem_0, global(L_u16_1_60)).
+Let x_6 = read_uint16(mem_0, a_1).
+Let x_7 = read_uint16(mem_0, global(L_u16_0_59)).
+Let x_8 = read_uint32(mem_0, shift_uint32(a_1, 1)).
+Let x_9 = read_uint32(mem_0, global(L_u32_1_58)).
+Let x_10 = read_uint32(mem_0, a_1).
+Let x_11 = read_uint32(mem_0, global(L_u32_0_57)).
+Let x_12 = read_uint64(mem_0, a_1).
+Let x_13 = read_uint64(mem_0, global(L_u64_0_56)).
+Assume {
+ Type: is_uint16(x_7) /\ is_uint16(x_5) /\ is_uint16(x_3) /\
+ is_uint16(x_1) /\ is_uint32(x_11) /\ is_uint32(x_9) /\
+ is_uint64(x_13) /\ is_uint16(x_6) /\ is_uint32(x_10) /\
+ is_uint64(x_12) /\ is_uint16(x_4) /\ is_uint16(x_2) /\ is_uint16(x) /\
+ is_uint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_55 <- 8][L_u64_0_56 <- 8][L_u32_0_57 <- 4]
+ [L_u32_1_58 <- 4][L_u16_0_59 <- 2][L_u16_1_60 <- 2]
+ [L_u16_2_61 <- 2][L_u16_3_62 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 34.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 68.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 102.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: x_3 = 26197.
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 137):
+Let a = global(L_array_55).
+Let a_1 = shift_uint8(a, 0).
+Let x = read_uint16(mem_0, shift_uint16(a_1, 3)).
+Let x_1 = read_uint16(mem_0, global(L_u16_3_62)).
+Let x_2 = read_uint16(mem_0, shift_uint16(a_1, 2)).
+Let x_3 = read_uint16(mem_0, global(L_u16_2_61)).
+Let x_4 = read_uint16(mem_0, shift_uint16(a_1, 1)).
+Let x_5 = read_uint16(mem_0, global(L_u16_1_60)).
+Let x_6 = read_uint16(mem_0, a_1).
+Let x_7 = read_uint16(mem_0, global(L_u16_0_59)).
+Let x_8 = read_uint32(mem_0, shift_uint32(a_1, 1)).
+Let x_9 = read_uint32(mem_0, global(L_u32_1_58)).
+Let x_10 = read_uint32(mem_0, a_1).
+Let x_11 = read_uint32(mem_0, global(L_u32_0_57)).
+Let x_12 = read_uint64(mem_0, a_1).
+Let x_13 = read_uint64(mem_0, global(L_u64_0_56)).
+Assume {
+ Type: is_uint16(x_7) /\ is_uint16(x_5) /\ is_uint16(x_3) /\
+ is_uint16(x_1) /\ is_uint32(x_11) /\ is_uint32(x_9) /\
+ is_uint64(x_13) /\ is_uint16(x_6) /\ is_uint32(x_10) /\
+ is_uint64(x_12) /\ is_uint16(x_4) /\ is_uint16(x_2) /\ is_uint16(x) /\
+ is_uint32(x_8).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_array_55 <- 8][L_u64_0_56 <- 8][L_u32_0_57 <- 4]
+ [L_u32_1_58 <- 4][L_u16_0_59 <- 2][L_u16_1_60 <- 2]
+ [L_u16_2_61 <- 2][L_u16_3_62 <- 2]).
+ (* Initializer *)
+ Init: read_uint8(mem_0, a_1) = 17.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 1)) = 34.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 2)) = 51.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 3)) = 68.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 4)) = 85.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 5)) = 102.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 6)) = 119.
+ (* Initializer *)
+ Init: read_uint8(mem_0, shift_uint8(a, 7)) = 136.
+ (* Initializer *)
+ Init: x_12 = x_13.
+ (* Initializer *)
+ Init: x_10 = x_11.
+ (* Initializer *)
+ Init: x_8 = x_9.
+ (* Initializer *)
+ Init: x_6 = x_7.
+ (* Initializer *)
+ Init: x_4 = x_5.
+ (* Initializer *)
+ Init: x_2 = x_3.
+ (* Initializer *)
+ Init: x = x_1.
+}
+Prove: x_1 = 34935.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function cast_unsigned_signed_neg
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 112):
+Let a = global(L_u64_50).
+Let a_1 = global(L_u16_51).
+Let m = write_uint16(write_uint64(mem_0, a, 9305056148684437384), a_1, 33154).
+Let x = read_sint64(m, a).
+Assume {
+ Type: is_sint8(read_sint8(m, shift_sint8(a_1, 1))) /\
+ is_sint16(read_sint16(m, a_1)) /\
+ is_sint32(read_sint32(m, shift_sint32(a, 1))) /\ is_sint64(x).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_50 <- 8][L_u16_51 <- 2][L_write_52 <- 4]).
+}
+Prove: (x = (-9141687925025114232)) /\ (x < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 113):
+Let a = global(L_u64_50).
+Let a_1 = global(L_u16_51).
+Let m = write_uint16(write_uint64(mem_0, a, 9305056148684437384), a_1, 33154).
+Let x = read_sint32(m, shift_sint32(a, 1)).
+Assume {
+ Type: is_sint8(read_sint8(m, shift_sint8(a_1, 1))) /\
+ is_sint16(read_sint16(m, a_1)) /\ is_sint32(x) /\
+ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_50 <- 8][L_u16_51 <- 2][L_write_52 <- 4]).
+}
+Prove: (x = (-2128465084)) /\ (x < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 114):
+Let a = global(L_u64_50).
+Let a_1 = global(L_u16_51).
+Let m = write_uint16(write_uint64(mem_0, a, 9305056148684437384), a_1, 33154).
+Let x = read_sint16(m, a_1).
+Assume {
+ Type: is_sint8(read_sint8(m, shift_sint8(a_1, 1))) /\ is_sint16(x) /\
+ is_sint32(read_sint32(m, shift_sint32(a, 1))) /\
+ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_50 <- 8][L_u16_51 <- 2][L_write_52 <- 4]).
+}
+Prove: (x = (-32382)) /\ (x < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 115):
+Let a = global(L_u64_50).
+Let a_1 = global(L_u16_51).
+Let m = write_uint16(write_uint64(mem_0, a, 9305056148684437384), a_1, 33154).
+Let x = read_sint8(m, shift_sint8(a_1, 1)).
+Assume {
+ Type: is_sint8(x) /\ is_sint16(read_sint16(m, a_1)) /\
+ is_sint32(read_sint32(m, shift_sint32(a, 1))) /\
+ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_50 <- 8][L_u16_51 <- 2][L_write_52 <- 4]).
+}
+Prove: (x = (-127)) /\ (x < 0).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function cast_unsigned_signed_pos
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 98):
+Let a = global(L_u64_45).
+Let a_1 = global(L_u16_46).
+Let m = write_uint16(write_uint64(mem_0, a, 81684111829661576), a_1, 290).
+Let x = read_sint64(m, a).
+Assume {
+ Type: is_sint8(read_sint8(m, shift_sint8(a_1, 1))) /\
+ is_sint16(read_sint16(m, a_1)) /\
+ is_sint32(read_sint32(m, shift_sint32(a, 1))) /\ is_sint64(x).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_45 <- 8][L_u16_46 <- 2][L_write_47 <- 4]).
+}
+Prove: (x = 81684111829661576) /\ (0 < x).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 99):
+Let a = global(L_u64_45).
+Let a_1 = global(L_u16_46).
+Let m = write_uint16(write_uint64(mem_0, a, 81684111829661576), a_1, 290).
+Let x = read_sint32(m, shift_sint32(a, 1)).
+Assume {
+ Type: is_sint8(read_sint8(m, shift_sint8(a_1, 1))) /\
+ is_sint16(read_sint16(m, a_1)) /\ is_sint32(x) /\
+ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_45 <- 8][L_u16_46 <- 2][L_write_47 <- 4]).
+}
+Prove: (x = 19018564) /\ (0 < x).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 100):
+Let a = global(L_u64_45).
+Let a_1 = global(L_u16_46).
+Let m = write_uint16(write_uint64(mem_0, a, 81684111829661576), a_1, 290).
+Let x = read_sint16(m, a_1).
+Assume {
+ Type: is_sint8(read_sint8(m, shift_sint8(a_1, 1))) /\ is_sint16(x) /\
+ is_sint32(read_sint32(m, shift_sint32(a, 1))) /\
+ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_45 <- 8][L_u16_46 <- 2][L_write_47 <- 4]).
+}
+Prove: (x = 290) /\ (0 < x).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 101):
+Let a = global(L_u64_45).
+Let a_1 = global(L_u16_46).
+Let m = write_uint16(write_uint64(mem_0, a, 81684111829661576), a_1, 290).
+Let x = read_sint8(m, shift_sint8(a_1, 1)).
+Assume {
+ Type: is_sint8(x) /\ is_sint16(read_sint16(m, a_1)) /\
+ is_sint32(read_sint32(m, shift_sint32(a, 1))) /\
+ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_45 <- 8][L_u16_46 <- 2][L_write_47 <- 4]).
+}
+Prove: (x = 1) /\ (0 < x).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function signed_neg
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 79):
+Let a = global(L_m64_38).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_m64_38 <- 8][L_m32_39 <- 4][L_m16_40 <- 2]
+ [L_m8_41 <- 1][L_write_42 <- 4]).
+}
+Prove: (read_init64(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ a, true),
+ global(L_m32_39),
+ true),
+ global(L_m16_40), true),
+ global(L_m8_41), true),
+ global(L_write_42), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 80):
+Let a = global(L_m32_39).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_m64_38 <- 8][L_m32_39 <- 4][L_m16_40 <- 2]
+ [L_m8_41 <- 1][L_write_42 <- 4]).
+}
+Prove: (read_init32(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ global(L_m64_38),
+ true), a, true),
+ global(L_m16_40), true),
+ global(L_m8_41), true),
+ global(L_write_42), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 81):
+Let a = global(L_m16_40).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_m64_38 <- 8][L_m32_39 <- 4][L_m16_40 <- 2]
+ [L_m8_41 <- 1][L_write_42 <- 4]).
+}
+Prove: (read_init16(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ global(L_m64_38),
+ true),
+ global(L_m32_39),
+ true), a, true),
+ global(L_m8_41), true),
+ global(L_write_42), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 82):
+Let a = global(L_m8_41).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_m64_38 <- 8][L_m32_39 <- 4][L_m16_40 <- 2]
+ [L_m8_41 <- 1][L_write_42 <- 4]).
+}
+Prove: (read_init8(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ global(L_m64_38),
+ true),
+ global(L_m32_39),
+ true),
+ global(L_m16_40), true), a,
+ true), global(L_write_42), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 84):
+Let a = global(L_m64_38).
+Let a_1 = global(L_m32_39).
+Let a_2 = global(L_m16_40).
+Let a_3 = global(L_m8_41).
+Let m = write_uint32(write_sint8(write_sint16(write_sint32(write_sint64(mem_0,
+ a,
+ -81684111829661576),
+ a_1, -19018564), a_2, -290),
+ a_3, -1), global(L_write_42), 0).
+Let x = read_sint64(m, a).
+Assume {
+ Type: is_sint8(read_sint8(m, a_3)) /\ is_sint16(read_sint16(m, a_2)) /\
+ is_sint32(read_sint32(m, a_1)) /\ is_sint64(x).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_m64_38 <- 8][L_m32_39 <- 4][L_m16_40 <- 2]
+ [L_m8_41 <- 1][L_write_42 <- 4]).
+}
+Prove: (x = (-81684111829661576)) /\ (x < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 85):
+Let a = global(L_m64_38).
+Let a_1 = global(L_m32_39).
+Let a_2 = global(L_m16_40).
+Let a_3 = global(L_m8_41).
+Let m = write_uint32(write_sint8(write_sint16(write_sint32(write_sint64(mem_0,
+ a,
+ -81684111829661576),
+ a_1, -19018564), a_2, -290),
+ a_3, -1), global(L_write_42), 0).
+Let x = read_sint32(m, a_1).
+Assume {
+ Type: is_sint8(read_sint8(m, a_3)) /\ is_sint16(read_sint16(m, a_2)) /\
+ is_sint32(x) /\ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_m64_38 <- 8][L_m32_39 <- 4][L_m16_40 <- 2]
+ [L_m8_41 <- 1][L_write_42 <- 4]).
+}
+Prove: (x = (-19018564)) /\ (x < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 86):
+Let a = global(L_m64_38).
+Let a_1 = global(L_m32_39).
+Let a_2 = global(L_m16_40).
+Let a_3 = global(L_m8_41).
+Let m = write_uint32(write_sint8(write_sint16(write_sint32(write_sint64(mem_0,
+ a,
+ -81684111829661576),
+ a_1, -19018564), a_2, -290),
+ a_3, -1), global(L_write_42), 0).
+Let x = read_sint16(m, a_2).
+Assume {
+ Type: is_sint8(read_sint8(m, a_3)) /\ is_sint16(x) /\
+ is_sint32(read_sint32(m, a_1)) /\ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_m64_38 <- 8][L_m32_39 <- 4][L_m16_40 <- 2]
+ [L_m8_41 <- 1][L_write_42 <- 4]).
+}
+Prove: (x = (-290)) /\ (x < 0).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 87):
+Let a = global(L_m64_38).
+Let a_1 = global(L_m32_39).
+Let a_2 = global(L_m16_40).
+Let a_3 = global(L_m8_41).
+Let m = write_uint32(write_sint8(write_sint16(write_sint32(write_sint64(mem_0,
+ a,
+ -81684111829661576),
+ a_1, -19018564), a_2, -290),
+ a_3, -1), global(L_write_42), 0).
+Let x = read_sint8(m, a_3).
+Assume {
+ Type: is_sint8(x) /\ is_sint16(read_sint16(m, a_2)) /\
+ is_sint32(read_sint32(m, a_1)) /\ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_m64_38 <- 8][L_m32_39 <- 4][L_m16_40 <- 2]
+ [L_m8_41 <- 1][L_write_42 <- 4]).
+}
+Prove: (x = (-1)) /\ (x < 0).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function signed_pos
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 54):
+Let a = global(L_p64_31).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_p64_31 <- 8][L_p32_32 <- 4][L_p16_33 <- 2]
+ [L_p8_34 <- 1][L_write_35 <- 4]).
+}
+Prove: (read_init64(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ a, true),
+ global(L_p32_32),
+ true),
+ global(L_p16_33), true),
+ global(L_p8_34), true),
+ global(L_write_35), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 55):
+Let a = global(L_p32_32).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_p64_31 <- 8][L_p32_32 <- 4][L_p16_33 <- 2]
+ [L_p8_34 <- 1][L_write_35 <- 4]).
+}
+Prove: (read_init32(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ global(L_p64_31),
+ true), a, true),
+ global(L_p16_33), true),
+ global(L_p8_34), true),
+ global(L_write_35), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 56):
+Let a = global(L_p16_33).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_p64_31 <- 8][L_p32_32 <- 4][L_p16_33 <- 2]
+ [L_p8_34 <- 1][L_write_35 <- 4]).
+}
+Prove: (read_init16(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ global(L_p64_31),
+ true),
+ global(L_p32_32),
+ true), a, true),
+ global(L_p8_34), true),
+ global(L_write_35), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 57):
+Let a = global(L_p8_34).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_p64_31 <- 8][L_p32_32 <- 4][L_p16_33 <- 2]
+ [L_p8_34 <- 1][L_write_35 <- 4]).
+}
+Prove: (read_init8(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ global(L_p64_31),
+ true),
+ global(L_p32_32),
+ true),
+ global(L_p16_33), true), a,
+ true), global(L_write_35), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 59):
+Let a = global(L_p64_31).
+Let a_1 = global(L_p32_32).
+Let a_2 = global(L_p16_33).
+Let a_3 = global(L_p8_34).
+Let m = write_uint32(write_sint8(write_sint16(write_sint32(write_sint64(mem_0,
+ a,
+ 81684111829661576),
+ a_1, 19018564), a_2, 290),
+ a_3, 1), global(L_write_35), 0).
+Let x = read_sint64(m, a).
+Assume {
+ Type: is_sint8(read_sint8(m, a_3)) /\ is_sint16(read_sint16(m, a_2)) /\
+ is_sint32(read_sint32(m, a_1)) /\ is_sint64(x).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_p64_31 <- 8][L_p32_32 <- 4][L_p16_33 <- 2]
+ [L_p8_34 <- 1][L_write_35 <- 4]).
+}
+Prove: (x = 81684111829661576) /\ (0 < x).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 60):
+Let a = global(L_p64_31).
+Let a_1 = global(L_p32_32).
+Let a_2 = global(L_p16_33).
+Let a_3 = global(L_p8_34).
+Let m = write_uint32(write_sint8(write_sint16(write_sint32(write_sint64(mem_0,
+ a,
+ 81684111829661576),
+ a_1, 19018564), a_2, 290),
+ a_3, 1), global(L_write_35), 0).
+Let x = read_sint32(m, a_1).
+Assume {
+ Type: is_sint8(read_sint8(m, a_3)) /\ is_sint16(read_sint16(m, a_2)) /\
+ is_sint32(x) /\ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_p64_31 <- 8][L_p32_32 <- 4][L_p16_33 <- 2]
+ [L_p8_34 <- 1][L_write_35 <- 4]).
+}
+Prove: (x = 19018564) /\ (0 < x).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 61):
+Let a = global(L_p64_31).
+Let a_1 = global(L_p32_32).
+Let a_2 = global(L_p16_33).
+Let a_3 = global(L_p8_34).
+Let m = write_uint32(write_sint8(write_sint16(write_sint32(write_sint64(mem_0,
+ a,
+ 81684111829661576),
+ a_1, 19018564), a_2, 290),
+ a_3, 1), global(L_write_35), 0).
+Let x = read_sint16(m, a_2).
+Assume {
+ Type: is_sint8(read_sint8(m, a_3)) /\ is_sint16(x) /\
+ is_sint32(read_sint32(m, a_1)) /\ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_p64_31 <- 8][L_p32_32 <- 4][L_p16_33 <- 2]
+ [L_p8_34 <- 1][L_write_35 <- 4]).
+}
+Prove: (x = 290) /\ (0 < x).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 62):
+Let a = global(L_p64_31).
+Let a_1 = global(L_p32_32).
+Let a_2 = global(L_p16_33).
+Let a_3 = global(L_p8_34).
+Let m = write_uint32(write_sint8(write_sint16(write_sint32(write_sint64(mem_0,
+ a,
+ 81684111829661576),
+ a_1, 19018564), a_2, 290),
+ a_3, 1), global(L_write_35), 0).
+Let x = read_sint8(m, a_3).
+Assume {
+ Type: is_sint8(x) /\ is_sint16(read_sint16(m, a_2)) /\
+ is_sint32(read_sint32(m, a_1)) /\ is_sint64(read_sint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_p64_31 <- 8][L_p32_32 <- 4][L_p16_33 <- 2]
+ [L_p8_34 <- 1][L_write_35 <- 4]).
+}
+Prove: (x = 1) /\ (0 < x).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function unsigned_
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 29):
+Let a = global(L_u64_22).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_22 <- 8][L_u32_23 <- 4][L_u16_24 <- 2]
+ [L_u8_25 <- 1][L_write_26 <- 4]).
+}
+Prove: (read_init64(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ a, true),
+ global(L_u32_23),
+ true),
+ global(L_u16_24), true),
+ global(L_u8_25), true),
+ global(L_write_26), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 30):
+Let a = global(L_u32_23).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_22 <- 8][L_u32_23 <- 4][L_u16_24 <- 2]
+ [L_u8_25 <- 1][L_write_26 <- 4]).
+}
+Prove: (read_init32(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ global(L_u64_22),
+ true), a, true),
+ global(L_u16_24), true),
+ global(L_u8_25), true),
+ global(L_write_26), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 31):
+Let a = global(L_u16_24).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_22 <- 8][L_u32_23 <- 4][L_u16_24 <- 2]
+ [L_u8_25 <- 1][L_write_26 <- 4]).
+}
+Prove: (read_init16(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ global(L_u64_22),
+ true),
+ global(L_u32_23),
+ true), a, true),
+ global(L_u8_25), true),
+ global(L_write_26), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 32):
+Let a = global(L_u8_25).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ cinits(init_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_22 <- 8][L_u32_23 <- 4][L_u16_24 <- 2]
+ [L_u8_25 <- 1][L_write_26 <- 4]).
+}
+Prove: (read_init8(write_init32(write_init8(write_init16(write_init32(
+ write_init64(init_0,
+ global(L_u64_22),
+ true),
+ global(L_u32_23),
+ true),
+ global(L_u16_24), true), a,
+ true), global(L_write_26), true), a)=true).
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 34):
+Let a = global(L_u64_22).
+Let a_1 = global(L_u32_23).
+Let a_2 = global(L_u16_24).
+Let a_3 = global(L_u8_25).
+Let m = write_uint32(write_uint8(write_uint16(write_uint32(write_uint64(mem_0,
+ a,
+ 1234605616436508552),
+ a_1, 287454020), a_2, 4386),
+ a_3, 17), global(L_write_26), 0).
+Let x = read_uint64(m, a).
+Assume {
+ Type: is_uint8(read_uint8(m, a_3)) /\ is_uint16(read_uint16(m, a_2)) /\
+ is_uint32(read_uint32(m, a_1)) /\ is_uint64(x).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_22 <- 8][L_u32_23 <- 4][L_u16_24 <- 2]
+ [L_u8_25 <- 1][L_write_26 <- 4]).
+}
+Prove: x = 1234605616436508552.
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 35):
+Let a = global(L_u64_22).
+Let a_1 = global(L_u32_23).
+Let a_2 = global(L_u16_24).
+Let a_3 = global(L_u8_25).
+Let m = write_uint32(write_uint8(write_uint16(write_uint32(write_uint64(mem_0,
+ a,
+ 1234605616436508552),
+ a_1, 287454020), a_2, 4386),
+ a_3, 17), global(L_write_26), 0).
+Let x = read_uint32(m, a_1).
+Assume {
+ Type: is_uint8(read_uint8(m, a_3)) /\ is_uint16(read_uint16(m, a_2)) /\
+ is_uint32(x) /\ is_uint64(read_uint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_22 <- 8][L_u32_23 <- 4][L_u16_24 <- 2]
+ [L_u8_25 <- 1][L_write_26 <- 4]).
+}
+Prove: x = 287454020.
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 36):
+Let a = global(L_u64_22).
+Let a_1 = global(L_u32_23).
+Let a_2 = global(L_u16_24).
+Let a_3 = global(L_u8_25).
+Let m = write_uint32(write_uint8(write_uint16(write_uint32(write_uint64(mem_0,
+ a,
+ 1234605616436508552),
+ a_1, 287454020), a_2, 4386),
+ a_3, 17), global(L_write_26), 0).
+Let x = read_uint16(m, a_2).
+Assume {
+ Type: is_uint8(read_uint8(m, a_3)) /\ is_uint16(x) /\
+ is_uint32(read_uint32(m, a_1)) /\ is_uint64(read_uint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_22 <- 8][L_u32_23 <- 4][L_u16_24 <- 2]
+ [L_u8_25 <- 1][L_write_26 <- 4]).
+}
+Prove: x = 4386.
+
+------------------------------------------------------------
+
+Goal Check (file integers.i, line 37):
+Let a = global(L_u64_22).
+Let a_1 = global(L_u32_23).
+Let a_2 = global(L_u16_24).
+Let a_3 = global(L_u8_25).
+Let m = write_uint32(write_uint8(write_uint16(write_uint32(write_uint64(mem_0,
+ a,
+ 1234605616436508552),
+ a_1, 287454020), a_2, 4386),
+ a_3, 17), global(L_write_26), 0).
+Let x = read_uint8(m, a_3).
+Assume {
+ Type: is_uint8(x) /\ is_uint16(read_uint16(m, a_2)) /\
+ is_uint32(read_uint32(m, a_1)) /\ is_uint64(read_uint64(m, a)).
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(alloc_0[L_u64_22 <- 8][L_u32_23 <- 4][L_u16_24 <- 2]
+ [L_u8_25 <- 1][L_write_26 <- 4]).
+}
+Prove: x = 17.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/pointers.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/pointers.res.oracle
new file mode 100644
index 00000000000..09ddbf4e0d4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle/pointers.res.oracle
@@ -0,0 +1,120 @@
+# frama-c -wp -wp-model 'Bytes' [...]
+[kernel] Parsing pointers.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal addr_formal_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal addr_formal_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal addr_glob_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal addr_glob_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal addr_local_ko_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal addr_local_ko_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal addr_local_ok_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal addr_local_ok_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal pointer_param_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal pointer_param_terminates (Cfg) (Trivial)
+------------------------------------------------------------
+ Function addr_formal
+------------------------------------------------------------
+
+Goal Check (file pointers.i, line 18):
+Let m = alloc_0[P_x_28 <- 4].
+Let m_1 = m[L_buffer_29 <- 8].
+Let a = shift_uint8(global(L_buffer_29), 0).
+Let a_1 = global(P_x_28).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Frame In *)
+ Have: wf_malloc(m).
+ (* Block In *)
+ Have: wf_malloc(m_1).
+}
+Prove: addr_of_int(m_1,
+ read_uint64(write_uint64(mem_0, a, int_of_addr(a_1)), a)) = a_1.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function addr_glob
+------------------------------------------------------------
+
+Goal Check (file pointers.i, line 10):
+Let m = alloc_0[L_buffer_23 <- 8].
+Let a = shift_uint8(global(L_buffer_23), 0).
+Let a_1 = global(G_x_20).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(m).
+}
+Prove: addr_of_int(m,
+ read_uint64(write_uint64(mem_0, a, int_of_addr(a_1)), a)) = a_1.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function addr_local_ko
+------------------------------------------------------------
+
+Goal Check (file pointers.i, line 40):
+Let m = alloc_0[L_buffer_39 <- 8].
+Let m_1 = m[L_x_41 <- 0].
+Let a = shift_uint8(global(L_buffer_39), 0).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(m).
+ (* Block In *)
+ Have: wf_malloc(m[L_x_41 <- 4]).
+ (* Block Out *)
+ Have: wf_malloc(m_1).
+}
+Prove: addr_of_int(m_1,
+ read_uint64(write_uint64(mem_0, a, int_of_addr(global(L_x_41))), a)) =
+ global(G_x_20).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function addr_local_ok
+------------------------------------------------------------
+
+Goal Check 'P' (file pointers.i, line 28):
+Let a = global(L_x_34).
+Let m = alloc_0[L_x_34 <- 4][L_buffer_35 <- 8].
+Let a_1 = shift_uint8(global(L_buffer_35), 0).
+Assume {
+ (* Heap *)
+ Type: linked(alloc_0) /\ wf_malloc(alloc_0) /\ sconst(mem_0) /\
+ framed(alloc_0, mem_0).
+ (* Block In *)
+ Have: wf_malloc(m).
+ (* Initializer *)
+ Init: read_sint32(mem_0, a) = 0.
+}
+Prove: addr_of_int(m,
+ read_uint64(write_uint64(mem_0, a_1, int_of_addr(a)), a_1)) = a.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function pointer_param
+------------------------------------------------------------
+
+Goal Check (file pointers.i, line 49):
+Let m = alloc_0[L_buffer_47 <- 8].
+Let a = shift_uint8(global(L_buffer_47), 0).
+Assume {
+ (* Heap *)
+ Type: (region(f.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, f, 4).
+ (* Block In *)
+ Have: wf_malloc(m).
+}
+Prove: addr_of_int(m, read_uint64(write_uint64(mem_0, a, int_of_addr(f)), a)) =
+ f.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle
new file mode 100644
index 00000000000..29d74ac5b4f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle
@@ -0,0 +1,46 @@
+# frama-c -wp -wp-model 'Bytes' [...]
+[kernel] Parsing structs.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] structs.i:14: Warning:
+ Neither code nor explicit exits and terminates for function callee,
+ generating default clauses. See -generated-spec-* options for more info
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function caller
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'caller':
+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)).
+Assume {
+ Type: IsS2_Y(a) /\ IsS2_Y(a_1).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ (region(y.base) <= 0) /\ sconst(mem_0).
+ (* Pre-condition *)
+ Have: separated(u, 32, y, 32).
+}
+Prove: EqS2_Y(a_1, a).
+
+------------------------------------------------------------
+
+Goal Exit-condition (generated) in 'caller':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file structs.i, line 17) in 'caller':
+Call Effect at line 21
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file structs.i, line 17) in 'caller':
+Call Effect at line 21
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
new file mode 100644
index 00000000000..4f9fea319f3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
@@ -0,0 +1,424 @@
+# frama-c -wp -wp-model 'Bytes' [...]
+[kernel] Parsing union.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal union_1_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal union_1_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal union_2_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal union_2_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal union_3_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal union_3_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal union_4_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal union_4_terminates (Cfg) (Trivial)
+------------------------------------------------------------
+ Function union_1
+------------------------------------------------------------
+
+Goal Check (file union.i, line 23):
+Let m = write_uint64(mem_0, shiftfield_F2_U_u(u), 4294967295).
+Let a = shiftfield_F2_U_x(u).
+Let x = read_sint32(m, shiftfield_F1_X_i(a)).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F2_U_s(u))) /\
+ is_uint32(read_uint32(m, shiftfield_F1_X_u(a))) /\ is_sint32(x).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 24):
+Let m = write_uint64(mem_0, shiftfield_F2_U_u(u), 4294967295).
+Let a = shiftfield_F2_U_x(u).
+Let x = read_uint32(m, shiftfield_F1_X_u(a)).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F2_U_s(u))) /\ is_uint32(x) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 4294967295.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 26):
+Let m = write_uint64(mem_0, shiftfield_F2_U_u(u), 4294967295).
+Let a = shiftfield_F2_U_x(u).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F2_U_s(u))) /\
+ is_uint32(read_uint32(m, shiftfield_F1_X_u(a))) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 3).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: read_uint8(m, shift_uint8(shiftfield_F2_U_a(u), i)) = 255.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 27):
+Let m = write_uint64(mem_0, shiftfield_F2_U_u(u), 4294967295).
+Let a = shiftfield_F2_U_x(u).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F2_U_s(u))) /\
+ is_uint32(read_uint32(m, shiftfield_F1_X_u(a))) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Goal *)
+ When: (4 <= i) /\ (i <= 7).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: read_uint8(m, shift_uint8(shiftfield_F2_U_a(u), i)) = 0.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 29):
+Let m = write_uint64(mem_0, shiftfield_F2_U_u(u), 4294967295).
+Let x = read_uint32(m, shiftfield_F2_U_s(u)).
+Let a = shiftfield_F2_U_x(u).
+Assume {
+ Type: is_uint32(x) /\ is_uint32(read_uint32(m, shiftfield_F1_X_u(a))) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 4294967295.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function union_2
+------------------------------------------------------------
+
+Goal Check (file union.i, line 43):
+Let a = shiftfield_F2_U_a(u).
+Let m = write_uint8(write_uint8(write_uint8(write_uint8(write_uint8(write_uint8(
+ write_uint8(
+ write_uint8(mem_0,
+ shift_uint8(a,
+ 0), 255),
+ shift_uint8(a,
+ 1), 255),
+ shift_uint8(a,
+ 2), 255),
+ shift_uint8(a, 3),
+ 255),
+ shift_uint8(a, 4), 0),
+ shift_uint8(a, 5), 0), shift_uint8(a, 6),
+ 0), shift_uint8(a, 7), 0).
+Let a_1 = shiftfield_F2_U_x(u).
+Let x = read_uint64(m, shiftfield_F2_U_u(u)).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F2_U_s(u))) /\
+ is_uint32(read_uint32(m, shiftfield_F1_X_u(a_1))) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a_1))) /\ is_uint64(x).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 4294967295.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 45):
+Let a = shiftfield_F2_U_a(u).
+Let m = write_uint8(write_uint8(write_uint8(write_uint8(write_uint8(write_uint8(
+ write_uint8(
+ write_uint8(mem_0,
+ shift_uint8(a,
+ 0), 255),
+ shift_uint8(a,
+ 1), 255),
+ shift_uint8(a,
+ 2), 255),
+ shift_uint8(a, 3),
+ 255),
+ shift_uint8(a, 4), 0),
+ shift_uint8(a, 5), 0), shift_uint8(a, 6),
+ 0), shift_uint8(a, 7), 0).
+Let a_1 = shiftfield_F2_U_x(u).
+Let x = read_sint32(m, shiftfield_F1_X_i(a_1)).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F2_U_s(u))) /\
+ is_uint32(read_uint32(m, shiftfield_F1_X_u(a_1))) /\ is_sint32(x) /\
+ is_uint64(read_uint64(m, shiftfield_F2_U_u(u))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 46):
+Let a = shiftfield_F2_U_a(u).
+Let m = write_uint8(write_uint8(write_uint8(write_uint8(write_uint8(write_uint8(
+ write_uint8(
+ write_uint8(mem_0,
+ shift_uint8(a,
+ 0), 255),
+ shift_uint8(a,
+ 1), 255),
+ shift_uint8(a,
+ 2), 255),
+ shift_uint8(a, 3),
+ 255),
+ shift_uint8(a, 4), 0),
+ shift_uint8(a, 5), 0), shift_uint8(a, 6),
+ 0), shift_uint8(a, 7), 0).
+Let a_1 = shiftfield_F2_U_x(u).
+Let x = read_uint32(m, shiftfield_F1_X_u(a_1)).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F2_U_s(u))) /\ is_uint32(x) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a_1))) /\
+ is_uint64(read_uint64(m, shiftfield_F2_U_u(u))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 4294967295.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 48):
+Let a = shiftfield_F2_U_a(u).
+Let m = write_uint8(write_uint8(write_uint8(write_uint8(write_uint8(write_uint8(
+ write_uint8(
+ write_uint8(mem_0,
+ shift_uint8(a,
+ 0), 255),
+ shift_uint8(a,
+ 1), 255),
+ shift_uint8(a,
+ 2), 255),
+ shift_uint8(a, 3),
+ 255),
+ shift_uint8(a, 4), 0),
+ shift_uint8(a, 5), 0), shift_uint8(a, 6),
+ 0), shift_uint8(a, 7), 0).
+Let x = read_uint32(m, shiftfield_F2_U_s(u)).
+Let a_1 = shiftfield_F2_U_x(u).
+Assume {
+ Type: is_uint32(x) /\ is_uint32(read_uint32(m, shiftfield_F1_X_u(a_1))) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a_1))) /\
+ is_uint64(read_uint64(m, shiftfield_F2_U_u(u))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 4294967295.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function union_3
+------------------------------------------------------------
+
+Goal Check (file union.i, line 56):
+Let a = shiftfield_F2_U_u(u).
+Let m = write_uint32(write_uint64(mem_0, a, 4294967295),
+ shiftfield_F2_U_s(u), 4294967295).
+Let a_1 = shiftfield_F2_U_x(u).
+Let x = read_uint64(m, a).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F1_X_u(a_1))) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a_1))) /\ is_uint64(x).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 4294967295.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 58):
+Let a = shiftfield_F2_U_u(u).
+Let m = write_uint32(write_uint64(mem_0, a, 4294967295),
+ shiftfield_F2_U_s(u), 4294967295).
+Let a_1 = shiftfield_F2_U_x(u).
+Let x = read_sint32(m, shiftfield_F1_X_i(a_1)).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F1_X_u(a_1))) /\ is_sint32(x) /\
+ is_uint64(read_uint64(m, a)).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 59):
+Let a = shiftfield_F2_U_u(u).
+Let m = write_uint32(write_uint64(mem_0, a, 4294967295),
+ shiftfield_F2_U_s(u), 4294967295).
+Let a_1 = shiftfield_F2_U_x(u).
+Let x = read_uint32(m, shiftfield_F1_X_u(a_1)).
+Assume {
+ Type: is_uint32(x) /\ is_sint32(read_sint32(m, shiftfield_F1_X_i(a_1))) /\
+ is_uint64(read_uint64(m, a)).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: x = 4294967295.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 61):
+Let a = shiftfield_F2_U_u(u).
+Let m = write_uint32(write_uint64(mem_0, a, 4294967295),
+ shiftfield_F2_U_s(u), 4294967295).
+Let a_1 = shiftfield_F2_U_x(u).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F1_X_u(a_1))) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a_1))) /\
+ is_uint64(read_uint64(m, a)).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 3).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: read_uint8(m, shift_uint8(shiftfield_F2_U_a(u), i)) = 255.
+
+------------------------------------------------------------
+
+Goal Check (file union.i, line 62):
+Let a = shiftfield_F2_U_u(u).
+Let m = write_uint32(write_uint64(mem_0, a, 4294967295),
+ shiftfield_F2_U_s(u), 4294967295).
+Let a_1 = shiftfield_F2_U_x(u).
+Assume {
+ Type: is_uint32(read_uint32(m, shiftfield_F1_X_u(a_1))) /\
+ is_sint32(read_sint32(m, shiftfield_F1_X_i(a_1))) /\
+ is_uint64(read_uint64(m, a)).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Goal *)
+ When: (4 <= i) /\ (i <= 7).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+}
+Prove: read_uint8(m, shift_uint8(shiftfield_F2_U_a(u), i)) = 0.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function union_4
+------------------------------------------------------------
+
+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 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).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+ (* Initializer *)
+ Init: read_uint32(a_1, shiftfield_F1_X_u(a)) = 4294967295.
+ (* Initializer *)
+ Init: read_sint32(a_1, shiftfield_F1_X_i(a)) = 0.
+}
+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).
+Assume {
+ Type: is_uint32(read_uint32(a_1, shiftfield_F2_U_s(u))) /\
+ is_uint64(read_uint64(a_1, shiftfield_F2_U_u(u))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 3).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+ (* Initializer *)
+ Init: read_uint32(a_1, shiftfield_F1_X_u(a)) = 4294967295.
+ (* Initializer *)
+ Init: read_sint32(a_1, shiftfield_F1_X_i(a)) = 0.
+}
+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).
+Assume {
+ Type: is_uint32(read_uint32(a_1, shiftfield_F2_U_s(u))) /\
+ is_uint64(read_uint64(a_1, shiftfield_F2_U_u(u))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Goal *)
+ When: (4 <= i) /\ (i <= 7).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+ (* Initializer *)
+ Init: read_uint32(a_1, shiftfield_F1_X_u(a)) = 4294967295.
+ (* Initializer *)
+ Init: read_sint32(a_1, shiftfield_F1_X_i(a)) = 0.
+}
+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 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))).
+ (* Heap *)
+ Type: (region(u.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
+ sconst(mem_0) /\ framed(alloc_0, mem_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, u, 8).
+ (* Initializer *)
+ Init: read_uint32(a_1, shiftfield_F1_X_u(a)) = 4294967295.
+ (* Initializer *)
+ Init: read_sint32(a_1, shiftfield_F1_X_i(a)) = 0.
+}
+Prove: x = 4294967295.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle_qualif/assigns_sep.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle_qualif/assigns_sep.res.oracle
new file mode 100644
index 00000000000..f8cf73fe311
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle_qualif/assigns_sep.res.oracle
@@ -0,0 +1,32 @@
+# frama-c -wp -wp-model 'Bytes' -wp-timeout 20 [...]
+[kernel] Parsing assigns_sep.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] assigns_sep.i:13: Warning:
+ Neither code nor explicit exits and terminates for function assigns,
+ generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] assigns_sep.i:16: Warning:
+ Neither code nor explicit exits and terminates for function assigns_r,
+ generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] assigns_sep.i:19: Warning:
+ Neither code nor explicit exits and terminates for function assigns_l2,
+ generating default clauses. See -generated-spec-* options for more info
+[wp] [Valid] Goal assignment_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal assignment_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Valid] bytes_assignment_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_assigns_clause_terminates (Qed)
+[wp] [Valid] bytes_assigns_clause_exits (Qed)
+[wp] [Valid] bytes_assigns_clause_check (Alt-Ergo) (Cached)
+[wp] [Unsuccess] bytes_assigns_clause_check_2 (Alt-Ergo) (Cached)
+[wp] Proved goals: 6 / 7
+ Terminating: 1
+ Unreachable: 1
+ Qed: 2
+ Alt-Ergo: 2
+ Unsuccess: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ assignment - 1 1 100%
+ assigns_clause 2 1 4 75.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle_qualif/floats.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle_qualif/floats.res.oracle
new file mode 100644
index 00000000000..b7d9a3d3cb4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle_qualif/floats.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp -wp-model 'Bytes' -wp-timeout 20 [...]
+[kernel] Parsing floats.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal double_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal double_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal float_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal float_terminates (Cfg) (Trivial)
+[wp] 2 goals scheduled
+[wp] [Valid] bytes_float_assert (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_double_assert (Alt-Ergo) (Cached)
+[wp] Proved goals: 6 / 6
+ Terminating: 2
+ Unreachable: 2
+ Alt-Ergo: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ float_ - 1 1 100%
+ double_ - 1 1 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle
new file mode 100644
index 00000000000..c58a719e673
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle
@@ -0,0 +1,90 @@
+# frama-c -wp -wp-model 'Bytes (Raw)' -wp-timeout 20 [...]
+[kernel] Parsing integers.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal cast_from_bytes_to_signed_neg_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_from_bytes_to_signed_neg_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal cast_from_bytes_to_signed_pos_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_from_bytes_to_signed_pos_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal cast_from_bytes_to_unsigned_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_from_bytes_to_unsigned_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal cast_unsigned_signed_neg_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_unsigned_signed_neg_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal cast_unsigned_signed_pos_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal cast_unsigned_signed_pos_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal signed_neg_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal signed_neg_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal signed_pos_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal signed_pos_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal unsigned_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal unsigned_terminates (Cfg) (Trivial)
+[wp] 53 goals scheduled
+[wp] [Valid] bytes_raw_unsigned_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_unsigned_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_unsigned_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_unsigned_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_unsigned_check_5 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_unsigned_check_6 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_unsigned_check_7 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_unsigned_check_8 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_pos_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_pos_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_pos_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_pos_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_pos_check_5 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_pos_check_6 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_pos_check_7 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_pos_check_8 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_neg_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_neg_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_neg_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_neg_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_neg_check_5 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_neg_check_6 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_neg_check_7 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_signed_neg_check_8 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_unsigned_signed_pos_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_unsigned_signed_pos_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_unsigned_signed_pos_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_unsigned_signed_pos_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_unsigned_signed_neg_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_unsigned_signed_neg_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_unsigned_signed_neg_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_unsigned_signed_neg_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_unsigned_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_unsigned_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_unsigned_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_unsigned_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_unsigned_check_5 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_unsigned_check_6 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_unsigned_check_7 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_pos_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_pos_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_pos_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_pos_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_pos_check_5 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_pos_check_6 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_pos_check_7 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_2 (Alt-Ergo) (Cached)
+[wp] [Unsuccess] bytes_raw_cast_from_bytes_to_signed_neg_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_5 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_6 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_7 (Alt-Ergo) (Cached)
+[wp] Proved goals: 68 / 69
+ Terminating: 8
+ Unreachable: 8
+ Alt-Ergo: 52
+ Unsuccess: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ unsigned_ - 8 8 100%
+ signed_pos - 8 8 100%
+ signed_neg - 8 8 100%
+ cast_unsigned_signed_pos - 4 4 100%
+ cast_unsigned_signed_neg - 4 4 100%
+ cast_from_bytes_to_unsigned - 7 7 100%
+ cast_from_bytes_to_signed_pos - 7 7 100%
+ cast_from_bytes_to_signed_neg - 6 7 85.7%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle_qualif/pointers.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle_qualif/pointers.res.oracle
new file mode 100644
index 00000000000..282cb21da04
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle_qualif/pointers.res.oracle
@@ -0,0 +1,33 @@
+# frama-c -wp -wp-model 'Bytes' -wp-timeout 20 [...]
+[kernel] Parsing pointers.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal addr_formal_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal addr_formal_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal addr_glob_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal addr_glob_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal addr_local_ko_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal addr_local_ko_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal addr_local_ok_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal addr_local_ok_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal pointer_param_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal pointer_param_terminates (Cfg) (Trivial)
+[wp] 5 goals scheduled
+[wp] [Valid] bytes_addr_glob_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_addr_formal_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_addr_local_ok_check_P (Alt-Ergo) (Cached)
+[wp] [Unsuccess] bytes_addr_local_ko_check (Alt-Ergo) (Cached)
+[wp] [Unsuccess] bytes_pointer_param_check (Alt-Ergo) (Cached)
+[wp] Proved goals: 13 / 15
+ Terminating: 5
+ Unreachable: 5
+ Alt-Ergo: 3
+ Unsuccess: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ addr_glob - 1 1 100%
+ addr_formal - 1 1 100%
+ addr_local_ok - 1 1 100%
+ addr_local_ko - - 1 0.0%
+ pointer_param - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle_qualif/structs.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle_qualif/structs.res.oracle
new file mode 100644
index 00000000000..cc3260b313a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle_qualif/structs.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp -wp-model 'Bytes' -wp-timeout 20 [...]
+[kernel] Parsing structs.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] structs.i:14: Warning:
+ Neither code nor explicit exits and terminates for function callee,
+ generating default clauses. See -generated-spec-* options for more info
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Valid] bytes_caller_terminates (Qed)
+[wp] [Valid] bytes_caller_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_caller_exits (Qed)
+[wp] [Valid] bytes_caller_assigns_exit (Qed)
+[wp] [Valid] bytes_caller_assigns_normal (Qed)
+[wp] Proved goals: 5 / 5
+ Qed: 4
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ caller 4 1 5 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/oracle_qualif/union.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle_qualif/union.res.oracle
new file mode 100644
index 00000000000..a653dbd9983
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/oracle_qualif/union.res.oracle
@@ -0,0 +1,43 @@
+# frama-c -wp -wp-model 'Bytes' -wp-timeout 20 [...]
+[kernel] Parsing union.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal union_1_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal union_1_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal union_2_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal union_2_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal union_3_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal union_3_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal union_4_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal union_4_terminates (Cfg) (Trivial)
+[wp] 18 goals scheduled
+[wp] [Valid] bytes_union_1_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_1_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_1_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_1_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_1_check_5 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_2_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_2_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_2_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_2_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_3_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_3_check_2 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_3_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_3_check_4 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_3_check_5 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_4_check (Alt-Ergo) (Cached)
+[wp] [Unsuccess] bytes_union_4_check_2 (Alt-Ergo) (Cached)
+[wp] [Unsuccess] bytes_union_4_check_3 (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_union_4_check_4 (Alt-Ergo) (Cached)
+[wp] Proved goals: 24 / 26
+ Terminating: 4
+ Unreachable: 4
+ Alt-Ergo: 16
+ Unsuccess: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ union_1 - 5 5 100%
+ union_2 - 4 4 100%
+ union_3 - 5 5 100%
+ union_4 - 2 4 50.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/pointers.i b/src/plugins/wp/tests/wp_bytes/pointers.i
new file mode 100644
index 00000000000..eb7ca1de529
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/pointers.i
@@ -0,0 +1,50 @@
+typedef unsigned char uint8 ;
+
+int x ;
+
+void addr_glob(void){
+ uint8 buffer[sizeof(int*)] ;
+ *((int**) buffer) = &x ;
+
+ int* r = *((int**) buffer) ;
+ //@ check r == &x ;
+}
+
+void addr_formal(int x){
+ uint8 buffer[sizeof(int*)] ;
+ *((int**) buffer) = &x ;
+ int* r = *((int**) buffer) ;
+
+ //@ check r == &x ;
+}
+
+void addr_local_ok(void){
+ int x = 0;
+
+ uint8 buffer[sizeof(int*)] ;
+ *((int**) buffer) = &x ;
+
+ int* r = *((int**) buffer) ;
+ //@ check P: r == &x ;
+}
+
+void addr_local_ko(void){
+ uint8 buffer[sizeof(int*)] ;
+
+ {
+ int x ;
+ *((int**) buffer) = &x ;
+ }
+
+ int* r = *((int**) buffer) ;
+ //@ check r == &x ;
+}
+
+//@ requires \valid(f);
+void pointer_param(int *f){
+ uint8 buffer[sizeof(int*)] ;
+ *((int**) buffer) = f ;
+
+ int* r = *((int**) buffer) ;
+ //@ check r == f ;
+}
diff --git a/src/plugins/wp/tests/wp_bytes/structs.i b/src/plugins/wp/tests/wp_bytes/structs.i
new file mode 100644
index 00000000000..6018ae03d83
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/structs.i
@@ -0,0 +1,22 @@
+struct X {
+ char c ;
+ short s ;
+ int i ;
+ int a[5] ;
+} ;
+
+struct Y {
+ char c ;
+ struct X x ;
+} ;
+
+//@ assigns *y ;
+void callee(struct Y* y);
+
+/*@ requires \separated(u, y) ;
+ assigns *y ;
+ ensures *u == \old(*u) ;
+*/
+void caller(struct Y const* u, struct Y* y){
+ callee(y) ;
+}
diff --git a/src/plugins/wp/tests/wp_bytes/test_config b/src/plugins/wp/tests/wp_bytes/test_config
new file mode 100644
index 00000000000..3ef26ad2d95
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/test_config
@@ -0,0 +1 @@
+OPT: -wp-model bytes
diff --git a/src/plugins/wp/tests/wp_bytes/test_config_qualif b/src/plugins/wp/tests/wp_bytes/test_config_qualif
new file mode 100644
index 00000000000..b669ba76f90
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/test_config_qualif
@@ -0,0 +1 @@
+OPT: -wp-model bytes -wp-prover Alt-Ergo -wp-timeout 20
diff --git a/src/plugins/wp/tests/wp_bytes/union.i b/src/plugins/wp/tests/wp_bytes/union.i
new file mode 100644
index 00000000000..548d6b072a1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bytes/union.i
@@ -0,0 +1,76 @@
+typedef unsigned long long uint64 ;
+typedef unsigned uint32 ;
+typedef unsigned char uint8 ;
+
+typedef int int32 ;
+
+struct X {
+ uint32 u ;
+ int32 i ;
+} ;
+
+union U {
+ struct X x ;
+ uint64 u ;
+ uint8 a[sizeof(struct X)] ;
+ uint32 s ;
+} ;
+
+//@ requires \valid(u) ;
+void union_1(union U* u){
+ u->u = 0x00000000FFFFFFFF ;
+
+ //@ check u->x.i == 0x00000000 ;
+ //@ check u->x.u == 0xFFFFFFFF ;
+
+ //@ check \forall integer i ; 0 <= i < 4 ==> u->a[i] == { 0xFF } ;
+ //@ check \forall integer i ; 4 <= i < 8 ==> u->a[i] == { 0x00 } ;
+
+ //@ check u->s == 0xFFFFFFFF ;
+}
+
+//@ requires \valid(u) ;
+void union_2(union U* u){
+ u->a[0] = 0xFF ;
+ u->a[1] = 0xFF ;
+ u->a[2] = 0xFF ;
+ u->a[3] = 0xFF ;
+ u->a[4] = 0x00 ;
+ u->a[5] = 0x00 ;
+ u->a[6] = 0x00 ;
+ u->a[7] = 0x00 ;
+
+ //@ check u->u == 0x00000000FFFFFFFF ;
+
+ //@ check u->x.i == 0x00000000 ;
+ //@ check u->x.u == 0xFFFFFFFF ;
+
+ //@ check u->s == 0xFFFFFFFF ;
+}
+
+//@ requires \valid(u) ;
+void union_3(union U* u){
+ u->u = 0x00000000FFFFFFFF ;
+ u->s = 0xFFFFFFFF ;
+
+ //@ check u->u == 0x00000000FFFFFFFF ;
+
+ //@ check u->x.i == 0x00000000 ;
+ //@ check u->x.u == 0xFFFFFFFF ;
+
+ //@ check \forall integer i ; 0 <= i < 4 ==> u->a[i] == { 0xFF } ;
+ //@ check \forall integer i ; 4 <= i < 8 ==> u->a[i] == { 0x00 } ;
+}
+
+//@ requires \valid(u) ;
+void union_4(union U* u){
+ struct X x = { .u = 0xFFFFFFFFu, .i = 0x00000000 } ;
+ u->x = x ;
+
+ //@ check u->u == 0x00000000FFFFFFFF ;
+
+ //@ check \forall integer i ; 0 <= i < 4 ==> u->a[i] == { 0xFF } ;
+ //@ check \forall integer i ; 4 <= i < 8 ==> u->a[i] == { 0x00 } ;
+
+ //@ check u->s == 0xFFFFFFFF ;
+}
--
GitLab