Add regression tests for the handling of unsigned integers.

Author: NlightNFotis

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.c

@@ -16,4 +16,31 @@ int main()
   __CPROVER_assert((a * a) / a == a, "a squared divided by a equals a");
   __CPROVER_assert((2 * a) / a == 2, "two times a divided by a equals two");
   __CPROVER_assert(a % a == 0, "a mod itself equals 0");
+
+  // Same round of tests, but for a type of different size
+  long long int b;
+  __CPROVER_assume(b < 100ll);
+  __CPROVER_assume(b > -100ll);
+  __CPROVER_assume(b != 0ll);
+
+  __CPROVER_assert(b + b == b * 2ll, "b plus b always equals two times b");
+  __CPROVER_assert(b - b == 0ll, "b minus b always equals 0");
+  __CPROVER_assert(b + -b == 0ll, "b plus its additive inverse equals 0");
+  __CPROVER_assert(
+    b - -b == 2ll * b, "b minus its additive inverse equals two times b");
+  __CPROVER_assert((b * b) / b == b, "b squared divided by b equals b");
+  __CPROVER_assert((2ll * b) / b == 2ll, "two times b divided by b equals two");
+  __CPROVER_assert(b % b == 0ll, "b mod itself equals 0");
+
+  char c = 0x0;
+  __CPROVER_assume(c != 0x00);
+
+  __CPROVER_assert(c + c == c * 0x2, "c plus c always equals two times c");
+  __CPROVER_assert(c - c == 0x0, "c minus c always equals 0");
+  __CPROVER_assert(c + -c == 0x0, "c plus its additive inverse equals 0");
+  __CPROVER_assert(
+    c - -c == 0x2 * c, "c minus its additive inverse equals two times c");
+  __CPROVER_assert((c * c) / c == c, "c squared divided by c equals c");
+  __CPROVER_assert((0x2 * c) / c == 0x2, "two times c divided by c equals two");
+  __CPROVER_assert(c % c == 0x0, "c mod itself equals 0");
 }

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc

@@ -8,6 +8,20 @@ simple_equation.c
 \[main\.assertion\.5\] line \d+ a squared divided by a equals a: SUCCESS
 \[main\.assertion\.6\] line \d+ two times a divided by a equals two: SUCCESS
 \[main\.assertion\.7\] line \d+ a mod itself equals 0: SUCCESS
+\[main\.assertion\.8\] line \d+ b plus b always equals two times b: SUCCESS
+\[main\.assertion\.9\] line \d+ b minus b always equals 0: SUCCESS
+\[main\.assertion\.10\] line \d+ b plus its additive inverse equals 0: SUCCESS
+\[main\.assertion\.11\] line \d+ b minus its additive inverse equals two times b: SUCCESS
+\[main\.assertion\.12\] line \d+ b squared divided by b equals b: SUCCESS
+\[main\.assertion\.13\] line \d+ two times b divided by b equals two: SUCCESS
+\[main\.assertion\.14\] line \d+ b mod itself equals 0: SUCCESS
+\[main\.assertion\.15\] line \d+ c plus c always equals two times c: SUCCESS
+\[main\.assertion\.16\] line \d+ c minus c always equals 0: SUCCESS
+\[main\.assertion\.17\] line \d+ c plus its additive inverse equals 0: SUCCESS
+\[main\.assertion\.18\] line \d+ c minus its additive inverse equals two times c: SUCCESS
+\[main\.assertion\.19\] line \d+ c squared divided by c equals c: SUCCESS
+\[main\.assertion\.20\] line \d+ two times c divided by c equals two: SUCCESS
+\[main\.assertion\.21\] line \d+ c mod itself equals 0: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.c

@@ -0,0 +1,21 @@
+int main()
+{
+  unsigned int a;
+  unsigned int b = 12;
+  __CPROVER_assume(a > 15);
+
+  // expected to fail by assigning a = 4294967284u in the trace
+  // and wrapping around to 0, which results in 0 > 27.
+  __CPROVER_assert(a + b > 27, "a plus b should be more than 27");
+  // expected to fail by assigning a = 2147483648u in the trace
+  // and evaluating to 2147483660 > 27, which is true.
+  __CPROVER_assert(!(a + b > 27), "a plus b should be more than 27");
+
+  // Same round of tests but for unsigned long long.
+  unsigned long long int c;
+  unsigned long long int d = 12llu;
+  __CPROVER_assume(c > 15llu);
+
+  __CPROVER_assert(c + d > 27, "c plus d should be more than 27");
+  __CPROVER_assert(!(c + d > 27), "c plus d should be more than 27");
+}

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc

@@ -0,0 +1,16 @@
+CORE
+unsigned_behaviour.c
+--incremental-smt2-solver 'z3 --smt2 -in' --trace
+\[main\.assertion\.1\] line \d+ a plus b should be more than 27: FAILURE
+\[main\.assertion\.2\] line \d+ a plus b should be more than 27: FAILURE
+\[main\.assertion\.3\] line \d+ c plus d should be more than 27: FAILURE
+\[main\.assertion\.4\] line \d+ c plus d should be more than 27: FAILURE
+a=\d+(u|ul)?
+c=\d+(u|ul)?
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test checks for the correct behaviour of unsigned integers around
+boundary values.