From 2142d5b67faaa1c032f326c3cb9754bcf0bdb22a Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 26 Nov 2020 16:53:38 +0100
Subject: [PATCH] [eacsl] Add functions to execute a closure with RTE on or off
---
src/plugins/e-acsl/src/code_generator/env.ml | 14 ++++++++++++++
src/plugins/e-acsl/src/code_generator/env.mli | 19 +++++++++++++++++++
2 files changed, 33 insertions(+)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 595dc566e1e..6372c26f3f6 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -135,6 +135,20 @@ let generate_rte env =
let local_env, _ = top env in
local_env.rte
+let with_rte ~f env rte_value =
+ let old_rte_value = generate_rte env in
+ let env = rte env rte_value in
+ let env = f env in
+ let env = rte env old_rte_value in
+ env
+
+let with_rte_and_result ~f env rte_value =
+ let old_rte_value = generate_rte env in
+ let env = rte env rte_value in
+ let other, env = f env in
+ let env = rte env old_rte_value in
+ other, env
+
(* ************************************************************************** *)
(* eta-expansion required for typing generalisation *)
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 3a5aebf2f5d..cb6633546cf 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -165,7 +165,26 @@ val pop_loop: t -> predicate list * t
(* ************************************************************************** *)
val rte: t -> bool -> t
+(** [rte env x] sets RTE generation to x for the given environment *)
+
val generate_rte: t -> bool
+(** Returns the current value of RTE generation for the given environment *)
+
+val with_rte: f:(t -> t) -> t -> bool -> t
+(** [with_rte ~f env x] executes the given closure with RTE generation set to x,
+ and reset RTE generation to its original value afterwards.
+ This function does not handle exceptions at all. The user must handle them
+ either directly in the [f] closure or around the call to the function. *)
+
+val with_rte_and_result: f:(t -> 'a * t) -> t -> bool -> 'a * t
+(** [with_rte_and_result ~f env x] executes the given closure with RTE
+ generation set to x, and reset RTE generation to its original value
+ afterwards. [f] is a closure that takes an environment an returns a pair
+ where the first member is an arbitrary value and the second member is the
+ environment. The function will return the first member of the returned pair
+ of the closure along with the updated environment.
+ This function does not handle exceptions at all. The user must handle them
+ either directly in the [f] closure or around the call to the function. *)
(* ************************************************************************** *)
(** {2 Context for error handling} *)
--
GitLab