Skip to content
Snippets Groups Projects
Commit c5882fde authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] bytes: use static_alloc

parent 79464946
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 184 additions and 459 deletions
src/plugins/wp/MemBytes.ml
+ 10
− 0
View file @ c5882fde
......@@ -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 ;
......
src/plugins/wp/tests/wp_bytes/oracle/assigns_sep.res.oracle
+ 3
− 3
View file @ c5882fde
......@@ -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)) ->
......
src/plugins/wp/tests/wp_bytes/oracle/floats.res.oracle
+ 2
− 14
View file @ c5882fde
......@@ -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).
......
src/plugins/wp/tests/wp_bytes/oracle/integers.res.oracle
+ 53
− 314
View file @ c5882fde
......@@ -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.
......
src/plugins/wp/tests/wp_bytes/oracle/pointers.res.oracle
+ 41
− 64
View file @ c5882fde
......@@ -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.
------------------------------------------------------------
src/plugins/wp/tests/wp_bytes/oracle/structs.res.oracle
+ 2
− 1
View file @ c5882fde
......@@ -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).
}
......
src/plugins/wp/tests/wp_bytes/oracle/union.res.oracle
+ 36
− 36
View file @ c5882fde
......@@ -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 *)
......
src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle
+ 4
− 5
View file @ c5882fde
......@@ -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%
------------------------------------------------------------
src/plugins/wp/tests/wp_bytes/oracle_qualif/pointers.res.oracle
+ 13
− 10
View file @ c5882fde
......@@ -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%
------------------------------------------------------------
src/plugins/wp/tests/wp_bytes/pointers.i
+ 20
− 12
View file @ c5882fde
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);
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment