From dc5b0b802749450fa35c0e665977094431e08c50 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Sat, 28 Jan 2017 18:51:22 +0100
Subject: [PATCH] wlp on arrayAccess now recurses correctly
---
WLP.hs | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/WLP.hs b/WLP.hs
index 4e13645..08ef61d 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -165,7 +165,9 @@ 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 (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)
+ fArrayAccess (ArrayIndex a i) inh = let (a', atrans) = foldExp wlpExpAlgebra a inh {acc = id}
+ i' = map (flip (foldExp wlpExpAlgebra) inh {acc = id}) i
+ in (arrayAccess a' (map fst i'), foldl (.) atrans (map snd i') . arrayAccessWlp a' (map fst i') inh)
fExpName name inh = (editName inh name, acc inh)
-- x++ increments x but evaluates to the original value
@@ -175,7 +177,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
exp -> (exp, trans)
fPostDecrement e inh = let (e', trans) = e inh in
case e' of
- var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Rem (Lit (Int 1))) . trans)
+ var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
exp -> (exp, trans)
-- ++x increments x and evaluates to the new value of x
fPreIncrement e inh = let (e', trans) = e inh in
@@ -184,8 +186,8 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
exp -> (BinOp exp Add (Lit (Int 1)), trans)
fPreDecrement e inh = let (e', trans) = e inh in
case e' of
- var@(ExpName name) -> (BinOp var Rem (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Rem (Lit (Int 1))) . trans)
- exp -> (BinOp exp Rem (Lit (Int 1)), trans)
+ var@(ExpName name) -> (BinOp var Sub (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
+ exp -> (BinOp exp Sub (Lit (Int 1)), trans)
fPrePlus e inh = let (e', trans) = e inh in (e', trans)
fPreMinus e inh = let (e', trans) = e inh in (PreMinus e', trans)
fPreBitCompl e inh = let (e', trans) = e inh in (PreBitCompl e', trans)
--
GitLab