From 7f3cadfaea69592fe03fb311613b14efc0cf4718 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 12 Oct 2023 16:42:09 +0200 Subject: [PATCH] Adapt comments to simplified global invariant --- src/framework/constraints.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 038068ea0d..b4b72146d5 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -1710,14 +1710,14 @@ module RecursionTermLifter (S: Spec) and module C = S.C = (* two global invariants: - - V -> G + - S.V -> S.G Needed to store the previously built global invariants - - fundec -> Map (S.C) (Set (fundec * S.C)) - The second global invariant maps from the callee fundec to a map, containing the callee context and the caller fundec and context. + - fundec * S.C -> (Set (fundec * S.C)) + The second global invariant maps from the callee fundec and context to a set of caller fundecs and contexts. This structure therefore stores the context-sensitive call graph. For example: let the function f in context c call function g in context c'. - In the global invariant structure it would be stored like this: g -> {c' -> {(f, c)}} + In the global invariant structure it would be stored like this: (g,c') -> {(f, c)} *) struct