Add tests of the affect of assumptions on coverage blocks

Author: thomasspriggs

regression/cbmc-cover/location-assume/end.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+void main()
+{
+  int i;
+  int *p = &i;
+  int j;
+  __CPROVER_assume(j == 1 / (*p));
+}

regression/cbmc-cover/location-assume/end.desc

@@ -0,0 +1,14 @@
+CORE
+end.c
+--pointer-check --div-by-zero-check --cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file end.c line 5 function main block 1 \(lines end\.c:main:5-8\): SATISFIED$
+^\[main.coverage.2\] file end.c line 9 function main block 2 \(lines end\.c:main:9\): SATISFIED$
+^\*\* 2 of 2 covered \(100.0%\)
+--
+^warning: ignoring
+--
+Test that in the case where multiple assertions are added on the same line of
+code due to the addition of instrumentation checks, these do not result in
+further splitting blocks.

regression/cbmc-cover/location-assume/middle.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  int i;
+  int j;
+  j = i;
+  __CPROVER_assume(0);
+  j = i + 2;
+  return 0;
+}

regression/cbmc-cover/location-assume/middle.desc

@@ -0,0 +1,15 @@
+CORE
+middle.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file middle.c line 5 function main block 1 \(lines middle\.c:main:5-8\): SATISFIED$
+^\[main.coverage.2\] file middle.c line 9 function main block 2 \(lines middle\.c:main:9-11\): FAILED$
+^\*\* 1 of 2 covered \(50.0%\)
+--
+^warning: ignoring
+--
+This test confirms that assumptions in the middle of what would otherwise be a
+single blocks without control flow will cause the code to be split into 2
+coverage blocks. This is required as an unsatisfiable assumption can result in
+the following statements being unreachable.