Add workaround for alpine regression test failure

CBMC doesn't handle assert on alpine-linux correctly.
This works around this issue by using __CPROVER_assert
directly in the tests that were previously failing.

This appears to be fixed already on the develop branch

Author: hannes-steffenhagen-diffblue

regression/goto-analyzer/sensitivity-function-call-array/main.c

@@ -1,4 +1,5 @@
 #include <assert.h>
+#define ASSERT(x) __CPROVER_assert((x), "assertion " #x)
 
 int *bar(int *arr_unmodified, int *arr_modified);
 
@@ -9,23 +10,23 @@ int main(int argc, char *argv[])
   int *p2arr = arr_x;
 
   p2arr = bar(arr_x, arr_y);
-  assert(*arr_y==2);
-  // assert(arr_y[1]==3);
+  ASSERT(*arr_y==2);
+  // ASSERT(arr_y[1]==3);
 
-  assert(p2arr==arr_y);
-  assert(*p2arr==2);
-  // assert(p2arr[1]==3);
+  ASSERT(p2arr==arr_y);
+  ASSERT(*p2arr==2);
+  // ASSERT(p2arr[1]==3);
 }
 
 int *bar(int *arr_unmodified, int *arr_modified)
 {
-  assert(*arr_unmodified==1);
-  // assert(arr_unmodified[1]==2);
+  ASSERT(*arr_unmodified==1);
+  // ASSERT(arr_unmodified[1]==2);
 
   (*arr_modified) += 1;
   // arr_modified[1] = 3;
 
-  assert(*arr_modified==2);
+  ASSERT(*arr_modified==2);
   // assert(arr_modified[1]==3);
 
   return arr_modified;

regression/goto-analyzer/sensitivity-function-call-opaque/main.c

@@ -1,4 +1,5 @@
 #include <assert.h>
+#define ASSERT(x) __CPROVER_assert((x), "assertion " #x)
 
 int global_value;
 
@@ -13,10 +14,10 @@ int main(int argc, char *argv[])
 
   int z=bar(x+1, &y);
 
-  assert(x==3); // Success
-  assert(y==4); // Unknown - the opaque function could have modified it
-  assert(z==0); // Unknown - the opaque function could have returned anything
-  assert(global_value==4); // Unknown - the opaque function could have modified this
+  ASSERT(x==3); // Success
+  ASSERT(y==4); // Unknown - the opaque function could have modified it
+  ASSERT(z==0); // Unknown - the opaque function could have returned anything
+  ASSERT(global_value==4); // Unknown - the opaque function could have modified this
 
   return 0;
 }

regression/goto-analyzer/sensitivity-function-call-pointer/main.c

@@ -1,4 +1,5 @@
 #include <assert.h>
+#define ASSERT(x) __CPROVER_assert((x), "assertion " #x)
 
 int *bar(int *unmodified, int *modifed);
 
@@ -8,18 +9,18 @@ int main(int argc, char *argv[])
   int y=4;
   int *p2x=&x;
   p2x = bar(&x, &y);
-  assert(y==5);
-  assert(p2x==&y);
-  assert(*p2x==5);
+  ASSERT(y==5);
+  ASSERT(p2x==&y);
+  ASSERT(*p2x==5);
 }
 
 int *bar(int *unmodified, int *modifed)
 {
-  assert(*unmodified==3);
+  ASSERT(*unmodified==3);
 
   (*modifed) += 1;
 
-  assert(*modifed==5);
+  ASSERT(*modifed==5);
 
   return modifed;
 }

regression/goto-analyzer/sensitivity-function-call-primitive/main.c

@@ -1,14 +1,15 @@
 #include <assert.h>
+#define ASSERT(x) __CPROVER_assert((x), "assertion " #x)
 
 int bar(int other)
 {
-  assert(other==4);
+  ASSERT(other==4);
   return other + 1;
 }
 
 int main(int argc, char *argv[])
 {
   int x=3;
   int y=bar(x+1);
-  assert(y==5);
+  ASSERT(y==5);
 }

regression/goto-analyzer/sensitivity-function-call-recursive/main.c

@@ -1,4 +1,5 @@
 #include <assert.h>
+#define ASSERT(x) __CPROVER_assert((x), "assertion " #x)
 
 int bar(int other)
 {
@@ -43,14 +44,14 @@ int main(int argc, char *argv[])
 {
   int x=3;
   int y=bar(x+1);
-  assert(y==4); // Unknown in the constants domain
+  ASSERT(y==4); // Unknown in the constants domain
 
   int y2 = bar(0);
-  assert(y2==0); // Unknown since we are not sensitive to call domain
+  ASSERT(y2==0); // Unknown since we are not sensitive to call domain
 
   int z = bar_clean(0);
-  assert(z==0); // Unknown as the function has parameter as top
+  ASSERT(z==0); // Unknown as the function has parameter as top
 
   int w = fun(5, 18);
-  assert(w==18);
+  ASSERT(w==18);
 }

regression/goto-analyzer/sensitivity-function-call-varargs/main.c

@@ -1,5 +1,6 @@
 #include <assert.h>
 #include <stdarg.h>
+#define ASSERT(x) __CPROVER_assert((x), "assertion " #x)
 
 int bar(int size, ...)
 {
@@ -19,8 +20,8 @@ int bar(int size, ...)
 int main(int argc, char *argv[])
 {
   int y=bar(4, 1, 2, 2, 1);
-  assert(y==6);
+  ASSERT(y==6);
 
   int z=bar(0);
-  assert(z==0);
+  ASSERT(z==0);
 }