Regression tests for not instrumenting built-ins

Author: peterschrammel

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

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

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

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

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

@@ -0,0 +1,19 @@
+struct mystruct {
+  int x;
+  char y;
+};
+
+int main()
+{
+  struct mystruct s;
+  char c;
+  __CPROVER_input("c", c);
+
+  memset(&s,c,sizeof(struct mystruct));
+
+  if(s.y=='A')
+  {
+    return 0;
+  }
+  return 1;
+}

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

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

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

@@ -0,0 +1,14 @@
+#include <stdio.h>
+
+int main()
+{
+  const char *s="test";
+  int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
+
+  if(ret<0)
+  {
+    return 1;
+  }
+
+  return 0;
+}

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

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

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

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover branch --unwind 5
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 5 of 5 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

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

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

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

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

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

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

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

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

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

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

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

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