From d27e6af38f2c865193df98c2dfada8b8f9b1d52d Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Wed, 20 Dec 2023 23:01:36 +0100
Subject: [PATCH] [e-acsl] Translate_predicates: simplify to_exp
inline non-trivial identity
---
.../src/code_generator/translate_predicates.ml | 12 +-----------
1 file changed, 1 insertion(+), 11 deletions(-)
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 45c63bdac6a..c885230cc46 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -327,17 +327,7 @@ and to_exp ~adata ?inplace ?name kf ?rte env p =
in
let env = if rte then !translate_rte_exp_ref kf env e else env in
let env = Assert.do_pending_register_data env in
- Extlib.nest
- adata
- (Typed_number.add_cast
- ~loc:p.pred_loc
- ?name
- env
- kf
- None
- Analyses_types.C_number
- None
- e)
+ (e, adata), env
)
env)
--
GitLab