From bcde99fbe99174a094f38fdda70ad69d65a423f4 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 30 Apr 2014 17:19:08 +0200 Subject: Fist commit (WIP) --- tests/sources/0600_bubble_sort.c | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 tests/sources/0600_bubble_sort.c (limited to 'tests/sources/0600_bubble_sort.c') diff --git a/tests/sources/0600_bubble_sort.c b/tests/sources/0600_bubble_sort.c new file mode 100644 index 0000000..5cad03d --- /dev/null +++ b/tests/sources/0600_bubble_sort.c @@ -0,0 +1,32 @@ +// Example from Cousot Habwachs POPL 1978 + +// Bubble sort, where array operations are abstracted away +// to get a non-deterministic scalar program + +// expected results: +// - with polyhedra, no assertion failure (proof of absence of array overflow) +// - with intervals, assertion failure + +int B,J,T; +int N = rand(0,100000); // array size + +B = N; +while (B >= 1) { + J = 1; + T = 0; + while (J <= B-1) { + + // array bound-check + assert(1 <= J && J <= N); + assert(1 <= (J+1) && (J+1) <= N); + + // the non-deterministic test models comparing TAB[J] and TAB[J+1] + if (rand(0,1)==0) { + // where, we would exchange TAB[J] and TAB[J+1]; + T = J; + } + + J = J + 1; + } + B = T; +} -- cgit v1.2.3