Fixed a bug with the verification of conditional expressions. Fixed a bug with...

Fixed a bug with the verification of conditional expressions. Fixed a bug with method calls on objects.

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

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()

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

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])