add null checks

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 -- (isNull, data, length) TODO: support proper null types
+               zero <- mkBitvector 32 0x1337 -- (isNull, data, length) TODO: support proper null types
                mkConstArray intSort zero
     fnConst n = mkBitvector 32 (fromIntegral n)
     fnUnop o a' = do a <- a'

src/SimpleFormulaChecker.hs

@@ -40,7 +40,7 @@ parseMethod (src, name) = do
     -- return the relevant data
     return (decls, mbody, env)
     where
-    -- | Parse a Java source file, and extracts the necessary information from the compilation unit
+    -- parse a Java source file, and extracts the necessary information from the compilation unit
     parseJava :: FilePath -> IO CompilationUnit
     parseJava s = do
         -- Get the source code
@@ -103,8 +103,7 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
        Sat   -> do
                 putStrLn "formulas are NOT equivalent, model:"
                 case model of
-                  Just m -> do env <- newItpEnv Nothing (Z3.Opts.opt ":pp.bv-literals" False)
-                               s <- evalZ3WithEnv (modelToString m) env 
+                  Just m -> do s <- evalZ3 (modelToString m)
                                putStr s
                   _      -> return ()
     where
@@ -132,4 +131,5 @@ testEq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec1")
 testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
 blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec2")
 blub2 = compareSpec (edslSrc, "test1") (edslSrc, "test2")
-blob = compareSpec (edslSrc, "blob1") (edslSrc, "blob1")
\ No newline at end of file
+blob = compareSpec (edslSrc, "blob1") (edslSrc, "blob1")
+nullTest = compareSpec (edslSrc, "null1") (edslSrc, "null2")
\ No newline at end of file

src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java

@@ -107,20 +107,27 @@ public class Main {
         post(a[i] == oldaj);
     }
 
-    public static void blob1(int[] a)
-    {
+    public static void null1(int[] a, int x) {
+        pre(a != null);
+        post(true);
+    }
+
+    public static void null2(int[] a, int x) {
+        pre(exists(a, i -> a[i] != 0x1337));
+        post(true);
+    }
+
+    public static void blob1(int[] a)  {
         pre(forall(a, i -> { return a[i] == 0; }));
         post(true);
     }
 
-    public static void test1(int[] a)
-    {
+    public static void test1(int[] a)  {
         pre(exists(a, i -> a[i+1] > a[i]));
         post(true);
     }
 
-    public static void test2(int[] a)
-    {
+    public static void test2(int[] a)  {
         pre(false);
         //pre(exists(a, i -> a[i+1] >= a[i]));
         post(true);