diff --git a/regression/cbmc/Eval_Order1/main.c b/regression/cbmc/Eval_Order1/main.c new file mode 100644 index 0000000000..c52ab5ba3b --- /dev/null +++ b/regression/cbmc/Eval_Order1/main.c @@ -0,0 +1,7 @@ +int main() { + int x = 0; + x = ++x + x; + // depending on the order of evaluation, the following may fail + assert(x == 1); + return 0; +} diff --git a/regression/cbmc/Eval_Order1/test.desc b/regression/cbmc/Eval_Order1/test.desc new file mode 100644 index 0000000000..aea17ee4da --- /dev/null +++ b/regression/cbmc/Eval_Order1/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Eval_Order2/main.c b/regression/cbmc/Eval_Order2/main.c new file mode 100644 index 0000000000..a5df5c6fc3 --- /dev/null +++ b/regression/cbmc/Eval_Order2/main.c @@ -0,0 +1,7 @@ +int main() { + int x = 0; + x = ++x + x; + // depending on the order of evaluation, the following may fail + assert(x == 2); + return 0; +} diff --git a/regression/cbmc/Eval_Order2/test.desc b/regression/cbmc/Eval_Order2/test.desc new file mode 100644 index 0000000000..aea17ee4da --- /dev/null +++ b/regression/cbmc/Eval_Order2/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Malloc12/main.c b/regression/cbmc/Malloc12/main.c new file mode 100644 index 0000000000..86337c280b --- /dev/null +++ b/regression/cbmc/Malloc12/main.c @@ -0,0 +1,10 @@ +void * malloc(unsigned); + +// if the implementation of malloc is sound, this one should fail + +int main() { + char * a; + a = malloc(5); + assert(a != 0); + return 0; +} diff --git a/regression/cbmc/Malloc12/test.desc b/regression/cbmc/Malloc12/test.desc new file mode 100644 index 0000000000..7cb31bd31f --- /dev/null +++ b/regression/cbmc/Malloc12/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--pointer-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/Malloc13/main.c b/regression/cbmc/Malloc13/main.c new file mode 100644 index 0000000000..5de5f2f9c7 --- /dev/null +++ b/regression/cbmc/Malloc13/main.c @@ -0,0 +1,11 @@ +void * malloc(unsigned); + +int main(int argc, char* argv[]) { + unsigned short len; + char * str; + __CPROVER_assume(len > 0); + str = malloc(len); + assert(__CPROVER_buffer_size(str) == len); + return 0; +} + diff --git a/regression/cbmc/Malloc13/test.desc b/regression/cbmc/Malloc13/test.desc new file mode 100644 index 0000000000..24c71045fd --- /dev/null +++ b/regression/cbmc/Malloc13/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--string-abstraction +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Malloc14/main.c b/regression/cbmc/Malloc14/main.c new file mode 100644 index 0000000000..16099d7d83 --- /dev/null +++ b/regression/cbmc/Malloc14/main.c @@ -0,0 +1,12 @@ +void *malloc(int); + +int main() +{ + int *p = malloc(sizeof(int)); + if(p != (int*)0) + { + int *q = malloc(sizeof(int)); + __CPROVER_assert (p != q, "same memory allocated twice"); + } + return 0; +} diff --git a/regression/cbmc/Malloc14/test.desc b/regression/cbmc/Malloc14/test.desc new file mode 100644 index 0000000000..9c96469df1 --- /dev/null +++ b/regression/cbmc/Malloc14/test.desc @@ -0,0 +1,7 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/cbmc/Malloc15/main.c b/regression/cbmc/Malloc15/main.c new file mode 100644 index 0000000000..a36e4b4705 --- /dev/null +++ b/regression/cbmc/Malloc15/main.c @@ -0,0 +1,15 @@ +void *malloc(int); + +int main() +{ + int *p; + + p = malloc(sizeof(int)); + unsigned int r = p; + if (r != 0) + *p = 1; + + if (p != 0) + __CPROVER_assert (*p == 1, "malloc"); + return 0; +} diff --git a/regression/cbmc/Malloc15/test.desc b/regression/cbmc/Malloc15/test.desc new file mode 100644 index 0000000000..f046159d04 --- /dev/null +++ b/regression/cbmc/Malloc15/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--32 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/cbmc/Malloc16/main.c b/regression/cbmc/Malloc16/main.c new file mode 100644 index 0000000000..6679a279ab --- /dev/null +++ b/regression/cbmc/Malloc16/main.c @@ -0,0 +1,25 @@ +void *malloc(int); + +int foo(int *x) +{ + *x = 1; +} + +int main() +{ + void *tmp; + int *dev; + + tmp = malloc(sizeof(int)); + dev = (int*)tmp; + + void *r = (void*)0; + unsigned int q = r; + unsigned int p = dev; + if(p != q) + { + foo(dev); + __CPROVER_assert(*dev==1, "WTF?"); + } + return 0; +} diff --git a/regression/cbmc/Malloc16/test.desc b/regression/cbmc/Malloc16/test.desc new file mode 100644 index 0000000000..f046159d04 --- /dev/null +++ b/regression/cbmc/Malloc16/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--32 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/cbmc/Memmove1/main.c b/regression/cbmc/Memmove1/main.c new file mode 100644 index 0000000000..102ba1c45d --- /dev/null +++ b/regression/cbmc/Memmove1/main.c @@ -0,0 +1,45 @@ +#include +#include + +void sort_items_by_criteria( int * item, int left, int right ) +{ + int lidx = left, ridx = (left+right)/2 + 1, lsize = (left+right)/2 - left + 1; + int tmp; + + if ( right - left < 1 ) return; + sort_items_by_criteria( item, left, (left+right)/2 ); + sort_items_by_criteria( item, (left+right)/2 + 1, right ); + + while ( ridx <= right && lidx < ridx ) { + if ( item[lidx] > item[ridx] ) { + tmp = item[ridx]; + memmove( item + lidx + 1, item + lidx, lsize * sizeof(int) ); + item[lidx] = tmp; + ++ridx; + ++lsize; + } + ++lidx; + --lsize; + } +} + +int main(int argc, char * argv[]) { + int a[7]; + + //CBMC reports wrong results for 256, -2147221455, -2147221455, -2147221455, 16, -2147483600, 16384 + a[0] = 256; + a[1] = -2147221455; + a[2] = -2147221455; + a[3] = -2147221455; + a[4] = 16; + a[5] = -2147483600; + a[6] = 16384; + + sort_items_by_criteria(a, 0, 6); + + printf("%d %d %d %d %d %d %d\n", a[0], a[1], a[2], a[3], a[4], a[5], a[6]); + + assert(a[0]==-2147483600); + return 0; +} + diff --git a/regression/cbmc/Memmove1/test.desc b/regression/cbmc/Memmove1/test.desc new file mode 100644 index 0000000000..c0092d0ee5 --- /dev/null +++ b/regression/cbmc/Memmove1/test.desc @@ -0,0 +1,8 @@ +THOROUGH +main.c +--unwind 17 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Pointer_Assume1/main.c b/regression/cbmc/Pointer_Assume1/main.c new file mode 100644 index 0000000000..edc9fe6187 --- /dev/null +++ b/regression/cbmc/Pointer_Assume1/main.c @@ -0,0 +1,8 @@ +int main() +{ + int * a; + int b=1; + __CPROVER_assume(a == &b); + assert(*a==1); + return 0; +} diff --git a/regression/cbmc/Pointer_Assume1/test.desc b/regression/cbmc/Pointer_Assume1/test.desc new file mode 100644 index 0000000000..a27d6e3414 --- /dev/null +++ b/regression/cbmc/Pointer_Assume1/test.desc @@ -0,0 +1,7 @@ +KNOWNBUG +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/cbmc/Unwinding_Assertions_Improved1/main.c b/regression/cbmc/Unwinding_Assertions_Improved1/main.c new file mode 100644 index 0000000000..e37c5830e2 --- /dev/null +++ b/regression/cbmc/Unwinding_Assertions_Improved1/main.c @@ -0,0 +1,14 @@ +int main() { + int a; + __CPROVER_assume(a >= 4); + while (a > 0) { + --a; + } + + // this one should be reported to fail, even with unwinding assertions turned + // on (first check all other claims, then unwinding assertions) + assert(a > 0); + // once the above is disabled, it should be possible to "prove" this one in + // that the unwinding assertion fails first + assert(a <= 0); +} diff --git a/regression/cbmc/Unwinding_Assertions_Improved1/test.desc b/regression/cbmc/Unwinding_Assertions_Improved1/test.desc new file mode 100644 index 0000000000..baaaf8dcc6 --- /dev/null +++ b/regression/cbmc/Unwinding_Assertions_Improved1/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--unwind 5 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Variadic1/main.c b/regression/cbmc/Variadic1/main.c new file mode 100644 index 0000000000..735907824f --- /dev/null +++ b/regression/cbmc/Variadic1/main.c @@ -0,0 +1,41 @@ +#include +#include + +// how to do it: +// once an ellipsis is seen in the called function, declare an array of +// appropriate size (sum of sizeofs+paddings) and pass the array to the called +// function +// function with ellipsis has ellipsis replaced by void* pointer +// use of va_list is turned into assignment of this pointer +// va_start is no-op, just like va_end +// va_arg returns casted memory at pointer and increments pointer afterwards by +// given size (+padding) + + int +add_em_up (int count,...) +{ + va_list ap; + int i, sum; + + va_start (ap, count); /* Initialize the argument list. */ + + sum = 0; + for (i = 0; i < count; i++) + sum += va_arg (ap, int); /* Get the next argument value. */ + + va_end (ap); /* Clean up. */ + return sum; +} + + int +main (void) +{ + /* This call prints 16. */ + assert(16 == add_em_up (3, 5, 5, 6)); + + /* This call prints 55. */ + assert(55 == add_em_up (10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)); + + return 0; +} + diff --git a/regression/cbmc/Variadic1/test.desc b/regression/cbmc/Variadic1/test.desc new file mode 100644 index 0000000000..aea17ee4da --- /dev/null +++ b/regression/cbmc/Variadic1/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Volatile1/main.c b/regression/cbmc/Volatile1/main.c new file mode 100644 index 0000000000..383e71c59d --- /dev/null +++ b/regression/cbmc/Volatile1/main.c @@ -0,0 +1,6 @@ +volatile int x; +int main() { + if (!x) + assert(!x); +} + diff --git a/regression/cbmc/Volatile1/test.desc b/regression/cbmc/Volatile1/test.desc new file mode 100644 index 0000000000..6b765c70f4 --- /dev/null +++ b/regression/cbmc/Volatile1/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cpp/sizeof3/main.cpp b/regression/cpp/sizeof3/main.cpp new file mode 100644 index 0000000000..27bbd5f40f --- /dev/null +++ b/regression/cpp/sizeof3/main.cpp @@ -0,0 +1,10 @@ +int iDebugRec [20] ; + +void bar() { + unsigned s; + s=sizeof(iDebugRec); + s=sizeof(iDebugRec[0]); + iDebugRec[0]=1; +} + + diff --git a/regression/cpp/sizeof3/test.desc b/regression/cpp/sizeof3/test.desc new file mode 100644 index 0000000000..7ed391809e --- /dev/null +++ b/regression/cpp/sizeof3/test.desc @@ -0,0 +1,7 @@ +CORE +main.cpp + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +--