Skip to content
Snippets Groups Projects
Commit 9cd62f0a authored by koen's avatar koen
Browse files

removed env from synthesized attributes

parent bfbbc2fd
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
HelperFunctions.hs
+ 22
− 0
View file @ 9cd62f0a
...@@ -4,6 +4,10 @@ module HelperFunctions where ...@@ -4,6 +4,10 @@ module HelperFunctions where
import Language.Java.Syntax import Language.Java.Syntax
import Language.Java.Pretty import Language.Java.Pretty
import Data.Maybe import Data.Maybe
import System.IO.Unsafe
import Data.IORef
type TypeEnv = [(Name, Type)] type TypeEnv = [(Name, Type)]
type CallCount = [(Ident, Int)] type CallCount = [(Ident, Int)]
...@@ -109,6 +113,24 @@ getStaticVars compUnit = concatMap fromTypeDecls (getDecls compUnit) where ...@@ -109,6 +113,24 @@ getStaticVars compUnit = concatMap fromTypeDecls (getDecls compUnit) where
fromMemberDecl _ = [] fromMemberDecl _ = []
fromVarDecl t (VarDecl varId _) = (Name [getId varId], t) fromVarDecl t (VarDecl varId _) = (Name [getId varId], t)
-- Checks if the var is introduced. Introduced variable names start with '$' voor return variables of methods and '#' for other variables
isIntroducedVar :: Name -> Bool
isIntroducedVar (Name (Ident ('#':_): _)) = True
isIntroducedVar (Name (Ident ('$':_): _)) = True
isIntroducedVar _ = False
-- The number of variables introduced
varPointer :: IORef Integer
varPointer = unsafePerformIO $ newIORef 0
--- | Gets the current var pointer and increases the pointer by 1
getIncrPointer :: IORef Integer -> Integer
getIncrPointer ref = unsafePerformIO $
do
p <- readIORef ref
writeIORef ref (p + 1)
return p
-- Used for debugging -- Used for debugging
fromJust' :: String -> Maybe a -> a fromJust' :: String -> Maybe a -> a
fromJust' s ma = case ma of fromJust' s ma = case ma of
......
Settings.hs
+ 2
− 2
View file @ 9cd62f0a
module Settings where module Settings where
testFile, postCond :: String testFile, postCond :: String
testFile = "2d-arrays1" testFile = "methods"
postCond = "(true)" postCond = "(x == 4)"
nrOfUnroll :: Int nrOfUnroll :: Int
nrOfUnroll = 1 nrOfUnroll = 1
\ No newline at end of file
Substitute.hs
+ 2
− 0
View file @ 9cd62f0a
...@@ -52,6 +52,8 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu ...@@ -52,6 +52,8 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
case lhs inh of case lhs inh of
NameLhs (Name lhsName) -> case lookupType (decls inh) (env inh) (Name lhsNameInit) of NameLhs (Name lhsName) -> case lookupType (decls inh) (env inh) (Name lhsNameInit) of
PrimType _ | lhsName == name -> rhs inh PrimType _ | lhsName == name -> rhs inh
RefType _ | isIntroducedVar (Name lhsName) && lhsName == name -> rhs inh
RefType _ | isIntroducedVar (Name lhsName) && lhsName /= name -> ExpName (Name name)
RefType t | lookupType (decls inh) (env inh) (Name nameInit) == RefType t -> case rhs inh of RefType t | lookupType (decls inh) (env inh) (Name nameInit) == RefType t -> case rhs inh of
ExpName (Name rhsName) | take (length lhsName) name == lhsName -> ExpName (Name (rhsName ++ drop (length lhsName) name)) ExpName (Name rhsName) | take (length lhsName) name == lhsName -> ExpName (Name (rhsName ++ drop (length lhsName) name))
-- accessing o1.x might affect o2.x if o1 and o2 point to the same object: -- accessing o1.x might affect o2.x if o1 and o2 point to the same object:
......
Tests/methods.java
+ 5
− 4
View file @ 9cd62f0a
...@@ -4,12 +4,12 @@ public static class Main ...@@ -4,12 +4,12 @@ public static class Main
public static void main(String[] args) public static void main(String[] args)
{ {
C c1, c2; C c1, c2;
/* c1 = new C(0); c1 = new C(0);
c2 = new C(1); c2 = new C(1);
c1.method1(1);*/ c1.method1(1);
c2.method1(1); c2.method1(1);
x = c1.c + c2.c; x = c1.c + c2.c;
C.staticMethod(); // C.staticMethod();
} }
...@@ -36,9 +36,10 @@ public class C ...@@ -36,9 +36,10 @@ public class C
public void method1(int n) public void method1(int n)
{ {
this.c += n; this.c += n;
if(this.c < 2) if(this.c < 2)
this.method1(); this.method1();
} }
public int method2() public int method2()
......
Verifier.hs
+ 12
− 24
View file @ 9cd62f0a
...@@ -99,63 +99,51 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual ...@@ -99,63 +99,51 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
Mult -> do Mult -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkMul [ast1, ast2]
if ast1 == t then mkTrue else mkMul [ast1, ast2]
Div -> do Div -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkDiv ast1 ast2
if ast1 == t then mkTrue else mkDiv ast1 ast2
Rem -> do Rem -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkRem ast1 ast2
if ast1 == t then mkTrue else mkRem ast1 ast2
Add -> do Add -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkAdd [ast1, ast2]
if ast1 == t then mkTrue else mkAdd [ast1, ast2]
Sub -> do Sub -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkSub [ast1, ast2]
if ast1 == t then mkTrue else mkSub [ast1, ast2]
LShift -> do LShift -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkBvshl ast1 ast2
if ast1 == t then mkTrue else mkBvshl ast1 ast2
RShift -> do RShift -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkBvashr ast1 ast2
if ast1 == t then mkTrue else mkBvashr ast1 ast2
RRShift -> do RRShift -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkBvlshr ast1 ast2
if ast1 == t then mkTrue else mkBvlshr ast1 ast2
LThan -> do LThan -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkLt ast1 ast2
if ast1 == t then mkTrue else mkLt ast1 ast2
GThan -> do GThan -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkGt ast1 ast2
if ast1 == t then mkTrue else mkGt ast1 ast2
LThanE -> do LThanE -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkLe ast1 ast2
if ast1 == t then mkTrue else mkLe ast1 ast2
GThanE -> do GThanE -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
t <- mkTrue mkGe ast1 ast2
if ast1 == t then mkTrue else mkGe ast1 ast2
Equal -> do Equal -> do
ast1 <- e1 ast1 <- e1
ast2 <- e2 ast2 <- e2
......
WLP.hs
+ 61
− 63
View file @ 9cd62f0a
This diff is collapsed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment