From e283b28e7a85095561f6a8ad32ce2e858b4b25f5 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Tue, 14 Nov 2023 14:28:57 +0100
Subject: [PATCH] [e-acsl] Translate_utils: cut comparison_to_exp into two
---
.../src/code_generator/translate_utils.ml | 38 ++++++++-----------
1 file changed, 16 insertions(+), 22 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 acaec461509..ef8b075abf9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -169,29 +169,9 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
let () =
Memory_translate.gmp_to_sizet_ref := gmp_to_sizet
-let comparison_to_exp
- ~adata
- ~loc
- kf
- env
- ity
- ?e1
- bop
- t1
- t2
- ?(name = Misc.name_of_binop bop)
- t_opt
- =
- let e1, adata, env =
- match e1 with
- | None ->
- let e1, adata, env = term_to_exp ~adata kf env t1 in
- e1, adata, env
- | Some e1 ->
- e1, adata, env
- in
+let exp_comparison_to_exp
+ ~loc kf env ity bop e1 e2 ?(name = Misc.name_of_binop bop) t_opt =
let ty1 = Cil.typeOf e1 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
@@ -221,6 +201,20 @@ let comparison_to_exp
Printer.pp_typ ty1
Printer.pp_typ ty2
in
+ e, env
+
+let comparison_to_exp ~adata ~loc kf env ity ?e1 bop t1 t2 ?name t_opt
+ =
+ let e1, adata, env =
+ match e1 with
+ | None ->
+ let e1, adata, env = term_to_exp ~adata kf env t1 in
+ e1, adata, env
+ | Some e1 ->
+ e1, adata, env
+ in
+ let e2, adata, env = term_to_exp ~adata kf env t2 in
+ let e, env = exp_comparison_to_exp ~loc kf env ity bop e1 e2 ?name t_opt in
e, adata, env
let conditional_to_exp ?(name="if") ~loc kf t_opt e1 (e2, env2) (e3, env3) =
--
GitLab