Add regression tests for initialization of Java main args

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

@@ -0,0 +1,11 @@
+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
+    }
+  }
+}

jbmc/regression/jbmc/main-args-elements-non-null1/test.desc

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

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

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

jbmc/regression/jbmc/main-args-elements-non-null2/test.desc

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

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

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

jbmc/regression/jbmc/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

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

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

jbmc/regression/jbmc/main-args-non-null1/test.desc

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

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

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

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

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

jbmc/regression/jbmc/no-main-args-elements-maybe-null2/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
+    }
+  }
+}

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

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

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

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

jbmc/regression/jbmc/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

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

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

jbmc/regression/jbmc/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

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

@@ -0,0 +1,16 @@
+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
+      }
+    }
+  }
+}

jbmc/regression/jbmc/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

jbmc/regression/jbmc/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
+  }
+}

jbmc/regression/jbmc/no-main-multi-array-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 5 function .* bytecode-index 24: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring

jbmc/regression/jbmc/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
+  }
+}

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

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

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

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

jbmc/regression/jbmc/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

jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java

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

jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/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

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

@@ -0,0 +1,18 @@
+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
+      }
+    }
+  }
+}

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

@@ -0,0 +1,11 @@
+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
+\*\* 2 of .* failed
+--
+^warning: ignoring

jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java

@@ -0,0 +1,18 @@
+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
+      }
+    }
+  }
+}

jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc

@@ -0,0 +1,11 @@
+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
+\*\* 2 of .* failed
+--
+^warning: ignoring