From 92a5f04f8a5f134d9757c57c6b7b41dfb6be05e9 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 9 Jun 2021 14:24:52 +0200
Subject: [PATCH] [eacsl] Expose `Translate.term_to_exp`

---
 src/plugins/e-acsl/src/code_generator/translate.mli | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/plugins/e-acsl/src/code_generator/translate.mli b/src/plugins/e-acsl/src/code_generator/translate.mli
index f5e814dfaf1..c65e1ab7eeb 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate.mli
@@ -53,6 +53,9 @@ val translate_predicate:
     If [pred_to_print] is set, then the runtime check will use this predicate as
     message. *)
 
+val term_to_exp: kernel_function -> Env.t -> term -> exp * Env.t
+(** Convert an ACSL term into a corresponding C expression. *)
+
 val translate_rte_annots:
   (Format.formatter -> 'a -> unit) ->
   'a ->
-- 
GitLab