From 22d96a09e593ed7ebdb8d1e5479ff896e37d583c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Thu, 25 Nov 2021 17:33:38 +0100
Subject: [PATCH] DataFlow: use [update] at the roots to allow a root to be
 seeded twice.

---
 src/DataFlow.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/DataFlow.ml b/src/DataFlow.ml
index de1831b..661b3a9 100644
--- a/src/DataFlow.ml
+++ b/src/DataFlow.ml
@@ -200,8 +200,11 @@ module ForCustomMaps
 
   (* Populate the queue with the root variables. *)
 
+  (* Our use of [update] here means that it is permitted for [foreach_root]
+     to seed several properties at a single root. *)
+
   let () =
-    G.foreach_root (fun x p -> V.set x p; schedule x)
+    G.foreach_root update
 
   (* As long as the queue is nonempty, take a variable and examine it. *)
 
-- 
GitLab