From b895f670072e43bc232f7e8eb87da6c29e092fce Mon Sep 17 00:00:00 2001
From: Joris ten Tusscher <joristt@gmail.com>
Date: Tue, 16 Jan 2018 00:19:10 +0100
Subject: [PATCH] =?UTF-8?q?Fixed=20bug=20that=20caused=20many=20of=20the?=
=?UTF-8?q?=20QuickCheck=20tests=20to=20fail,=20but=20there=E2=80=99s=20st?=
=?UTF-8?q?ill=20another=20bug.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
.../src/nl/uu/javawlp_edsl/Main.java | 4 ++--
src/LogicIR/Eval.hs | 2 +-
src/SimpleFormulaChecker.hs | 18 +++++++++---------
3 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
index f1cf99f..8976438 100644
--- a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -5,13 +5,13 @@ import static nl.uu.impress.EDSL.*;
public class Main {
- public static void test1(int[] b) {
+ public static void quickcheck_test1(int[] b) {
pre(~(-a * c) == (79 & 41));
pre(a > 0);
pre(forall(b, i -> b[i] > -10));
}
- public static void test2(int[] b) {
+ public static void quickcheck_test2(int[] b) {
pre(~(-a * c) == (79 & 41));
pre(a > 0);
pre(forall(b, i -> b[i] >= -10)); // note the >=, whereas test1 has >.
diff --git a/src/LogicIR/Eval.hs b/src/LogicIR/Eval.hs
index e9f9eee..d274afa 100644
--- a/src/LogicIR/Eval.hs
+++ b/src/LogicIR/Eval.hs
@@ -48,7 +48,7 @@ evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
-- Things that should never happen.
quant _ _ e1 e2 = error "Quantifiers cannot be evaluated and should be replaced using LogicIR.Rewrite.replaceQuantifiers."
- arr v a = error "You can't contain eval on an LExpr that contains uninstantiated arrays."
+ arr v a = error "You can't call eval on an LExpr that contains uninstantiated arrays."
var v = error "You can't call eval on an LExpr that contains uninstantiated vars."
-- Evaluates a binary operator expression.
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 8a67ca0..ec442ec 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -205,15 +205,6 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
showZ3AST :: Z3 AST -> IO String
showZ3AST ast' = evalZ3 $ ast' >>= astToString
-parse :: (FilePath, String) -> (FilePath, String) -> IO (MethodDef, MethodDef)
-parse method1@(_, name1) method2@(_, name2) = do
- -- load the methods
- m1@(decls1, mbody1, env1) <- parseMethod method1
- m2@(decls2, mbody2, env2) <- parseMethod method2
- when (env1 /= env2) $ fail "inconsistent method parameters"
- when (decls1 /= decls2) $ fail "inconsistent class declarations (TODO)"
- return (m1, m2)
-
-- Function that compares both the pre and the post condition for two methods.
-- It is assumed that both methods have the same environment (parameter names, class member names, etc).
compareSpec :: (FilePath, String) -> (FilePath, String) -> IO Bool
@@ -225,6 +216,15 @@ compareSpec method1@(_, name1) method2@(_, name2) = do
postAns <- determineFormulaEq m1 m2 "post"
return $ preAns && postAns
+parse :: (FilePath, String) -> (FilePath, String) -> IO (MethodDef, MethodDef)
+parse method1@(_, name1) method2@(_, name2) = do
+ -- load the methods
+ m1@(decls1, mbody1, env1) <- parseMethod method1
+ m2@(decls2, mbody2, env2) <- parseMethod method2
+ when (env1 /= env2) $ fail "inconsistent method parameters"
+ when (decls1 /= decls2) $ fail "inconsistent class declarations (TODO)"
+ return (m1, m2)
+
methodDefToLExpr :: MethodDef -> MethodDef -> String -> (LExpr, LExpr)
methodDefToLExpr m1@(decls1, _, env1) m2@(decls2, _, env2) name = do
-- get pre/post condition
--
GitLab