diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index 8a64b099206bdf104d7a53fb0ccd00152f35d1e4..c12574a1ad429d810ceec67dd46553ad98606663 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.mli
+++ b/src/plugins/e-acsl/src/code_generator/constructor.mli
@@ -29,6 +29,8 @@ val mk_deref: loc:Location.t -> exp -> exp
 (** Construct a dereference of an expression. *)
 
 val mk_block: stmt -> block -> stmt
+(** Create a block statement from a block to replace a given statement.
+    Requires that (1) the block is not empty, or (2) the statement is a skip. *)
 
 (* ********************************************************************** *)
 (* E-ACSL specific code: build calls to its RTL API *)