From 0b4854a911ab91e46620c92de1e853866eb834fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 23 Jan 2025 07:43:41 +0100
Subject: [PATCH] [wp] fix doc

---
 src/plugins/wp/Sigma.mli | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/plugins/wp/Sigma.mli b/src/plugins/wp/Sigma.mli
index 94f5cc611dc..1c357a5e2c0 100644
--- a/src/plugins/wp/Sigma.mli
+++ b/src/plugins/wp/Sigma.mli
@@ -80,10 +80,14 @@ sig
   (** Whether the chunk tracks memory initialization (used for filtering). *)
 
   val is_primary : t -> bool
-  (** Used to sort memory chunk parameters in ACSL symbols.
+  (** Used to sort memory chunk parameters in compiled ACSL symbols.
 
-      Single chunks represents values of variables or individual l-values.
-      They are sorted last among memory chunk parameters. *)
+      Non-primary chunk parameters come first, followed by primary ones,
+      followed by logical parameters.
+
+      Typical primary chunks are memory chunks with a single location,
+      like hoare of ref variables in MemVar or singleton regions in
+      MemRegion. *)
 
   val is_framed : t -> bool
   (** Whether the chunk is local to a function call.
-- 
GitLab