Add comments to tests

Author: hannes-steffenhagen-diffblue

regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc

@@ -1,11 +1,14 @@
 CORE paths-lifo-expected-failure
 test.c
 --cover location --pointer-check --malloc-may-fail --malloc-fail-null
-\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:13,14\): SATISFIED
-\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:11\): FAILED
-\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,8,10\): SATISFIED
+\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED
+\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): FAILED
+\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED
 \[main\.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+This is checking that without the --cover-failed-assertions flag we still get the same result as we did before adding
+it in this example.

regression/cbmc/cover-failed-assertions/test.c

@@ -5,6 +5,10 @@ int main()
   int *ptr = malloc(sizeof(*ptr));
   int a;
 
+  // pointer check would detect the dereference of a null pointer here
+  // default --cover lines behaviour is to treat non-cover assertions as
+  // assumptions instead, so in the ptr == NULL case we don't get past this line
+  // leading to failed coverage for the body of the if statement down below
   a = *ptr;
 
   if(ptr == NULL)

regression/cbmc/cover-failed-assertions/test.desc

@@ -1,11 +1,13 @@
 CORE paths-lifo-expected-failure
 test.c
 --cover location --cover-failed-assertions --pointer-check --malloc-may-fail --malloc-fail-null
-\[main.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:13,14\): SATISFIED
-\[main.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:11\): SATISFIED
-\[main.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,8,10\): SATISFIED
+\[main.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED
+\[main.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): SATISFIED
+\[main.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED
 \[main.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+This is checking that the if statement body can actually be covered with the new flag