From 28773784b000fb0bc837a4a15eb1c7cfeea0acd3 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 1 Dec 2021 16:14:30 +0100
Subject: [PATCH] [eacsl] Rename some translation functions
- `Translate_terms.term_to_exp` -> `Translate_terms.to_exp`
- `Translate_predicates.predicate_to_exp` -> `Translate_predicates.to_exp`
- `Translate_predicates.translate_predicate` -> `Translate_predicate.do_it`
- `Translate_rtes.translate_rte_annots` -> `Translate_rtes.rte_annots`
- `Translate_rtes.translate_rte` -> `Translate_rtes.exp`
---
src/plugins/e-acsl/E_ACSL.mli | 12 +--
.../e-acsl/src/code_generator/contract.ml | 10 +--
.../e-acsl/src/code_generator/injector.ml | 2 +-
src/plugins/e-acsl/src/code_generator/libc.ml | 2 +-
.../src/code_generator/translate_annots.ml | 4 +-
.../code_generator/translate_predicates.ml | 54 ++++++------
.../code_generator/translate_predicates.mli | 14 +--
.../src/code_generator/translate_rtes.ml | 16 ++--
.../src/code_generator/translate_rtes.mli | 4 +-
.../src/code_generator/translate_terms.ml | 88 +++++++++----------
.../src/code_generator/translate_terms.mli | 8 +-
11 files changed, 107 insertions(+), 107 deletions(-)
diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index 62c147d84b9..300d3eb1c37 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -30,22 +30,22 @@ module Error: sig
end
module Translate_terms: sig
- exception No_simple_term_translation of term
- val untyped_term_to_exp: typ option -> term -> exp
+ exception No_simple_translation of term
+ val untyped_to_exp: typ option -> term -> exp
(** @raise Typing_error when the given term cannot be typed (something wrong
happened with this term)
@raise Not_yet when the given term contains an unsupported construct.
- @raise No_simple_term_translation when the given term cannot be translated
+ @raise No_simple_translation when the given term cannot be translated
into a single expression. *)
end
module Translate_predicates: sig
- exception No_simple_predicate_translation of predicate
- val untyped_predicate_to_exp: predicate -> exp
+ exception No_simple_translation of predicate
+ val untyped_to_exp: predicate -> exp
(** @raise Typing_error when the given predicate cannot be typed
(something wrong happened with this predicate).
@raise Not_yet when the given predicate contains an unsupported construct.
- @raise No_simple_predicate_translation when the given predicate cannot be
+ @raise No_simple_translation when the given predicate cannot be
translated into a single expression. *)
end
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 1ed15a8d553..f1543b1ad5b 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -99,7 +99,7 @@ end = struct
let set_assumes ~loc env kf contract idx assumes =
let idx_e = Cil.integer ~loc idx in
let assumes_e, _, env =
- Translate_predicates.generalized_untyped_predicate_to_exp
+ Translate_predicates.generalized_untyped_to_exp
~adata:Assert.no_data
kf
env
@@ -327,7 +327,7 @@ let check_default_requires kf kinstr env contract =
let tp_requires = ip_requires.ip_content in
let loc = tp_requires.tp_statement.pred_loc in
Cil.CurrentLoc.set loc;
- Translate_predicates.translate_predicate kf env tp_requires
+ Translate_predicates.do_it kf env tp_requires
else
env)
env
@@ -368,7 +368,7 @@ let check_other_requires kf kinstr env contract =
(* Create runtime check *)
let adata, env = Assert.empty ~loc kf env in
let requires_e, adata, env =
- Translate_predicates.generalized_untyped_predicate_to_exp
+ Translate_predicates.generalized_untyped_to_exp
~adata
kf
env
@@ -653,7 +653,7 @@ let check_post_conds kf kinstr env contract =
| Normal ->
(* If translating the default behavior, directly translate the
predicate *)
- Translate_predicates.translate_predicate kf env tp_post_cond
+ Translate_predicates.do_it kf env tp_post_cond
| Exits | Breaks | Continues | Returns ->
Error.print_not_yet "abnormal termination case in behavior";
env
@@ -691,7 +691,7 @@ let check_post_conds kf kinstr env contract =
(* Create runtime check *)
let adata, env = Assert.empty ~loc kf env in
let post_cond_e, adata, env =
- Translate_predicates.generalized_untyped_predicate_to_exp
+ Translate_predicates.generalized_untyped_to_exp
~adata
kf
env
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 1a953ebb8fe..fba0a65795d 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -215,7 +215,7 @@ let add_new_block_in_stmt env kf stmt =
List.iter
(Typing.preprocess_rte ~lenv:(Env.Local_vars.get env))
rtes;
- Translate_rtes.translate_rte_annots Printer.pp_stmt stmt kf env rtes
+ Translate_rtes.rte_annots Printer.pp_stmt stmt kf env rtes
end else
env
in
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 5c1a5f60c8e..5c0ddb10d20 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -203,7 +203,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
e, env
| Typing.(C_integer _ | C_float _) as nty ->
(* We know that [t] can be translated to a C type, so we start with that *)
- let e, _, env = Translate_terms.term_to_exp ~adata:Assert.no_data kf env t in
+ let e, _, env = Translate_terms.to_exp ~adata:Assert.no_data kf env t in
(* Then we can check if the expression will fit in a [size_t] *)
let sizet = Cil.(theMachine.typeOfSizeOf) in
let sizet_kind = Cil.(theMachine.kindOfSizeOf) in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index 3b88b8ccdd4..20dd56af84a 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -63,7 +63,7 @@ let pre_code_annotation kf stmt env annot =
if l <> [] then
Env.not_yet env "@[assertion applied only on some behaviors@]";
Env.with_rte env true
- ~f:(fun env -> Translate_predicates.translate_predicate kf env p)
+ ~f:(fun env -> Translate_predicates.do_it kf env p)
else
env
| AStmtSpec(l, spec) ->
@@ -81,7 +81,7 @@ let pre_code_annotation kf stmt env annot =
Env.not_yet env "@[invariant applied only on some behaviors@]";
let env =
Env.with_rte env true
- ~f:(fun env -> Translate_predicates.translate_predicate kf env p)
+ ~f:(fun env -> Translate_predicates.do_it kf env p)
in
if loop_invariant then
Env.add_loop_invariant env p
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 f0616ff4952..1a696ce517b 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -92,9 +92,9 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
Extlib.flatten
(Env.with_rte_and_result env true
~f:(fun env ->
- let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
+ let e1, adata, env1 = to_exp ~adata kf env p1 in
let e2, adata, env2 =
- predicate_to_exp ~adata kf (Env.push env1) p2 in
+ to_exp ~adata kf (Env.push env1) p2 in
let res2 = e2, env2 in
let env3 = Env.push env2 in
let name = match name with None -> "and" | Some n -> n in
@@ -114,10 +114,10 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
Extlib.flatten
(Env.with_rte_and_result env true
~f:(fun env ->
- let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
+ let e1, adata, env1 = to_exp ~adata kf env p1 in
let env' = Env.push env1 in
let e2, adata, env2 =
- predicate_to_exp ~adata kf (Env.push env') p2
+ to_exp ~adata kf (Env.push env') p2
in
let res2 = e2, env2 in
let name = match name with None -> "or" | Some n -> n in
@@ -135,7 +135,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
| Pxor _ -> Env.not_yet env "xor"
| Pimplies(p1, p2) ->
(* (p1 ==> p2) <==> !p1 || p2 *)
- predicate_to_exp
+ to_exp
~adata
~name:"implies"
kf
@@ -143,7 +143,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
(Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
| Piff(p1, p2) ->
(* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
- predicate_to_exp
+ to_exp
~adata
~name:"equiv"
kf
@@ -152,18 +152,18 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
(Logic_const.pimplies ~loc (p1, p2),
Logic_const.pimplies ~loc (p2, p1)))
| Pnot p ->
- let e, adata, env = predicate_to_exp ~adata kf env p in
+ let e, adata, env = to_exp ~adata kf env p in
Smart_exp.lnot ~loc e, adata, env
| Pif(t, p2, p3) ->
Extlib.flatten
(Env.with_rte_and_result env true
~f:(fun env ->
- let e1, adata, env1 = Translate_terms.term_to_exp ~adata kf env t in
+ let e1, adata, env1 = Translate_terms.to_exp ~adata kf env t in
let e2, adata, env2 =
- predicate_to_exp ~adata kf (Env.push env1) p2 in
+ to_exp ~adata kf (Env.push env1) p2 in
let res2 = e2, env2 in
let e3, adata, env3 =
- predicate_to_exp ~adata kf (Env.push env2) p3
+ to_exp ~adata kf (Env.push env2) p3
in
let res3 = e3, env3 in
Extlib.nest
@@ -174,7 +174,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
let lvs = Lscope.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 = predicate_to_exp ~adata kf env p in
+ let e, adata, env = to_exp ~adata kf env p in
Interval.Env.remove li.l_var_info;
e, adata, env
| Pforall _ | Pexists _ ->
@@ -182,7 +182,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
let adata, env = Assert.register_pred ~loc kf env p e adata in
e, adata, env
| Pat(p, BuiltinLabel Here) ->
- predicate_to_exp ~adata 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
@@ -192,7 +192,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
e, adata, env
else begin
(* convert [t'] to [e] in a separated local env *)
- let e, adata, env = predicate_to_exp ~adata kf (Env.push env) p' in
+ let e, adata, env = to_exp ~adata kf (Env.push env) p' in
let e, env, sty = Translate_utils.at_to_exp_no_lscope kf env None label e in
assert (sty = Typed_number.C_number);
let adata, env = Assert.register_pred ~loc kf env p e adata in
@@ -281,9 +281,9 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
| Pfreeable _ -> Env.not_yet env "labeled \\freeable"
| Pfresh _ -> Env.not_yet env "\\fresh"
-and predicate_to_exp ~adata ?name kf ?rte env p =
+and to_exp ~adata ?name kf ?rte env p =
match Logic_normalizer.get_pred p with
- | PoT_term t -> Translate_terms.term_to_exp ~adata kf env t
+ | PoT_term t -> Translate_terms.to_exp ~adata kf env t
| PoT_pred p ->
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
Extlib.flatten
@@ -311,19 +311,19 @@ and predicate_to_exp ~adata ?name kf ?rte env p =
e)
))
-let generalized_untyped_predicate_to_exp ~adata ?name kf ?rte env p =
+let generalized_untyped_to_exp ~adata ?name kf ?rte env p =
(* If [rte] is true, it means we're translating the root predicate of an
assertion and we need to generate the RTE for it. The typing environment
must be cleared. Otherwise, if [rte] is false, it means we're already
translating RTE predicates as part of the translation of another root
predicate, and the typing environment must be kept. *)
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
- let e, adata, env = predicate_to_exp ~adata ?name kf ~rte env p in
+ let e, adata, env = to_exp ~adata ?name kf ~rte env p in
assert (Typ.equal (Cil.typeOf e) Cil.intType);
let env = Env.Logic_scope.reset env in
e, adata, env
-let translate_predicate ?pred_to_print kf env p =
+let do_it ?pred_to_print kf env p =
match p.tp_kind with
| Assert | Check ->
Options.feedback ~dkey ~level:3 "translating predicate %a"
@@ -338,7 +338,7 @@ let translate_predicate ?pred_to_print kf env p =
in
let adata, env = Assert.empty ~loc:p.tp_statement.pred_loc kf env in
let e, adata, env =
- generalized_untyped_predicate_to_exp ~adata kf env p.tp_statement
+ generalized_untyped_to_exp ~adata kf env p.tp_statement
in
let stmt, env =
Assert.runtime_check
@@ -358,34 +358,34 @@ let translate_predicate ?pred_to_print kf env p =
let predicate_to_exp_without_rte ~adata kf env p =
(* forget optional argument ?rte and ?name*)
- predicate_to_exp ~adata kf env p
+ to_exp ~adata kf env p
let () =
- Translate_utils.predicate_to_exp_ref := predicate_to_exp;
- Loops.translate_predicate_ref := translate_predicate;
+ Translate_utils.predicate_to_exp_ref := to_exp;
+ Loops.translate_predicate_ref := do_it;
Loops.predicate_to_exp_ref := predicate_to_exp_without_rte;
Quantif.predicate_to_exp_ref := predicate_to_exp_without_rte;
At_with_lscope.predicate_to_exp_ref := predicate_to_exp_without_rte;
Memory_translate.predicate_to_exp_ref := predicate_to_exp_without_rte;
Logic_functions.predicate_to_exp_ref := predicate_to_exp_without_rte
-exception No_simple_predicate_translation of predicate
+exception No_simple_translation of predicate
(* This function is used by Guillaume.
However, it is correct to use it only in specific contexts. *)
-let untyped_predicate_to_exp p =
+let untyped_to_exp p =
let env = Env.push Env.empty in
let env = Env.rte env false in
let e, _, env =
- try generalized_untyped_predicate_to_exp
+ try generalized_untyped_to_exp
~adata:Assert.no_data
(Kernel_function.dummy ())
env
p
- with Rtl.Symbols.Unregistered _ -> raise (No_simple_predicate_translation p)
+ with Rtl.Symbols.Unregistered _ -> raise (No_simple_translation p)
in
if not (Env.has_no_new_stmt env)
- then raise (No_simple_predicate_translation p);
+ then raise (No_simple_translation p);
e
(*
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.mli b/src/plugins/e-acsl/src/code_generator/translate_predicates.mli
index 8bdae9d2b9e..31b470f1ec9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.mli
@@ -24,7 +24,7 @@ open Cil_types
(** Generate C implementations of E-ACSL predicates. *)
-val predicate_to_exp:
+val to_exp:
adata:Assert.t ->
?name:string ->
kernel_function ->
@@ -34,7 +34,7 @@ val predicate_to_exp:
exp * Assert.t * Env.t
(** Convert an ACSL predicate into a corresponding C expression. *)
-val generalized_untyped_predicate_to_exp:
+val generalized_untyped_to_exp:
adata:Assert.t ->
?name:string ->
kernel_function ->
@@ -44,7 +44,7 @@ val generalized_untyped_predicate_to_exp:
exp * Assert.t * Env.t
(** Convert an untyped ACSL predicate into a corresponding C expression. *)
-val translate_predicate:
+val do_it:
?pred_to_print:predicate ->
kernel_function ->
Env.t ->
@@ -54,11 +54,11 @@ val translate_predicate:
If [pred_to_print] is set, then the runtime check will use this predicate as
message. *)
-exception No_simple_predicate_translation of predicate
-(** Exceptin raised if [untyped_predicate_to_exp] would generate new statements
- in the environment *)
+exception No_simple_translation of predicate
+(** Exceptin raised if [untyped_to_exp] would generate new statements in the
+ environment *)
-val untyped_predicate_to_exp: predicate -> exp
+val untyped_to_exp: predicate -> exp
(** Convert an untyped ACSL predicate into a corresponding C expression. This
expression is valid only in certain contexts and shouldn't be used. *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
index 59be7b215c3..5aca164b247 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
@@ -25,7 +25,7 @@
open Cil_types
let dkey = Options.dkey_translation
-let translate_rte_annots pp elt kf env l =
+let rte_annots pp elt kf env l =
let old_kind = Env.annotation_kind env in
let env = Env.set_annotation_kind env Smart_stmt.RTE in
let env =
@@ -42,7 +42,7 @@ let translate_rte_annots pp elt kf env l =
let env = Env.Logic_scope.set_reset env false in
let env =
Env.with_rte env false
- ~f:(fun env -> Translate_predicates.translate_predicate kf env p)
+ ~f:(fun env -> Translate_predicates.do_it kf env p)
in
let env = Env.Logic_scope.set_reset env lscope_reset_old in
env)
@@ -54,9 +54,9 @@ let translate_rte_annots pp elt kf env l =
Env.set_annotation_kind env old_kind
let () =
- Translate_predicates.translate_rte_annots_ref := translate_rte_annots
+ Translate_predicates.translate_rte_annots_ref := rte_annots
-let translate_rte ?filter kf env e =
+let exp ?filter kf env e =
let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
let l = Rte.exp kf stmt e in
let l =
@@ -65,12 +65,12 @@ let translate_rte ?filter kf env e =
| None -> l
in
List.iter (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
- translate_rte_annots Printer.pp_exp e kf env l
+ rte_annots Printer.pp_exp e kf env l
let () =
- Translate_terms.translate_rte_exp_ref := translate_rte;
- Translate_predicates.translate_rte_exp_ref := translate_rte;
- Logic_array.translate_rte_ref := translate_rte
+ Translate_terms.translate_rte_exp_ref := exp;
+ Translate_predicates.translate_rte_exp_ref := exp;
+ Logic_array.translate_rte_ref := exp
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.mli b/src/plugins/e-acsl/src/code_generator/translate_rtes.mli
index 8934e503dcb..11dbe511042 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_rtes.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.mli
@@ -24,7 +24,7 @@ open Cil_types
(** Generate and translate RTE annotations. *)
-val translate_rte_annots:
+val rte_annots:
(Format.formatter -> 'a -> unit) ->
'a ->
kernel_function ->
@@ -34,7 +34,7 @@ val translate_rte_annots:
(** Translate the given RTE annotations into runtime checks in the given
environment. *)
-val translate_rte: ?filter:(code_annotation -> bool) -> kernel_function -> Env.t -> exp -> Env.t
+val exp: ?filter:(code_annotation -> bool) -> kernel_function -> Env.t -> exp -> Env.t
(** Generate RTE annotations from the given expression and translate them in the
given environment. *)
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 e403fc6441e..6c86517b598 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -135,7 +135,7 @@ let rec thost_to_host kf env th = match th with
| Var v -> Var v, env, "result"
| _ -> assert false)
| TMem t ->
- let e, _, env = term_to_exp ~adata:Assert.no_data kf env t in
+ let e, _, env = to_exp ~adata:Assert.no_data kf env t in
Mem e, env, ""
and toffset_to_offset ?loc kf env = function
@@ -144,7 +144,7 @@ and toffset_to_offset ?loc kf env = function
let offset, env = toffset_to_offset ?loc kf env offset in
Field(f, offset), env
| TIndex(t, offset) ->
- let e, _, env = term_to_exp ~adata:Assert.no_data kf env t in
+ let e, _, env = to_exp ~adata:Assert.no_data kf env t in
let offset, env = toffset_to_offset kf env offset in
Index(e, offset), env
| TModel _ -> Env.not_yet env "model"
@@ -171,8 +171,8 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
| Some e -> e
| _ -> Options.fatal "unexpected error in \\sum translation"
in
- let e_min, adata, env = term_to_exp ~adata kf env t_min in
- let e_max, adata, env = term_to_exp ~adata kf env t_max in
+ let e_min, adata, env = to_exp ~adata kf env t_min in
+ let e_max, adata, env = to_exp ~adata kf env t_max in
let k_as_varinfo, k_as_exp, env = Env.Logic_binding.add ~ty:ty_k env kf k in
let init_k_stmt = Gmp.init_set ~loc (Cil.var k_as_varinfo) k_as_exp e_min in
(* variable initialization *)
@@ -196,7 +196,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
in
(* lambda_as_varinfo assignment *)
let env = Env.push env in
- let e_lbd, _, env = term_to_exp ~adata:Assert.no_data kf env lt in
+ let e_lbd, _, env = to_exp ~adata:Assert.no_data kf env lt in
Interval.Env.remove k;
let lbd_stmt,env =
Env.pop_and_get env
@@ -276,7 +276,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
let adata, env = Assert.register_term ~loc kf env ~force:true t e adata in
e, adata, env, Typed_number.C_number, "sizeof"
| TSizeOfE t' ->
- let e', _, env = term_to_exp ~adata:Assert.no_data kf env t' in
+ let e', _, env = to_exp ~adata:Assert.no_data kf env t' in
let e = Cil.sizeOf ~loc (Cil.typeOf e') in
let adata, env = Assert.register_term ~loc kf env ~force:true t e adata in
e, adata, env, Typed_number.C_number, "sizeof"
@@ -289,13 +289,13 @@ and context_insensitive_term_to_exp ~adata kf env t =
let adata, env = Assert.register_term ~loc kf env t e adata in
e, adata, env, Typed_number.C_number, "alignof"
| TAlignOfE t' ->
- let e', _, env = term_to_exp ~adata:Assert.no_data kf env t' in
+ let e', _, env = to_exp ~adata:Assert.no_data kf env t' in
let e = Cil.new_exp ~loc (AlignOfE e') in
let adata, env = Assert.register_term ~loc kf env t e adata in
e, adata, env, Typed_number.C_number, "alignof"
| TUnOp(Neg | BNot as op, t') ->
let ty = Typing.get_typ ~lenv t in
- let e, adata, env = term_to_exp ~adata kf env t' in
+ let e, adata, env = to_exp ~adata kf env t' in
if Gmp_types.Z.is_t ty then
let name, vname = match op with
| Neg -> "__gmpz_neg", "neg"
@@ -339,14 +339,14 @@ and context_insensitive_term_to_exp ~adata kf env t =
e, adata, env, Typed_number.C_number, ""
else begin
assert (Cil.isIntegralType ty);
- let e, adata, env = term_to_exp ~adata kf env t in
+ let e, adata, env = to_exp ~adata kf env t in
let e = Smart_exp.lnot ~loc e in
e, adata, env, Typed_number.C_number, ""
end
| TBinOp(PlusA | MinusA | Mult as bop, t1, t2) ->
let ty = Typing.get_typ ~lenv t in
- let e1, adata, env = term_to_exp ~adata kf env t1 in
- let e2, adata, env = term_to_exp ~adata kf env t2 in
+ let e1, adata, env = to_exp ~adata kf env t1 in
+ let e2, adata, env = to_exp ~adata kf env t2 in
if Gmp_types.Z.is_t ty then
let name = Gmp.name_of_mpz_arith_bop bop in
let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
@@ -368,8 +368,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
end
| TBinOp(Div | Mod as bop, t1, t2) ->
let ty = Typing.get_typ ~lenv t in
- let e1, adata, env = term_to_exp ~adata kf env t1 in
- let t2_to_exp adata env = term_to_exp ~adata kf env t2 in
+ let e1, adata, env = to_exp ~adata kf env t1 in
+ let t2_to_exp adata env = to_exp ~adata kf env t2 in
if Gmp_types.Z.is_t ty then
(* Creating a second assertion context that will hold the data contributing
to the guard of the denominator. The context will be merged to [adata]
@@ -434,8 +434,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
| TBinOp((Shiftlt | Shiftrt) as bop, t1, t2) ->
(* left/right shift *)
let ty = Typing.get_typ ~lenv t in
- let t1_to_exp adata env = term_to_exp ~adata kf env t1 in
- let t2_to_exp adata env = term_to_exp ~adata kf env t2 in
+ let t1_to_exp adata env = to_exp ~adata kf env t1 in
+ let t2_to_exp adata env = to_exp ~adata kf env t2 in
if Gmp_types.Z.is_t ty then
(* Creating secondary assertion contexts [adata1] and [adata2] to hold the
data contributing to the guards of [t1] and [t2].
@@ -621,10 +621,10 @@ and context_insensitive_term_to_exp ~adata kf env t =
Extlib.flatten
(Env.with_rte_and_result env true
~f:(fun env ->
- let e1, adata, env1 = term_to_exp ~adata kf env t1 in
+ let e1, adata, env1 = to_exp ~adata kf env t1 in
let env' = Env.push env1 in
let e2, adata, env2 =
- term_to_exp ~adata kf (Env.push env') t2
+ to_exp ~adata kf (Env.push env') t2
in
let res2 = e2, env2 in
Extlib.nest
@@ -640,9 +640,9 @@ and context_insensitive_term_to_exp ~adata kf env t =
Extlib.flatten
(Env.with_rte_and_result env true
~f:(fun env ->
- let e1, adata, env1 = term_to_exp ~adata kf env t1 in
+ let e1, adata, env1 = to_exp ~adata kf env t1 in
let e2, adata, env2 =
- term_to_exp ~adata kf (Env.push env1) t2
+ to_exp ~adata kf (Env.push env1) t2
in
let res2 = e2, env2 in
let env3 = Env.push env2 in
@@ -656,8 +656,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
| TBinOp((BOr | BXor | BAnd) as bop, t1, t2) ->
(* other logic/arith operators *)
let ty = Typing.get_typ ~lenv t in
- let e1, adata, env = term_to_exp ~adata kf env t1 in
- let e2, adata, env = term_to_exp ~adata kf env t2 in
+ let e1, adata, env = to_exp ~adata kf env t1 in
+ let e2, adata, env = to_exp ~adata kf env t2 in
if Gmp_types.Z.is_t ty then
let mk_stmts _v e =
let name = Gmp.name_of_mpz_arith_bop bop in
@@ -685,15 +685,15 @@ and context_insensitive_term_to_exp ~adata kf env t =
| Ctype ty -> ty
| _ -> assert false
in
- let e1, adata, env = term_to_exp ~adata kf env t1 in
- let e2, adata, env = term_to_exp ~adata kf env t2 in
+ let e1, adata, env = to_exp ~adata kf env t1 in
+ let e2, adata, env = to_exp ~adata kf env t2 in
let e = Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)) in
e, adata, env, Typed_number.C_number, ""
| TBinOp(MinusPP, t1, t2) ->
begin match Typing.get_number_ty ~lenv t with
| Typing.C_integer _ ->
- let e1, adata, env = term_to_exp ~adata kf env t1 in
- let e2, adata, env = term_to_exp ~adata kf env t2 in
+ let e1, adata, env = to_exp ~adata kf env t1 in
+ let e2, adata, env = to_exp ~adata kf env t2 in
let ty = Typing.get_typ ~lenv t in
let e = Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)) in
e, adata, env, Typed_number.C_number, ""
@@ -703,7 +703,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
assert false
end
| TCastE(ty, t') ->
- let e, adata, env = term_to_exp ~adata kf env t' in
+ let e, adata, env = to_exp ~adata kf env t' in
let e, env =
Typed_number.add_cast
~loc
@@ -742,7 +742,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
| Tapp(_, _ :: _, _) ->
Env.not_yet env "logic functions with labels"
| Tlambda(_, lt) ->
- let exp, adata, env = term_to_exp ~adata kf env lt in
+ let exp, adata, env = to_exp ~adata kf env lt in
exp, adata, env, Typed_number.C_number, ""
| TDataCons _ -> Env.not_yet env "constructor"
| Tif(t1, t2, t3) ->
@@ -750,13 +750,13 @@ and context_insensitive_term_to_exp ~adata kf env t =
Extlib.flatten
(Env.with_rte_and_result env true
~f:(fun env ->
- let e1, adata, env1 = term_to_exp ~adata kf env t1 in
+ let e1, adata, env1 = to_exp ~adata kf env t1 in
let e2, adata, env2 =
- term_to_exp ~adata kf (Env.push env1) t2
+ to_exp ~adata kf (Env.push env1) t2
in
let res2 = e2, env2 in
let e3, adata, env3 =
- term_to_exp ~adata kf (Env.push env2) t3
+ to_exp ~adata kf (Env.push env2) t3
in
let res3 = e3, env3 in
Extlib.nest
@@ -766,7 +766,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
in
e, adata, env, Typed_number.C_number, ""
| Tat(t, BuiltinLabel Here) ->
- let e, adata, env = term_to_exp ~adata kf env t in
+ let e, adata, env = to_exp ~adata kf env t in
e, adata, env, Typed_number.C_number, ""
| Tat(t', label) ->
let lscope = Env.Logic_scope.get env in
@@ -776,7 +776,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
let adata, env = Assert.register_term ~loc kf env t e adata in
e, adata, env, Typed_number.C_number, ""
else
- let e, _, env = term_to_exp ~adata:Assert.no_data kf (Env.push env) t' in
+ let e, _, env = to_exp ~adata:Assert.no_data kf (Env.push env) t' in
let e, env, sty = Translate_utils.at_to_exp_no_lscope kf env (Some t) label e in
let adata, env = Assert.register_term ~loc kf env t e adata in
e, adata, env, sty, ""
@@ -828,14 +828,14 @@ and context_insensitive_term_to_exp ~adata kf env t =
let lvs = Lscope.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 = term_to_exp ~adata kf env t in
+ let e, adata, env = to_exp ~adata kf env t in
Interval.Env.remove li.l_var_info;
e, adata, env, Typed_number.C_number, ""
(* Convert an ACSL term into a corresponding C expression (if any) in the given
environment. Also extend this environment in order to include the generating
constructs. *)
-and term_to_exp ~adata kf env t =
+and to_exp ~adata 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'"
@@ -865,16 +865,16 @@ and term_to_exp ~adata kf env t =
))
let () =
- Translate_utils.term_to_exp_ref := term_to_exp;
- Loops.term_to_exp_ref := term_to_exp;
- At_with_lscope.term_to_exp_ref := term_to_exp;
- Memory_translate.term_to_exp_ref := term_to_exp;
- Logic_functions.term_to_exp_ref := term_to_exp
+ Translate_utils.term_to_exp_ref := to_exp;
+ Loops.term_to_exp_ref := to_exp;
+ At_with_lscope.term_to_exp_ref := to_exp;
+ Memory_translate.term_to_exp_ref := to_exp;
+ Logic_functions.term_to_exp_ref := to_exp
-exception No_simple_term_translation of term
+exception No_simple_translation of term
(* This function is used by plug-in [Cfp]. *)
-let untyped_term_to_exp typ t =
+let untyped_to_exp typ t =
(* infer a context from the given [typ] whenever possible *)
let ctx_of_typ ty =
if Gmp_types.Z.is_t ty then Typing.gmpz
@@ -890,10 +890,10 @@ let untyped_term_to_exp typ t =
let env = Env.push Env.empty in
let env = Env.rte env false in
let e, _, env =
- try term_to_exp ~adata:Assert.no_data (Kernel_function.dummy ()) env t
- with Rtl.Symbols.Unregistered _ -> raise (No_simple_term_translation t)
+ try to_exp ~adata:Assert.no_data (Kernel_function.dummy ()) env t
+ with Rtl.Symbols.Unregistered _ -> raise (No_simple_translation t)
in
- if not (Env.has_no_new_stmt env) then raise (No_simple_term_translation t);
+ if not (Env.has_no_new_stmt env) then raise (No_simple_translation t);
e
(*
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.mli b/src/plugins/e-acsl/src/code_generator/translate_terms.mli
index ac50cf18e80..0bb31e3c4b2 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.mli
@@ -24,7 +24,7 @@ open Cil_types
(** Generate C implementations of E-ACSL terms. *)
-val term_to_exp:
+val to_exp:
adata:Assert.t ->
kernel_function ->
Env.t ->
@@ -32,11 +32,11 @@ val term_to_exp:
exp * Assert.t * Env.t
(** Convert an ACSL term into a corresponding C expression. *)
-exception No_simple_term_translation of term
-(** Exceptin raised if [untyped_term_to_exp] would generate new statements in
+exception No_simple_translation of term
+(** Exceptin raised if [untyped_to_exp] would generate new statements in
the environment *)
-val untyped_term_to_exp: typ option -> term -> exp
+val untyped_to_exp: typ option -> term -> exp
(** Convert an untyped ACSL term into a corresponding C expression. *)
(**************************************************************************)
--
GitLab