[e-acsl:archi] add doc for Constructor

src/plugins/e-acsl/src/code_generator/constructor.mli

@@ -26,29 +26,47 @@ open Cil_types
 open Cil_datatype
 
 val mk_deref: loc:Location.t -> exp -> exp
-(** Make a dereference of an expression *)
+(** Construct a dereference of an expression. *)
 
 val mk_block: stmt -> block -> stmt
 
 (* ********************************************************************** *)
-(* E-ACSL specific code *)
+(* E-ACSL specific code: build calls to its API *)
 (* ********************************************************************** *)
 
 val mk_lib_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
-(** Call of a library function.
+(** Construct a call to a library function with the given name.
     @raise Unregistered_library_function if the given string does not represent
-    such a function or if these functions were never registered (only possible
+    such a function or if library functions were never registered (only possible
     when using E-ACSL through its API). *)
 
 val mk_rtl_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
 (** Special version of [mk_lib_call] for E-ACSL's RTL functions. *)
 
 val mk_store_stmt: ?str_size:exp -> varinfo -> stmt
+(** Construct a call to [__e_acsl_store_block] that observes the allocation of
+    the given varinfo. See [share/e-acsl/e_acsl.h] for details about this
+    function. *)
+
 val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
+(** Same as [mk_store_stmt] for [__e_acsl_duplicate_store_block] that first
+    checks for a previous allocation of the given varinfo. *)
+
 val mk_delete_stmt: varinfo -> stmt
+(** Same as [mk_store_stmt] for [__e_acsl_delete_block] that observes the
+    de-allocation of the given varinfo. *)
+
 val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
+(** Same as [mk_store_stmt] for [__e_acsl_full_init] that observes the
+    initialization of the given varinfo. *)
+
 val mk_initialize: loc:location -> lval -> stmt
+(** Same as [mk_store_stmt] for [__e_acsl_initialize] that observes the
+    initialization of the given left-value. *)
+
 val mk_mark_readonly: varinfo -> stmt
+(** Same as [mk_store_stmt] for [__e_acsl_markreadonly] that observes the
+    read-onlyness of the given varinfo. *)
 
 type annotation_kind =
   | Assertion
@@ -60,7 +78,10 @@ type annotation_kind =
 val mk_runtime_check:
   ?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate ->
   stmt
-(** Generate a runtime check of the given expression. *)
+(** [mk_runtime_check kind kf e p] generates a runtime check for predicate [p]
+   by building a call to [__e_acsl_assert]. [e] (or [!e] if [reverse] is set to
+   [true]) is the C translation of [p], [kf] is the current kernel_function and
+   [kind] is the annotation kind of [p]. *)
 
 (*
 Local Variables: