Commit 2f39567a authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] renamed compound operations

parent 85c0b2e5
...@@ -159,7 +159,7 @@ struct ...@@ -159,7 +159,7 @@ struct
(Lang.generated_p (C.prefix ^ Lang.comp_id c)) (Lang.generated_p (C.prefix ^ Lang.comp_id c))
(fun lfun -> (fun lfun ->
let basename = if c.cstruct then "S" else "U" in let basename = if c.cstruct then "S" else "U" in
let s = Lang.freshvar ~basename (Lang.tau_of_comp c) in let s = Lang.freshvar ~basename (Lang.t_comp c) in
let def = p_all let def = p_all
(fun f -> (fun f ->
is_typ f.ftype (e_getfield (e_var s) (Lang.Cfield (f, KValue)))) is_typ f.ftype (e_getfield (e_var s) (Lang.Cfield (f, KValue))))
...@@ -303,8 +303,9 @@ module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo) ...@@ -303,8 +303,9 @@ module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
Lang.F.set_builtin lfun reduce_eqcomp ; Lang.F.set_builtin lfun reduce_eqcomp ;
(* Definition of the symbol *) (* Definition of the symbol *)
let basename = if c.cstruct then "S" else "U" in let basename = if c.cstruct then "S" else "U" in
let xa = Lang.freshvar ~basename (Lang.tau_of_comp c) in let tc = Lang.t_comp c in
let xb = Lang.freshvar ~basename (Lang.tau_of_comp c) in let xa = Lang.freshvar ~basename tc in
let xb = Lang.freshvar ~basename tc in
let ra = e_var xa in let ra = e_var xa in
let rb = e_var xb in let rb = e_var xb in
let def = p_all let def = p_all
......
...@@ -180,38 +180,37 @@ let sort_of_ltype t = match Logic_utils.unroll_type ~unroll_typedef:false t with ...@@ -180,38 +180,37 @@ let sort_of_ltype t = match Logic_utils.unroll_type ~unroll_typedef:false t with
| Linteger -> Logic.Sint | Linteger -> Logic.Sint
| Lreal -> Logic.Sreal | Lreal -> Logic.Sreal
let tau_of_comp c = Logic.Data(Comp (c, KValue),[])
let t_int = Logic.Int let t_int = Logic.Int
let t_bool = Logic.Bool let t_bool = Logic.Bool
let t_real = Logic.Real let t_real = Logic.Real
let t_prop = Logic.Prop let t_prop = Logic.Prop
let t_addr () = Context.get pointer let t_addr () = Context.get pointer
let t_float f = Context.get floats f
let t_comp c = Logic.Data(Comp (c, KValue),[])
let t_init c = Logic.Data(Comp (c, KInit), [])
let t_array a = Logic.Array(Logic.Int,a) let t_array a = Logic.Array(Logic.Int,a)
let t_farray a b = Logic.Array(a,b) let t_farray a b = Logic.Array(a,b)
let t_datatype adt ts = Logic.Data(adt,ts) let t_datatype adt ts = Logic.Data(adt,ts)
let rec t_matrix a n = if n > 0 then t_matrix (t_array a) (pred n) else a
let rec tau_of_object = function let rec tau_of_object = function
| C_int _ -> Logic.Int | C_int _ -> Logic.Int
| C_float f -> Context.get floats f | C_float f -> t_float f
| C_comp c -> tau_of_comp c
| C_pointer _ -> Context.get pointer | C_pointer _ -> Context.get pointer
| C_comp c -> t_comp c
| C_array { arr_element = typ } -> t_array (tau_of_ctype typ) | C_array { arr_element = typ } -> t_array (tau_of_ctype typ)
and tau_of_ctype typ = tau_of_object (Ctypes.object_of typ) and tau_of_ctype typ = tau_of_object (Ctypes.object_of typ)
let init_of_comp c = Logic.Data(Comp (c, KInit), [])
let poly = Context.create "Wp.Lang.poly" let poly = Context.create "Wp.Lang.poly"
let rec init_of_object = function let rec init_of_object = function
| C_int _ | C_float _ | C_pointer _ -> Logic.Bool | C_int _ | C_float _ | C_pointer _ -> Logic.Bool
| C_comp c -> init_of_comp c | C_comp c -> t_init c
| C_array { arr_element = typ } -> t_array (init_of_ctype typ) | C_array { arr_element = typ } -> t_array (init_of_ctype typ)
and init_of_ctype typ = init_of_object (Ctypes.object_of typ) and init_of_ctype typ = init_of_object (Ctypes.object_of typ)
let rec varpoly k x = function let rec varpoly k x = function
| [] -> Warning.error "Unbound type parameter <%s>" x | [] -> Warning.error "Unbound type parameter <%s>" x
| y::ys -> if x = y then k else varpoly (succ k) x ys | y::ys -> if x = y then k else varpoly (succ k) x ys
...@@ -370,8 +369,8 @@ let tau_of_field = function ...@@ -370,8 +369,8 @@ let tau_of_field = function
let tau_of_record = function let tau_of_record = function
| Mfield(mdt,fs,_,_) -> Logic.Data(Mrecord(mdt,fs),[]) | Mfield(mdt,fs,_,_) -> Logic.Data(Mrecord(mdt,fs),[])
| Cfield(f, KValue) -> tau_of_comp f.fcomp | Cfield(f, KValue) -> t_comp f.fcomp
| Cfield(f, KInit) -> init_of_comp f.fcomp | Cfield(f, KInit) -> t_init f.fcomp
module Field = module Field =
struct struct
......
...@@ -160,7 +160,6 @@ val extern_t: ...@@ -160,7 +160,6 @@ val extern_t:
(** {2 Sorting and Typing} *) (** {2 Sorting and Typing} *)
val tau_of_comp : compinfo -> tau
val tau_of_object : c_object -> tau val tau_of_object : c_object -> tau
val tau_of_ctype : typ -> tau val tau_of_ctype : typ -> tau
val tau_of_ltype : logic_type -> tau val tau_of_ltype : logic_type -> tau
...@@ -169,7 +168,6 @@ val tau_of_lfun : lfun -> tau option list -> tau ...@@ -169,7 +168,6 @@ val tau_of_lfun : lfun -> tau option list -> tau
val tau_of_field : field -> tau val tau_of_field : field -> tau
val tau_of_record : field -> tau val tau_of_record : field -> tau
val init_of_comp : compinfo -> tau
val init_of_object : c_object -> tau val init_of_object : c_object -> tau
val init_of_ctype : typ -> tau val init_of_ctype : typ -> tau
...@@ -178,9 +176,13 @@ val t_real : tau ...@@ -178,9 +176,13 @@ val t_real : tau
val t_bool : tau val t_bool : tau
val t_prop : tau val t_prop : tau
val t_addr : unit -> tau val t_addr : unit -> tau
val t_comp : compinfo -> tau
val t_init : compinfo -> tau
val t_float : c_float -> tau
val t_array : tau -> tau val t_array : tau -> tau
val t_farray : tau -> tau -> tau val t_farray : tau -> tau -> tau
val t_datatype : adt -> tau list -> tau val t_datatype : adt -> tau list -> tau
val t_matrix : tau -> int -> tau
val pointer : tau Context.value (** type of pointers *) val pointer : tau Context.value (** type of pointers *)
val floats : (c_float -> tau) Context.value (** type of floats *) val floats : (c_float -> tau) Context.value (** type of floats *)
......
...@@ -189,7 +189,7 @@ struct ...@@ -189,7 +189,7 @@ struct
let obj = C_comp c in let obj = C_comp c in
let loc = M.of_region_pointer r obj v in (* t_pointer -> loc *) let loc = M.of_region_pointer r obj v in (* t_pointer -> loc *)
let domain = M.value_footprint obj loc in let domain = M.value_footprint obj loc in
let result = Lang.tau_of_comp c in let result = Lang.t_comp c in
let lfun = let lfun =
Lang.generated_f ~result "Load%a_%s" pp_rid r (Lang.comp_id c) Lang.generated_f ~result "Load%a_%s" pp_rid r (Lang.comp_id c)
in in
......
...@@ -338,7 +338,7 @@ module ShiftGen = WpContext.StaticGenerator(Cobj) ...@@ -338,7 +338,7 @@ module ShiftGen = WpContext.StaticGenerator(Cobj)
| C_int i -> pp_int fmt i | C_int i -> pp_int fmt i
| C_float f -> pp_float fmt f | C_float f -> pp_float fmt f
| C_pointer _ -> Format.fprintf fmt "PTR" | C_pointer _ -> Format.fprintf fmt "PTR"
| C_comp c -> Format.pp_print_string fmt c.cname | C_comp c -> Format.pp_print_string fmt (Lang.comp_id c)
| C_array a -> | C_array a ->
let te = object_of a.arr_element in let te = object_of a.arr_element in
match a.arr_flat with match a.arr_flat with
......
...@@ -39,7 +39,7 @@ ...@@ -39,7 +39,7 @@
Goal Post-condition (file tests/wp_acsl/logic.i, line 21) in 'h': Goal Post-condition (file tests/wp_acsl/logic.i, line 21) in 'h':
Let a = global(G_t_29). Let a = global(G_t_29).
Let m = Array1_S1(shift___anonstruct_Point_1(a, 0), 3, Mint_0). Let m = Array1_S1(shift_S1(a, 0), 3, Mint_0).
Let m_1 = Array1_S1(a, 3, Mint_0). Let m_1 = Array1_S1(a, 3, Mint_0).
Assume { Type: IsArray1S1(m_1) /\ IsArray1S1(m). (* Call 'f' *) Have: P_P(m). Assume { Type: IsArray1S1(m_1) /\ IsArray1S1(m). (* Call 'f' *) Have: P_P(m).
} }
...@@ -67,9 +67,9 @@ Prove: true. ...@@ -67,9 +67,9 @@ Prove: true.
Goal Pre-condition 'qed_ok' in 'main': Goal Pre-condition 'qed_ok' in 'main':
Let a = global(G_tr_35). Let a = global(G_tr_35).
Let a_1 = shift___anonstruct_Point_1(a, 2). Let a_1 = shift_S1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1). Let a_2 = shift_S1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0). Let a_3 = shift_S1(a, 0).
Let m = Array1_S1(a, 3, Mint_0). Let m = Array1_S1(a, 3, Mint_0).
Assume { Assume {
Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)). Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
...@@ -92,9 +92,9 @@ Prove: P_P(m). ...@@ -92,9 +92,9 @@ Prove: P_P(m).
Goal Pre-condition 'qed_ok' in 'main': Goal Pre-condition 'qed_ok' in 'main':
Let a = global(G_tr_35). Let a = global(G_tr_35).
Let a_1 = shift___anonstruct_Point_1(a, 2). Let a_1 = shift_S1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1). Let a_2 = shift_S1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0). Let a_3 = shift_S1(a, 0).
Let m = Array1_S1(a, 3, Mint_0). Let m = Array1_S1(a, 3, Mint_0).
Assume { Assume {
Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)). Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
...@@ -117,9 +117,9 @@ Prove: P_P(m). ...@@ -117,9 +117,9 @@ Prove: P_P(m).
Goal Pre-condition 'qed_ok' in 'main': Goal Pre-condition 'qed_ok' in 'main':
Let a = global(G_tr_35). Let a = global(G_tr_35).
Let a_1 = shift___anonstruct_Point_1(a, 2). Let a_1 = shift_S1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1). Let a_2 = shift_S1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0). Let a_3 = shift_S1(a, 0).
Let m = Array1_S1(a_3, 3, Mint_0). Let m = Array1_S1(a_3, 3, Mint_0).
Assume { Assume {
Type: IsArray1S1(Array1_S1(a, 3, Mint_0)) /\ IsArray1S1(m). Type: IsArray1S1(Array1_S1(a, 3, Mint_0)) /\ IsArray1S1(m).
......
...@@ -15,11 +15,10 @@ Assume { ...@@ -15,11 +15,10 @@ Assume {
(* Heap *) (* Heap *)
Type: (region(tbl_0.base) <= 0) /\ linked(Malloc_0). Type: (region(tbl_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *) (* Goal *)
When: !invalid(Malloc_0, When: !invalid(Malloc_0, shiftfield_F1_size(shift_S1(a, x)), 1).
shiftfield_F1_size(shift___anonstruct_Buckets_1(a, x)), 1).
(* Pre-condition *) (* Pre-condition *)
Have: (0 <= d) /\ (d <= 16) /\ valid_rw(Malloc_0, tbl_0, 35) /\ Have: (0 <= d) /\ (d <= 16) /\ valid_rw(Malloc_0, tbl_0, 35) /\
valid_rw(Malloc_0, shift___anonstruct_Buckets_1(a, 0), 34). valid_rw(Malloc_0, shift_S1(a, 0), 34).
} }
Prove: (x <= d) /\ (d <= x). Prove: (x <= d) /\ (d <= x).
......
...@@ -204,7 +204,7 @@ Prove: true. ...@@ -204,7 +204,7 @@ Prove: true.
Goal Post-condition 'Preset_5_tps' in 'call_reset_5_tps': Goal Post-condition 'Preset_5_tps' in 'call_reset_5_tps':
Let a = tps_0[9]. Let a = tps_0[9].
Let a_1 = shift_T(a, 0). Let a_1 = shift_S1_T(a, 0).
Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, 10). Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, 10).
Assume { Assume {
(* Heap *) (* Heap *)
...@@ -215,9 +215,9 @@ Assume { ...@@ -215,9 +215,9 @@ Assume {
Have: valid_rw(Malloc_0, a_1, 10). Have: valid_rw(Malloc_0, a_1, 10).
(* Call 'reset_5' *) (* Call 'reset_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
(a_2[shiftfield_F1_T_a(shift_T(a, i_1))] = 0))). (a_2[shiftfield_F1_T_a(shift_S1_T(a, i_1))] = 0))).
} }
Prove: a_2[shiftfield_F1_T_a(shift_T(a, i))] = 0. Prove: a_2[shiftfield_F1_T_a(shift_S1_T(a, i))] = 0.
------------------------------------------------------------ ------------------------------------------------------------
......
...@@ -37,7 +37,7 @@ Assume { ...@@ -37,7 +37,7 @@ Assume {
(* Assertion 'Ok_A' *) (* Assertion 'Ok_A' *)
Have: (0 <= i) /\ (i <= 9). Have: (0 <= i) /\ (i <= 9).
(* Call 'fopen' *) (* Call 'fopen' *)
Have: included(p, 2, shift___fc_FILE(global(G___fc_fopen_21), 0), 1024). Have: included(p, 2, shift_S4___fc_FILE(global(G___fc_fopen_21), 0), 1024).
} }
Prove: valid_rw(Malloc_0, p, 2). Prove: valid_rw(Malloc_0, p, 2).
......
...@@ -47,9 +47,7 @@ Prove: x_1 = x. ...@@ -47,9 +47,7 @@ Prove: x_1 = x.
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 27) in 'fits3': Goal Post-condition (file tests/wp_typed/cast_fits.i, line 27) in 'fits3':
Let x = Mint_0[shiftfield_F2_i2(p)]. Let x = Mint_0[shiftfield_F2_i2(p)].
Let x_1 = Mint_0 Let x_1 = Mint_0[shiftfield_F1_i1(shift_S1(shiftfield_F4_ic4(p), 0))].
[shiftfield_F1_i1(shift___anonstruct_L1_1(shiftfield_F4_ic4(p),
0))].
Assume { Assume {
Type: is_sint32(x) /\ is_sint32(x_1). Type: is_sint32(x) /\ is_sint32(x_1).
(* Heap *) (* Heap *)
...@@ -64,9 +62,7 @@ Prove: x_1 = x. ...@@ -64,9 +62,7 @@ Prove: x_1 = x.
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4': Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
Let x = Mchar_0[shiftfield_F6_c6(p)]. Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0 Let x_1 = Mchar_0[shiftfield_F3_c3(shift_S3(shiftfield_F5_ci5(p), 1))].
[shiftfield_F3_c3(shift___anonstruct_L3_3(shiftfield_F5_ci5(p),
1))].
Assume { Assume {
Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1). Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
(* Heap *) (* Heap *)
......
...@@ -47,9 +47,7 @@ Prove: x_1 = x. ...@@ -47,9 +47,7 @@ Prove: x_1 = x.
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 27) in 'fits3': Goal Post-condition (file tests/wp_typed/cast_fits.i, line 27) in 'fits3':
Let x = Mint_0[shiftfield_F2_i2(p)]. Let x = Mint_0[shiftfield_F2_i2(p)].
Let x_1 = Mint_0 Let x_1 = Mint_0[shiftfield_F1_i1(shift_S1(shiftfield_F4_ic4(p), 0))].
[shiftfield_F1_i1(shift___anonstruct_L1_1(shiftfield_F4_ic4(p),
0))].
Assume { Assume {
Type: is_sint32(x) /\ is_sint32(x_1). Type: is_sint32(x) /\ is_sint32(x_1).
(* Heap *) (* Heap *)
...@@ -64,9 +62,7 @@ Prove: x_1 = x. ...@@ -64,9 +62,7 @@ Prove: x_1 = x.
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4': Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
Let x = Mchar_0[shiftfield_F6_c6(p)]. Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0 Let x_1 = Mchar_0[shiftfield_F3_c3(shift_S3(shiftfield_F5_ci5(p), 1))].
[shiftfield_F3_c3(shift___anonstruct_L3_3(shiftfield_F5_ci5(p),
1))].
Assume { Assume {
Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1). Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
(* Heap *) (* Heap *)
......
...@@ -11,8 +11,8 @@ Let x = Mint_0[shiftfield_F2_s_d(p)]. ...@@ -11,8 +11,8 @@ Let x = Mint_0[shiftfield_F2_s_d(p)].
Let a = shiftfield_F2_s_u(p). Let a = shiftfield_F2_s_u(p).
Assume { Assume {
Type: is_sint32(x) /\ is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\ Type: is_sint32(x) /\ is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\
is_sint32(Mint_0[shiftfield_F1_t_c(shift_t(a, 0))]) /\ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
is_sint32(Mint_0[shiftfield_F1_t_c(shift_t(a, 1))]). is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
(* Heap *) (* Heap *)
Type: region(p.base) <= 0. Type: region(p.base) <= 0.
(* Pre-condition *) (* Pre-condition *)
...@@ -26,8 +26,8 @@ Goal Assertion (file tests/wp_typed/shift_lemma.i, line 22): ...@@ -26,8 +26,8 @@ Goal Assertion (file tests/wp_typed/shift_lemma.i, line 22):
Let a = shiftfield_F2_s_u(p). Let a = shiftfield_F2_s_u(p).
Assume { Assume {
Type: is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\ Type: is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\
is_sint32(Mint_0[shiftfield_F1_t_c(shift_t(a, 0))]) /\ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
is_sint32(Mint_0[shiftfield_F1_t_c(shift_t(a, 1))]). is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
(* Heap *) (* Heap *)
Type: region(p.base) <= 0. Type: region(p.base) <= 0.
(* Goal *) (* Goal *)
...@@ -37,7 +37,7 @@ Assume { ...@@ -37,7 +37,7 @@ Assume {
(* Assertion *) (* Assertion *)
Have: Mint_0[shiftfield_F2_s_d(p)] = 0. Have: Mint_0[shiftfield_F2_s_d(p)] = 0.
} }
Prove: Mint_0[shiftfield_F1_t_c(shift_t(a, i))] = 0. Prove: Mint_0[shiftfield_F1_t_c(shift_S1_t(a, i))] = 0.
------------------------------------------------------------ ------------------------------------------------------------
...@@ -63,7 +63,7 @@ Assume { ...@@ -63,7 +63,7 @@ Assume {
Have: Mint_0[shiftfield_F2_s_d(p)] = 0. Have: Mint_0[shiftfield_F2_s_d(p)] = 0.
(* Assertion *) (* Assertion *)
Have: forall i : Z. ((0 <= i) -> ((i <= 9) -> Have: forall i : Z. ((0 <= i) -> ((i <= 9) ->
(Mint_0[shiftfield_F1_t_c(shift_t(shiftfield_F2_s_u(p), i))] = 0))). (Mint_0[shiftfield_F1_t_c(shift_S1_t(shiftfield_F2_s_u(p), i))] = 0))).
} }
Prove: x = 0. Prove: x = 0.
......
...@@ -11,8 +11,8 @@ Let x = Mint_0[shiftfield_F2_s_d(p)]. ...@@ -11,8 +11,8 @@ Let x = Mint_0[shiftfield_F2_s_d(p)].
Let a = shiftfield_F2_s_u(p). Let a = shiftfield_F2_s_u(p).
Assume { Assume {
Type: is_sint32(x) /\ is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\ Type: is_sint32(x) /\ is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\
is_sint32(Mint_0[shiftfield_F1_t_c(shift_t(a, 0))]) /\ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
is_sint32(Mint_0[shiftfield_F1_t_c(shift_t(a, 1))]). is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
(* Heap *) (* Heap *)
Type: region(p.base) <= 0. Type: region(p.base) <= 0.
(* Pre-condition *) (* Pre-condition *)
...@@ -26,8 +26,8 @@ Goal Assertion (file tests/wp_typed/shift_lemma.i, line 22): ...@@ -26,8 +26,8 @@ Goal Assertion (file tests/wp_typed/shift_lemma.i, line 22):
Let a = shiftfield_F2_s_u(p). Let a = shiftfield_F2_s_u(p).
Assume { Assume {
Type: is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\ Type: is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\
is_sint32(Mint_0[shiftfield_F1_t_c(shift_t(a, 0))]) /\ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
is_sint32(Mint_0[shiftfield_F1_t_c(shift_t(a, 1))]). is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
(* Heap *) (* Heap *)
Type: region(p.base) <= 0. Type: region(p.base) <= 0.
(* Goal *) (* Goal *)
...@@ -37,7 +37,7 @@ Assume { ...@@ -37,7 +37,7 @@ Assume {
(* Assertion *) (* Assertion *)
Have: Mint_0[shiftfield_F2_s_d(p)] = 0. Have: Mint_0[shiftfield_F2_s_d(p)] = 0.
} }
Prove: Mint_0[shiftfield_F1_t_c(shift_t(a, i))] = 0. Prove: Mint_0[shiftfield_F1_t_c(shift_S1_t(a, i))] = 0.
------------------------------------------------------------ ------------------------------------------------------------
...@@ -63,7 +63,7 @@ Assume { ...@@ -63,7 +63,7 @@ Assume {
Have: Mint_0[shiftfield_F2_s_d(p)] = 0. Have: Mint_0[shiftfield_F2_s_d(p)] = 0.
(* Assertion *) (* Assertion *)
Have: forall i : Z. ((0 <= i) -> ((i <= 9) -> Have: forall i : Z. ((0 <= i) -> ((i <= 9) ->
(Mint_0[shiftfield_F1_t_c(shift_t(shiftfield_F2_s_u(p), i))] = 0))). (Mint_0[shiftfield_F1_t_c(shift_S1_t(shiftfield_F2_s_u(p), i))] = 0))).
} }
Prove: x = 0. Prove: x = 0.
......
...@@ -8,59 +8,59 @@ ...@@ -8,59 +8,59 @@
Goal Post-condition (file tests/wp_usage/caveat_range.i, line 12) in 'reset': Goal Post-condition (file tests/wp_usage/caveat_range.i, line 12) in 'reset':
Let a = global(G_p_22). Let a = global(G_p_22).
Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S(a, 0), 20). Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
Assume { Assume {
Type: is_sint32(i_1). Type: is_sint32(i_1).
(* Goal *) (* Goal *)
When: (0 <= i) /\ (i <= 9). When: (0 <= i) /\ (i <= 9).
(* Invariant *) (* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_1[shiftfield_F1_S_g(shift_S(a, i_2))] = 2))). (a_1[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
(* Invariant *) (* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_1[shiftfield_F1_S_f(shift_S(a, i_2))] = 1))). (a_1[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
(* Invariant *) (* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10). Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *) (* Else *)
Have: 10 <= i_1. Have: 10 <= i_1.
} }
Prove: a_1[shiftfield_F1_S_f(shift_S(a, i))] = 1. Prove: a_1[shiftfield_F1_S_f(shift_S1_S(a, i))] = 1.
------------------------------------------------------------ ------------------------------------------------------------
Goal Post-condition (file tests/wp_usage/caveat_range.i, line 13) in 'reset': Goal Post-condition (file tests/wp_usage/caveat_range.i, line 13) in 'reset':
Let a = global(G_p_22). Let a = global(G_p_22).
Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S(a, 0), 20). Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
Assume { Assume {
Type: is_sint32(i_1). Type: is_sint32(i_1).
(* Goal *) (* Goal *)
When: (0 <= i) /\ (i <= 9). When: (0 <= i) /\ (i <= 9).
(* Invariant *) (* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_1[shiftfield_F1_S_g(shift_S(a, i_2))] = 2))). (a_1[shiftfield_F1_S_g(shift_S1_S(a, i_2))] = 2))).
(* Invariant *) (* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_1[shiftfield_F1_S_f(shift_S(a, i_2))] = 1))). (a_1[shiftfield_F1_S_f(shift_S1_S(a, i_2))] = 1))).
(* Invariant *) (* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10). Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *) (* Else *)
Have: 10 <= i_1. Have: 10 <= i_1.
} }
Prove: a_1[shiftfield_F1_S_g(shift_S(a, i))] = 2. Prove: a_1[shiftfield_F1_S_g(shift_S1_S(a, i))] = 2.
------------------------------------------------------------ ------------------------------------------------------------
Goal Preservation of Invariant (file tests/wp_usage/caveat_range.i, line 19): Goal Preservation of Invariant (file tests/wp_usage/caveat_range.i, line 19):
Let a = global(G_p_22). Let a = global(G_p_22).
Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S(a, 0), 20). Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
Assume { Assume {
Type: is_sint32(i) /\ is_sint32(1 + i). Type: is_sint32(i) /\ is_sint32(1 + i).
(* Invariant *) (* Invariant *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
(a_1[shiftfield_F1_S_g(shift_S(a, i_1))] = 2))). (a_1[shiftfield_F1_S_g(shift_S1_S(a, i_1))] = 2))).
(* Invariant *) (* Invariant *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
(a_1[shiftfield_F1_S_f(shift_S(a, i_1))] = 1))). (a_1[shiftfield_F1_S_f(shift_S1_S(a, i_1))] = 1))).
(* Invariant *) (* Invariant *)
Have: (0 <= i) /\ (i <= 10). Have: (0 <= i) /\ (i <= 10).
(* Then *) (* Then *)
...@@ -77,24 +77,24 @@ Prove: true. ...@@ -77,24 +77,24 @@ Prove: true.
Goal Preservation of Invariant (file tests/wp_usage/caveat_range.i, line 20):