From 5b735c1afafb9b3abf64c9d72ac0a57b94ce2e03 Mon Sep 17 00:00:00 2001
From: Joris ten Tusscher <joristt@gmail.com>
Date: Tue, 9 Jan 2018 00:07:11 +0100
Subject: [PATCH] Added evalPossible checks to the test suite too.
---
src/SimpleFormulaChecker.hs | 8 +++++---
test/TIREval.hs | 16 +++++++++-------
2 files changed, 14 insertions(+), 10 deletions(-)
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index c13d930..ed0de20 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -220,12 +220,14 @@ compareSpec method1@(_, name1) method2@(_, name2) = do
postAns <- determineFormulaEq m1 m2 "post"
return $ preAns && postAns
-
-evaluate :: (FilePath, String) -> IO Bool
+evaluate :: (FilePath, String) -> IO (Bool, Maybe Bool)
evaluate method = do
m@(decls, mbody, env) <- parseMethod method
let e = extractExpr (getMethodCalls m "pre")
let lexpr = javaExpToLExpr e env decls
putStrLn (prettyLExpr lexpr)
- return ((prettyLExpr (LConst (LogicIR.Eval.eval lexpr))) == "true")
+ let t = CBool True
+ let possible = LogicIR.Eval.evalPossible lexpr
+ let res = if possible then Just (LogicIR.Eval.eval lexpr == t) else Nothing
+ return (possible, res)
diff --git a/test/TIREval.hs b/test/TIREval.hs
index 1c60a47..b42ddcd 100644
--- a/test/TIREval.hs
+++ b/test/TIREval.hs
@@ -8,13 +8,15 @@ import SimpleFormulaChecker
edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
-testEval :: Bool -> String -> Assertion
-testEval b s =
- unsafePerformIO (silence $ evaluate (edslSrc, s)) @?= b
-(.=) = testEval True
-(.!) = testEval False
+testEval :: (Bool, Maybe Bool) -> String -> Assertion
+testEval t@(evalPoss, evals2True) s =
+ unsafePerformIO (silence $ evaluate (edslSrc, s)) @?= t
+(.==) = testEval (True, Just True)
+(.=!) = testEval (True, Just False)
+(.!) = testEval (False, Nothing)
evalTests =
- [ (.=) "simple_eval1"
- , (.!) "simple_eval2"
+ [ (.==) "simple_eval1"
+ , (.=!) "simple_eval2"
+ , (.!) "simple_eval3"
]
--
GitLab