From 15e806d3e259fc2bf71531b41f45ba0e3c724c01 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 15 Jul 2021 16:03:25 +0200
Subject: [PATCH] [eacsl] Handle `TLogic_coerce` in
`context_sensitive_term_to_exp`
The previous solution removed the first `TLogic_coerce` of a term in
`term_to_exp`, which would result in errors if several successive
`TLogic_coerce` were in a term. This commit recursively call
`context_sensitive_term_to_exp` on `TLogic_coerce`.
---
src/plugins/e-acsl/src/code_generator/translate.ml | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 2c4ace3aea3..1cd687f70b2 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -533,7 +533,7 @@ and context_insensitive_term_to_exp kf env t =
e
in
e, env, Typed_number.C_number, ""
- | TLogic_coerce _ -> assert false (* handle in [term_to_exp] *)
+ | TLogic_coerce (_, t) -> context_insensitive_term_to_exp kf env t
| TAddrOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
Cil.mkAddrOf ~loc lv, env, Typed_number.C_number, "addrof"
@@ -616,7 +616,6 @@ and term_to_exp kf env t =
Printer.pp_term t generate_rte;
Env.with_rte_and_result env false
~f:(fun env ->
- let t = match t.term_node with TLogic_coerce(_, t) -> t | _ -> t in
let e, env, sty, name = context_insensitive_term_to_exp kf env t in
let env = if generate_rte then translate_rte kf env e else env in
let cast = Typing.get_cast t in
--
GitLab