Regression tests for enums in incr SMT2 solver

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/enums/enum_in_array.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+enum E
+{
+  V0 = 0,
+  V1 = 1,
+  V2 = 2
+};
+
+int main()
+{
+  unsigned i;
+  __CPROVER_assume(i < 3);
+  enum E e[3];
+  e[0] = V0;
+  e[1] = V1;
+  e[2] = V2;
+  __CPROVER_assert(e[i] > 0, "Array at index 0 is V0, so this should fail");
+}

regression/cbmc-incr-smt2/enums/enum_in_array.desc

@@ -0,0 +1,15 @@
+CORE
+enum_in_array.c
+--trace
+Passing problem to incremental SMT2 solving
+line 18 Array at index 0 is V0, so this should fail: FAILURE
+i=0u \(00000000 00000000 00000000 00000000\)
+e\[0l+\]=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
+e\[1l+\]=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
+e\[2l+\]=/\*enum\*/V2 \(00000000 00000000 00000000 00000010\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that we support enum values and traces for an array of enums. At the time of adding the
+regression test, this exercised the conversion code specific to c_enum_tag_typet.

regression/cbmc-incr-smt2/enums/enum_in_struct.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+enum E
+{
+  V0 = 0,
+  V1 = 1,
+  V2 = 2
+};
+
+struct S
+{
+  enum E a;
+  int b;
+};
+
+int main()
+{
+  struct S s;
+  s.a = V1;
+  __CPROVER_assume(__CPROVER_enum_is_in_range(s.a));
+  __CPROVER_assert(s.a > 10, "Struct field s.a is V1, so this should fail");
+}

regression/cbmc-incr-smt2/enums/enum_in_struct.desc

@@ -0,0 +1,12 @@
+CORE
+enum_in_struct.c
+--trace
+Passing problem to incremental SMT2 solving
+line 21 Struct field s\.a is V1, so this should fail: FAILURE
+s\.a=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that we support enum values and traces for an struct with enums fields. At the time of adding
+the regression test, this exercised the conversion code specific to c_enum_tag_typet.

regression/cbmc-incr-smt2/enums/simple.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+enum E
+{
+  V0 = 0,
+  V1 = 1,
+  V2 = 2
+};
+
+int main()
+{
+  enum E e;
+  e = V1;
+  __CPROVER_assume(__CPROVER_enum_is_in_range(e));
+  __CPROVER_assert(e > 10, "Variable e is V1, so this should fail");
+}

regression/cbmc-incr-smt2/enums/simple.desc

@@ -0,0 +1,14 @@
+CORE
+simple.c
+--trace
+Passing problem to incremental SMT2 solving
+line 15 Variable e is V1, so this should fail: FAILURE
+e=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
+e=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that we support enum values and traces for a trivial example. At the
+time of adding the regression test, this exercised the conversion code specific
+to c_enum_tag_typet.