diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli index 3c521f8635eaedc7fbb6c2e47538343b07a76789..6009e221e9f734ad60b3ff0b490495ac20b40ad0 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