Adding a test that demonstrates the non-duplication.

Author: Remi Delmas

regression/contracts/no_redudant_checks/main.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+const int N = 100;
+int main()
+{
+  int *buf = malloc(N * sizeof(*buf));
+  char *lb = (((char *)buf) - __CPROVER_POINTER_OFFSET(buf));
+  char *ub = (((char *)buf) - __CPROVER_POINTER_OFFSET(buf)) +
+             __CPROVER_OBJECT_SIZE(buf) - 1;
+}

regression/contracts/no_redudant_checks/test.desc

@@ -0,0 +1,42 @@
+CORE
+main.c
+--pointer-overflow-check _ --pointer-overflow-check --unsigned-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^\[malloc.assertion.1\].*: SUCCESS
+^\[malloc.assertion.2\].*: SUCCESS
+^\[main.overflow.1\].*: SUCCESS
+^\[main.pointer_arithmetic.1\].*: SUCCESS
+^\[main.pointer_arithmetic.2\].*: SUCCESS
+^\[main.pointer_arithmetic.3\].*: SUCCESS
+^\[main.pointer_arithmetic.4\].*: SUCCESS
+^\[main.pointer_arithmetic.5\].*: SUCCESS
+^\[main.pointer_arithmetic.6\].*: SUCCESS
+^\[main.pointer_arithmetic.7\].*: SUCCESS
+^\[main.pointer_arithmetic.8\].*: SUCCESS
+^\[main.pointer_arithmetic.9\].*: SUCCESS
+^\[main.pointer_arithmetic.10\].*: SUCCESS
+^\[main.pointer_arithmetic.11\].*: SUCCESS
+^\[main.pointer_arithmetic.12\].*: SUCCESS
+^\[main.pointer_arithmetic.13\].*: SUCCESS
+^\[main.pointer_arithmetic.14\].*: SUCCESS
+^\[main.pointer_arithmetic.15\].*: SUCCESS
+^\[main.pointer_arithmetic.16\].*: SUCCESS
+^\[main.pointer_arithmetic.17\].*: SUCCESS
+^\*\* 0 of 20 failed \(1 iterations\)
+^VERIFICATION SUCCESSFUL$
+--
+^\[main.overflow.\d+\].*: FAILURE
+--
+Checks that assertions generated by the first --pointer-overflow-check:
+- do not get duplicated by the second --unsigned-overflow-check
+- do not get instrumented with --unsigned-overflow-check (would fail the proof)
+
+We expect 20 assertions to be generated:
+In the goto-instrument run:
+- 2 for using malloc
+- 17 caused by --pointer-overflow-check
+
+In the final cbmc run:
+- 0 caused by --pointer-overflow-check
+- 1 caused by the --unsigned-overflow-check