diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index e405d452408ba13afe41a1a12c42089059605491..abccad645fd295fe3733a967595931f799a1e8e8 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -248,3 +248,185 @@ module At_data = struct
Ext_logic_label.pretty elabel
end)
end
+
+module Ival_datatype =
+ Datatype.Make_with_collections
+ (struct
+ type t = ival
+ let name = "E_ACSL.Interval.t"
+ let reprs = [ Float (FFloat, Some 0.); Rational; Real; Nan ]
+ include Datatype.Undefined
+
+ let compare i1 i2 =
+ if i1 == i2 then 0
+ else
+ match i1, i2 with
+ | Ival i1, Ival i2 ->
+ Ival.compare i1 i2
+ | Float (k1, f1), Float (k2, f2) ->
+ (* faster to compare a kind than a float *)
+ let n = Stdlib.compare k1 k2 in
+ if n = 0 then Stdlib.compare f1 f2 else n
+ | Ival _, (Float _ | Rational | Real | Nan)
+ | Float _, (Rational | Real | Nan)
+ | Rational, (Real | Nan)
+ | Real, Nan ->
+ -1
+ | Nan, (Ival _ | Float _ | Rational | Real)
+ | Real, (Ival _ | Float _ | Rational)
+ | Rational, (Ival _ | Float _)
+ | Float _, Ival _ ->
+ 1
+ | Rational, Rational | Real, Real | Nan, Nan ->
+ assert false
+
+ let equal = Datatype.from_compare
+
+ let hash = function
+ | Ival i -> 7 * Ival.hash i
+ | Float(k, f) -> 17 * Hashtbl.hash f + 97 * Hashtbl.hash k
+ | Rational -> 787
+ | Real -> 1011
+ | Nan -> 1277
+
+ let pretty fmt = function
+ | Ival i -> Ival.pretty fmt i
+ | Float(_, Some f) -> Format.pp_print_float fmt f
+ | Float(FFloat, None) -> Format.pp_print_string fmt "float"
+ | Float(FDouble, None) -> Format.pp_print_string fmt "double"
+ | Float(FLongDouble, None) -> Format.pp_print_string fmt "long double"
+ | Rational -> Format.pp_print_string fmt "Rational"
+ | Real -> Format.pp_print_string fmt "Real"
+ | Nan -> Format.pp_print_string fmt "NaN"
+
+ end)
+
+(* Profiles of functions are the interval ranges of their arguments. For
+ memoization purposes, we need need them as keys of hashtables, even though
+ they are implemented as maps. Functions typically do not have many arguments
+ so it is acceptable to do so.*)
+module Profile =
+struct
+ let rec make args ival =
+ match args,ival with
+ | [],[] -> Logic_var.Map.empty
+ | x::args, i::ival -> Logic_var.Map.add x i (make args ival)
+ | [], _::_ | _::_, [] -> assert false
+
+ include
+ Datatype.Make_with_collections
+ (struct
+ include (Logic_var.Map)
+ include Datatype.Undefined
+
+ type t = ival Logic_var.Map.t
+
+ let equal = Logic_var.Map.equal (Ival_datatype.equal)
+ let compare = Logic_var.Map.compare (Ival_datatype.compare)
+
+ let mem_project = Datatype.never_any_project
+ let copy m = Logic_var.Map.fold Logic_var.Map.add m Logic_var.Map.empty
+ let hash m =
+ Logic_var.Map.fold
+ (fun v i h -> h + Logic_var.hash v + Ival_datatype.hash i)
+ m
+ 0
+ let reprs =
+ let v = List.hd Logic_var.reprs in
+ let i = List.hd Ival_datatype.reprs in
+ [ Logic_var.Map.add v i Logic_var.Map.empty ]
+ let structural_descr = Structural_descr.t_abstract
+ let rehash = Datatype.identity
+ let name = "E-ACSL.Profile"
+ end)
+
+ let is_empty = Logic_var.Map.is_empty
+
+ let empty = Logic_var.Map.empty
+end
+
+module Id_term_in_profile =
+ Datatype.Pair_with_collections
+ (Misc.Id_term)
+ (Profile)
+ (struct let module_name = "E_ACSL.Analyse.Id_term_in_profile" end)
+
+(* Environment to handle recursive functions: this environment stores the logic
+ functions that we have already started inferring along with their
+ profiles. This is necessary for the fixpoint algorithm. *)
+module LFProf =
+ Datatype.Pair_with_collections (Cil_datatype.Logic_info) (Profile)
+ (struct
+ let module_name = "E_ACSL.Interval.LFProf"
+ end)
+
+module Logic_env
+= struct
+ type t = { profile : Profile.t;
+ let_quantif_bind : Profile.t}
+
+ let add env x i =
+ { env with let_quantif_bind = Logic_var.Map.add x i env.let_quantif_bind}
+
+ let empty =
+ {profile = Logic_var.Map.empty;
+ let_quantif_bind = Logic_var.Map.empty}
+
+ let make profile =
+ { profile = profile;
+ let_quantif_bind = Logic_var.Map.empty }
+
+ let find env x =
+ try Logic_var.Map.find x env.let_quantif_bind
+ with Not_found ->
+ Logic_var.Map.find x env.profile
+
+ let get_profile env = env.profile
+
+end
+
+(* Imperative environment to perform fixpoint algorithm for recursive
+ functions *)
+module LF_env
+= struct
+
+ let tbl = LFProf.Hashtbl.create 17
+
+ let clear () = LFProf.Hashtbl.clear tbl
+
+ let find li profile = LFProf.Hashtbl.find tbl (li,profile)
+
+ exception Recursive
+
+ let contain li = object
+ inherit Visitor.frama_c_inplace
+
+ method! vpredicate p =
+ match p.pred_content with
+ | Papp (li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
+ raise Recursive;
+ | _ -> Cil.DoChildren
+
+ method! vterm t =
+ match t.term_node with
+ | Tapp(li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
+ raise Recursive
+ | _ -> Cil.DoChildren
+
+ method! vlogic_type _ = Cil.SkipChildren
+ end
+
+ let is_rec li =
+ match li.l_body with
+ | LBpred p ->
+ (try ignore (Visitor.visitFramacPredicate (contain li) p); false
+ with Recursive -> true)
+ | LBterm t ->
+ (try ignore (Visitor.visitFramacTerm (contain li) t); false
+ with Recursive -> true)
+ | LBreads _ | LBnone -> false
+ | LBinductive _ -> Error.not_yet "Inductive"
+
+ let replace li args_ival ival = LFProf.Hashtbl.replace tbl (li, args_ival) ival
+
+end
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 7b19f984097738c2225a969ed1dc507f9b84ca35..87d08eff0f59ed97cf032168cd5073f239361205 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -43,3 +43,56 @@ module At_data: sig
(** [create ?error kf kinstr lscope pot label] creates an [at_data] from the
given arguments. *)
end
+
+module Ival_datatype: Datatype.S_with_collections with type t = ival
+
+(** profile which maps logic variables that are function parameters to their
+ interval depending on the arguments at the callsite of the function *)
+module Profile: sig
+ include
+ Datatype.S_with_collections
+ with type t = ival Cil_datatype.Logic_var.Map.t
+
+ val make: logic_var list -> ival list -> t
+ val is_empty: t -> bool
+ val empty: t
+
+end
+
+module Id_term_in_profile: Datatype.S_with_collections
+ with type t = term * Profile.t
+
+module LFProf: Datatype.S_with_collections
+ with type t = logic_info * Profile.t
+
+(* logic environment: interval of all bound variables. It consists in two
+ components
+ - a profile for variables bound through functions arguments
+ - an association list for variables bound by a let or a quantification *)
+module Logic_env : sig
+ type t
+ (* add a new binding for a let or a quantification binder only *)
+ val add : t -> logic_var -> ival -> t
+ (* the empty environment *)
+ val empty : t
+ (* create a new environment from a profile, for function calls *)
+ val make : Profile.t -> t
+ (* find a logic variable in the environment *)
+ val find : t -> logic_var -> ival
+ (* get the profile of the logic environment, i.e. bindings through function
+ arguments*)
+ val get_profile : t -> Profile.t
+end
+
+
+(* Imperative environment to perform fixpoint algorithm for recursive
+ functions *)
+module LF_env : sig
+ val find : logic_info -> Profile.t -> ival
+
+ val clear : unit -> unit
+
+ val is_rec : logic_info -> bool
+
+ val replace : logic_info -> Profile.t -> ival -> unit
+end
diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.mli b/src/plugins/e-acsl/src/analyses/analyses_types.mli
index 06f9eddb5a09fb4cbe80497516bef543e1ee6cdc..148dff16a515e51509591cd802c9079c7416b129 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_types.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_types.mli
@@ -67,3 +67,11 @@ type annotation_kind =
| Invariant
| Variant
| RTE
+
+
+type ival =
+ | Ival of Ival.t
+ | Float of fkind * float option (* a float constant, if any *)
+ | Rational
+ | Real
+ | Nan
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 15e3a7347292bec6e963e8d9d9bc77ae880caebe..1ec511d4c67a22cf49f0119a1137eb6498c09488 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -21,6 +21,9 @@
(**************************************************************************)
open Cil_types
+open Cil_datatype
+open Analyses_types
+open Analyses_datatype
(* Implements Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour
devenir plus rapide, plus précis et plus mince".
@@ -32,64 +35,6 @@ module Error = Error.Make(struct let phase = dkey end)
(* Basic datatypes and operations *)
(* ********************************************************************* *)
-type ival =
- | Ival of Ival.t
- | Float of fkind * float option (* a float constant, if any *)
- | Rational
- | Real
- | Nan
-
-module D =
- Datatype.Make_with_collections
- (struct
- type t = ival
- let name = "E_ACSL.Interval.t"
- let reprs = [ Float (FFloat, Some 0.); Rational; Real; Nan ]
- include Datatype.Undefined
-
- let compare i1 i2 =
- if i1 == i2 then 0
- else
- match i1, i2 with
- | Ival i1, Ival i2 ->
- Ival.compare i1 i2
- | Float (k1, f1), Float (k2, f2) ->
- (* faster to compare a kind than a float *)
- let n = Stdlib.compare k1 k2 in
- if n = 0 then Stdlib.compare f1 f2 else n
- | Ival _, (Float _ | Rational | Real | Nan)
- | Float _, (Rational | Real | Nan)
- | Rational, (Real | Nan)
- | Real, Nan ->
- -1
- | Nan, (Ival _ | Float _ | Rational | Real)
- | Real, (Ival _ | Float _ | Rational)
- | Rational, (Ival _ | Float _)
- | Float _, Ival _ ->
- 1
- | Rational, Rational | Real, Real | Nan, Nan ->
- assert false
-
- let equal = Datatype.from_compare
-
- let hash = function
- | Ival i -> 7 * Ival.hash i
- | Float(k, f) -> 17 * Hashtbl.hash f + 97 * Hashtbl.hash k
- | Rational -> 787
- | Real -> 1011
- | Nan -> 1277
-
- let pretty fmt = function
- | Ival i -> Ival.pretty fmt i
- | Float(_, Some f) -> Format.pp_print_float fmt f
- | Float(FFloat, None) -> Format.pp_print_string fmt "float"
- | Float(FDouble, None) -> Format.pp_print_string fmt "double"
- | Float(FLongDouble, None) -> Format.pp_print_string fmt "long double"
- | Rational -> Format.pp_print_string fmt "Rational"
- | Real -> Format.pp_print_string fmt "Real"
- | Nan -> Format.pp_print_string fmt "NaN"
-
- end)
let is_included i1 i2 = match i1, i2 with
| Ival i1, Ival i2 -> Ival.is_included i1 i2
@@ -393,163 +338,35 @@ let ikind_of_ival iv =
(* TODO: do not raise an exception, but returns a value instead *)
raise Cil.Not_representable (* GMP *)
-(* function call profiles (intervals for their formal parameters) *)
-module Profile = struct
- include Datatype.List_with_collections
- (D)
- (struct
- let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
- end)
-end
-
-module Id_term_in_profile =
- Datatype.Pair_with_collections
- (Misc.Id_term)
- (Profile)
- (struct let module_name = "E_ACSL.Interval.Id_term_in_profile" end)
-
-(* logic environment: interval of all bound variables. It is built of two
- components
- - a profile for variables bound through functions arguments
- - an association list for variables bound by a let or a quantification *)
-module Logic_env : sig
- type t
- (* add a new binding for a let or a quantification binder*)
- val add_let_quantif_binding : t -> logic_var -> ival -> t
- (* create a new environment from a profile, for function calls *)
- val make : logic_var list -> ival list -> t
- (* find a logic variable in the environment *)
- val find : t -> logic_var -> ival
- (* get the profile of the logic environment, i.e. bindings through function
- arguments*)
- val get_profile : t -> ival list
-end
-= struct
- type t = { profile : logic_var list * Profile.t;
- let_quantif_bind : (logic_var * ival) list}
-
- let add_let_quantif_binding env x i =
- { env with let_quantif_bind = (x, i) :: env.let_quantif_bind }
-
- let make args params_ival =
- { profile = args , params_ival;
- let_quantif_bind = [] }
-
- let find env x =
- (* Programs typically do not have many variables simulatneously bound, so a
- linear search is fine here*)
- try List.assoc x env.let_quantif_bind
- with Not_found ->
- let rec find = function
- |(y::_), (i ::_) when Cil_datatype.Logic_var.equal x y -> i
- | (_ :: l) , (_ :: l') -> find (l, l')
- | [] , _ :: _
- | _ :: _, [] -> Options.abort "inconsistent function profile"
- |[], [] -> raise Not_found
- in find env.profile
-
- let get_profile env = snd env.profile
-
-end
-
-(* Imperative environment to perform fixpoint algorithm for recursive
- functions *)
-module LF_env : sig
- val find : logic_info -> Profile.t -> ival
-
- val clear : unit -> unit
- val interv_of_typ_containing_interv : ival -> ival
-
- val is_rec : logic_info -> bool
-
- val fixpoint :
- infer : (
- force:bool ->
- logic_env: Logic_env.t ->
- term ->
- ival Error.result) ->
- logic_info ->
- Profile.t ->
- term ->
- ival ->
+let interv_of_typ_containing_interv = function
+ | Float _ | Rational | Real | Nan as x ->
+ x
+ | Ival i ->
+ try
+ let kind = ikind_of_ival i in
+ interv_of_typ (TInt(kind, []))
+ with Cil.Not_representable ->
+ top_ival
+
+let widen_profile =
+ Cil_datatype.Logic_var.Map.map interv_of_typ_containing_interv
+
+let rec fixpoint ~(infer : force:bool ->
+ logic_env:Logic_env.t ->
+ term ->
+ ival Error.result)
+ li args_ival t' ival =
+ LF_env.replace li args_ival ival;
+ let get_res = Error.map (fun x -> x) in
+ let logic_env = Logic_env.make args_ival in
+ let inferred_ival = get_res (infer ~force:true ~logic_env t') in
+ if is_included inferred_ival ival
+ then
ival
+ else
+ fixpoint ~infer li args_ival t' inferred_ival
-end
-= struct
-
- (* Environment to handle recursive functions: this environment stores the
- logic functions that we have already started inferring along with their
- profiles. This is necessary for the fixpoint algorithm. *)
- module LFProf =
- Datatype.Pair_with_collections (Cil_datatype.Logic_info) (Profile)
- (struct
- let module_name = "E_ACSL.Interval.LF_env.LFProf"
- end)
-
- let tbl = LFProf.Hashtbl.create 17
-
- let clear () = LFProf.Hashtbl.clear tbl
-
- let find li profile = LFProf.Hashtbl.find tbl (li,profile)
-
- exception Recursive
-
- let contain li = object
- inherit Visitor.frama_c_inplace
-
- method! vpredicate p =
- match p.pred_content with
- | Papp (li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
- raise Recursive;
- | _ -> Cil.DoChildren
-
- method! vterm t =
- match t.term_node with
- | Tapp(li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
- raise Recursive
- | _ -> Cil.DoChildren
-
- method! vlogic_type _ = Cil.SkipChildren
- end
-
- let is_rec li =
- match li.l_body with
- | LBpred p ->
- (try ignore (Visitor.visitFramacPredicate (contain li) p); false
- with Recursive -> true)
- | LBterm t ->
- (try ignore (Visitor.visitFramacTerm (contain li) t); false
- with Recursive -> true)
- | LBreads _ | LBnone -> false
- | LBinductive _ -> Error.not_yet "Inductive"
-
- let interv_of_typ_containing_interv = function
- | Float _ | Rational | Real | Nan as x ->
- x
- | Ival i ->
- try
- let kind = ikind_of_ival i in
- interv_of_typ (TInt(kind, []))
- with Cil.Not_representable ->
- top_ival
-
- let rec fixpoint ~(infer : force:bool ->
- logic_env:Logic_env.t ->
- term ->
- ival Error.result)
- li args_ival t' ival =
- LFProf.Hashtbl.replace tbl (li, args_ival) ival;
- let get_res = Error.map (fun x -> x) in
- let logic_env = Logic_env.make li.l_profile args_ival in
- let inferred_ival = get_res (infer ~force:true ~logic_env t') in
- if is_included inferred_ival ival
- then
- ival
- else
- fixpoint ~infer li args_ival t' inferred_ival
-
-end
(* Memoization module which retrieves the computed info of some terms *)
module Memo: sig
@@ -619,14 +436,14 @@ end = struct
module Dep = Accesses (Id_term_in_profile) (struct let tbl = dep_tbl end)
let get profile t =
- match profile with
- | [] -> Nondep.get t
- | _ :: _ -> Dep.get (t,profile)
+ if Profile.is_empty profile
+ then Nondep.get t
+ else Dep.get (t,profile)
let memo ~force_infer profile f t =
- match profile with
- | [] -> Nondep.memo ~force_infer f t t
- | _::_ -> Dep.memo ~force_infer f t (t,profile)
+ if Profile.is_empty profile
+ then Nondep.memo ~force_infer f t t
+ else Dep.memo ~force_infer f t (t,profile)
let clear () =
Options.feedback ~level:4 "clearing the typing tables";
@@ -638,23 +455,23 @@ end
the table (because of the fixpoint algorithm). This module associates to a
term in a profile, the profile that should be used to query the table *)
module Widened_profile: sig
- val get: Profile.t -> term -> Profile.t
- val add: Profile.t -> term -> Profile.t -> unit
+ val get: Profile.t -> logic_info -> Profile.t
+ val add: Profile.t -> logic_info -> Profile.t -> unit
val clear: unit -> unit
end = struct
- let widened_profile_tbl : Profile.t Id_term_in_profile.Hashtbl.t
- = Id_term_in_profile.Hashtbl.create 97
+ let widened_profile_tbl : Profile.t LFProf.Hashtbl.t
+ = LFProf.Hashtbl.create 97
- let get profile t =
- Id_term_in_profile.Hashtbl.find_def widened_profile_tbl (t, profile) profile
+ let get profile li =
+ LFProf.Hashtbl.find_def widened_profile_tbl (li, profile) profile
- let add profile t args_ival =
- Id_term_in_profile.Hashtbl.add widened_profile_tbl (t, profile) args_ival
+ let add profile i args_ival =
+ LFProf.Hashtbl.add widened_profile_tbl (i, profile) args_ival
let clear () =
Options.feedback ~level:4 "clearing the typing tables";
- Id_term_in_profile.Hashtbl.clear widened_profile_tbl
+ LFProf.Hashtbl.clear widened_profile_tbl
end
@@ -903,25 +720,25 @@ let rec infer ~force ~logic_env t =
(match li.l_body with
| LBpred _ | LBterm _ ->
let profile =
- List.map
- (fun arg -> get_res (infer ~force ~logic_env arg))
- args
+ Profile.make
+ li.l_profile
+ (List.map
+ (fun arg -> get_res (infer ~force ~logic_env arg))
+ args)
in
(match li.l_body with
| LBpred p ->
- let logic_env = Logic_env.make li.l_profile profile in
+ let logic_env = Logic_env.make profile in
ignore (infer_predicate ~logic_env p);
Ival Ival.zero_or_one
| LBterm t' when LF_env.is_rec li ->
- let
- args_ival = List.map LF_env.interv_of_typ_containing_interv profile
- in
- Widened_profile.add profile t' args_ival;
- (try LF_env.find li args_ival
+ let widened_profile = widen_profile profile in
+ Widened_profile.add profile li widened_profile;
+ (try LF_env.find li widened_profile
with Not_found ->
- LF_env.fixpoint ~infer li args_ival t' (Ival Ival.bottom))
+ fixpoint ~infer li widened_profile t' (Ival Ival.bottom))
| LBterm t' ->
- let logic_env = Logic_env.make li.l_profile profile in
+ let logic_env = Logic_env.make profile in
get_res (infer ~force ~logic_env t')
| _ -> assert false)
| LBnone when li.l_var_info.lv_name = "\\sum" ||
@@ -932,7 +749,7 @@ let rec infer ~force ~logic_env t =
let t2_iv = infer ~force ~logic_env t2 in
let k_iv = Error.map2 join t1_iv t2_iv in
let logic_env_with_k =
- Logic_env.add_let_quantif_binding logic_env k k_iv
+ Logic_env.add logic_env k k_iv
in
let lambda_iv = infer ~force ~logic_env:logic_env_with_k lambda in
Error.map3 (infer_sum_product li.l_var_info) lambda_iv t1_iv t2_iv
@@ -963,7 +780,7 @@ let rec infer ~force ~logic_env t =
let li_v = li.l_var_info in
let i1 = infer ~force ~logic_env li_t in
let logic_env =
- Error.map (Logic_env.add_let_quantif_binding logic_env li_v) i1
+ Error.map (Logic_env.add logic_env li_v) i1
in
get_res (infer ~force ~logic_env t)
| TConst (LReal lr) ->
@@ -1108,7 +925,7 @@ and infer_bound_variable ~loc ~logic_env (t1, lv, t2) =
in
ignore (infer ~force:false ~logic_env t1);
ignore (infer ~force:false ~logic_env t2);
- Logic_env.add_let_quantif_binding logic_env lv i, (t1, lv, t2)
+ Logic_env.add logic_env lv i, (t1, lv, t2)
and infer_predicate ~logic_env p =
let get_res = Error.map (fun x -> x) in
@@ -1118,12 +935,14 @@ and infer_predicate ~logic_env p =
| Papp(li, _, args) ->
(match li.l_body with
| LBpred p ->
- let args_ival =
- List.map
- (fun arg -> get_res (infer ~force:false ~logic_env arg))
- args
+ let profile =
+ Profile.make
+ li.l_profile
+ (List.map
+ (fun arg -> get_res (infer ~force:false ~logic_env arg))
+ args)
in
- let logic_env = Logic_env.make li.l_profile args_ival in
+ let logic_env = Logic_env.make profile in
ignore (infer_predicate ~logic_env p)
| LBnone -> ()
| LBreads _ -> ()
@@ -1154,7 +973,7 @@ and infer_predicate ~logic_env p =
let li_v = li.l_var_info in
let i = infer ~force:false ~logic_env li_t in
let logic_env =
- Error.map (Logic_env.add_let_quantif_binding logic_env li_v) i
+ Error.map (Logic_env.add logic_env li_v) i
in
infer_predicate ~logic_env p
| Pforall _
@@ -1198,7 +1017,7 @@ let infer t =
let i = infer t in
i
-include D
+include Ival_datatype
let typer_visitor ~logic_env = object
inherit E_acsl_visitor.visitor dkey
@@ -1216,7 +1035,7 @@ let typer_visitor ~logic_env = object
end
let infer_program ast =
- let visitor = typer_visitor ~logic_env:(Logic_env.make [] []) in
+ let visitor = typer_visitor ~logic_env:Logic_env.empty in
visitor#visit_file ast
let preprocess_predicate ~logic_env p =
diff --git a/src/plugins/e-acsl/src/analyses/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli
index 3cd608d064774d5f96345cacc17df1c61bf6d3bd..9e4d32ae02e25db53a27eb7b9bd6aae0110d8b9d 100644
--- a/src/plugins/e-acsl/src/analyses/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -47,17 +47,12 @@
Note: this is a partial wrapper on top of [Ival.t], to which most
functions are delegated. *)
+open Analyses_types
+open Analyses_datatype
+
(* ************************************************************************** *)
(** {3 Useful operations on intervals} *)
(* ************************************************************************** *)
-
-type ival =
- | Ival of Ival.t
- | Float of Cil_types.fkind * float option
- | Rational
- | Real
- | Nan
-
type t = ival
val is_included: t -> t -> bool
@@ -92,29 +87,6 @@ val plus_one : ival -> ival
(** @return the result of adding one to an interval. This is because when we
have a condition [x<t], we need to generate [t+1] *)
-(* ************************************************************************** *)
-(** {3 Environment for interval computations} *)
-(* ************************************************************************** *)
-
-(** profile which maps logic variables that are function parameters to their
- interval depending on the arguments at the callsite of the function *)
-module Profile:
- Datatype.S_with_collections with type t = ival list
-
-(** logic environment which maps logic variables to their interval. It is
- composed of:
- - a profile for bindings of function arguments
- - additional bindings for let and quantification binds *)
-module Logic_env: sig
- type t
- (* make a new environment with no bindings for let and quantifications, and
- a profile, to be called at a function callsite. The two lists are assumed
- to have the same length *)
- val make: Cil_types.logic_var list -> ival list -> t
- val add_let_quantif_binding: t -> Cil_types.logic_var -> ival -> t
- val get_profile: t -> Profile.t
-end
-
(* ************************************************************************** *)
(** {3 Inference system} *)
(* ************************************************************************** *)
@@ -152,7 +124,7 @@ val preprocess_code_annot :
val preprocess_term :
logic_env:Logic_env.t -> Cil_types.term -> unit
-val get_widened_profile : Profile.t -> Cil_types.term -> Profile.t
+val get_widened_profile : Profile.t -> Cil_types.logic_info -> Profile.t
val clear : unit -> unit
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index 96b6b3ae3c3784ecaa79f0bc2448f9bd71ce4f64..1b0830126927676e793b79ea589dc27bde37cdb4 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -493,7 +493,7 @@ module rec Transfer
in
if stmt.ghost then
let rtes = Rte.stmt kf stmt in
- let logic_env = Interval.Logic_env.make [] [] in
+ let logic_env = Analyses_datatype.Logic_env.empty in
List.iter (Typing.preprocess_rte ~logic_env) rtes;
List.fold_left
(fun state a -> register_code_annot kf a state) state rtes
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index e7f4c04262e42fa8da45e2e8101850aff5d9222b..038254859b167d67f91ab3d274598b5e87322733 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -21,6 +21,8 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
+open Analyses_datatype
(* Implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour
devenir plus rapide, plus précis et plus mince". *)
@@ -179,21 +181,17 @@ type computed_info =
must be casted to. If [None], no cast needed. *)
}
-module Id_term_with_profile =
- Datatype.Pair_with_collections
- (Misc.Id_term)
- (Interval.Profile)
- (struct let module_name = "E_ACSL.Typing.Id_term_with_profile" end)
-
(* Memoization module which retrieves the computed info of some terms. If the
info is already computed for a term, it is never recomputed *)
module Memo: sig
val memo:
- profile:Interval.Profile.t ->
+ profile: Profile.t ->
(term -> computed_info) ->
term ->
computed_info Error.result
- val get: profile:Interval.Profile.t -> term -> computed_info Error.result
+ val get: profile: Profile.t ->
+ term ->
+ computed_info Error.result
val clear: unit -> unit
end = struct
@@ -224,11 +222,11 @@ end = struct
We distinguish the calls to the function by storing the type of the
arguments corresponding to each call, and we weaken the typing so that it
is invariant when the arguments have the same type. *)
- let dep_tbl : computed_info Error.result Id_term_with_profile.Hashtbl.t
- = Id_term_with_profile.Hashtbl.create 97
+ let dep_tbl : computed_info Error.result Id_term_in_profile.Hashtbl.t
+ = Id_term_in_profile.Hashtbl.create 97
let get_dep profile t =
- try Id_term_with_profile.Hashtbl.find dep_tbl (t,profile)
+ try Id_term_in_profile.Hashtbl.find dep_tbl (t,profile)
with Not_found -> Error.not_memoized ()
let get_nondep t =
@@ -236,9 +234,9 @@ end = struct
with Not_found -> Error.not_memoized ()
let get ~profile t =
- match profile with
- | [] -> get_nondep t
- | _::_ -> get_dep profile t
+ if Profile.is_empty profile
+ then get_nondep t
+ else get_dep profile t
let memo_nondep f t =
try Misc.Id_term.Hashtbl.find tbl t
@@ -252,24 +250,24 @@ end = struct
let memo_dep f t profile =
try
- Id_term_with_profile.Hashtbl.find dep_tbl (t, profile)
+ Id_term_in_profile.Hashtbl.find dep_tbl (t, profile)
with Not_found ->
let x =
try Result.Ok (f t)
with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
in
- Id_term_with_profile.Hashtbl.add dep_tbl (t, profile) x;
+ Id_term_in_profile.Hashtbl.add dep_tbl (t, profile) x;
x
let memo ~profile f t =
- match profile with
- | [] -> memo_nondep f t
- | _::_ -> memo_dep f t profile
+ if Profile.is_empty profile
+ then memo_nondep f t
+ else memo_dep f t profile
let clear () =
Options.feedback ~dkey ~level:4 "clearing the typing tables";
Misc.Id_term.Hashtbl.clear tbl;
- Id_term_with_profile.Hashtbl.clear dep_tbl
+ Id_term_in_profile.Hashtbl.clear dep_tbl
end
@@ -289,11 +287,11 @@ let assert_nan = function
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
let ty_of_interv ?ctx ?(use_gmp_opt = false) = function
- | Interval.Float(fk, _) -> C_float fk
- | Interval.Rational -> Rational
- | Interval.Real -> Real
- | Interval.Nan -> Nan
- | Interval.Ival iv ->
+ | Float(fk, _) -> C_float fk
+ | Rational -> Rational
+ | Real -> Real
+ | Nan -> Nan
+ | Ival iv ->
try
let kind = Interval.ikind_of_ival iv in
(match ctx with
@@ -591,7 +589,11 @@ let rec type_term
?ctx
~profile x))
args;
- let new_profile = List.map (Interval.get_from_profile ~profile) args in
+ let new_profile =
+ Profile.make
+ li.l_profile
+ (List.map (Interval.get_from_profile ~profile) args)
+ in
Stack.push
(fun () ->
ignore (type_predicate ~profile:new_profile p))
@@ -620,8 +622,12 @@ let rec type_term
?ctx
~profile x))
args;
- let new_profile = List.map (Interval.get_from_profile ~profile) args in
- let new_profile = Interval.get_widened_profile new_profile t_body in
+ let new_profile =
+ Profile.make
+ li.l_profile
+ (List.map (Interval.get_from_profile ~profile) args)
+ in
+ let new_profile = Interval.get_widened_profile new_profile li in
let gmp,ctx_body = match li.l_type with
| Some (Ctype typ) ->
false, Some (number_ty_of_typ ~post:false typ)
@@ -776,7 +782,11 @@ and type_predicate ~profile p =
List.iter
(fun x -> ignore (type_term ~use_gmp_opt: true ~profile x))
args;
- let new_profile = List.map (Interval.get_from_profile ~profile) args in
+ let new_profile =
+ Profile.make
+ li.l_profile
+ (List.map (Interval.get_from_profile ~profile) args)
+ in
ignore (type_predicate ~profile:new_profile p);
| LBnone -> ()
| LBreads _ -> ()
@@ -869,7 +879,7 @@ let type_named_predicate ~profile p =
done
let unsafe_set t ?ctx ~logic_env ty =
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
let ctx = match ctx with None -> ty | Some ctx -> ctx in
let mk _ = coerce ~arith_operand:false ~ctx ~op:ty ty in
ignore (Memo.memo mk ~profile t)
@@ -879,15 +889,15 @@ let unsafe_set t ?ctx ~logic_env ty =
(******************************************************************************)
let get_number_ty ~logic_env t =
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
(Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term).ty
let get_integer_op ~logic_env t =
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
(Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term).op
let get_integer_op_of_predicate ~logic_env p =
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
(type_predicate ~profile p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
@@ -903,26 +913,26 @@ let extract_typ t ty =
| Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
let get_typ ~logic_env t =
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
let info =
Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term in
extract_typ t info.ty
let get_op ~logic_env t =
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
let info =
Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term in
extract_typ t info.op
let get_cast ~logic_env t =
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
let info =
Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> None
let get_cast_of_predicate ~logic_env p =
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
let info = type_predicate ~profile p in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> assert false
@@ -946,7 +956,7 @@ let typing_visitor profile = object
end
let type_program ast =
- let visitor = typing_visitor [] in
+ let visitor = typing_visitor Profile.empty in
visitor#visit_file ast
let type_code_annot lenv annot =
@@ -957,7 +967,7 @@ let preprocess_predicate ~logic_env p =
Logic_normalizer.preprocess_predicate p;
Bound_variables.preprocess_predicate p;
Interval.preprocess_predicate ~logic_env p;
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
let visitor = typing_visitor profile in
ignore @@ visitor#visit_predicate p
@@ -965,12 +975,12 @@ let preprocess_rte ~logic_env rte =
Logic_normalizer.preprocess_annot rte;
Bound_variables.preprocess_annot rte;
ignore (Interval.preprocess_code_annot ~logic_env rte);
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
type_code_annot profile rte
let preprocess_term ~use_gmp_opt ?ctx ~logic_env t =
ignore (Interval.preprocess_term ~logic_env t);
- let profile = Interval.Logic_env.get_profile logic_env in
+ let profile = Logic_env.get_profile logic_env in
ignore (type_term ~use_gmp_opt ?ctx ~profile t);
(*
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 2a256562d4b5bcdfbd629dfe0230cc8820b75eb1..a9be9966bbb6b67cbf1364e95a69fe26a478ad89 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -45,6 +45,7 @@
safely be computed in [int]: its result belongs to [[-2;4]]. *)
open Cil_types
+open Analyses_datatype
(******************************************************************************)
(** {2 Datatypes} *)
@@ -91,7 +92,7 @@ val join: number_ty -> number_ty -> number_ty
the other argument is also {!Other}. In this case, the result is [Other]. *)
val number_ty_bound_variable:
- profile:Interval.Profile.t -> term * logic_var * term -> number_ty
+ profile:Profile.t -> term * logic_var * term -> number_ty
(** return the type of a quantified logic variable *)
(******************************************************************************)
@@ -106,36 +107,36 @@ val clear: unit -> unit
{!type_named_predicate} has been previously computed for the given term or
predicate. *)
-val get_number_ty: logic_env:Interval.Logic_env.t -> term -> number_ty
+val get_number_ty: logic_env:Logic_env.t -> term -> number_ty
(** @return the infered type for the given term. *)
-val get_integer_op: logic_env:Interval.Logic_env.t -> term -> number_ty
+val get_integer_op: logic_env:Logic_env.t -> term -> number_ty
(** @return the infered type for the top operation of the given term.
It is meaningless to call this function over a non-arithmetical/logical
operator. *)
val get_integer_op_of_predicate:
- logic_env:Interval.Logic_env.t -> predicate -> number_ty
+ logic_env:Logic_env.t -> predicate -> number_ty
(** @return the infered type for the top operation of the given predicate. *)
-val get_typ: logic_env:Interval.Logic_env.t -> term -> typ
+val get_typ: logic_env:Logic_env.t -> term -> typ
(** Get the type which the given term must be generated to. *)
-val get_op: logic_env:Interval.Logic_env.t -> term -> typ
+val get_op: logic_env:Logic_env.t -> term -> typ
(** Get the type which the operation on top of the given term must be generated
to. *)
-val get_cast: logic_env:Interval.Logic_env.t -> term -> typ option
+val get_cast: logic_env:Logic_env.t -> term -> typ option
(** Get the type which the given term must be converted to (if any). *)
val get_cast_of_predicate:
- logic_env:Interval.Logic_env.t -> predicate -> typ option
+ logic_env:Logic_env.t -> predicate -> typ option
(** Like {!get_cast}, but for predicates. *)
val unsafe_set:
term ->
?ctx:number_ty ->
- logic_env:Interval.Logic_env.t ->
+ logic_env:Logic_env.t ->
number_ty ->
unit
(** Register that the given term has the given type in the given context (if
@@ -157,13 +158,13 @@ val type_program : file -> unit
in a program *)
val preprocess_predicate :
- logic_env:Interval.Logic_env.t ->
+ logic_env:Logic_env.t ->
predicate ->
unit
(** compute and store the types of all the terms in a given predicate *)
val preprocess_rte :
- logic_env:Interval.Logic_env.t ->
+ logic_env:Logic_env.t ->
code_annotation ->
unit
(** compute and store the type of all the terms in a code annotation *)
@@ -171,7 +172,7 @@ val preprocess_rte :
val preprocess_term:
use_gmp_opt:bool ->
?ctx:number_ty ->
- logic_env:Interval.Logic_env.t ->
+ logic_env:Logic_env.t ->
term ->
unit
(** Compute the type of each subterm of the given term in the given context. If
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 6303f0f94b3836181da7e4e460229a939d7ae6f4..5189b00ad2c0f04ddc5d00ee608e4f0977bbd274 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -77,7 +77,7 @@ type t = {
(* list of loop environment for each currently visited loops *)
cpt: int;
(* counter used when generating variables *)
- logic_env_stack: Interval.Logic_env.t list;
+ logic_env_stack: Analyses_datatype.Logic_env.t list;
(* type of variables used in calls to logic functions and predicates *)
kinstr: kinstr;
(* Current kinstr of the environment *)
@@ -112,7 +112,7 @@ let empty =
var_mapping = Logic_var.Map.empty;
loop_envs = [];
cpt = 0;
- logic_env_stack = [ Interval.Logic_env.make [] [] ];
+ logic_env_stack = [ Analyses_datatype.Logic_env.empty ];
kinstr = Kglobal }
let top env = match env.env_stack with
@@ -542,17 +542,17 @@ end
module Logic_env = struct
- let push_new env l_profile profile =
+ let push_new env profile =
let logic_env_stack =
- Interval.Logic_env.make l_profile profile :: env.logic_env_stack
+ Analyses_datatype.Logic_env.make profile :: env.logic_env_stack
in
{env with logic_env_stack = logic_env_stack}
- let add_let_quantif_binding env x ival =
+ let add env x ival =
match env.logic_env_stack with
| curr::_ as logic_env ->
let logic_env_stack =
- Interval.Logic_env.add_let_quantif_binding curr x ival :: logic_env
+ Analyses_datatype.Logic_env.add curr x ival :: logic_env
in
{env with logic_env_stack = logic_env_stack}
| [] -> Options.fatal "logic environment stack is empty"
@@ -563,7 +563,7 @@ module Logic_env = struct
| [] -> Options.fatal "logic environment stack is empty"
let get_profile env =
- Interval.Logic_env.get_profile (get env)
+ Analyses_datatype.Logic_env.get_profile (get env)
let pop env =
match env.logic_env_stack with
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index c6ce8041e037db479a5c59ad507675cd523d7476..a3f7e3c08032f76150163e5bbc542cbf5b0c358f 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -22,6 +22,7 @@
open Cil_types
open Analyses_types
+open Analyses_datatype
open Contract_types
(** Environments.
@@ -177,10 +178,10 @@ val generate_rte: t -> bool
(** Returns the current value of RTE generation for the given environment *)
module Logic_env: sig
- val push_new: t -> logic_var list -> Interval.ival list -> t
- val add_let_quantif_binding : t -> logic_var -> Interval.ival -> t
- val get: t -> Interval.Logic_env.t
- val get_profile : t -> Interval.Profile.t
+ val push_new: t -> Profile.t -> t
+ val add : t -> logic_var -> ival -> t
+ val get: t -> Logic_env.t
+ val get_profile : t -> Profile.t
val pop: t -> t
end
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 47857b638039cba9be0697afb836f99fcdcb3564..bd64174a3f0a07d7bba2b1e08ac7076d7b5913f9 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -22,6 +22,7 @@
open Cil_types
open Cil_datatype
+open Analyses_datatype
module Error = Translation_error
(**************************************************************************)
@@ -196,7 +197,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
let env = Env.push env in
(* fill the typing environment with the function's parameters
before generating the code (code generation invokes typing) *)
- let env = Env.Logic_env.push_new env li.l_profile params_ival in
+ let env = Env.Logic_env.push_new env params_ival in
let env =
List.fold_left2 (Env.Logic_binding.add_binding) env li.l_profile params
in
@@ -268,7 +269,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
(* for each logic_info, associate its possible profiles, i.e. the types of its
parameters + the generated varinfo for the function *)
let memo_tbl:
- kernel_function Interval.Profile.Hashtbl.t Logic_info.Hashtbl.t
+ kernel_function Profile.Hashtbl.t Logic_info.Hashtbl.t
= Logic_info.Hashtbl.create 7
let reset () = Logic_info.Hashtbl.clear memo_tbl
@@ -288,7 +289,7 @@ let add_generated_functions globals =
:: acc
in
aux
- (Interval.Profile.Hashtbl.fold_sorted
+ (Profile.Hashtbl.fold_sorted
(fun _ -> add_fundecl)
params
acc)
@@ -309,7 +310,7 @@ let add_generated_functions globals =
in
let rev_globals =
Logic_info.Hashtbl.fold_sorted
- (fun _ -> Interval.Profile.Hashtbl.fold_sorted
+ (fun _ -> Profile.Hashtbl.fold_sorted
(fun _ -> add_fundec))
memo_tbl
rev_globals
@@ -318,7 +319,7 @@ let add_generated_functions globals =
(* Generate (and memoize) the function body and create the call to the
generated function. *)
-let function_to_exp ~loc ?tapp fname env kf li params_ty params_ival args =
+let function_to_exp ~loc ?tapp fname env kf li params_ty profile args =
let ret_ty =
match tapp with
| Some tapp ->
@@ -328,8 +329,8 @@ let function_to_exp ~loc ?tapp fname env kf li params_ty params_ival args =
in
let gen tbl =
let vi, kf, gen_body =
- generate_kf fname ~loc env ret_ty params_ty params_ival li in
- Interval.Profile.Hashtbl.add tbl params_ival kf;
+ generate_kf fname ~loc env ret_ty params_ty profile li in
+ Profile.Hashtbl.add tbl profile kf;
vi, gen_body
in
(* memoise the function's varinfo *)
@@ -337,12 +338,12 @@ let function_to_exp ~loc ?tapp fname env kf li params_ty params_ival args =
try
let h = Logic_info.Hashtbl.find memo_tbl li in
try
- let kf = Interval.Profile.Hashtbl.find h params_ival in
+ let kf = Profile.Hashtbl.find h profile in
Kernel_function.get_vi kf,
(fun () -> ()) (* body generation already planified *)
with Not_found -> gen h
with Not_found ->
- let h = Interval.Profile.Hashtbl.create 7 in
+ let h = Profile.Hashtbl.create 7 in
Logic_info.Hashtbl.add memo_tbl li h;
gen h
in
@@ -489,13 +490,10 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs =
let gen_fname =
Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
in
- let params_ival = match li.l_body with
- | LBterm t -> Interval.get_widened_profile params_ival t
- | LBpred _ -> params_ival
- | _ -> assert false
- in
+ let profile = Profile.make li.l_profile params_ival in
+ let profile = Interval.get_widened_profile profile li in
let vi, e, env =
- function_to_exp ~loc ?tapp gen_fname env kf li params_ty params_ival args
+ function_to_exp ~loc ?tapp gen_fname env kf li params_ty profile args
in
vi, e, adata, env
end
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 89d2a800aa7c815ba9b7b3b001750c848147a5f4..30128ffc1aa2af95e56f231b91c19a9cfa0b7632 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -64,7 +64,7 @@ let rec has_empty_quantif_with_false_negative ~logic_env = function
let () =
Labels.has_empty_quantif_ref :=
- let logic_env = Interval.Logic_env.make [] [] in
+ let logic_env = Analyses_datatype.Logic_env.empty in
has_empty_quantif_with_false_negative ~logic_env
(* Since we do not support logic functions with labels, we do not need to
pass an actual logic environment *)
@@ -106,7 +106,7 @@ let convert kf env loc ~is_forall quantif =
let env = Env.Logic_scope.extend env lvs in
let logic_env = Env.Logic_env.get env in
let i = Interval.(join (get ~logic_env t1) (get ~logic_env t2)) in
- let env = Env.Logic_env.add_let_quantif_binding env lv i in
+ let env = Env.Logic_env.add env lv i in
lvs :: lvs_guards, env)
([], env)
bound_vars
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index 68e1ed5baca5a65e818a6d460c13b931f444d25a..718ff8816a189ebd9efb54b4d7013e46d63647f8 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -259,7 +259,7 @@ let translations: varinfo Error.result At_data.Hashtbl.t =
let pretranslate_to_exp ~loc kf env pot =
Options.debug ~level:4 "pre-translating %a in profile '%a'"
Pred_or_term.pretty pot
- Interval.Profile.pretty
+ Profile.pretty
(Env.Logic_env.get_profile env);
let e, env, t_opt =
let adata = Assert.no_data in
@@ -299,7 +299,7 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
Options.debug ~level:4
"pre-translating %a in local environment '%a' with lscope '%a'"
Pred_or_term.pretty pot
- Interval.Profile.pretty
+ Profile.pretty
(Env.Logic_env.get_profile env)
Lscope.D.pretty lscope;
let term_to_exp = !term_to_exp_ref in
@@ -315,7 +315,7 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
(Interval.get ~logic_env t2)
in
add_lscope_to_logic_env
- (Env.Logic_env.add_let_quantif_binding env x i)
+ (Env.Logic_env.add env x i)
lscope
| _::_ -> env
in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 63cb0e747fa2fdd5cdc4384940e555f3ee69ee8a..bfa0d27b5ffbd40945bce7928ca3756179cac17f 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -24,6 +24,7 @@
open Cil_types
open Analyses_types
+open Analyses_datatype
let dkey = Options.Dkey.translation
(**************************************************************************)
@@ -868,7 +869,7 @@ and to_exp ~adata ?inplace kf env t =
let generate_rte = Env.generate_rte env in
Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)in local \
environment '%a'"
- Printer.pp_term t generate_rte Interval.Profile.pretty
+ Printer.pp_term t generate_rte Profile.pretty
(Env.Logic_env.get_profile env);
let logic_env = Env.Logic_env.get env in
let t = Logic_normalizer.get_term t in
@@ -922,7 +923,7 @@ let untyped_to_exp typ t =
| _ -> Typing.nan
in
let ctx = Option.map ctx_of_typ typ in
- let logic_env = Interval.Logic_env.make [] [] in
+ let logic_env = Logic_env.empty in
Typing.preprocess_term ~use_gmp_opt:true ~logic_env ?ctx t;
let env = Env.push Env.empty in
let env = Env.set_rte env false in