Add tests for nondet initialization of enums

The tests check that for a nondeterministic non-null enum, any of the
constants of its type can be chosen, and nothing other than these
constants.

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,46 @@
+public class NondetEnumArg {
+
+    public static void canChooseSomeConstant(Color c) {
+        if (c == null)
+            return;
+        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);
+    }
+
+    public static void canChooseRed(Color c) {
+        if (c == null)
+            return;
+        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 (isGreen || isBlue);
+    }
+
+    public static void canChooseGreen(Color c) {
+        if (c == null)
+            return;
+        boolean isRed = c.name().startsWith("RED") && c.name().length() == 3
+            && c.ordinal() == 0;
+        boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4
+            && c.ordinal() == 2;
+        assert (isRed || isBlue);
+    }
+
+    public static void canChooseBlue(Color c) {
+        if (c == null)
+            return;
+        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;
+        assert (isRed || isGreen);
+    }
+
+}

jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.class

@@ -0,0 +1,10 @@
+CORE
+NondetEnumArg.class
+--function NondetEnumArg.canChooseSomeConstant --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.

jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.java

@@ -0,0 +1,7 @@
+CORE
+NondetEnumArg.class
+--function NondetEnumArg.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION FAILED$
+--
+--
+Test 1 of 3 to check that any of the enum constants can be chosen.

jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc

@@ -0,0 +1,7 @@
+CORE
+NondetEnumArg.class
+--function NondetEnumArg.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION FAILED$
+--
+--
+Test 2 of 3 to check that any of the enum constants can be chosen.

jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc

@@ -0,0 +1,7 @@
+CORE
+NondetEnumArg.class
+--function NondetEnumArg.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION FAILED$
+--
+--
+Test 3 of 3 to check that any of the enum constants can be chosen.