Add regression tests for initialization of Java main args

regression/cbmc-java/main-args-elements-non-null1/Main.java

@@ -0,0 +1,9 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    if(args.length>0)
+      assert(args[0] != null); // must hold
+  }
+}
+

regression/cbmc-java/main-args-elements-non-null1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/main-args-elements-non-null2/Main.java

@@ -0,0 +1,17 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    try {
+      if(args.length>0)
+      {
+        String s = args[0];
+        int i = s.length(); // must not fail
+      }
+    }
+    catch(Exception e) {
+      assert false; // unreachable
+    }
+  }
+}
+

regression/cbmc-java/main-args-elements-non-null2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--java-throw-runtime-exceptions --refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/main-args-elements-non-null3/Main.java

@@ -0,0 +1,12 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    if(args.length>1)
+    {
+      assert(args[0] != null); // must hold
+      assert(args[1] != null); // must hold
+    }
+  }
+}
+

regression/cbmc-java/main-args-elements-non-null3/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/main-args-elements-non-null4/Main.java

@@ -0,0 +1,18 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    try {
+      if(args.length>0) {
+        String s = args[0];
+        if(s != null) {
+          int i = s.length(); // definitely must not fail
+        }
+      }
+    }
+    catch(Exception e) {
+      assert false; // unreachable
+    }
+  }
+}
+

regression/cbmc-java/main-args-elements-non-null4/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--java-throw-runtime-exceptions --refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/main-args-non-null-with-function1/Main.java

@@ -0,0 +1,8 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    assert(args != null); // must hold
+  }
+}
+

regression/cbmc-java/main-args-non-null-with-function1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/main-args-non-null1/Main.java

@@ -0,0 +1,8 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    assert(args != null); // must hold
+  }
+}
+

regression/cbmc-java/main-args-non-null1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/main-args-non-null2/Main.java

@@ -0,0 +1,12 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    try {
+      int i = args.length; // args must be non-null
+    }
+    catch(Exception e) {
+      assert false; // unreachable
+    }
+  }
+}

regression/cbmc-java/main-args-non-null2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--java-throw-runtime-exceptions --refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/main-args-non-null3/Main.java

@@ -0,0 +1,8 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    assert(args == null); // must fail
+  }
+}
+

regression/cbmc-java/main-args-non-null3/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/no-main-args-elements-maybe-null1/Main.java

@@ -0,0 +1,9 @@
+public class Main
+{
+  static void main(String[] args) // not public!
+  {
+    if(args != null && args.length>0)
+      assert(args[0] != null); // allowed to fail
+  }
+}
+

regression/cbmc-java/no-main-args-elements-maybe-null1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main --refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/no-main-args-elements-maybe-null2/Main.java

@@ -0,0 +1,10 @@
+public class Main
+{
+  static void main(String[] args) // not public!
+  {
+    if(args != null && args.length>0 && args[0] != null) {
+      assert(false); // allowed to fail
+    }
+  }
+}
+

regression/cbmc-java/no-main-args-elements-maybe-null2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main --refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/no-main-args-maybe-null1/Main.java

@@ -0,0 +1,8 @@
+public class Main
+{
+  public void main(String[] args) // not static!
+  {
+    assert(args != null); // allowed to fail
+  }
+}
+

regression/cbmc-java/no-main-args-maybe-null1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/no-main-args-maybe-null2/Main.java

@@ -0,0 +1,8 @@
+public class Main
+{
+  public void main(String[] args) // not static!
+  {
+    assert(args == null); // allowed to fail
+  }
+}
+

regression/cbmc-java/no-main-args-maybe-null2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/no-main-int-array-maybe-null1/Main.java

@@ -0,0 +1,17 @@
+public class Main
+{
+  public static void main(int[] args)
+  {
+    assert(args == null); // allowed to fail
+    assert(args != null); // allowed to fail
+    if(args != null && args.length > 0) {
+      try {
+        int i = args[0];
+      }
+      catch(Exception e) {
+        assert false; // must hold
+      }
+    }
+  }
+}
+

regression/cbmc-java/no-main-int-array-maybe-null1/test.desc

@@ -0,0 +1,12 @@
+CORE
+Main.class
+--function Main.main --java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE
+assertion at file Main.java line 6 function .* bytecode-index 14: FAILURE
+assertion at file Main.java line 12 function .* bytecode-index 31: SUCCESS
+\*\* 2 of .* failed
+--
+^warning: ignoring

regression/cbmc-java/no-main-multi-array-maybe-null1/Main.java

@@ -0,0 +1,11 @@
+public class Main
+{
+  public static void main(String[][] args)
+  {
+    assert(args == null ||
+	    args.length == 0 ||
+	    args[0] == null ||
+	    args[0].length == 0 ||
+	    args[0][0] != null); // allowed to fail
+  }
+}

regression/cbmc-java/no-main-multi-array-maybe-null1/test.desc

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main --refine-strings --java-max-input-array-length 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring

regression/cbmc-java/no-main-multi-array-maybe-null2/Main.java

@@ -0,0 +1,11 @@
+public class Main
+{
+  public static void main(String[][] args)
+  {
+    assert(args == null ||
+	    args.length == 0 ||
+	    args[0] == null ||
+	    args[0].length == 0 ||
+	    args[0][0] == null); // allowed to fail
+  }
+}

regression/cbmc-java/no-main-multi-array-maybe-null2/test.desc

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main --refine-strings --java-max-input-array-length 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring

regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main.java

@@ -0,0 +1,16 @@
+public class Main
+{
+  public static class A {
+    int x;
+  }
+  public A a;
+
+  public static void main(Main[] args)
+  {
+    if(args != null && args.length > 0) {
+      Main m = args[0];
+      assert(m == null); // allowed to fail
+    }
+  }
+}
+

regression/cbmc-java/no-main-object-array-elements-maybe-null1/test.desc

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 12 function .* bytecode-index 15: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring

regression/cbmc-java/no-main-object-array-maybe-null1/Main.java

@@ -0,0 +1,20 @@
+public class Main
+{
+  public static class A {
+    int x;
+  }
+  public A a;
+
+  public static void main(Main[] args)
+  {
+    assert(args != null); // allowed to fail
+    if(args != null && args.length > 0) {
+      Main m = args[0];
+      if(m != null) {
+        assert(m.a == null); // allowed to fail
+        assert(m.a != null); // allowed to fail
+      }
+    }
+  }
+}
+

regression/cbmc-java/no-main-object-array-maybe-null1/test.desc

@@ -0,0 +1,12 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
+assertion at file Main.java line 14 function .* bytecode-index 26: FAILURE
+assertion at file Main.java line 15 function .* bytecode-index 35: FAILURE
+\*\* 3 of .* failed
+--
+^warning: ignoring