Skip to content
Snippets Groups Projects
Commit 06519072 authored by ISWB Prasetya's avatar ISWB Prasetya
Browse files

adding comment on complication with lazy-eval and unsafeIO

parent 1d70f704
No related branches found
No related tags found
No related merge requests found
...@@ -61,6 +61,13 @@ wlpMethod conf env decls methodName postCondition = do ...@@ -61,6 +61,13 @@ wlpMethod conf env decls methodName postCondition = do
-- reset the counters for assigning fresh names -- reset the counters for assigning fresh names
-- dummy1 <- resetVarPointer -- dummy1 <- resetVarPointer
-- dummy2 <- resetVarMethodInvokesCount -- 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: -- Calculate the wlp:
let p = wlpWithEnv conf decls env' methodBody postCondition let p = wlpWithEnv conf decls env' methodBody postCondition
return $ normalizeInvocationNumbers p return $ normalizeInvocationNumbers p
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment