From 7d56db6e4657176d03ab28ed7e8b2b599414a537 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Sat, 31 Dec 2016 17:40:20 +0100
Subject: [PATCH] fixed a bug where accessing an array A wouldn't throw errors
if A wasn't part of the post-condition
---
Settings.hs | 4 ++--
Tests/methods.java | 2 +-
WLP.hs | 11 ++++++-----
3 files changed, 9 insertions(+), 8 deletions(-)
diff --git a/Settings.hs b/Settings.hs
index e7dc8c0..edabe42 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,8 +1,8 @@
module Settings where
testFile, postCond :: String
-testFile = "side-effects"
-postCond = "(x == 2)"
+testFile = "debug"
+postCond = "(true)"
nrOfUnroll :: Int
nrOfUnroll = 1
\ No newline at end of file
diff --git a/Tests/methods.java b/Tests/methods.java
index d524111..47b8dfd 100644
--- a/Tests/methods.java
+++ b/Tests/methods.java
@@ -4,7 +4,7 @@ public static class Main
public static void main(String[] args)
{
C c1, c2;
- c1 = new C(0);
+ c1 = new C(1);
c2 = new C(0);
c1.method1(1);
c2.method1(1);
diff --git a/WLP.hs b/WLP.hs
index 295691a..344b106 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -168,9 +168,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
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))
- fArrayAccess (ArrayIndex a i) inh = case catch inh of
- Nothing -> (arrayAccess a i, snd ((foldExp wlpExpAlgebra a) inh))
- Just (cs, f) -> (arrayAccess a i, snd ((foldExp wlpExpAlgebra a) inh {acc = id}) . arrayAccessWlp a i 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))
-- x++ increments x but evaluates to the original value
@@ -208,14 +206,17 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fAssign lhs op e inh = let lhs' = foldLhs inh lhs
rhs' = desugarAssign lhs' op e'
(e', trans) = e inh {acc = id}
- in (rhs', trans . substVar (env inh) (decls inh) lhs' rhs' . acc inh)
+ lhsTrans = case lhs' of
+ ArrayLhs (ArrayIndex a i) -> arrayAccessWlp a i inh {acc = id}
+ _ -> id
+ in (rhs', lhsTrans . trans . substVar (env inh) (decls inh) lhs' rhs' . acc inh)
fLambda = error "lambda"
fMethodRef = error "method reference"
-- gets the transformer for array access (as array access may throw an error)
arrayAccessWlp :: Exp -> [Exp] -> Inh -> Exp -> Exp
arrayAccessWlp a i inh q = case catch inh of
- Nothing -> q
+ Nothing -> Cond (foldr (\(i, l) e -> e &* (BinOp i LThan l) &* (BinOp i GThanE (Lit (Int 0)))) true (zip i (dimLengths a))) q false
Just (cs, f) -> let e = InstanceCreation [] (ClassType [(Ident "ArrayIndexOutOfBoundsException", [])]) [] Nothing
in Cond (foldr (\(i, l) e -> e &* (BinOp i LThan l) &* (BinOp i GThanE (Lit (Int 0)))) true (zip i (dimLengths a))) q ((maybe (if f then q else q &* throwException e)) (\b -> wlp' (inh {acc = id, catch = Nothing}) (StmtBlock b) q) (getCatch (decls inh) (env inh) e cs))
--
GitLab