Merge pull request #1372 from diffblue/preconditions

Preconditions

Author: peterschrammel

regression/cbmc-cover/branch3/test.desc

@@ -3,6 +3,7 @@ main.c
 --cover branch --unwind 6
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* .* of .* covered \(100.0%\)$
+^\*\* .* of .* covered \(.*\)$
 --
 ^warning: ignoring
+^\[main.coverage.*\] file main.c line .* function main block .* branch .*: FAILED$

regression/cbmc-cover/built-ins1/main.c

@@ -1,9 +1,11 @@
+#include <string.h>
+
 int main()
 {
   char a[10];
   __CPROVER_input("a[3]", a[3]);
 
-  int len = strlen(a);
+  int len=strlen(a);
 
   if(len==3)
   {
@@ -13,5 +15,6 @@ int main()
   {
     return -1;
   }
+
   return 1;
 }

regression/cbmc-cover/built-ins1/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 4 of 7 covered
+^\*\* 5 of 8 covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-

regression/cbmc-cover/built-ins3/main.c

@@ -5,6 +5,8 @@ int main()
   const char *s="test";
   int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
 
+  __CPROVER_input("return value puts", ret);
+
   if(ret<0)
   {
     return 1;

regression/cbmc-cover/built-ins3/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 4 of 4 covered
+^\*\* 5 of .* covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-

regression/cbmc-cover/built-ins4/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/built-ins5/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/built-ins6/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/built-ins7/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/inlining1/main.c

@@ -1,3 +1,5 @@
+// Discussion point: is the branch below one goal or two?
+
 inline void my_func(int x)
 {
   if(x)