diff --git a/src/Javawlp/API.hs b/src/Javawlp/API.hs index ce395a27fcbd9269ba4998323d4a4e7fcd2bbdfb..3ec6876e8483b059bbc894f79a9c3952e7b48548 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