From 065190720a595332e62e7ae56a20946fb0412ec2 Mon Sep 17 00:00:00 2001
From: ISWB Prasetya <iswbprasetya@iswbs-mbp.cs.uu.nl>
Date: Thu, 31 Aug 2017 18:34:53 +0200
Subject: [PATCH] adding comment on complication with lazy-eval and unsafeIO
---
src/Javawlp/API.hs | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/Javawlp/API.hs b/src/Javawlp/API.hs
index ce395a2..3ec6876 100644
--- a/src/Javawlp/API.hs
+++ b/src/Javawlp/API.hs
@@ -61,6 +61,13 @@ wlpMethod conf env decls methodName postCondition = do
-- reset the counters for assigning fresh names
-- dummy1 <- resetVarPointer
-- dummy2 <- resetVarMethodInvokesCount
+
+ -- We need to resent the method-invocation counters to make generated names the same accross multiple
+ -- invocation of the wlp over the same method. However the above resets do not really work, due to
+ -- the combination of lazy-evaluation and unsafeIO that screw things up. The above resets are not
+ -- guaranteed to be executed. Messy. So instead, we enforce renumbering by applying post-processing
+ -- normalization:
+
-- Calculate the wlp:
let p = wlpWithEnv conf decls env' methodBody postCondition
return $ normalizeInvocationNumbers p
--
GitLab