Add regression tests for initialization of Java main args

Author: peterschrammel

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

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

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

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

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

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

regression/cbmc-java/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 fail
+  }
+}
+

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

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