From 70882b718a7edeb32941636546a5a07788c4d1f9 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Mon, 8 Jan 2018 14:31:42 +0000 Subject: [PATCH] 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 --- .../sensitivity-function-call-array/main.c | 17 +++++++++-------- .../sensitivity-function-call-opaque/main.c | 9 +++++---- .../sensitivity-function-call-pointer/main.c | 11 ++++++----- .../sensitivity-function-call-primitive/main.c | 5 +++-- .../sensitivity-function-call-recursive/main.c | 9 +++++---- .../sensitivity-function-call-varargs/main.c | 5 +++-- 6 files changed, 31 insertions(+), 25 deletions(-) diff --git a/regression/goto-analyzer/sensitivity-function-call-array/main.c b/regression/goto-analyzer/sensitivity-function-call-array/main.c index 4137d35003a..a1bf575001c 100644 --- a/regression/goto-analyzer/sensitivity-function-call-array/main.c +++ b/regression/goto-analyzer/sensitivity-function-call-array/main.c @@ -1,4 +1,5 @@ #include +#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; diff --git a/regression/goto-analyzer/sensitivity-function-call-opaque/main.c b/regression/goto-analyzer/sensitivity-function-call-opaque/main.c index 7a370b56c4b..c038c456b99 100644 --- a/regression/goto-analyzer/sensitivity-function-call-opaque/main.c +++ b/regression/goto-analyzer/sensitivity-function-call-opaque/main.c @@ -1,4 +1,5 @@ #include +#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; } diff --git a/regression/goto-analyzer/sensitivity-function-call-pointer/main.c b/regression/goto-analyzer/sensitivity-function-call-pointer/main.c index 246e40b4100..92089f70367 100644 --- a/regression/goto-analyzer/sensitivity-function-call-pointer/main.c +++ b/regression/goto-analyzer/sensitivity-function-call-pointer/main.c @@ -1,4 +1,5 @@ #include +#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; } diff --git a/regression/goto-analyzer/sensitivity-function-call-primitive/main.c b/regression/goto-analyzer/sensitivity-function-call-primitive/main.c index c9afbfc927d..db8f0e85b41 100644 --- a/regression/goto-analyzer/sensitivity-function-call-primitive/main.c +++ b/regression/goto-analyzer/sensitivity-function-call-primitive/main.c @@ -1,8 +1,9 @@ #include +#define ASSERT(x) __CPROVER_assert((x), "assertion " #x) int bar(int other) { - assert(other==4); + ASSERT(other==4); return other + 1; } @@ -10,5 +11,5 @@ int main(int argc, char *argv[]) { int x=3; int y=bar(x+1); - assert(y==5); + ASSERT(y==5); } diff --git a/regression/goto-analyzer/sensitivity-function-call-recursive/main.c b/regression/goto-analyzer/sensitivity-function-call-recursive/main.c index b9e6daf3347..786887f060d 100644 --- a/regression/goto-analyzer/sensitivity-function-call-recursive/main.c +++ b/regression/goto-analyzer/sensitivity-function-call-recursive/main.c @@ -1,4 +1,5 @@ #include +#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); } diff --git a/regression/goto-analyzer/sensitivity-function-call-varargs/main.c b/regression/goto-analyzer/sensitivity-function-call-varargs/main.c index 1f35e93715f..b94d37a3ad8 100644 --- a/regression/goto-analyzer/sensitivity-function-call-varargs/main.c +++ b/regression/goto-analyzer/sensitivity-function-call-varargs/main.c @@ -1,5 +1,6 @@ #include #include +#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); }