From 0d326d65e99aa1c171775e3aba08cbd0840d3a51 Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Mon, 2 Sep 2019 14:42:45 +0200 Subject: [PATCH] minor: adding comments --- src/kernel_internals/typing/allocates.mli | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/kernel_internals/typing/allocates.mli b/src/kernel_internals/typing/allocates.mli index 8e03dec8759..db5e15c991b 100644 --- a/src/kernel_internals/typing/allocates.mli +++ b/src/kernel_internals/typing/allocates.mli @@ -20,7 +20,12 @@ (* *) (**************************************************************************) -(** Generation of default [allocates \nothing] clauses. *) +(** Generation of default [allocates \nothing] clauses. + + Automatic generation of [allocates \nothing] and [loop allocates \nothing] + clauses has been removed until a plugin supports them. + To force generation, the following functions can be used. +*) val add_allocates_nothing_funspec: Cil_types.kernel_function -> unit (** Adds [allocates \nothing] to the default behavior of the function -- GitLab