From 8cec1c9389541e124224079050bf3ed3e88a866d Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 2 Aug 2021 17:41:30 +0200
Subject: [PATCH] [eacsl] Update comment of Env.add_stmt
Clarify the use of `~before` and `~post`.
---
src/plugins/e-acsl/src/code_generator/env.mli | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 3c521f8635e..6009e221e9f 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -93,7 +93,8 @@ val add_stmt: ?post:bool -> ?before:stmt -> t -> kernel_function -> stmt -> t
(** [add_stmt env s] extends [env] with the new statement [s].
[before] may define which stmt the new one is included before. This is to
say that any labels attached to [before] are moved to [stmt]. [post]
- indicates that [stmt] should be added after the target statement. *)
+ indicates that [stmt] should be added after the target statement.
+ [before] and [post] are mutually exclusive. *)
val extend_stmt_in_place: t -> stmt -> label:logic_label -> block -> t
(** [extend_stmt_in_place env stmt ~label b] modifies [stmt] in place in
--
GitLab