diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index d1e1b4015f0766102e8d1a390fc7cfa40a7396ff..8f4676a6ad61437bad9697f6289472fcd27d471f 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -56,7 +56,12 @@ SRC_PROJECT_INITIALIZER:=\
$(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
# analyses
+ANALYSES_CMI:= \
+ analyses_types
+ANALYSES_CMI:=$(addprefix src/analyses/, $(ANALYSES_CMI))
+
SRC_ANALYSES:= \
+ analyses_datatype \
rte \
lscope \
e_acsl_visitor \
@@ -128,6 +133,7 @@ PLUGIN_CMO:= src/local_config \
src/main
PLUGIN_CMI:= \
$(LIBRARIES_CMI) \
+ $(ANALYSES_CMI) \
$(CODE_GENERATOR_CMI)
PLUGIN_HAS_MLI:=yes
PLUGIN_DISTRIBUTED:=yes
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 7830de6a9bfb72ffc80a22dee953fb2e95f922ee..d98aa7a680f80010b2338159bef7b5018c389b70 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -79,6 +79,9 @@ share/e-acsl/observation_model/e_acsl_observation_model.c: CEA_LGPL_OR_PROPRIETA
share/e-acsl/observation_model/e_acsl_observation_model.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/analyses_datatype.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/analyses_datatype.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/analyses_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/bound_variables.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/bound_variables.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/e_acsl_visitor.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b638097ad1f4515525721ceb90d1be5a8e13b1b8
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Datatypes for analyses types *)
+
+open Cil_datatype
+open Analyses_types
+
+module PredOrTerm =
+ Datatype.Make_with_collections
+ (struct
+ type t = pred_or_term
+
+ let name = "E_ACSL.PredOrTerm"
+
+ let reprs =
+ let reprs =
+ List.fold_left
+ (fun reprs t -> PoT_term t :: reprs)
+ []
+ Term.reprs
+ in
+ List.fold_left
+ (fun reprs p -> PoT_pred p :: reprs)
+ reprs
+ Predicate.reprs
+
+ include Datatype.Undefined
+
+ let compare pot1 pot2 =
+ match pot1, pot2 with
+ | PoT_pred _, PoT_term _ -> -1
+ | PoT_term _, PoT_pred _ -> 1
+ | PoT_pred p1, PoT_pred p2 -> PredicateStructEq.compare p1 p2
+ | PoT_term t1, PoT_term t2 -> Term.compare t1 t2
+
+ let equal = Datatype.from_compare
+
+ let hash = function
+ | PoT_pred p -> 7 * PredicateStructEq.hash p
+ | PoT_term t -> 97 * Term.hash t
+
+ let pretty fmt = function
+ | PoT_pred p -> Printer.pp_predicate fmt p
+ | PoT_term t -> Printer.pp_term fmt t
+
+ let varname _ = "pred_or_term"
+ end)
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
new file mode 100644
index 0000000000000000000000000000000000000000..212b5887cd5e0eec1b4acbb766b7b28a05ef1c75
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Datatypes for analyses types *)
+
+open Analyses_types
+
+module PredOrTerm: Datatype.S_with_collections with type t = pred_or_term
diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.mli b/src/plugins/e-acsl/src/analyses/analyses_types.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d670f9d0e2052217223c588532bda38eb7f278e4
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/analyses_types.mli
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Types used by E-ACSL analyses *)
+
+open Cil_types
+
+type lscope_var =
+ | Lvs_let of logic_var * term (* the expression to which the lv is binded *)
+ | Lvs_quantif of term * relation * logic_var * relation * term
+ | Lvs_formal of logic_var * logic_info (* the logic definition *)
+ | Lvs_global of logic_var * term (* same as Lvs_let *)
+
+type lscope = lscope_var list
+
+type pred_or_term =
+ | PoT_pred of predicate
+ | PoT_term of term
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
index 2f48bf1f49dd81b70298cc4166004c646b76f53d..bc2b125769d3f2132e603764a329775e06911caf 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
@@ -21,8 +21,7 @@
(**************************************************************************)
open Cil_types
-
-type pred_or_term = Lscope.pred_or_term
+open Analyses_types
module Id_predicate =
Datatype.Make_with_collections
@@ -53,7 +52,7 @@ end = struct
let get_pred p =
try Id_predicate.Hashtbl.find tbl_pred p
- with Not_found -> Lscope.PoT_pred p
+ with Not_found -> PoT_pred p
let memo_pred process p =
try ignore (Id_predicate.Hashtbl.find tbl_pred p) with
@@ -98,7 +97,7 @@ let preprocess_pred ~loc p =
| Pvalid _ -> Logic_const.pvalid ~loc (llabel, t)
| _ -> assert false
in
- Some (Lscope.PoT_pred (Logic_const.pand ~loc (init, p_copy)))
+ Some (PoT_pred (Logic_const.pand ~loc (init, p_copy)))
| _ -> None
end
| _ -> None
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
index f0cc0782b21005038303b71f706ce3444c26c1d2..7eafabeb5287e0dcae03d0a935438077ad5117d7 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
@@ -30,6 +30,7 @@
*)
open Cil_types
+open Analyses_types
val preprocess : file -> unit
(** Preprocess all the predicates of the ast and store the results *)
@@ -41,7 +42,7 @@ val preprocess_annot : code_annotation -> unit
val preprocess_predicate : predicate -> unit
(** Preprocess a predicate and its children and store the results *)
-val get_pred : predicate -> Lscope.pred_or_term
+val get_pred : predicate -> pred_or_term
(** Retrieve the preprocessed form of a predicate *)
val get_term : term -> term
(** Retrieve the preprocessed form of a term *)
diff --git a/src/plugins/e-acsl/src/analyses/lscope.ml b/src/plugins/e-acsl/src/analyses/lscope.ml
index 6d98b00323987bc5912e9610af6d24819e7a689e..f47297a7cd0a167fff2a19d03f47aa101f1c8202 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.ml
+++ b/src/plugins/e-acsl/src/analyses/lscope.ml
@@ -21,14 +21,9 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
-type lscope_var =
- | Lvs_let of logic_var * term
- | Lvs_quantif of term * relation * logic_var * relation * term
- | Lvs_formal of logic_var * logic_info
- | Lvs_global of logic_var * term
-
-type t = lscope_var list
+type t = lscope
(* The logic scope is usually small, so a list is fine instead of a Map *)
let empty = []
@@ -47,8 +42,6 @@ let exists lv t =
in
List.exists is_lv t
-type pred_or_term = PoT_pred of predicate | PoT_term of term
-
exception Lscope_used
let is_used lscope pot =
let o = object inherit Visitor.frama_c_inplace
diff --git a/src/plugins/e-acsl/src/analyses/lscope.mli b/src/plugins/e-acsl/src/analyses/lscope.mli
index 56d5707fdaaccdb61ef16d49d46d7883fc7da833..a268624a7845d84473f3dc731c518e27a8a842e4 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.mli
+++ b/src/plugins/e-acsl/src/analyses/lscope.mli
@@ -20,19 +20,13 @@
(* *)
(**************************************************************************)
-open Cil_types
+open Analyses_types
(* Handle the logic scope of a term.
We define the logic scope of a term [t] to be the set of PURELY logic
variables that are bound in [t] in case of use. *)
-type lscope_var =
- | Lvs_let of logic_var * term (* the expression to which the lv is binded *)
- | Lvs_quantif of term * relation * logic_var * relation * term
- | Lvs_formal of logic_var * logic_info (* the logic definition *)
- | Lvs_global of logic_var * term (* same as Lvs_let *)
-
-type t
+type t = lscope
val empty: t
(* Create an empty logic scope. *)
@@ -48,7 +42,6 @@ val get_all: t -> lscope_var list
The first element is the first [lscope_var] that was added to [t], the
second element is the second [lscope_var] that was added to [t], an so on. *)
-type pred_or_term = PoT_pred of predicate | PoT_term of term
val is_used: t -> pred_or_term -> bool
(* [is_used lscope pot] returns [true] iff [pot] uses a variable from
[lscope]. *)
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index d5e5e2dd5649cbd2d79f790c84389f93460d2bf4..875e75bbb287c7e92cd8c80a838a6b710c0fc29c 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
(**************************************************************************)
(********************** Forward references ********************************)
@@ -85,10 +86,10 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
match lscope with
| [] ->
sizes_and_shifts
- | Lscope.Lvs_quantif(tmin, _, _, _, tmax) ::_
+ | Lvs_quantif(tmin, _, _, _, tmax) ::_
when Misc.term_has_lv_from_vi tmin || Misc.term_has_lv_from_vi tmax ->
Error.not_yet "\\at with logic variable linked to C variable"
- | Lscope.Lvs_quantif(tmin, rel1, lv, rel2, tmax) :: lscope' ->
+ | Lvs_quantif(tmin, rel1, lv, rel2, tmax) :: lscope' ->
let t_size = Logic_const.term ~loc (TBinOp(MinusA, tmax, tmin)) Linteger in
let t_size = match rel1, rel2 with
| Rle, Rle ->
@@ -146,14 +147,14 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
(* Returning *)
let sizes_and_shifts = (t_size, t_shifted) :: sizes_and_shifts in
sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
- | (Lscope.Lvs_let(_, t) | Lscope.Lvs_global(_, t)) :: _
+ | (Lvs_let(_, t) | Lvs_global(_, t)) :: _
when Misc.term_has_lv_from_vi t ->
Error.not_yet "\\at with logic variable linked to C variable"
- | Lscope.Lvs_let _ :: lscope' ->
+ | Lvs_let _ :: lscope' ->
sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
- | Lscope.Lvs_formal _ :: _ ->
+ | Lvs_formal _ :: _ ->
Error.not_yet "\\at using formal variable of a logic function"
- | Lscope.Lvs_global _ :: _ ->
+ | Lvs_global _ :: _ ->
Error.not_yet "\\at using global logic variable"
let size_from_sizes_and_shifts ~loc = function
@@ -240,9 +241,9 @@ let to_exp ~loc kf env pot label =
in
(* Creating the pointer *)
let ty = match pot with
- | Lscope.PoT_pred _ ->
+ | PoT_pred _ ->
Cil.intType
- | Lscope.PoT_term t ->
+ | PoT_term t ->
let lenv = (Env.Local_vars.get env) in
begin match Typing.get_number_ty ~lenv t with
| Typing.(C_integer _ | C_float _ | Nan) ->
@@ -310,7 +311,7 @@ let to_exp ~loc kf env pot label =
let term_to_exp = !term_to_exp_ref ~adata:Assert.no_data in
let named_predicate_to_exp = !predicate_to_exp_ref ~adata:Assert.no_data in
match pot with
- | Lscope.PoT_pred p ->
+ | PoT_pred p ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e, _, env = named_predicate_to_exp kf env p in
@@ -324,7 +325,7 @@ let to_exp ~loc kf env pot label =
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Smart_stmt.block_stmt block ], env
- | Lscope.PoT_term t ->
+ | PoT_term t ->
begin match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
| Typing.(C_integer _ | C_float _ | Nan) ->
let env = Env.push env in
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli b/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
index 2f23c959c3ec89aaf8425b8d7f9ccf239c409c7f..989404e5a2b5a37d99db7b89b8c3a16f4d9a172d 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
@@ -22,6 +22,7 @@
open Cil_types
open Cil_datatype
+open Analyses_types
(* Convert \at on terms or predicates in which we can find purely
logic variable. *)
@@ -32,7 +33,7 @@ open Cil_datatype
val to_exp:
loc:Location.t -> kernel_function -> Env.t ->
- Lscope.pred_or_term -> logic_label -> exp * Env.t
+ pred_or_term -> logic_label -> exp * Env.t
(*****************************************************************************)
(**************************** Handling memory ********************************)
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 22101128c078bb92b59e976952a9c42d0edd217e..ab80eef94300e29825d0f6ce24909311a5e12d9d 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
open Contract_types
(** Environments.
@@ -129,7 +130,7 @@ module Logic_scope: sig
val get: t -> Lscope.t
(** Return the logic scope associated to the environment. *)
- val extend: t -> Lscope.lscope_var -> t
+ val extend: t -> lscope_var -> t
(** Add a new logic variable with its associated information in the
logic scope of the environment. *)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 0b3150015a18099bc1f675d5b6ef1b7735b28505..39d5e48204f1572c8eb19af1fd8935a9e15908d6 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -22,6 +22,7 @@
open Cil
open Cil_types
+open Analyses_types
(**************************************************************************)
(********************** Forward references ********************************)
@@ -291,7 +292,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
match lscope_vars with
| [] ->
mk_innermost_block env
- | Lscope.Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
+ | Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
assert (rel1 == Rle && rel2 == Rlt);
Typing.type_term ~use_gmp_opt:false ~lenv t1;
Typing.type_term ~use_gmp_opt:false ~lenv t2;
@@ -418,7 +419,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
(* remove logic binding before returning *)
Env.Logic_binding.remove env logic_x;
[ start ; stmt ], env
- | Lscope.Lvs_let(lv, t) :: lscope_vars' ->
+ | Lvs_let(lv, t) :: lscope_vars' ->
let ty = Typing.get_typ ~lenv t in
let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env kf lv in
let e, _, env = term_to_exp kf env t in
@@ -434,10 +435,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Env.Logic_binding.remove env lv;
(* return *)
let_stmt :: stmts, env
- | Lscope.Lvs_formal _ :: _ ->
+ | Lvs_formal _ :: _ ->
Error.not_yet
"creating nested loops from formal variable of a logic function"
- | Lscope.Lvs_global _ :: _ ->
+ | Lvs_global _ :: _ ->
Error.not_yet
"creating nested loops from global logic variable"
diff --git a/src/plugins/e-acsl/src/code_generator/loops.mli b/src/plugins/e-acsl/src/code_generator/loops.mli
index 6e07b47cc7d3a1490e90ee5195fe063d1844214c..9ac68edab8b98aa546a8375d629446e493b044d0 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.mli
+++ b/src/plugins/e-acsl/src/code_generator/loops.mli
@@ -23,6 +23,7 @@
(** Loop specific actions. *)
open Cil_types
+open Analyses_types
(**************************************************************************)
(************************* Loop annotations *******************************)
@@ -40,7 +41,7 @@ val handle_annotations:
val mk_nested_loops:
loc:location -> (Env.t -> stmt list * Env.t) -> kernel_function -> Env.t ->
- Lscope.lscope_var list -> stmt list * Env.t
+ lscope_var list -> stmt list * Env.t
(** [mk_nested_loops ~loc mk_innermost_block kf env lvars] creates nested
loops (with the proper statements for initializing the loop counters)
from the list of logic variables [lvars]. Quantified variables create
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index ee06ec1a361e00a594d3074f20d374b0b81886d2..ed874a35d5e73792b22f433a4fe36c5628bc529b 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -22,6 +22,7 @@
open Cil_types
open Cil
+open Analyses_types
(** Forward reference for [Translate_predicates.to_exp]. *)
let predicate_to_exp_ref
@@ -92,7 +93,7 @@ let convert kf env loc ~is_forall quantif =
and update logic scope in the process *)
let lvs_guards, env = List.fold_right
(fun (t1, lv, t2) (lvs_guards, env) ->
- let lvs = Lscope.Lvs_quantif (t1, Rle, lv, Rlt, t2) in
+ let lvs = Lvs_quantif (t1, Rle, lv, Rlt, t2) in
let env = Env.Logic_scope.extend env lvs in
lvs :: lvs_guards, env)
bound_vars
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index ad2490808de071d5a3775c82dd9c53fac67f44ea..cdef74589fc2d34d1b09de4257f79d414ef152b1 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -24,6 +24,7 @@
open Cil_types
open Cil_datatype
+open Analyses_types
let dkey = Options.Dkey.translation
(**************************************************************************)
@@ -180,7 +181,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
(Translate_utils.conditional_to_exp ~loc kf None e1 res2 res3)
))
| Plet(li, p) ->
- let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
+ let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
let env = Env.Logic_scope.extend env lvs in
let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
let e, adata, env = to_exp ~adata kf env p in
@@ -194,7 +195,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
to_exp ~adata kf env p
| Pat(p', label) ->
let lscope = Env.Logic_scope.get env in
- let pot = Lscope.PoT_pred p' in
+ let pot = PoT_pred p' in
if Lscope.is_used lscope pot then
let e, env = At_with_lscope.to_exp ~loc kf env pot label in
let adata, env = Assert.register_pred ~loc kf env p e adata 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 3e03d9b22a4a31a3012051e1109c4822e548469f..fd58e8af3acc640d4f4362e59eb189fbd94e0fe6 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -23,6 +23,7 @@
(** Generate C implementations of E-ACSL terms. *)
open Cil_types
+open Analyses_types
let dkey = Options.Dkey.translation
(**************************************************************************)
@@ -797,7 +798,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
e, adata, env, Typed_number.C_number, ""
| Tat(t', label) ->
let lscope = Env.Logic_scope.get env in
- let pot = Lscope.PoT_term t' in
+ let pot = PoT_term t' in
if Lscope.is_used lscope pot then
let e, env = At_with_lscope.to_exp ~loc kf env pot label in
let adata, env = Assert.register_term ~loc kf env t e adata in
@@ -854,7 +855,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
| Tcomprehension _ -> Env.not_yet env "tset comprehension"
| Trange _ -> Env.not_yet env "range"
| Tlet(li, t) ->
- let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
+ let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
let env = Env.Logic_scope.extend env lvs in
let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
let e, adata, env = to_exp ~adata kf env t in