Add tests for enums returned by opaque methods

The tests were copied from jbmc/regression/jbmc/NondetEnumArg and
adapted for the case where the enum is returned by an opaque method
(Opaque.class has been deleted).

Author: antlechner

jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.class

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

jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.java

@@ -0,0 +1,54 @@
+public class NondetEnumOpaqueReturn {
+
+  public static void canChooseSomeConstant() {
+    Opaque o = new Opaque();
+    Color c = o.getC();
+    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() {
+    Opaque o = new Opaque();
+    Color c = o.getC();
+    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() {
+    Opaque o = new Opaque();
+    Color c = o.getC();
+    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() {
+    Opaque o = new Opaque();
+    Color c = o.getC();
+    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/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.class

@@ -0,0 +1,9 @@
+public class Opaque {
+
+  Color c;
+
+  public Color getC() {
+    return c;
+  }
+
+}

jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java

@@ -0,0 +1,11 @@
+CORE
+NondetEnumOpaqueReturn.class
+--function NondetEnumOpaqueReturn.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
+which have been returned by an opaque method correspond to those of an enum
+constant of the same type.

jbmc/regression/jbmc/NondetEnumOpaqueReturn/Opaque.java

@@ -0,0 +1,7 @@
+CORE
+NondetEnumOpaqueReturn.class
+--function NondetEnumOpaqueReturn.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/NondetEnumOpaqueReturn/test_some_constant.desc

@@ -0,0 +1,7 @@
+CORE
+NondetEnumOpaqueReturn.class
+--function NondetEnumOpaqueReturn.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/NondetEnumOpaqueReturn/test_specific_constant1.desc

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