From 2f39567a897df31bbc013f70ec4c654536ff8798 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 15 Oct 2020 12:08:26 +0200
Subject: [PATCH] [wp] renamed compound operations
---
src/plugins/wp/Cvalues.ml | 7 ++--
src/plugins/wp/Lang.ml | 19 ++++-----
src/plugins/wp/Lang.mli | 6 ++-
src/plugins/wp/MemLoader.ml | 2 +-
src/plugins/wp/MemTyped.ml | 2 +-
.../wp/tests/wp_acsl/oracle/logic.res.oracle | 20 ++++-----
.../tests/wp_bts/oracle/issue_508.res.oracle | 5 +--
.../oracle/reference_and_struct.res.oracle | 6 +--
.../wp_plugin/oracle/subset_fopen.res.oracle | 2 +-
.../wp_typed/oracle/cast_fits.0.res.oracle | 8 +---
.../wp_typed/oracle/cast_fits.1.res.oracle | 8 +---
.../wp_typed/oracle/shift_lemma.0.res.oracle | 12 +++---
.../wp_typed/oracle/shift_lemma.1.res.oracle | 12 +++---
.../wp_usage/oracle/caveat_range.res.oracle | 42 +++++++++----------
14 files changed, 72 insertions(+), 79 deletions(-)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 7fba0357ad0..216b2cedafe 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -159,7 +159,7 @@ struct
(Lang.generated_p (C.prefix ^ Lang.comp_id c))
(fun lfun ->
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
(fun f ->
is_typ f.ftype (e_getfield (e_var s) (Lang.Cfield (f, KValue))))
@@ -303,8 +303,9 @@ module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
Lang.F.set_builtin lfun reduce_eqcomp ;
(* Definition of the symbol *)
let basename = if c.cstruct then "S" else "U" in
- let xa = Lang.freshvar ~basename (Lang.tau_of_comp c) in
- let xb = Lang.freshvar ~basename (Lang.tau_of_comp c) in
+ let tc = Lang.t_comp c in
+ let xa = Lang.freshvar ~basename tc in
+ let xb = Lang.freshvar ~basename tc in
let ra = e_var xa in
let rb = e_var xb in
let def = p_all
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index c4c9997e469..bb621655ffe 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -180,38 +180,37 @@ let sort_of_ltype t = match Logic_utils.unroll_type ~unroll_typedef:false t with
| Linteger -> Logic.Sint
| Lreal -> Logic.Sreal
-let tau_of_comp c = Logic.Data(Comp (c, KValue),[])
-
let t_int = Logic.Int
let t_bool = Logic.Bool
let t_real = Logic.Real
let t_prop = Logic.Prop
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_farray a b = Logic.Array(a,b)
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
| C_int _ -> Logic.Int
- | C_float f -> Context.get floats f
- | C_comp c -> tau_of_comp c
+ | C_float f -> t_float f
| C_pointer _ -> Context.get pointer
+ | C_comp c -> t_comp c
| C_array { arr_element = typ } -> t_array (tau_of_ctype 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 rec init_of_object = function
| 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)
and init_of_ctype typ = init_of_object (Ctypes.object_of typ)
-
let rec varpoly k x = function
| [] -> Warning.error "Unbound type parameter <%s>" x
| y::ys -> if x = y then k else varpoly (succ k) x ys
@@ -370,8 +369,8 @@ let tau_of_field = function
let tau_of_record = function
| Mfield(mdt,fs,_,_) -> Logic.Data(Mrecord(mdt,fs),[])
- | Cfield(f, KValue) -> tau_of_comp f.fcomp
- | Cfield(f, KInit) -> init_of_comp f.fcomp
+ | Cfield(f, KValue) -> t_comp f.fcomp
+ | Cfield(f, KInit) -> t_init f.fcomp
module Field =
struct
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index d8a13b4ad92..0b9750495aa 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -160,7 +160,6 @@ val extern_t:
(** {2 Sorting and Typing} *)
-val tau_of_comp : compinfo -> tau
val tau_of_object : c_object -> tau
val tau_of_ctype : typ -> tau
val tau_of_ltype : logic_type -> tau
@@ -169,7 +168,6 @@ val tau_of_lfun : lfun -> tau option list -> tau
val tau_of_field : field -> tau
val tau_of_record : field -> tau
-val init_of_comp : compinfo -> tau
val init_of_object : c_object -> tau
val init_of_ctype : typ -> tau
@@ -178,9 +176,13 @@ val t_real : tau
val t_bool : tau
val t_prop : 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_farray : tau -> tau -> tau
val t_datatype : adt -> tau list -> tau
+val t_matrix : tau -> int -> tau
val pointer : tau Context.value (** type of pointers *)
val floats : (c_float -> tau) Context.value (** type of floats *)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index b1abfb6af8f..734097fb74a 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -189,7 +189,7 @@ struct
let obj = C_comp c in
let loc = M.of_region_pointer r obj v in (* t_pointer -> loc *)
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 =
Lang.generated_f ~result "Load%a_%s" pp_rid r (Lang.comp_id c)
in
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 36c8e0facd5..041f4844363 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -338,7 +338,7 @@ module ShiftGen = WpContext.StaticGenerator(Cobj)
| C_int i -> pp_int fmt i
| C_float f -> pp_float fmt f
| 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 ->
let te = object_of a.arr_element in
match a.arr_flat with
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index 631003d71ae..b941722cdbd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -39,7 +39,7 @@
Goal Post-condition (file tests/wp_acsl/logic.i, line 21) in 'h':
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).
Assume { Type: IsArray1S1(m_1) /\ IsArray1S1(m). (* Call 'f' *) Have: P_P(m).
}
@@ -67,9 +67,9 @@ Prove: true.
Goal Pre-condition 'qed_ok' in 'main':
Let a = global(G_tr_35).
-Let a_1 = shift___anonstruct_Point_1(a, 2).
-Let a_2 = shift___anonstruct_Point_1(a, 1).
-Let a_3 = shift___anonstruct_Point_1(a, 0).
+Let a_1 = shift_S1(a, 2).
+Let a_2 = shift_S1(a, 1).
+Let a_3 = shift_S1(a, 0).
Let m = Array1_S1(a, 3, Mint_0).
Assume {
Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
@@ -92,9 +92,9 @@ Prove: P_P(m).
Goal Pre-condition 'qed_ok' in 'main':
Let a = global(G_tr_35).
-Let a_1 = shift___anonstruct_Point_1(a, 2).
-Let a_2 = shift___anonstruct_Point_1(a, 1).
-Let a_3 = shift___anonstruct_Point_1(a, 0).
+Let a_1 = shift_S1(a, 2).
+Let a_2 = shift_S1(a, 1).
+Let a_3 = shift_S1(a, 0).
Let m = Array1_S1(a, 3, Mint_0).
Assume {
Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
@@ -117,9 +117,9 @@ Prove: P_P(m).
Goal Pre-condition 'qed_ok' in 'main':
Let a = global(G_tr_35).
-Let a_1 = shift___anonstruct_Point_1(a, 2).
-Let a_2 = shift___anonstruct_Point_1(a, 1).
-Let a_3 = shift___anonstruct_Point_1(a, 0).
+Let a_1 = shift_S1(a, 2).
+Let a_2 = shift_S1(a, 1).
+Let a_3 = shift_S1(a, 0).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
Type: IsArray1S1(Array1_S1(a, 3, Mint_0)) /\ IsArray1S1(m).
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle
index 69016b5d1ff..3e0d3075cbf 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle
@@ -15,11 +15,10 @@ Assume {
(* Heap *)
Type: (region(tbl_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: !invalid(Malloc_0,
- shiftfield_F1_size(shift___anonstruct_Buckets_1(a, x)), 1).
+ When: !invalid(Malloc_0, shiftfield_F1_size(shift_S1(a, x)), 1).
(* Pre-condition *)
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).
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index 49db1a0e743..d6202c41035 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -204,7 +204,7 @@ Prove: true.
Goal Post-condition 'Preset_5_tps' in 'call_reset_5_tps':
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).
Assume {
(* Heap *)
@@ -215,9 +215,9 @@ Assume {
Have: valid_rw(Malloc_0, a_1, 10).
(* Call 'reset_5' *)
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.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
index 00afcb0afdf..dff824a3ae2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
@@ -37,7 +37,7 @@ Assume {
(* Assertion 'Ok_A' *)
Have: (0 <= i) /\ (i <= 9).
(* 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).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
index 175f532ae7f..d6b74e7cf50 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
@@ -47,9 +47,7 @@ Prove: x_1 = x.
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 27) in 'fits3':
Let x = Mint_0[shiftfield_F2_i2(p)].
-Let x_1 = Mint_0
- [shiftfield_F1_i1(shift___anonstruct_L1_1(shiftfield_F4_ic4(p),
- 0))].
+Let x_1 = Mint_0[shiftfield_F1_i1(shift_S1(shiftfield_F4_ic4(p), 0))].
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
(* Heap *)
@@ -64,9 +62,7 @@ Prove: x_1 = x.
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
Let x = Mchar_0[shiftfield_F6_c6(p)].
-Let x_1 = Mchar_0
- [shiftfield_F3_c3(shift___anonstruct_L3_3(shiftfield_F5_ci5(p),
- 1))].
+Let x_1 = Mchar_0[shiftfield_F3_c3(shift_S3(shiftfield_F5_ci5(p), 1))].
Assume {
Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
index 0db2247f414..9d3df4c1c60 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
@@ -47,9 +47,7 @@ Prove: x_1 = x.
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 27) in 'fits3':
Let x = Mint_0[shiftfield_F2_i2(p)].
-Let x_1 = Mint_0
- [shiftfield_F1_i1(shift___anonstruct_L1_1(shiftfield_F4_ic4(p),
- 0))].
+Let x_1 = Mint_0[shiftfield_F1_i1(shift_S1(shiftfield_F4_ic4(p), 0))].
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
(* Heap *)
@@ -64,9 +62,7 @@ Prove: x_1 = x.
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
Let x = Mchar_0[shiftfield_F6_c6(p)].
-Let x_1 = Mchar_0
- [shiftfield_F3_c3(shift___anonstruct_L3_3(shiftfield_F5_ci5(p),
- 1))].
+Let x_1 = Mchar_0[shiftfield_F3_c3(shift_S3(shiftfield_F5_ci5(p), 1))].
Assume {
Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
index 4d36bdaa42c..ec48cd67a6b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
@@ -11,8 +11,8 @@ Let x = Mint_0[shiftfield_F2_s_d(p)].
Let a = shiftfield_F2_s_u(p).
Assume {
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_t(a, 1))]).
+ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
+ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
(* Heap *)
Type: region(p.base) <= 0.
(* Pre-condition *)
@@ -26,8 +26,8 @@ Goal Assertion (file tests/wp_typed/shift_lemma.i, line 22):
Let a = shiftfield_F2_s_u(p).
Assume {
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_t(a, 1))]).
+ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
+ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
(* Heap *)
Type: region(p.base) <= 0.
(* Goal *)
@@ -37,7 +37,7 @@ Assume {
(* Assertion *)
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 {
Have: Mint_0[shiftfield_F2_s_d(p)] = 0.
(* Assertion *)
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.
diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
index 4b06e83a958..74d83866d55 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
@@ -11,8 +11,8 @@ Let x = Mint_0[shiftfield_F2_s_d(p)].
Let a = shiftfield_F2_s_u(p).
Assume {
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_t(a, 1))]).
+ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
+ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
(* Heap *)
Type: region(p.base) <= 0.
(* Pre-condition *)
@@ -26,8 +26,8 @@ Goal Assertion (file tests/wp_typed/shift_lemma.i, line 22):
Let a = shiftfield_F2_s_u(p).
Assume {
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_t(a, 1))]).
+ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
+ is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
(* Heap *)
Type: region(p.base) <= 0.
(* Goal *)
@@ -37,7 +37,7 @@ Assume {
(* Assertion *)
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 {
Have: Mint_0[shiftfield_F2_s_d(p)] = 0.
(* Assertion *)
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.
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
index 82cb1e098dc..ed2e13b4896 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
@@ -8,59 +8,59 @@
Goal Post-condition (file tests/wp_usage/caveat_range.i, line 12) in 'reset':
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 {
Type: is_sint32(i_1).
(* Goal *)
When: (0 <= i) /\ (i <= 9).
(* Invariant *)
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 *)
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 *)
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
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':
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 {
Type: is_sint32(i_1).
(* Goal *)
When: (0 <= i) /\ (i <= 9).
(* Invariant *)
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 *)
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 *)
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
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):
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 {
Type: is_sint32(i) /\ is_sint32(1 + i).
(* Invariant *)
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 *)
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 *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
@@ -77,24 +77,24 @@ Prove: true.
Goal Preservation of Invariant (file tests/wp_usage/caveat_range.i, line 20):
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 {
Type: is_sint32(i) /\ is_sint32(1 + i).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (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 *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (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 *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
}
-Prove: a_1[shiftfield_F1_S_f(shift_S(a, i)) <- 1]
- [shiftfield_F1_S_f(shift_S(a, i_1))] = 1.
+Prove: a_1[shiftfield_F1_S_f(shift_S1_S(a, i)) <- 1]
+ [shiftfield_F1_S_f(shift_S1_S(a, i_1))] = 1.
------------------------------------------------------------
@@ -105,25 +105,25 @@ Prove: true.
Goal Preservation of Invariant (file tests/wp_usage/caveat_range.i, line 21):
Let a = global(G_p_22).
-Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S(a, 0), 20).
-Let a_2 = shift_S(a, i).
+Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
+Let a_2 = shift_S1_S(a, i).
Assume {
Type: is_sint32(i) /\ is_sint32(1 + i).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (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 *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (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 *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
}
Prove: a_1[shiftfield_F1_S_f(a_2) <- 1][shiftfield_F1_S_g(a_2) <- 2]
- [shiftfield_F1_S_g(shift_S(a, i_1))] = 2.
+ [shiftfield_F1_S_g(shift_S1_S(a, i_1))] = 2.
------------------------------------------------------------
--
GitLab