From a25e5e7eaff67b2e6efd91348360eab10b6127d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 15 Oct 2020 11:49:29 +0200
Subject: [PATCH] [wp] refactor matrix loaders
---
src/plugins/wp/Cvalues.ml | 82 ++++++++---
src/plugins/wp/Cvalues.mli | 4 +-
src/plugins/wp/Definitions.ml | 7 +-
src/plugins/wp/Definitions.mli | 3 +-
src/plugins/wp/LogicSemantics.ml | 8 +-
src/plugins/wp/Matrix.ml | 131 +++++++-----------
src/plugins/wp/Matrix.mli | 30 ++--
src/plugins/wp/MemLoader.ml | 127 ++++++++++-------
...signed_not_initialized_memtyped.res.oracle | 6 +-
.../wp/tests/wp_acsl/oracle/equal.res.oracle | 8 +-
.../wp_acsl/oracle/init_label.res.oracle | 2 +-
.../oracle/initialized_memtyped.res.oracle | 9 +-
.../wp/tests/wp_acsl/oracle/logic.res.oracle | 16 +--
.../wp/tests/wp_acsl/oracle/record.res.oracle | 2 +-
.../tests/wp_hoare/oracle/logicarr.res.oracle | 12 +-
.../wp_typed/oracle/user_collect.0.res.oracle | 44 +++---
.../wp_typed/oracle/user_collect.1.res.oracle | 44 +++---
17 files changed, 285 insertions(+), 250 deletions(-)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index a56d4459849..fe1589813a2 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -168,17 +168,24 @@ struct
})
[s]
- and is_array te ds t =
+ and is_array elt ds t =
Definitions.call_pred
- (Lang.generated_p (array_name te ds))
+ (Lang.generated_p (array_name elt ds))
(fun lfun ->
- let x = Lang.freshvar ~basename:"T" (Matrix.tau te ds) in
- let ks = List.map (fun _d -> Lang.freshvar ~basename:"k" Logic.Int) ds in
+ let cluster =
+ match elt with
+ | C_comp c -> Definitions.compinfo c
+ | _ -> Definitions.matrix () in
+ let te = Lang.tau_of_object elt in
+ let d = List.length ds in
+ let x = Lang.freshvar ~basename:"T" (Lang.t_matrix te d) in
+ let fk _d = Lang.freshvar ~basename:"k" Logic.Int in
+ let ks = List.map fk ds in
let e = List.fold_left (fun a k -> e_get a (e_var k)) (e_var x) ks in
- let def = p_forall ks (is_obj te e) in
+ let def = p_forall ks (is_obj elt e) in
{
d_lfun = lfun ; d_types = 0 ; d_params = [x] ;
- d_cluster = Definitions.matrix te ;
+ d_cluster = cluster ;
d_definition = Predicate(Def,def) ;
}
) [t]
@@ -250,34 +257,68 @@ let rec reduce_eqcomp = function
(* --- ACSL Array Equality --- *)
(* -------------------------------------------------------------------------- *)
-module EQARRAY = WpContext.Generator(Matrix.NATURAL)
+module AKEY =
+struct
+ type t = base * Matrix.t
+ and base = I | F of c_float | P | C of compinfo
+ let make elt ds =
+ let base = match elt with
+ | C_int _ -> I
+ | C_float f -> F f
+ | C_pointer _ -> P
+ | C_comp c -> C c
+ | C_array _ -> assert false
+ in base , ds
+ let key = function
+ | I -> "int"
+ | P -> "ptr"
+ | F f -> Ctypes.f_name f
+ | C c -> Lang.comp_id c
+ let cluster = function
+ | I | P | F _ -> Definitions.matrix ()
+ | C c -> Definitions.compinfo c
+ let tau = function
+ | I -> Lang.t_int
+ | F f -> Lang.t_float f
+ | P -> Lang.t_addr ()
+ | C c -> Lang.t_comp c
+ let equal = function
+ | I | F _ | P -> F.p_equal
+ | C c -> !equal_rec (C_comp c)
+ let compare (a,p) (b,q) =
+ let cmp = String.compare (key a) (key b) in
+ if cmp <> 0 then cmp else Matrix.compare p q
+ let pretty fmt (a,ds) =
+ Format.fprintf fmt "%s%a" (key a) Matrix.pp_suffix_id ds
+end
+
+module EQARRAY = WpContext.Generator(AKEY)
(struct
- open Matrix
let name = "Cvalues.EqArray"
- type key = matrix
+ type key = AKEY.t
type data = lfun
- let compile (te,ds) =
+ let compile (a,ds) =
(* Contextual Symbol *)
let lfun = Lang.generated_f
~context:true
~sort:Logic.Sprop
- "EqArray%s_%s" (Matrix.id ds) (Matrix.natural_id te) in
+ "EqArray_%s%a" (AKEY.key a) Matrix.pp_suffix_id ds in
(* Simplification of the symbol *)
Lang.F.set_builtin lfun reduce_eqcomp ;
(* Definition of the symbol *)
- let denv = Matrix.denv ds in
- let tau = Matrix.tau te ds in
+ let denv = Matrix.cc_env ds in
+ let tau = Matrix.cc_tau (AKEY.tau a) ds in
let xa = Lang.freshvar ~basename:"T" tau in
let xb = Lang.freshvar ~basename:"T" tau in
let ta = e_var xa in
let tb = e_var xb in
let ta_xs = List.fold_left e_get ta denv.index_val in
let tb_xs = List.fold_left e_get tb denv.index_val in
- let property = p_hyps (denv.index_range) (!equal_rec te ta_xs tb_xs) in
+ let property = p_hyps (denv.index_range) (AKEY.equal a ta_xs tb_xs) in
let definition = p_forall denv.index_var property in
(* Registration *)
Definitions.define_symbol {
- d_cluster = Definitions.matrix te ;
+ d_cluster = AKEY.cluster a ;
d_lfun = lfun ; d_types = 0 ;
d_params = denv.size_var @ [xa ; xb ] ;
d_definition = Predicate(Def,definition) ;
@@ -324,17 +365,20 @@ module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
(* --- ACSL Equality --- *)
(* -------------------------------------------------------------------------- *)
+type matrixinfo = c_object * int option list
+
let equal_comp c a b = p_call (EQCOMP.get c) [a;b]
let equal_array m a b =
- match m with
- | _obj , [None] -> p_equal a b
- | m -> p_call (EQARRAY.get m) (Matrix.size m @ [a;b])
+ let elt,ns = m in
+ let ds = Matrix.of_dims ns in
+ let ms = Matrix.cc_dims ns in
+ p_call (EQARRAY.get @@ AKEY.make elt ds) (ms @ [a;b])
let equal_object obj a b =
match obj with
| C_int _ | C_float _ | C_pointer _ -> p_equal a b
| C_comp c -> equal_comp c a b
- | C_array t -> equal_array (Matrix.of_array t) a b
+ | C_array m -> equal_array (Ctypes.array_dimensions m) a b
let () = equal_rec := equal_object
diff --git a/src/plugins/wp/Cvalues.mli b/src/plugins/wp/Cvalues.mli
index be11dc8ad66..6c113daf413 100644
--- a/src/plugins/wp/Cvalues.mli
+++ b/src/plugins/wp/Cvalues.mli
@@ -83,9 +83,11 @@ val volatile : ?warn:string -> unit -> bool
(** {2 ACSL Equality} *)
+type matrixinfo = c_object * int option list
+
val equal_object : c_object -> term -> term -> pred
val equal_comp : compinfo -> term -> term -> pred
-val equal_array : Matrix.matrix -> term -> term -> pred
+val equal_array : matrixinfo -> term -> term -> pred
(** {2 C and ACSL Constants} *)
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index ce9733e12df..e265f9dbf24 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -27,7 +27,6 @@
open LogicUsage
open Cil_types
open Cil_datatype
-open Ctypes
open Qed.Logic
open Lang
open Lang.F
@@ -255,11 +254,7 @@ let icompinfo c =
in cluster.c_irecords <- [c] ; cluster)
(Lang.comp_init_id c)
-let matrix = function
- | C_array _ -> assert false
- | C_comp c -> compinfo c
- | C_int _ | C_float _ | C_pointer _ ->
- cluster ~id:"Matrix" ~title:"Basic Arrays" ()
+let matrix () = cluster ~id:"Matrix" ~title:"Basic Arrays" ()
let call_fun ~result lfun cc es =
Symbol.compile (Lang.local cc) lfun ;
diff --git a/src/plugins/wp/Definitions.mli b/src/plugins/wp/Definitions.mli
index dde165a9726..c77e040c7b9 100644
--- a/src/plugins/wp/Definitions.mli
+++ b/src/plugins/wp/Definitions.mli
@@ -22,7 +22,6 @@
open LogicUsage
open Cil_types
-open Ctypes
open Lang
open Lang.F
@@ -33,7 +32,7 @@ val cluster : id:string -> ?title:string -> ?position:Filepath.position -> unit
val axiomatic : axiomatic -> cluster
val section : logic_section -> cluster
val compinfo : compinfo -> cluster
-val matrix : c_object -> cluster
+val matrix : unit -> cluster
val cluster_id : cluster -> string (** Unique *)
val cluster_title : cluster -> string
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 47cbf26bed3..c235b68f103 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -274,10 +274,12 @@ struct
| EQ_loc
| EQ_plain
| EQ_float of c_float
- | EQ_array of Matrix.matrix
+ | EQ_array of matrixinfo
| EQ_comp of compinfo
| EQ_incomparable
+ and matrixinfo = c_object * int option list
+
let eqsort_of_type t =
match Logic_utils.unroll_type ~unroll_typedef:false t with
| Ltype({lt_name="set"},[_]) -> EQ_set
@@ -288,7 +290,7 @@ struct
| C_int _ -> EQ_plain
| C_float f -> EQ_float f
| C_comp c -> EQ_comp c
- | C_array a -> EQ_array (Matrix.of_array a)
+ | C_array a -> EQ_array (Ctypes.array_dimensions a)
let eqsort_of_comparison a b =
match eqsort_of_type a.term_type , eqsort_of_type b.term_type with
@@ -296,7 +298,7 @@ struct
| EQ_loc , EQ_loc -> EQ_loc
| EQ_comp c1 , EQ_comp c2 ->
if Compinfo.equal c1 c2 then EQ_comp c1 else EQ_incomparable
- | EQ_array (t1,d1) , EQ_array (t2,d2) ->
+ | EQ_array(t1,d1) , EQ_array(t2,d2) ->
if Ctypes.equal t1 t2 then
match Matrix.merge d1 d2 with
| Some d -> EQ_array(t1,d)
diff --git a/src/plugins/wp/Matrix.ml b/src/plugins/wp/Matrix.ml
index e850da840c5..e3774cc9949 100644
--- a/src/plugins/wp/Matrix.ml
+++ b/src/plugins/wp/Matrix.ml
@@ -24,83 +24,49 @@
(* --- Array Dimensions --- *)
(* -------------------------------------------------------------------------- *)
-open Ctypes
+(* private *)
+type t = [ `Fix | `Ext ] list
+
+let of_dims = List.map (function None -> `Ext | Some _ -> `Fix)
+
+let compare (ps : t) (qs : t) = Stdlib.compare ps qs
+
+let rec pp_hdims fmt = function
+ | [] -> ()
+ | `Fix :: ps -> pp_ndims `Fix 1 fmt ps
+ | `Ext :: ps -> pp_ndims `Ext 1 fmt ps
+
+and pp_ndims p k fmt = function
+ | q :: qs when p = q -> pp_ndims p (succ k) fmt qs
+ | ps -> pp_kdim p k fmt ; pp_hdims fmt ps
+
+and pp_kdim p k fmt =
+ begin
+ if p = `Fix then Format.pp_print_char fmt 'd' ;
+ if p = `Ext then Format.pp_print_char fmt 'w' ;
+ if k > 1 then Format.pp_print_int fmt k ;
+ end
+
+let pp_suffix_id fmt = function
+ | [] | [`Fix] -> ()
+ | ps -> Format.pp_print_char fmt '_' ; pp_hdims fmt ps
+
+let pretty fmt ps = pp_hdims fmt ps
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compilation Environment --- *)
+(* -------------------------------------------------------------------------- *)
+
open Lang.F
-type dim = int option
-type matrix = c_object * dim list
-
-let of_array = Ctypes.array_dimensions
-
-module KEY(E : sig val compare : c_object -> c_object -> int end) =
-struct
- type t = matrix
-
- let compare_dim d1 d2 = match d1 , d2 with
- | None,None -> 0
- | Some _,None -> (-1)
- | None,Some _ -> 1
- | Some _,Some _ -> 0
-
- let compare (e1,ds1) (e2,ds2) =
- let cmp = E.compare e1 e2 in
- if cmp = 0 then Qed.Hcons.compare_list compare_dim ds1 ds2 else cmp
-
- let pretty fmt (obj,ds) =
- Ctypes.pretty fmt obj ;
- List.iter
- (function
- | None -> Format.pp_print_string fmt "[]"
- | Some d -> Format.fprintf fmt "[%d]" d
- ) ds
-end
-
-module COBJ =
-struct
- let compare e1 e2 = match e1 , e2 with
- | C_int _ , C_int _ -> 0
- | C_int _ , _ -> (-1)
- | _ , C_int _ -> 1
- | C_float _ , C_float _ -> 0
- | C_float _ , _ -> (-1)
- | _ , C_float _ -> 1
- | C_pointer _ , C_pointer _ -> 0
- | C_pointer _ , _ -> (-1)
- | _ , C_pointer _ -> 1
- | C_comp a , C_comp b -> Cil_datatype.Compinfo.compare a b
- | C_comp _ , _ -> (-1)
- | _ , C_comp _ -> 1
- | C_array _ , C_array _ -> assert false
-end
-
-module MACHINE = KEY(Ctypes)
-module NATURAL = KEY(COBJ)
-
-let natural_id = function
- | C_int _ -> "int"
- | C_float _ -> "float"
- | C_pointer _ -> "pointer"
- | C_array _ -> "array"
- | C_comp c -> Lang.comp_id c
-
-let add_rank buffer k = if k > 0 then Buffer.add_string buffer (string_of_int k)
-let add_dim buffer rank = function
- | None -> add_rank buffer rank ; Buffer.add_string buffer "w" ; 0
- | Some _ -> succ rank
-
-let id ds =
- let buffer = Buffer.create 8 in
- add_rank buffer (List.fold_left (add_dim buffer) 0 ds) ;
- Buffer.contents buffer
-
-type denv = {
+type env = {
size_var : var list ; (* size variables *)
size_val : term list ; (* size values *)
index_var : var list ; (* index variables *)
index_val : term list ; (* index values *)
index_range : pred list ; (* indices are in range of size variables *)
- index_offset : term list ; (* polynomial of indices *)
- monotonic : bool ;
+ index_offset : term list ; (* polynomial of indices multiplied by previous sizes *)
+ monotonic : bool ; (* all dimensions are fixed *)
}
let rec collect rank = function
@@ -121,14 +87,14 @@ let rec collect rank = function
let k_val = e_var k_var in
let k_ofs = e_prod (k_val :: denv.size_val) in
match d with
- | None ->
+ | `Ext ->
{ denv with
index_var = k_var :: denv.index_var ;
index_val = k_val :: denv.index_val ;
index_offset = k_ofs :: denv.index_offset ;
monotonic = false ;
}
- | Some _ ->
+ | `Fix ->
let n_base = match rank with 0 -> "n" | 1 -> "m" | _ -> "d" in
let n_var = Lang.freshvar ~basename:n_base Qed.Logic.Int in
let n_val = e_var n_var in
@@ -144,20 +110,19 @@ let rec collect rank = function
monotonic = denv.monotonic ;
}
-let denv = collect 0
+let cc_env = collect 0
-let rec dval = function
+let rec cc_dims ns =
+ match ns with
| [] -> []
- | None :: ds -> dval ds
- | Some n :: ds -> e_int n :: dval ds
-let size (_,ds) = dval ds
+ | Some n :: ns -> e_int n :: cc_dims ns
+ | None :: ns -> cc_dims ns
-let rec kind on_leaf obj = function
- | [] -> on_leaf obj
- | _ :: ds -> Qed.Logic.Array( Qed.Logic.Int , kind on_leaf obj ds )
+let cc_tau te ds = Lang.t_matrix te (List.length ds)
-let tau = kind Lang.tau_of_object
-let init = kind Lang.init_of_object
+(* -------------------------------------------------------------------------- *)
+(* --- Dimension Merging --- *)
+(* -------------------------------------------------------------------------- *)
let rec do_merge ds1 ds2 =
match ds1 , ds2 with
@@ -172,3 +137,5 @@ let rec do_merge ds1 ds2 =
let merge ds1 ds2 =
try Some(do_merge ds1 ds2)
with Exit -> None
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Matrix.mli b/src/plugins/wp/Matrix.mli
index 62a58d3b6ee..d138d00ddc3 100644
--- a/src/plugins/wp/Matrix.mli
+++ b/src/plugins/wp/Matrix.mli
@@ -24,22 +24,19 @@
(* --- Array Dimensions --- *)
(* -------------------------------------------------------------------------- *)
-open Ctypes
-open Lang.F
-
-type dim = int option
-type matrix = c_object * dim list
+type t (** Matrix dimensions.
+ Encodes the number of dimensions and their kind *)
-module MACHINE : WpContext.Key with type t = matrix
-module NATURAL : WpContext.Key with type t = matrix
+val of_dims : int option list -> t
+val compare : t -> t -> int
+val pretty : Format.formatter -> t -> unit
+val pp_suffix_id : Format.formatter -> t -> unit
-val of_array : arrayinfo -> matrix
-val id : dim list -> string (** unique w.r.t [equal] *)
-val natural_id : c_object -> string (** name for elements in NATURAL *)
+val merge : int option list -> int option list -> int option list option
-val merge : dim list -> dim list -> dim list option
+open Lang.F
-type denv = {
+type env = {
size_var : var list ; (** size variables *)
size_val : term list ; (** size values *)
index_var : var list ; (** index variables *)
@@ -49,7 +46,8 @@ type denv = {
monotonic : bool ; (** all dimensions are defined *)
}
-val denv : dim list -> denv
-val size : matrix -> term list
-val tau : c_object -> dim list -> tau
-val init : c_object -> dim list -> tau
+val cc_tau : tau -> t -> tau (** Type of matrix *)
+val cc_env : t -> env (** Dimension environment *)
+val cc_dims : int option list -> term list (** Value of size variables *)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 734097fb74a..31a1bf4b891 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -217,46 +217,72 @@ struct
(* --- Array Loader --- *)
(* -------------------------------------------------------------------------- *)
- module ARRAY_KEY =
+ module AKEY =
struct
- type t = int * arrayinfo * Matrix.matrix
- let pretty fmt (r,_,m) =
- Format.fprintf fmt "%d:%a" r Matrix.NATURAL.pretty m
- let compare (r1,_,m1) (r2,_,m2) =
- if r1 = r2 then Matrix.NATURAL.compare m1 m2 else r1-r2
+ type t = int * base * Matrix.t
+ and base = I of c_int | F of c_float | P | C of compinfo
+ let make r elt ds =
+ let base = match elt with
+ | C_int i -> I i
+ | C_float f -> F f
+ | C_pointer _ -> P
+ | C_comp c -> C c
+ | C_array _ -> raise (Invalid_argument "Wp.EqArray")
+ in r, base , ds
+ let key = function
+ | I i -> Ctypes.i_name i
+ | F f -> Ctypes.f_name f
+ | P -> "ptr"
+ | C c -> Lang.comp_id c
+ let obj = function
+ | I i -> C_int i
+ | F f -> C_float f
+ | P -> C_pointer Cil.voidPtrType
+ | C c -> C_comp c
+ let tau = function
+ | I _ -> Lang.t_int
+ | F f -> Lang.t_float f
+ | P -> Lang.t_addr ()
+ | C c -> Lang.t_comp c
+ let compare (r,a,p) (s,b,q) =
+ if r = s then
+ let cmp = String.compare (key a) (key b) in
+ if cmp <> 0 then cmp else Matrix.compare p q
+ else r - s
+ let pretty fmt (r,a,ds) =
+ Format.fprintf fmt "%s%a%a" (key a) pp_rid r Matrix.pp_suffix_id ds
end
- module ARRAY = WpContext.Generator(ARRAY_KEY)
+ module ARRAY = WpContext.Generator(AKEY)
(struct
open Matrix
let name = M.name ^ ".ARRAY"
- type key = int * arrayinfo * Matrix.matrix
+ type key = AKEY.t
type data = lfun * chunk list
- let generate (r,ainfo,(obj_e,ds)) =
+ let generate (r,a,ds) =
let x = Lang.freshvar ~basename:"p" (Lang.t_addr()) in
let v = e_var x in
- let obj_a = C_array ainfo in
- let loc = M.of_region_pointer r obj_a v in (* t_pointer -> loc *)
- let domain = M.value_footprint obj_a loc in
- let result = Matrix.tau obj_e ds in
+ let obj = AKEY.obj a in
+ let loc = M.of_region_pointer r obj v in (* t_pointer -> loc *)
+ let domain = M.value_footprint obj loc in
+ let result = Matrix.cc_tau (AKEY.tau a) ds in
let lfun =
- Lang.generated_f ~result "Array%a%s_%s"
- pp_rid r (Matrix.id ds) (Matrix.natural_id obj_e)
- in
+ Lang.generated_f ~result "Array%a_%s%a"
+ pp_rid r (AKEY.key a) Matrix.pp_suffix_id ds in
let prefix = Lang.Fun.debug lfun in
let name = prefix ^ "_access" in
let xmem,chunks,sigma = signature domain in
- let denv = Matrix.denv ds in
- let phi = e_fun lfun (v :: denv.size_val @ List.map e_var xmem) in
- let va = List.fold_left e_get phi denv.index_val in
- let ofs = e_sum denv.index_offset in
- let vm = !loadrec sigma obj_e (M.shift loc obj_e ofs) in
- let lemma = p_hyps denv.index_range (p_equal va vm) in
+ let env = Matrix.cc_env ds in
+ let phi = e_fun lfun (v :: env.size_val @ List.map e_var xmem) in
+ let va = List.fold_left e_get phi env.index_val in
+ let ofs = e_sum env.index_offset in
+ let vm = !loadrec sigma obj (M.shift loc obj ofs) in
+ let lemma = p_hyps env.index_range (p_equal va vm) in
let cluster = cluster () in
Definitions.define_symbol {
d_lfun = lfun ; d_types = 0 ;
- d_params = x :: denv.size_var @ xmem ;
+ d_params = x :: env.size_var @ xmem ;
d_definition = Logic result ;
d_cluster = cluster ;
} ;
@@ -268,10 +294,10 @@ struct
l_lemma = lemma ;
l_cluster = cluster ;
} ;
- if denv.monotonic then
+ if env.monotonic then
begin
- let ns = List.map F.e_var denv.size_var in
- frame_lemmas lfun obj_a loc (v::ns) chunks
+ let ns = List.map F.e_var env.size_var in
+ frame_lemmas lfun obj loc (v::ns) chunks
end ;
lfun , chunks
@@ -288,10 +314,11 @@ struct
F.e_fun f (p :: memories sigma m)
let load_array sigma a loc =
- let d = Matrix.of_array a in
let r , p = M.to_region_pointer loc in
- let f , m = ARRAY.get (r,a,d) in
- F.e_fun f (p :: Matrix.size d @ memories sigma m)
+ let e , ns = Ctypes.array_dimensions a in
+ let ds = Matrix.of_dims ns in
+ let f , m = ARRAY.get @@ AKEY.make r e ds in
+ F.e_fun f (p :: Matrix.cc_dims ns @ memories sigma m)
let loadvalue sigma obj loc =
match obj with
@@ -368,40 +395,39 @@ struct
let compile = Lang.local generate
end)
- module ARRAYINIT = WpContext.Generator(ARRAY_KEY)
+ module IS_ARRAY_INIT = WpContext.Generator(AKEY)
(struct
open Matrix
- let name = M.name ^ ".ARRAYINIT"
- type key = int * arrayinfo * Matrix.matrix
+ let name = M.name ^ ".IS_ARRAY_INIT"
+ type key = AKEY.t
type data = lfun * chunk list
- let generate (r,ainfo,(obj_e,ds)) =
+ let generate (r,a,ds) =
let x = Lang.freshvar ~basename:"p" (Lang.t_addr()) in
let v = e_var x in
- let obj_a = C_array ainfo in
- let loc = M.of_region_pointer r obj_a v in (* t_pointer -> loc *)
- let domain = M.init_footprint obj_a loc in
- let name = Format.asprintf "IsInitArray%a%s_%s"
- pp_rid r (Matrix.id ds) (Matrix.natural_id obj_e)
- in
+ let obj = AKEY.obj a in
+ let loc = M.of_region_pointer r obj v in
+ let domain = M.init_footprint obj loc in
+ let name = Format.asprintf "IsInitArray%a_%s%a"
+ pp_rid r (AKEY.key a) Matrix.pp_suffix_id ds in
let lfun = Lang.generated_p name in
let xmem,chunks,sigma = signature domain in
- let denv = Matrix.denv ds in
- let ofs = e_sum denv.index_offset in
- let vm = !isinitrec sigma obj_e (M.shift loc obj_e ofs) in
- let def = p_forall denv.index_var (p_hyps denv.index_range vm) in
+ let env = Matrix.cc_env ds in
+ let ofs = e_sum env.index_offset in
+ let vm = !isinitrec sigma obj (M.shift loc obj ofs) in
+ let def = p_forall env.index_var (p_hyps env.index_range vm) in
let cluster = cluster () in
Definitions.define_symbol {
d_lfun = lfun ; d_types = 0 ;
- d_params = x :: denv.size_var @ xmem ;
+ d_params = x :: env.size_var @ xmem ;
d_definition = Predicate (Def, def) ;
d_cluster = cluster ;
} ;
(* Lemma for low-level view of the memory *)
Definitions.define_lemma
(initialization_lemma cluster name
- (sigma, obj_a, loc)
- (lfun, x :: denv.size_var @ xmem)) ;
+ (sigma, obj, loc)
+ (lfun, x :: env.size_var @ xmem)) ;
lfun , chunks
let compile = Lang.local generate
@@ -412,11 +438,12 @@ struct
let f , m = IS_INIT_COMP.get (r,comp) in
F.p_call f (p :: memories sigma m)
- let initialized_array sigma a loc =
- let d = Matrix.of_array a in
+ let initialized_array sigma ainfo loc =
let r , p = M.to_region_pointer loc in
- let f , m = ARRAYINIT.get (r,a,d) in
- F.p_call f (p :: Matrix.size d @ memories sigma m)
+ let e , ns = Ctypes.array_dimensions ainfo in
+ let ds = Matrix.of_dims ns in
+ let f , m = IS_ARRAY_INIT.get @@ AKEY.make r e ds in
+ F.p_call f (p :: Matrix.cc_dims ns @ memories sigma m)
let initialized_loc sigma obj loc =
match obj with
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
index ebcccafc2c7..89ab8bf1720 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
@@ -17,7 +17,7 @@ Assume {
(* Else *)
Have: 10 <= i.
}
-Prove: IsInitArray1_int(array_0, 10, a).
+Prove: IsInitArray_sint32(array_0, 10, a).
------------------------------------------------------------
------------------------------------------------------------
@@ -37,7 +37,7 @@ Assume {
(* Else *)
Have: 10 <= i.
}
-Prove: IsInitArray1_int(pg_array_0, 10, a_1).
+Prove: IsInitArray_sint32(pg_array_0, 10, a_1).
------------------------------------------------------------
@@ -54,7 +54,7 @@ Assume {
(* Else *)
Have: 10 <= i.
}
-Prove: IsInitArray1_int(a, 10, a_2).
+Prove: IsInitArray_sint32(a, 10, a_2).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
index 202dde2b9d6..39aa840de42 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
@@ -13,7 +13,7 @@ Assume {
Type: IsArray_sint32(t0_0) /\ IsArray_sint32(t1_0) /\ is_sint32(x) /\
is_sint32(x_1).
}
-Prove: EqArray1_int(2, t0_0, t1_0[0 <- x][1 <- x_1]).
+Prove: EqArray_int(2, t0_0, t1_0[0 <- x][1 <- x_1]).
------------------------------------------------------------
------------------------------------------------------------
@@ -35,7 +35,7 @@ Assume {
Type: IsS2_St(st0_0) /\ IsS2_St(st1_0) /\ IsArray_sint32(a) /\
IsArray_sint32(a_1).
(* Goal *)
- When: EqArray1_int(10, a, a_1).
+ When: EqArray_int(10, a, a_1).
}
Prove: EqS2_St(st0_0, st1_0).
@@ -57,7 +57,7 @@ Assume {
(* Heap *)
Type: (region(a_1.base) <= 0) /\ (region(a.base) <= 0).
(* Goal *)
- When: (a = a_1) /\ EqS1_S(a_2, a_3) /\ EqArray1_int(2, a_4, a_5).
+ When: (a = a_1) /\ EqS1_S(a_2, a_3) /\ EqArray_int(2, a_4, a_5).
}
Prove: EqS4_Q(q0_0, q1_0).
@@ -74,7 +74,7 @@ Assume {
(* Goal *)
When: forall i : Z. ((0 <= i) -> ((i <= 4) -> (tp1_0[i] = tp0_0[i]))).
}
-Prove: EqArray1_pointer(5, tp0_0, tp1_0).
+Prove: EqArray_ptr(5, tp0_0, tp1_0).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
index af8d7fd203c..561960415e8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
@@ -39,7 +39,7 @@ Assume {
(* Initializer *)
Init: forall i : Z. ((3 <= i) -> ((i <= 19) -> (A_1[i] = 0))).
(* Pre-condition *)
- Have: EqArray1_int(20, A, A_1).
+ Have: EqArray_int(20, A, A_1).
}
Prove: x = 12.
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
index 1a01091dabd..ef64e214217 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
@@ -83,7 +83,7 @@ Prove: (Init_0[x]=true).
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 13):
Assume { (* Heap *) Type: (region(a.base) <= 0) /\ cinits(Init_0). }
-Prove: IsInitArray1_int(a, 2, Init_0).
+Prove: IsInitArray_sint32(a, 2, Init_0).
------------------------------------------------------------
@@ -117,7 +117,8 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(x.base) <= 0) /\ cinits(Init_0).
}
-Prove: IsInitArray1_int(a, 2, Init_0[x <- true][shift_sint32(a, 0) <- true]).
+Prove: IsInitArray_sint32(a, 2,
+ Init_0[x <- true][shift_sint32(a, 0) <- true]).
------------------------------------------------------------
@@ -136,7 +137,7 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(x.base) <= 0) /\ cinits(Init_0).
}
-Prove: IsInitArray1_int(a, 2,
+Prove: IsInitArray_sint32(a, 2,
Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
<- true]).
@@ -165,7 +166,7 @@ Assume {
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0) /\ cinits(Init_0).
}
-Prove: IsInitArray1_int(shiftfield_F2_C_a(c), 10,
+Prove: IsInitArray_sint32(shiftfield_F2_C_a(c), 10,
Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
<- true][shiftfield_F2_C_x(c) <- true]).
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 cebaff887df..e5f7a31927d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -39,8 +39,8 @@
Goal Post-condition (file tests/wp_acsl/logic.i, line 21) in 'h':
Let a = global(G_t_29).
-Let m = Array1_S1(shift_S1(a, 0), 3, Mint_0).
-Let m_1 = Array1_S1(a, 3, Mint_0).
+Let m = Array_S1(shift_S1(a, 0), 3, Mint_0).
+Let m_1 = Array_S1(a, 3, Mint_0).
Assume { Type: IsArray_S1(m_1) /\ IsArray_S1(m). (* Call 'f' *) Have: P_P(m).
}
Prove: P_P(m_1).
@@ -70,9 +70,9 @@ Let a = global(G_tr_35).
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).
+Let m = Array_S1(a, 3, Mint_0).
Assume {
- Type: IsArray_S1(m) /\ IsArray_S1(Array1_S1(a_3, 3, Mint_0)).
+ Type: IsArray_S1(m) /\ IsArray_S1(Array_S1(a_3, 3, Mint_0)).
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -95,9 +95,9 @@ Let a = global(G_tr_35).
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).
+Let m = Array_S1(a, 3, Mint_0).
Assume {
- Type: IsArray_S1(m) /\ IsArray_S1(Array1_S1(a_3, 3, Mint_0)).
+ Type: IsArray_S1(m) /\ IsArray_S1(Array_S1(a_3, 3, Mint_0)).
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -120,9 +120,9 @@ Let a = global(G_tr_35).
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).
+Let m = Array_S1(a_3, 3, Mint_0).
Assume {
- Type: IsArray_S1(Array1_S1(a, 3, Mint_0)) /\ IsArray_S1(m).
+ Type: IsArray_S1(Array_S1(a, 3, Mint_0)) /\ IsArray_S1(m).
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle
index 02cc1e7481d..02e2face2d5 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle
@@ -54,7 +54,7 @@ Assume {
(* Goal *)
When: forall i : Z. ((0 <= i) -> ((i <= 9) -> (t2_0[i] = t1_0[i]))).
}
-Prove: EqArray1_int(10, t1_0, t2_0).
+Prove: EqArray_int(10, t1_0, t2_0).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
index d53c4143c88..921a9d48bb6 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
@@ -14,8 +14,8 @@ Let a_2 = shift_sint32(a, j).
Let m = Mint_0[a_1 <- Mint_0[a_2]][a_2 <- x][shift_sint32(a, k) <- x].
Assume {
Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(k) /\
- IsArray_sint32(Array1_int(a, 10, Mint_0)) /\ is_sint32(x) /\
- IsArray_sint32(Array1_int(a, 10, m)).
+ IsArray_sint32(Array_sint32(a, 10, Mint_0)) /\ is_sint32(x) /\
+ IsArray_sint32(Array_sint32(a, 10, m)).
(* Pre-condition *)
Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
}
@@ -25,11 +25,11 @@ Prove: P_p_pointer(m, Mint_0, shift_sint32(a, 0), i, j).
Goal Post-condition 'ARR' in 'job':
Let a = global(G_arr_35).
-Let m = Array1_int(a, 10, Mint_0).
+Let m = Array_sint32(a, 10, Mint_0).
Let a_1 = shift_sint32(a, i).
Let x = Mint_0[a_1].
Let a_2 = shift_sint32(a, j).
-Let m_1 = Array1_int(a, 10,
+Let m_1 = Array_sint32(a, 10,
Mint_0[a_1 <- Mint_0[a_2]][a_2 <- x][shift_sint32(a, k) <- x]).
Assume {
Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(k) /\ IsArray_sint32(m) /\
@@ -46,11 +46,11 @@ Let a = global(G_arr_35).
Let a_1 = shift_sint32(a, i).
Let x = Mint_0[a_1].
Let a_2 = shift_sint32(a, j).
-Let m = Array1_int(a, 10,
+Let m = Array_sint32(a, 10,
Mint_0[a_1 <- Mint_0[a_2]][a_2 <- x][shift_sint32(a, k) <- x]).
Assume {
Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(k) /\
- IsArray_sint32(Array1_int(a, 10, Mint_0)) /\ is_sint32(x) /\
+ IsArray_sint32(Array_sint32(a, 10, Mint_0)) /\ is_sint32(x) /\
IsArray_sint32(m).
(* Pre-condition *)
Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
index 111dc92f510..57e3cdd6d9c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
@@ -22,9 +22,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job' *)
- Have: (k <= 10) /\ EqArray1_int(10, m, p[x <- x1_0]).
+ Have: (k <= 10) /\ EqArray_int(10, m, p[x <- x1_0]).
(* Call 'job' *)
- Have: EqArray1_int(10, m_1, m[k <- x2_0]).
+ Have: EqArray_int(10, m_1, m[k <- x2_0]).
}
Prove: x1_0 = v.
@@ -41,9 +41,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job' *)
- Have: (k <= 10) /\ EqArray1_int(10, m, p[x <- x1_0]).
+ Have: (k <= 10) /\ EqArray_int(10, m, p[x <- x1_0]).
(* Call 'job' *)
- Have: EqArray1_int(10, m_1, m[k <- x2_0]).
+ Have: EqArray_int(10, m_1, m[k <- x2_0]).
}
Prove: x2_0 = v.
@@ -66,7 +66,7 @@ Assume {
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
(* Call 'job' *)
- Have: (k <= 9) /\ EqArray1_int(10, m, p[k <- x1_0]).
+ Have: (k <= 9) /\ EqArray_int(10, m, p[k <- x1_0]).
}
Prove: (-1) <= k.
@@ -91,9 +91,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, q[x <- s1_0]).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, q[x <- s1_0]).
(* Call 'job2' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
Prove: EqS1_S(v, s1_0).
@@ -110,9 +110,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, q[x <- s1_0]).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, q[x <- s1_0]).
(* Call 'job2' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
Prove: EqS1_S(v, s2_0).
@@ -130,11 +130,11 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, m_2).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, m_2).
(* Call 'job2' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
-Prove: EqArray1_S1_S(10, m_1, m_2[k <- s2_0]).
+Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
------------------------------------------------------------
@@ -155,7 +155,7 @@ Assume {
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
(* Call 'job2' *)
- Have: (k <= 9) /\ EqArray1_S1_S(10, m, q[k <- s1_0]).
+ Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
}
Prove: (-1) <= k.
@@ -180,9 +180,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, q[x <- s1_0]).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, q[x <- s1_0]).
(* Call 'job3' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
Prove: EqS1_S(v, s1_0).
@@ -199,9 +199,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, q[x <- s1_0]).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, q[x <- s1_0]).
(* Call 'job3' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
Prove: EqS1_S(v, s2_0).
@@ -219,11 +219,11 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, m_2).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, m_2).
(* Call 'job3' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
-Prove: EqArray1_S1_S(10, m_1, m_2[k <- s2_0]).
+Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
------------------------------------------------------------
@@ -244,7 +244,7 @@ Assume {
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
(* Call 'job3' *)
- Have: (k <= 9) /\ EqArray1_S1_S(10, m, q[k <- s1_0]).
+ Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
}
Prove: (-1) <= k.
@@ -326,7 +326,7 @@ Assume {
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 9).
}
-Prove: EqArray1_S1_S(10, m, q[k <- s]).
+Prove: EqArray_S1_S(10, m, q[k <- s]).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
index 1b950374764..4462e762cfa 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
@@ -22,9 +22,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job' *)
- Have: (k <= 10) /\ EqArray1_int(10, m, p[x <- x1_0]).
+ Have: (k <= 10) /\ EqArray_int(10, m, p[x <- x1_0]).
(* Call 'job' *)
- Have: EqArray1_int(10, m_1, m[k <- x2_0]).
+ Have: EqArray_int(10, m_1, m[k <- x2_0]).
}
Prove: x1_0 = v.
@@ -41,9 +41,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job' *)
- Have: (k <= 10) /\ EqArray1_int(10, m, p[x <- x1_0]).
+ Have: (k <= 10) /\ EqArray_int(10, m, p[x <- x1_0]).
(* Call 'job' *)
- Have: EqArray1_int(10, m_1, m[k <- x2_0]).
+ Have: EqArray_int(10, m_1, m[k <- x2_0]).
}
Prove: x2_0 = v.
@@ -66,7 +66,7 @@ Assume {
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
(* Call 'job' *)
- Have: (k <= 9) /\ EqArray1_int(10, m, p[k <- x1_0]).
+ Have: (k <= 9) /\ EqArray_int(10, m, p[k <- x1_0]).
}
Prove: (-1) <= k.
@@ -91,9 +91,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, q[x <- s1_0]).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, q[x <- s1_0]).
(* Call 'job2' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
Prove: EqS1_S(v, s1_0).
@@ -110,9 +110,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, q[x <- s1_0]).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, q[x <- s1_0]).
(* Call 'job2' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
Prove: EqS1_S(v, s2_0).
@@ -130,11 +130,11 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, m_2).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, m_2).
(* Call 'job2' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
-Prove: EqArray1_S1_S(10, m_1, m_2[k <- s2_0]).
+Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
------------------------------------------------------------
@@ -155,7 +155,7 @@ Assume {
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
(* Call 'job2' *)
- Have: (k <= 9) /\ EqArray1_S1_S(10, m, q[k <- s1_0]).
+ Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
}
Prove: (-1) <= k.
@@ -180,9 +180,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, q[x <- s1_0]).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, q[x <- s1_0]).
(* Call 'job3' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
Prove: EqS1_S(v, s1_0).
@@ -199,9 +199,9 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, q[x <- s1_0]).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, q[x <- s1_0]).
(* Call 'job3' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
Prove: EqS1_S(v, s2_0).
@@ -219,11 +219,11 @@ Assume {
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
- Have: (k <= 10) /\ EqArray1_S1_S(10, m, m_2).
+ Have: (k <= 10) /\ EqArray_S1_S(10, m, m_2).
(* Call 'job3' *)
- Have: EqArray1_S1_S(10, m_1, m[k <- s2_0]).
+ Have: EqArray_S1_S(10, m_1, m[k <- s2_0]).
}
-Prove: EqArray1_S1_S(10, m_1, m_2[k <- s2_0]).
+Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
------------------------------------------------------------
@@ -244,7 +244,7 @@ Assume {
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
(* Call 'job3' *)
- Have: (k <= 9) /\ EqArray1_S1_S(10, m, q[k <- s1_0]).
+ Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
}
Prove: (-1) <= k.
@@ -326,7 +326,7 @@ Assume {
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 9).
}
-Prove: EqArray1_S1_S(10, m, q[k <- s]).
+Prove: EqArray_S1_S(10, m, q[k <- s]).
------------------------------------------------------------
--
GitLab