Merge pull request #6665 from NlightNFotis/flag_tests_smt_arithop

Add tests for `--div-by-zero` and `--signed-overflow` checks for the new SMT backend

Author: NlightNFotis

regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int x = 5;
+  int y;
+  int z = 8;
+
+  // Negative case
+  __CPROVER_assert(x / y != 0, "This assertion is falsifiable");
+
+  // Positive case
+  __CPROVER_assert(
+    x / z != 0, "This assertion is valid under all interpretations");
+
+  return 0;
+}

regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc

@@ -0,0 +1,14 @@
+CORE
+div_by_zero.c
+--incremental-smt2-solver 'z3 --smt2 -in' --div-by-zero-check --trace
+\[main\.division-by-zero\.1\] line \d division by zero in x / y: FAILURE
+\[main\.division-by-zero\.2\] line \d+ division by zero in x / z: SUCCESS
+y=0
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test is designed to drive the `--div-by-zero-check` in both the positive
+and the negative case, and show that it's working for our current implementation-in-progress
+of the new SMT backend.

regression/cbmc-incr-smt2/bitvector-flag-tests/readme.md

@@ -0,0 +1,12 @@
+# Flag tests
+
+Up until this point, the tests we have for the new SMT backend focus on getting
+simple arithmetic or relational operator verification runs done.
+
+This folder contains a couple of tests that are being run with CBMC flags, adding
+extra assertions such as `--div-by-zero` or `--signed-overflow-check`.
+
+Long term the plan is for this folder to be deleted, and the tests that are being
+run as part of the old SMT backend (or maybe even the whole of CBMC's regression
+test suite) to be run through a label or a flag. But for now, this should do well
+enough to allow us to track the progress of our completion of the new backend.

regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.c

@@ -0,0 +1,10 @@
+#include <limits.h>
+
+int main()
+{
+  int x = INT_MAX;
+  int y;
+  int z = x + y;
+
+  __CPROVER_assert(z < INT_MIN, "This assertion is falsifiable");
+}

regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+signed_overflow.c
+--incremental-smt2-solver 'z3 --smt2 -in' --signed-overflow-check --trace
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+Invariant check failed
+Reason: Reached unimplemented Generation of SMT formula for unknown kind of expression: overflow-\+
+--
+This tests exercise the driving of the `--signed-overflow-check` flag.