Fix255

regression/cbmc-concurrency/deadlock1/main.c

@@ -19,4 +19,4 @@ void main() {
   pthread_join(tid2, NULL); 
   // deadlock in the threads; assertion should not be reachable
   assert(0);
-} 
+}

regression/cbmc-cover/location10/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int myfunc(int x, int y)
+{
+  int z = x + y;
+  return z;
+}
+
+int main(void)
+{
+  _Bool x=0, y;
+  if (x)
+    assert(myfunc(2,3)==5);
+  else
+    y=1;
+
+  if (y)
+    assert(myfunc(4,3)==7);
+  else 
+    assume(0);
+
+  assert(y==1);
+}

regression/cbmc-cover/location10/test.desc

@@ -0,0 +1,20 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 13 function main block 2: FAILED$
+^\[main.coverage.3\] file main.c line 13 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 15 function main block 5: SATISFIED$
+^\[main.coverage.5\] file main.c line 17 function main block 6: SATISFIED$
+^\[main.coverage.6\] file main.c line 18 function main block 7: SATISFIED$
+^\[main.coverage.7\] file main.c line 18 function main block 8: SATISFIED$
+^\[main.coverage.8\] file main.c line 20 function main block 10: FAILED$
+^\[main.coverage.9\] file main.c line 22 function main block 11: SATISFIED$
+^\[main.coverage.10\] file main.c line 23 function main block 12: SATISFIED$
+^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: SATISFIED$
+^\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: SATISFIED$
+^\*\* 9 of 12 covered (75.0%)
+--
+^warning: ignoring

regression/cbmc-cover/location11/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int myfunc(int x, int y)
+{
+  int z = x + y;
+  return z;
+}
+
+int main(void)
+{
+  _Bool x=0, y;
+  if (x)
+    assert(myfunc(2,3)==5);
+  else
+    y=1;
+
+  if (y)
+    y=0;
+  else 
+    __CPROVER_assume(0);
+
+  assert(y==1);
+}

regression/cbmc-cover/location11/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 13 function main block 2: FAILED$
+^\[main.coverage.3\] file main.c line 13 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 15 function main block 5: SATISFIED$
+^\[main.coverage.5\] file main.c line 17 function main block 6: SATISFIED$
+^\[main.coverage.6\] file main.c line 18 function main block 7: SATISFIED$
+^\[main.coverage.7\] file main.c line 20 function main block 8: FAILED$
+^\[main.coverage.8\] file main.c line 22 function main block 9: SATISFIED$
+^\[main.coverage.9\] file main.c line 23 function main block 10: SATISFIED$
+^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
+^\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: FAILED$
+^\*\* 6 of 11 covered (54.5%)
+--
+^warning: ignoring

regression/cbmc-cover/location12/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int foo (int iX, int iY)
+{
+  return iX + iY;
+  __CPROVER_assume(0);
+}
+
+int main(void)
+{
+  assert(foo(5,3)==8);
+}

regression/cbmc-cover/location12/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 11 function main block 2: SATISFIED$
+^\[main.coverage.3\] file main.c line 12 function main block 3: SATISFIED$
+^\[foo.coverage.1\] file main.c line 5 function foo block 1: SATISFIED$
+^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
+^\[foo.coverage.3\] file main.c line 7 function foo block 3: FAILED$
+^\[foo.coverage.4\] file main.c line 7 function foo block 4: SATISFIED$
+^\*\* 5 of 7 covered (71.4%)
+--
+^warning: ignoring

regression/cbmc-cover/location13/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int myfunc(int a, int b)
+{
+  return a+b;
+}
+
+int foo (int iX, int iY)
+{
+  return iX + iY;
+  assert(myfunc(iX,iY)==8);
+}
+
+int main(void)
+{
+  assert(foo(5,3)==8);
+}

regression/cbmc-cover/location13/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 16 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 16 function main block 2: SATISFIED$
+^\[main.coverage.3\] file main.c line 17 function main block 3: SATISFIED$
+^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
+^\[myfunc.coverage.2\] file main.c line 6 function myfunc block 2: FAILED$
+^\[foo.coverage.1\] file main.c line 10 function foo block 1: SATISFIED$
+^\[foo.coverage.2\] file main.c line 11 function foo block 2: FAILED$
+^\[foo.coverage.3\] file main.c line 11 function foo block 3: FAILED$
+^\[foo.coverage.4\] file main.c line 12 function foo block 4: FAILED$
+^\[foo.coverage.5\] file main.c line 12 function foo block 5: SATISFIED$
+^\*\* 5 of 10 covered (50.0%)
+--
+^warning: ignoring

regression/cbmc-cover/location14/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int foo (int iX, int iY)
+{
+  return iX + iY;
+}
+
+int main(void)
+{
+  int iN = 2 + 1;
+  if (iN == 4)
+    assert(foo(5,3)==8);
+}

regression/cbmc-cover/location14/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 10 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 12 function main block 2: FAILED$
+^\[main.coverage.3\] file main.c line 12 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
+^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
+^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
+^\*\* 2 of 6 covered (33.3%)
+--
+^warning: ignoring

regression/cbmc-cover/location15/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <math.h>
+
+int foo (int iX, int iY)
+{
+  return iX + iY;
+}
+
+int main(void)
+{
+  double dX = sqrt(2);
+  if (dX > 5)
+  {
+    __CPROVER_assume(0);
+    assert(foo(5,3)==1);
+  }    
+}

regression/cbmc-cover/location15/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 11 function main block 2: SATISFIED$
+^\[main.coverage.3\] file main.c line 14 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 15 function main block 4: FAILED$
+^\[main.coverage.5\] file main.c line 15 function main block 5: FAILED$
+^\[main.coverage.6\] file main.c line 16 function main block 6: FAILED$
+^\[main.coverage.7\] file main.c line 17 function main block 7: SATISFIED$
+^\[foo.coverage.1\] file main.c line 6 function foo block 1: FAILED$
+^\[foo.coverage.2\] file main.c line 7 function foo block 2: FAILED$
+^\*\* 3 of 9 covered (33.3%)
+--
+^warning: ignoring

regression/cbmc-cover/location16/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+int func(int a)
+{
+  int b = a*2;
+  return b;
+
+  if (b < 10)
+  {
+    b += 10;
+  }
+
+  assert(0);
+
+  return b;
+}
+
+int main(void)
+{
+  func(2);
+}

regression/cbmc-cover/location16/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 20 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 21 function main block 2: SATISFIED$
+^\[func.coverage.1\] file main.c line 5 function func block 1: SATISFIED$
+^\[func.coverage.2\] file main.c line 8 function func block 2: FAILED$
+^\[func.coverage.3\] file main.c line 10 function func block 3: FAILED$
+^\[func.coverage.4\] file main.c line 13 function func block 4: FAILED$
+^\[func.coverage.5\] file main.c line 13 function func block 5: FAILED$
+^\[func.coverage.6\] file main.c line 15 function func block 6: FAILED$
+^\[func.coverage.7\] file main.c line 16 function func block 7: SATISFIED$
+^\*\* 4 of 9 covered (44.4%)
+--
+^warning: ignoring

regression/cbmc-cover/location2/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  int i, j;
+
+  i = 1;
+
+  if(j > 0)
+    j += i;
+  else
+    j = 0;
+
+  assert(i != j);
+}

regression/cbmc-cover/location2/main.json

@@ -0,0 +1,2 @@
+[ { "file": "main.c", "function": "main", "lines": [ {"number": 3}, {"number": 8}, {"number": 10}, {"number": 12} ] }
+]

regression/cbmc-cover/location2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--cover location --existing-coverage main.json
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 0 of 0 covered (100.0%)
+--
+^warning: ignoring

regression/cbmc-cover/location3/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  int i, j;
+
+  i = 1;
+
+  if(j > 0)
+    j += i;
+  else
+    j = 0;
+
+  assert(i != j);
+}

regression/cbmc-cover/location3/main.json

@@ -0,0 +1,2 @@
+[ { "file": "main.c", "function": "main", "lines": [ {"number": 3}, {"number": 8}, {"number": 12} ] }
+]

regression/cbmc-cover/location3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover location --existing-coverage main.json
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 10 function main block 3: SATISFIED$
+^\*\* 1 of 1 covered (100.0%)
+--
+^warning: ignoring

regression/cbmc-cover/location4/main.c

@@ -0,0 +1,41 @@
+#include <stdio.h>
+#include <assert.h>
+#include "single-linked-list.h"
+
+int main(void)
+{
+
+	int i;
+	mlist *mylist, *temp;
+
+	insert_list(mylist,2);
+	insert_list(mylist,5);
+	insert_list(mylist,1);
+	insert_list(mylist,3);
+
+	mylist = head;
+
+	printf("list all elements: ");
+	while(mylist)
+	{
+		printf("%d ", mylist->key);
+		mylist = mylist->next;
+	}
+	printf("\n");
+
+	temp = search_list(mylist,2);
+	printf("search for element 2: %s\n", temp->key == 2 ? "found" : "not found");
+	assert(temp->key == 2);
+
+	delete_list(temp);
+
+	mylist = head;
+
+	printf("list all elements except 2: ");
+	while(mylist)
+	{
+		printf("%d ", mylist->key);
+		mylist = mylist->next;
+	}
+	printf("\n");
+}

regression/cbmc-cover/location4/main.json

@@ -0,0 +1,7 @@
+[ { "file": "<builtin-library-free>", "function": "free", "lines": [ {"number": 22} ] },
+{ "file": "main.c", "function": "main", "lines": [ {"number": 8}, {"number": 12}, {"number": 13}, {"number": 14}, {"number": 16}, {"number": 19}, {"number": 21}, {"number": 24}, {"number": 26}, {"number": 30}, {"number": 32}, {"number": 35}, {"number": 37}, {"number": 40} ] },
+{"file": "single-linked-list.c", "function": "search_list", "lines": [ {"number": 9}, {"number": 10}, {"number": 15} ] },
+{"file": "single-linked-list.c", "function": "delete_list", "lines": [ {"number": 19}, {"number": 23}, {"number": 24}, {"number": 25}, {"number": 29}, {"number": 31}, {"number": 37}, {"number": 40}, {"number": 45}, {"number": 48} ] },
+{"file": "single-linked-list.c", "function": "insert_list", "lines": [ {"number": 37}, {"number": 40}, {"number": 45}, {"number": 48} ] }
+]
+