From 57aa01bb5db35253514189423bc2f625cabfedff Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Fri, 8 Sep 2023 09:39:59 +0200
Subject: [PATCH] [e-acsl] cosmetics: wrapper function for refs
---
.../src/code_generator/translate_utils.ml | 17 +++++++++++------
1 file changed, 11 insertions(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index 8ebd2f18213..acaec461509 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -39,6 +39,8 @@ let term_to_exp_ref
=
ref (fun ~adata:_ _kf _env _t -> Extlib.mk_labeled_fun "term_to_exp_ref")
+let term_to_exp ~adata kf env t = !term_to_exp_ref ~adata kf env t
+
let predicate_to_exp_ref
: (adata:Assert.t ->
?name:string ->
@@ -51,6 +53,9 @@ let predicate_to_exp_ref
ref (fun ~adata:_ ?name:_ _kf ?rte:_ _env _p ->
Extlib.mk_labeled_fun "predicate_to_exp_ref")
+let predicate_to_exp ~adata ?name kf ?rte env p =
+ !predicate_to_exp_ref ~adata ?name kf ?rte env p
+
(**************************************************************************)
(********************** Utility functions *********************************)
(**************************************************************************)
@@ -97,7 +102,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
Typing.preprocess_predicate ~logic_env lower_guard;
let adata_lower_guard, env = Assert.empty ~loc kf env in
let lower_guard, adata_lower_guard, env =
- !predicate_to_exp_ref ~adata:adata_lower_guard kf env lower_guard
+ predicate_to_exp ~adata:adata_lower_guard kf env lower_guard
in
let assertion, env =
Assert.runtime_check
@@ -127,7 +132,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
Typing.preprocess_predicate ~logic_env upper_guard;
let adata_upper_guard, env = Assert.empty ~loc kf env in
let upper_guard, adata_upper_guard, env =
- !predicate_to_exp_ref ~adata:adata_upper_guard kf env upper_guard
+ predicate_to_exp ~adata:adata_upper_guard kf env upper_guard
in
let assertion, env =
Assert.runtime_check
@@ -141,7 +146,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
in
let stmts = assertion :: stmts in
(* Translate term [t] into an exp of type [size_t] *)
- let gmp_e, adata, env = !term_to_exp_ref ~adata kf env t in
+ let gmp_e, adata, env = term_to_exp ~adata kf env t in
let _, e, env = Env.new_var
~loc
~name:"size"
@@ -180,13 +185,13 @@ let comparison_to_exp
let e1, adata, env =
match e1 with
| None ->
- let e1, adata, env = !term_to_exp_ref ~adata kf env t1 in
+ let e1, adata, env = term_to_exp ~adata kf env t1 in
e1, adata, env
| Some e1 ->
e1, adata, env
in
let ty1 = Cil.typeOf e1 in
- let e2, adata, env = !term_to_exp_ref ~adata kf env t2 in
+ let e2, adata, env = term_to_exp ~adata kf env t2 in
let ty2 = Cil.typeOf e2 in
let e, env =
match Logic_aggr.get_t ty1, Logic_aggr.get_t ty2 with
@@ -265,7 +270,7 @@ let env_of_li ~adata ~loc kf env li =
let logic_env = Env.Logic_env.get env in
let ty = Typing.get_typ ~logic_env t in
let vi, vi_e, env = Env.Logic_binding.add ~ty env kf li.l_var_info in
- let e, adata, env = !term_to_exp_ref ~adata kf env t in
+ let e, adata, env = term_to_exp ~adata kf env t in
let stmt = match Typing.get_number_ty ~logic_env t with
| C_integer _ | C_float _ | Nan ->
Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
--
GitLab