Add test for enum field of argument type

Author: antlechner

jbmc/regression/jbmc/NondetEnumArgField/Color.class

@@ -0,0 +1,5 @@
+public enum Color {
+    RED,
+    GREEN,
+    BLUE
+}

jbmc/regression/jbmc/NondetEnumArgField/Color.java

@@ -0,0 +1,11 @@
+public class MyClass {
+
+    private Color c;
+
+    public int myMethod() {
+        if (c == null)
+            return 10;
+        return 20;
+    }
+
+}

jbmc/regression/jbmc/NondetEnumArgField/MyClass.class

@@ -0,0 +1,8 @@
+public class NondetEnumArgField {
+
+    public static void test(MyClass mc) {
+        int result = mc.myMethod();
+        assert result == 10;
+    }
+
+}

jbmc/regression/jbmc/NondetEnumArgField/MyClass.java

@@ -0,0 +1,9 @@
+CORE
+NondetEnumArgField.class
+--function NondetEnumArgField.test --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION FAILED$
+--
+--
+The test checks that even when none of the enum constants are referenced in user
+code, a nondet enum (in this case, a field of an argument) is still correctly
+loaded and initialized.