Add test for nondet initialization of enums

Author: antlechner

jbmc/regression/jbmc/NondetEnumArg/Color.class

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

jbmc/regression/jbmc/NondetEnumArg/Color.java

@@ -0,0 +1,17 @@
+public class NondetEnumArg {
+
+    public static Color test(Color c) {
+        if (c == null)
+            return c;
+        assert c != null;
+        boolean isRed = c.name().startsWith("RED") && c.name().length() == 3
+            && c.ordinal() == 0;
+        boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5
+            && c.ordinal() == 1;
+        boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4
+            && c.ordinal() == 2;
+        assert (isRed || isGreen || isBlue);
+        return c;
+    }
+
+}

jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.class

@@ -0,0 +1,10 @@
+CORE
+NondetEnumArg.class
+--function NondetEnumArg.test --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The test checks that the name and ordinal fields of nondet-initialized enums
+correspond to those of an enum constant of the same type.