From 18f10a0dc363cb6c7504d4a34349be93770fd62a Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Sun, 1 Jan 2017 17:08:56 +0100
Subject: [PATCH] brainfart fixed concerning method calls
---
Settings.hs | 2 +-
WLP.hs | 10 +++++-----
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/Settings.hs b/Settings.hs
index edabe42..80effa4 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,7 +1,7 @@
module Settings where
testFile, postCond :: String
-testFile = "debug"
+testFile = "2d-arrays1"
postCond = "(true)"
nrOfUnroll :: Int
diff --git a/WLP.hs b/WLP.hs
index 344b106..89327e5 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -162,12 +162,12 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fArrayCreateInit t dim init inh = (ArrayCreateInit t dim init, acc inh)
fFieldAccess fieldAccess inh = (ExpName (foldFieldAccess inh fieldAccess), (acc inh))
fMethodInv invocation inh = case invocation of
- MethodCall (Name [Ident "*assume"]) [e] -> (false, (if e == false then const true else imp e))
- _ -> if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll
- then (false, const true)
- else let varId = getReturnVar invocation
+ MethodCall (Name [Ident "*assume"]) [e] -> (false, (if e == false then const true else imp e)) -- *assume is the regular assume function
+ _ -> if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll -- Check the recursion depth
+ then (undefined, const true) -- Recursion limit reached: we just assume the post codition will hold
+ else let varId = getReturnVar invocation
callWlp = wlp' (inh {acc = id, calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just varId, object = getObject inh invocation}) (inlineMethod inh invocation)
- in (callWlp (ExpName (Name [varId])), (callWlp . acc inh))
+ in (ExpName (Name [varId]), (callWlp . acc inh))
fArrayAccess (ArrayIndex a i) inh = (arrayAccess a i, snd ((foldExp wlpExpAlgebra a) inh {acc = id}) . arrayAccessWlp a i inh)
fExpName name inh = (ExpName name, (acc inh))
--
GitLab