From 1a1aa48d077cbc18902598d324e3c6b13d461da1 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 6 Mar 2020 10:34:32 +0100
Subject: [PATCH] [eacsl:codegen] Add documentation to `Constructor.mk_block`

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

diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index 8a64b099206..c12574a1ad4 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 *)
-- 
GitLab