Add regression tests for initialization of Java main args

Author: peterschrammel

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

@@ -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/Main.java

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

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

@@ -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/Main.class

@@ -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,7 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    assert(args != null); // must hold
+  }
+}

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

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