From 08af0783004e1ad4706e23ea3dbaa74f6fec6561 Mon Sep 17 00:00:00 2001
From: "Ogilvie, D.H. (Duncan)" <d.h.ogilvie2@students.uu.nl>
Date: Sat, 14 Oct 2017 15:52:44 +0200
Subject: [PATCH] small improvements
---
src/LogicIR/Backend/Z3.hs | 2 +-
src/LogicIR/Frontend/Java.hs | 4 ++--
src/SimpleFormulaChecker.hs | 3 ++-
src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java | 14 ++++++++++++++
4 files changed, 19 insertions(+), 4 deletions(-)
diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index f40a117..93b5c9e 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -50,7 +50,7 @@ lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray,
a <- a'
mkSelect v a
flNil = do intSort <- mkBvSort 32
- zero <- mkBitvector 32 0
+ zero <- mkBitvector 32 0 -- (isNull, data, length) TODO
mkConstArray intSort zero
fnConst n = mkBitvector 32 (fromIntegral n)
fnUnop o a' = do a <- a'
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index fcc1314..d2cbd8e 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -47,8 +47,8 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
_
-> error $ "Unimplemented fMethodInv: " ++ show inv
fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking
- ArrayIndex (ExpName name) [ExpName index]
- -> LArray (nameToVar name env decls) (LVar (nameToVar index env decls))
+ ArrayIndex (ExpName name) [expr]
+ -> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls) -- (LVar (nameToVar index env decls))
_
-> error $ "Multidimensional arrays are not supported: " ++ show (arrayIndex)
fExpName name env decls = case name of -- TODO: type checking
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 161b978..22d5505 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -171,4 +171,5 @@ compareSpec method1@(_, name1) method2@(_, name2) = do
edslSrc = "javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
testEq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec1")
testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
-blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec2")
\ No newline at end of file
+blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec2")
+blub2 = compareSpec (edslSrc, "test1") (edslSrc, "test2")
\ No newline at end of file
diff --git a/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java b/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
index e9f2b96..9a61276 100644
--- a/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -107,7 +107,21 @@ public class Main {
post(a[i] == oldaj);
}
+ public static void test1(int[] a)
+ {
+ pre(exists(a, i -> a[i+1] > a[i]));
+ post(true);
+ }
+
+ public static void test2(int[] a)
+ {
+ pre(false);
+ //pre(exists(a, i -> a[i+1] >= a[i]));
+ post(true);
+ }
+
public static void swap_spec2(int[] a, int i, int j) {
+ pre(a != null && a[0] == 0);
pre(a != null && a.length > 0 && i >= 0 && j > 0);
// introducing vars to remember old values
int oldai = a[i], oldaj = a[j];
--
GitLab