diff --git a/src/plugins/wp/Sigma.mli b/src/plugins/wp/Sigma.mli index 94f5cc611dc45c0a44ba769b59655776cf70d819..1c357a5e2c0b6a67e266a8a5f0ecbec81f0217df 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.