Add regression tests for enum_is_in_range

Adds regression tests for enum_is_in_range to
test positive, negative and error outcomes on both named
and typedef'd enumerations.

Author: TGWDB

regression/ansi-c/enum_is_in_range/enum_test10.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  int i = 0;
+  while(i < 10)
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(i));
+    i++;
+  }
+  return 0;
+}

regression/ansi-c/enum_is_in_range/enum_test10.desc

@@ -0,0 +1,12 @@
+CORE
+enum_test10.c
+
+^EXIT=(6|70)$
+^SIGNAL=0$
+^file enum_test10.c line \d+ function main: __CPROVER_enum_is_in_range expects enum, but \(i\) has type `signed int`$
+--
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): SUCCESS$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): FAILURE$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test the type checking of argument for __CPROVER_enum_is_in_range

regression/ansi-c/enum_is_in_range/enum_test12.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  assert(__CPROVER_enum_is_in_range(ev1, ev2));
+  return 0;
+}

regression/ansi-c/enum_is_in_range/enum_test12.desc

@@ -0,0 +1,12 @@
+CORE
+enum_test12.c
+
+^EXIT=(6|70)$
+^SIGNAL=0$
+^file enum_test12.c line \d+ function main: __CPROVER_enum_is_in_range takes exactly 1 argument, but 2 were provided$
+--
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): SUCCESS$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): FAILURE$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test the type checking of argument for __CPROVER_enum_is_in_range

regression/cbmc/enum_is_in_range/enum_test3.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  while(ev1 != ev2)
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(ev1));
+  }
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test3.desc

@@ -0,0 +1,11 @@
+CORE
+enum_test3.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS
+--
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range
+--
+This test is for the enum_is_in_range working properly, the negation
+is if the function is not defined.

regression/cbmc/enum_is_in_range/enum_test4.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  int i = 0;
+  while(i < 10)
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(ev1));
+    i++;
+  }
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test4.desc

@@ -0,0 +1,13 @@
+CORE
+enum_test4.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): FAILURE$
+--
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test is for the enum_is_in_range working properly and detecting
+when the enum is not in range. The negation tests are to ensure the
+out of range is detected, and if the function is not defined.

regression/cbmc/enum_is_in_range/enum_test5.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+void testfun(enum my_enum ee)
+{
+}
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  __CPROVER_assume(__CPROVER_enum_is_in_range(ev1));
+  enum my_enum ev3 = ev1;
+  testfun(ev3);
+  testfun(ev2);
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test5.desc

@@ -0,0 +1,16 @@
+CORE
+enum_test5.c
+--enum-range-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main.enum-range-check.6\] line \d+ enum range check in ev3: SUCCESS$
+^\[main.enum-range-check.7\] line \d+ enum range check in ev2: FAILURE$
+--
+^\[main.enum-range-check.6\] line \d+ enum range check in ev3: FAILURE$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test is for the enum_is_in_range working in assume statements
+(and also value passing through assignments of enums). The failure
+test case is checking that range checks do work on enums.
+The negation tests are to ensure the assumption is taken into account
+for ev1 and thus ev3, and if the function is not defined.

regression/cbmc/enum_is_in_range/enum_test7.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+typedef enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+} my_enum;
+
+int main()
+{
+  my_enum ev1;
+  my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  while(!(ev1 == ev2))
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(ev1));
+  }
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test7.desc

@@ -0,0 +1,11 @@
+CORE
+enum_test7.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS
+--
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range
+--
+This test is for the enum_is_in_range working properly, the negation
+is if the function is not defined.

regression/cbmc/enum_is_in_range/enum_test8.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+typedef enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+} my_enum;
+
+int main()
+{
+  my_enum ev1;
+  my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  int i = 0;
+  while(i < 10)
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(ev1));
+    i++;
+  }
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test8.desc

@@ -0,0 +1,13 @@
+CORE
+enum_test8.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): FAILURE$
+--
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test is for the enum_is_in_range working properly and detecting
+when the enum is not in range. The negation tests are to ensure the
+out of range is detected, and if the function is not defined.