From c5882fde5f697d6f88983bafd06e98cfb17d24d8 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 23 Sep 2024 14:35:30 +0200
Subject: [PATCH] [wp] bytes: use static_alloc
---
src/plugins/wp/MemBytes.ml | 10 +
.../wp_bytes/oracle/assigns_sep.res.oracle | 6 +-
.../tests/wp_bytes/oracle/floats.res.oracle | 16 +-
.../tests/wp_bytes/oracle/integers.res.oracle | 367 +++---------------
.../tests/wp_bytes/oracle/pointers.res.oracle | 105 ++---
.../tests/wp_bytes/oracle/structs.res.oracle | 3 +-
.../wp/tests/wp_bytes/oracle/union.res.oracle | 72 ++--
.../oracle_qualif/integers.res.oracle | 9 +-
.../oracle_qualif/pointers.res.oracle | 23 +-
src/plugins/wp/tests/wp_bytes/pointers.i | 32 +-
10 files changed, 184 insertions(+), 459 deletions(-)
diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index 2c83da1b35a..b3d3dad054f 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -738,6 +738,15 @@ module BASE = WpContext.Generator(Cil_datatype.Varinfo)
open Cil_types
+ let static_alloc prefix base =
+ let name = prefix ^ "_static_alloc" in
+ Definitions.define_lemma {
+ l_kind = Admit ;
+ l_name = name ; l_triggers = [] ; l_forall = [] ;
+ l_lemma = MemAddr.static_alloc base ;
+ l_cluster = cluster_globals () ;
+ }
+
let region prefix x base =
let name = prefix ^ "_region" in
let region =
@@ -810,6 +819,7 @@ module BASE = WpContext.Generator(Cil_datatype.Varinfo)
let prefix = Lang.Fun.debug lfun in
let base = e_fun lfun [] in
RegisterBASE.define lfun vi ;
+ static_alloc prefix base ;
region prefix vi base ;
alloc prefix vi base ;
pointer_type prefix base ;
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle
index db98c5be956..c2ac0df24d1 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle
@@ -24,7 +24,7 @@ Let x_1 = read_uint32(write_uint8(mem_0, shift_uint8(array_0, 7), 0),
Assume {
Type: is_uint32(x) /\ is_uint32(x_1).
(* Heap *)
- Type: (region(array_0.base) <= 0) /\ sconst(mem_0).
+ Type: (region(array_0.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
}
Prove: x_1 = x.
@@ -52,7 +52,7 @@ Let x_2 = read_uint32(havoc(mem_undef_0, m, shift_uint8(array_0, 4), 4),
Assume {
Type: is_uint32(x) /\ is_uint32(x_1) /\ is_uint32(x_2).
(* Heap *)
- Type: (region(array_0.base) <= 0) /\ sconst(mem_0).
+ Type: (region(array_0.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
}
Prove: (x_1 = x) /\ (x_2 = x_1).
@@ -67,7 +67,7 @@ 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).
+ Type: (region(array_0.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
(* Call Effects *)
Have: forall a_1 : addr.
((forall i : Z. (((i = 4) \/ (i = 6)) ->
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/floats.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/floats.res.oracle
index af3805ad36e..5e7f855ba3d 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle/floats.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle/floats.res.oracle
@@ -12,13 +12,7 @@
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]).
-}
+Assume { (* Heap *) Type: framed(mem_0) /\ sconst(mem_0). }
Prove: of_f64(int_to_float64(read_uint64(write_uint64(mem_0, a,
float64_to_int(d)), a)))
= of_f64(d).
@@ -30,13 +24,7 @@ Prove: of_f64(int_to_float64(read_uint64(write_uint64(mem_0, a,
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]).
-}
+Assume { (* Heap *) Type: framed(mem_0) /\ sconst(mem_0). }
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
index 99ddd415285..85659e3660a 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle/integers.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle/integers.res.oracle
@@ -46,12 +46,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -111,12 +106,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -176,12 +166,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -241,12 +226,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -306,12 +286,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -371,12 +346,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -436,12 +406,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -504,12 +469,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -569,12 +529,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -634,12 +589,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -699,12 +649,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -764,12 +709,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -829,12 +769,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -894,12 +829,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -962,12 +892,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -1027,12 +952,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -1092,12 +1012,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -1157,12 +1072,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -1222,12 +1132,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -1287,12 +1192,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -1352,12 +1252,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* Initializer *)
Init: read_uint8(mem_0, a_1) = 17.
(* Initializer *)
@@ -1406,10 +1301,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = (-9141687925025114232)) /\ (x < 0).
@@ -1425,10 +1317,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = (-2128465084)) /\ (x < 0).
@@ -1444,10 +1333,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = (-32382)) /\ (x < 0).
@@ -1463,10 +1349,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = (-127)) /\ (x < 0).
@@ -1485,10 +1368,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = 81684111829661576) /\ (0 < x).
@@ -1504,10 +1384,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = 19018564) /\ (0 < x).
@@ -1523,10 +1400,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = 290) /\ (0 < x).
@@ -1542,10 +1416,7 @@ Assume {
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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = 1) /\ (0 < x).
@@ -1555,14 +1426,7 @@ Prove: (x = 1) /\ (0 < x).
------------------------------------------------------------
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]).
-}
+Let a = global(L_m64_38). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init64(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
a, true),
@@ -1575,14 +1439,7 @@ Prove: (read_init64(write_init32(write_init8(write_init16(write_init32(
------------------------------------------------------------
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]).
-}
+Let a = global(L_m32_39). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init32(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
global(L_m64_38),
@@ -1594,14 +1451,7 @@ Prove: (read_init32(write_init32(write_init8(write_init16(write_init32(
------------------------------------------------------------
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]).
-}
+Let a = global(L_m16_40). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init16(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
global(L_m64_38),
@@ -1614,14 +1464,7 @@ Prove: (read_init16(write_init32(write_init8(write_init16(write_init32(
------------------------------------------------------------
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]).
-}
+Let a = global(L_m8_41). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init8(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
global(L_m64_38),
@@ -1648,11 +1491,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = (-81684111829661576)) /\ (x < 0).
@@ -1673,11 +1512,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = (-19018564)) /\ (x < 0).
@@ -1698,11 +1533,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = (-290)) /\ (x < 0).
@@ -1723,11 +1554,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = (-1)) /\ (x < 0).
@@ -1737,14 +1564,7 @@ Prove: (x = (-1)) /\ (x < 0).
------------------------------------------------------------
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]).
-}
+Let a = global(L_p64_31). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init64(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
a, true),
@@ -1757,14 +1577,7 @@ Prove: (read_init64(write_init32(write_init8(write_init16(write_init32(
------------------------------------------------------------
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]).
-}
+Let a = global(L_p32_32). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init32(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
global(L_p64_31),
@@ -1776,14 +1589,7 @@ Prove: (read_init32(write_init32(write_init8(write_init16(write_init32(
------------------------------------------------------------
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]).
-}
+Let a = global(L_p16_33). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init16(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
global(L_p64_31),
@@ -1796,14 +1602,7 @@ Prove: (read_init16(write_init32(write_init8(write_init16(write_init32(
------------------------------------------------------------
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]).
-}
+Let a = global(L_p8_34). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init8(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
global(L_p64_31),
@@ -1830,11 +1629,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = 81684111829661576) /\ (0 < x).
@@ -1855,11 +1650,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = 19018564) /\ (0 < x).
@@ -1880,11 +1671,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = 290) /\ (0 < x).
@@ -1905,11 +1692,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: (x = 1) /\ (0 < x).
@@ -1919,14 +1702,7 @@ Prove: (x = 1) /\ (0 < x).
------------------------------------------------------------
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]).
-}
+Let a = global(L_u64_22). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init64(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
a, true),
@@ -1939,14 +1715,7 @@ Prove: (read_init64(write_init32(write_init8(write_init16(write_init32(
------------------------------------------------------------
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]).
-}
+Let a = global(L_u32_23). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init32(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
global(L_u64_22),
@@ -1958,14 +1727,7 @@ Prove: (read_init32(write_init32(write_init8(write_init16(write_init32(
------------------------------------------------------------
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]).
-}
+Let a = global(L_u16_24). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init16(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
global(L_u64_22),
@@ -1978,14 +1740,7 @@ Prove: (read_init16(write_init32(write_init8(write_init16(write_init32(
------------------------------------------------------------
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]).
-}
+Let a = global(L_u8_25). Assume { (* Heap *) Type: cinits(init_0). }
Prove: (read_init8(write_init32(write_init8(write_init16(write_init32(
write_init64(init_0,
global(L_u64_22),
@@ -2012,11 +1767,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: x = 1234605616436508552.
@@ -2037,11 +1788,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: x = 287454020.
@@ -2062,11 +1809,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
Prove: x = 4386.
@@ -2087,11 +1830,7 @@ 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]).
+ Type: framed(mem_0) /\ sconst(mem_0).
}
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
index 09ddbf4e0d4..a3a50ae3743 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle/pointers.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle/pointers.res.oracle
@@ -10,111 +10,88 @@
[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 null_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal null_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.
+Goal Check (file pointers.i, line 26):
+Let a = shift_uint8(global(L_buffer_34), 0).
+Let a_1 = global(P_f_33).
+Assume { (* Heap *) Type: framed(mem_0) /\ sconst(mem_0). }
+Prove: addr_of_int(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.
+Goal Check (file pointers.i, line 18):
+Let a = shift_uint8(global(L_buffer_29), 0).
+Let a_1 = global(G_g_26).
+Assume { (* Heap *) Type: framed(mem_0) /\ sconst(mem_0). }
+Prove: addr_of_int(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).
+Goal Check (file pointers.i, line 48):
+Let a = shift_uint8(global(L_buffer_43), 0).
+Assume { (* Heap *) Type: framed(mem_0) /\ linked(alloc_0) /\ sconst(mem_0).
}
-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).
+Prove: !valid_rw(alloc_0[L_buffer_43 <- 8][L_l_44 <- 0],
+ addr_of_int(read_uint64(write_uint64(mem_0, a,
+ int_of_addr(global(L_l_44))), a)), 4).
------------------------------------------------------------
------------------------------------------------------------
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).
+Goal Check 'P' (file pointers.i, line 36):
+Let a = global(L_l_38).
+Let a_1 = 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).
+ Type: framed(mem_0) /\ sconst(mem_0).
(* 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.
+Prove: addr_of_int(read_uint64(write_uint64(mem_0, a_1, int_of_addr(a)), a_1)) =
+ a.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function null
+------------------------------------------------------------
+
+Goal Check (file pointers.i, line 8):
+Let a = shift_uint8(global(L_buffer_22), 0).
+Assume { (* Heap *) Type: framed(mem_0) /\ sconst(mem_0). }
+Prove: addr_of_int(read_uint64(write_uint64(mem_0, a, 0), a)) = null.
------------------------------------------------------------
------------------------------------------------------------
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).
+Goal Check (file pointers.i, line 57):
+Let a = shift_uint8(global(L_buffer_50), 0).
Assume {
(* Heap *)
- Type: (region(f.base) <= 0) /\ linked(alloc_0) /\ wf_malloc(alloc_0) /\
- sconst(mem_0) /\ framed(alloc_0, mem_0).
+ Type: (region(f.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(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)) =
+Prove: addr_of_int(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
index 29d74ac5b4f..898225de015 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle
@@ -20,7 +20,8 @@ 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).
+ Type: (region(u.base) <= 0) /\ (region(y.base) <= 0) /\ framed(mem_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: separated(u, 32, y, 32).
}
diff --git a/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
index 4f9fea319f3..23b86bc3588 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
@@ -22,8 +22,8 @@ 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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -39,8 +39,8 @@ 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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -56,8 +56,8 @@ Assume {
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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Goal *)
When: (0 <= i) /\ (i <= 3).
(* Pre-condition *)
@@ -75,8 +75,8 @@ Assume {
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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Goal *)
When: (4 <= i) /\ (i <= 7).
(* Pre-condition *)
@@ -94,8 +94,8 @@ 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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -129,8 +129,8 @@ Assume {
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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -161,8 +161,8 @@ Assume {
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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -193,8 +193,8 @@ Assume {
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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -225,8 +225,8 @@ Assume {
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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -247,8 +247,8 @@ 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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -266,8 +266,8 @@ 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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -285,8 +285,8 @@ 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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
}
@@ -304,8 +304,8 @@ Assume {
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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Goal *)
When: (0 <= i) /\ (i <= 3).
(* Pre-condition *)
@@ -325,8 +325,8 @@ Assume {
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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Goal *)
When: (4 <= i) /\ (i <= 7).
(* Pre-condition *)
@@ -346,8 +346,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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
(* Initializer *)
@@ -366,8 +366,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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Goal *)
When: (0 <= i) /\ (i <= 3).
(* Pre-condition *)
@@ -388,8 +388,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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Goal *)
When: (4 <= i) /\ (i <= 7).
(* Pre-condition *)
@@ -410,8 +410,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).
+ Type: (region(u.base) <= 0) /\ framed(mem_0) /\ linked(alloc_0) /\
+ sconst(mem_0).
(* Pre-condition *)
Have: valid_rw(alloc_0, u, 8).
(* Initializer *)
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
index c58a719e673..6e3206deee0 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle
@@ -67,16 +67,15 @@
[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_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
+[wp] Proved goals: 69 / 69
Terminating: 8
Unreachable: 8
- Alt-Ergo: 52
- Unsuccess: 1
+ Alt-Ergo: 53
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
unsigned_ - 8 8 100%
@@ -86,5 +85,5 @@
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%
+ cast_from_bytes_to_signed_neg - 7 7 100%
------------------------------------------------------------
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
index 282cb21da04..b37bbb59a2c 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle_qualif/pointers.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle_qualif/pointers.res.oracle
@@ -10,24 +10,27 @@
[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 null_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal null_terminates (Cfg) (Trivial)
[wp] [Valid] Goal pointer_param_exits (Cfg) (Unreachable)
[wp] [Valid] Goal pointer_param_terminates (Cfg) (Trivial)
-[wp] 5 goals scheduled
+[wp] 6 goals scheduled
+[wp] [Valid] bytes_null_check (Alt-Ergo) (Cached)
[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
+[wp] [Valid] bytes_addr_local_ko_check (Alt-Ergo) (Cached)
+[wp] [Valid] bytes_pointer_param_check (Alt-Ergo) (Cached)
+[wp] Proved goals: 18 / 18
+ Terminating: 6
+ Unreachable: 6
+ Alt-Ergo: 6
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
+ null - 1 1 100%
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%
+ addr_local_ko - 1 1 100%
+ pointer_param - 1 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bytes/pointers.i b/src/plugins/wp/tests/wp_bytes/pointers.i
index eb7ca1de529..1f7e8530bd2 100644
--- a/src/plugins/wp/tests/wp_bytes/pointers.i
+++ b/src/plugins/wp/tests/wp_bytes/pointers.i
@@ -1,43 +1,51 @@
typedef unsigned char uint8 ;
-int x ;
+void null(void){
+ uint8 buffer[sizeof(int*)] ;
+ *((int**) buffer) = (void*) 0 ;
+
+ int* r = *((int**) buffer) ;
+ //@ check r == \null ;
+}
+
+int g ;
void addr_glob(void){
uint8 buffer[sizeof(int*)] ;
- *((int**) buffer) = &x ;
+ *((int**) buffer) = &g ;
int* r = *((int**) buffer) ;
- //@ check r == &x ;
+ //@ check r == &g ;
}
-void addr_formal(int x){
+void addr_formal(int f){
uint8 buffer[sizeof(int*)] ;
- *((int**) buffer) = &x ;
+ *((int**) buffer) = &f ;
int* r = *((int**) buffer) ;
- //@ check r == &x ;
+ //@ check r == &f ;
}
void addr_local_ok(void){
- int x = 0;
+ int l = 0;
uint8 buffer[sizeof(int*)] ;
- *((int**) buffer) = &x ;
+ *((int**) buffer) = &l ;
int* r = *((int**) buffer) ;
- //@ check P: r == &x ;
+ //@ check P: r == &l ;
}
void addr_local_ko(void){
uint8 buffer[sizeof(int*)] ;
{
- int x ;
- *((int**) buffer) = &x ;
+ int l ;
+ *((int**) buffer) = &l ;
}
int* r = *((int**) buffer) ;
- //@ check r == &x ;
+ //@ check ! \valid(r) ;
}
//@ requires \valid(f);
--
GitLab