From f5c9ca1db960d276f36e06ec45c8321d05437448 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 15 Oct 2020 10:34:54 +0200
Subject: [PATCH] [wp] Clarifies Sigs.CodeSemantics.init doc
---
src/plugins/wp/Sigs.ml | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 0e82aeb893b..1b594803754 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -612,8 +612,10 @@ sig
Remark: [None] initializer are interpreted as zeroes. This is consistent
with the [init option] associated with global variables in CIL,
- for which the default initializer are zeroes. There is no
- [init option] value associated with local initializers.
+ for which the default initializer are zeroes. This function is called
+ for global initializers and local initializers ([Cil.Local_init]).
+ It is not called for local variables without initializers as they do not
+ have a [Cil.init option].
*)
end
--
GitLab