From 2fcfa57e9fef2f98ede34988c9da5afc0e60824c Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Sat, 10 Dec 2016 19:05:31 +0100
Subject: [PATCH] Fixed a bug with the verification of conditional expressions.
Fixed a bug with method calls on objects.
---
Settings.hs | 4 ++--
Tests/methods.java | 13 ++++++++-----
Verifier.hs | 6 +++---
WLP.hs | 16 +++++++++-------
4 files changed, 22 insertions(+), 17 deletions(-)
diff --git a/Settings.hs b/Settings.hs
index 689be15..16d451a 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -2,7 +2,7 @@ module Settings where
testFile, postCond :: String
testFile = "methods"
-postCond = "x == 5"
+postCond = "(x == 4)"
nrOfUnroll :: Int
-nrOfUnroll = 6
\ No newline at end of file
+nrOfUnroll = 8
\ No newline at end of file
diff --git a/Tests/methods.java b/Tests/methods.java
index 0ded15c..538642c 100644
--- a/Tests/methods.java
+++ b/Tests/methods.java
@@ -3,10 +3,11 @@ public static class Main
static int x, y;
public static void main(String[] args)
{
- C1 c1 = new C1();
+ C c1 = new C();
+ C c2 = new C();
c1.method1();
- c1.method1();
- x = c1.c;
+ c2.method1();
+ x = c1.c + c2.c;
}
@@ -17,17 +18,19 @@ public static class Main
}
}
-public class C1
+public class C
{
int c;
- public C1()
+ public C()
{
}
public void method1()
{
this.c += 1;
+ if(this.c < 2)
+ this.method1();
}
public int method2()
diff --git a/Verifier.hs b/Verifier.hs
index c24e996..b636463 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -171,13 +171,13 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
mkOr [ast1, ast2]
fInstanceOf = undefined
fCond g e1 e2 = do
- astg <- g
+ astg <- (g >>= mkNot)
assert astg
result <- check
solverReset
case result of
- Sat -> e1
- Unsat -> e2
+ Sat -> e2
+ Unsat -> e1
_ -> error "can't evaluate if-condition"
fAssign = undefined
fLambda = undefined
diff --git a/WLP.hs b/WLP.hs
index eaaf3c1..e0eb1ba 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -154,7 +154,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fMethodInv invocation inh = (ExpName (Name [getReturnVar inh invocation]),
(if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll
then const true
- else fst (wlp' (inh {acc = id, calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just (getReturnVar inh invocation), object = getObject invocation}) (inlineMethod inh invocation)) . acc inh, env inh))
+ else fst (wlp' (inh {acc = id, calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just (getReturnVar inh invocation), object = getObject inh invocation}) (inlineMethod inh invocation)) . acc inh, env inh))
fArrayAccess (ArrayIndex a i) inh = case catch inh of
Nothing -> (arrayAccess a i, (acc inh, env inh))
Just (cs, f) -> (arrayAccess a i, (arrayAccessWlp a i inh, env inh))
@@ -210,11 +210,13 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
getReturnVar inh invocation = Ident (makeReturnVarName (invocationToId invocation) ++ show (getCallCount (calls inh) (invocationToId invocation)))
-- Gets the object a method is called from
- getObject :: MethodInvocation -> Maybe Exp
- getObject (MethodCall name _) | length (fromName name) > 1 = Just (ExpName (Name (take (length (fromName name) - 1) (fromName name))))
- | otherwise = Nothing
- getObject (PrimaryMethodCall e _ _ _) = Just e
- getObject _ = undefined
+ getObject :: Inh -> MethodInvocation -> Maybe Exp
+ getObject inh (MethodCall name _) | length (fromName name) > 1 = Just (ExpName (Name (take (length (fromName name) - 1) (fromName name))))
+ | otherwise = Nothing
+ getObject inh (PrimaryMethodCall e _ _ _) = case e of
+ This -> object inh
+ _ -> Just e
+ getObject inh _ = undefined
-- Gets the return type of a method
getType :: Inh -> MethodInvocation -> Maybe Type
@@ -240,7 +242,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
foldFieldAccess inh fieldAccess = case fieldAccess of
PrimaryFieldAccess e id -> case getExp (foldExp wlpExpAlgebra e) inh of
ExpName name -> Name (fromName name ++ [id])
- _ -> error "foldFieldAccess"
+ x -> error ("foldFieldAccess: " ++ show x ++ show id)
SuperFieldAccess id -> foldFieldAccess inh (PrimaryFieldAccess (fromJust (object inh)) id)
ClassFieldAccess name id -> Name (fromName name ++ [id])
--
GitLab