From 8f7a277acc38af76272afc83613bcd32b64d6630 Mon Sep 17 00:00:00 2001
From: Nikolai Kosmatov <Nikolai.Kosmatov@cea.fr>
Date: Mon, 19 May 2014 20:48:47 +0200
Subject: [PATCH] benchmark3 tentative (quicksort)
---
src/plugins/e-acsl/tests/csrv14/benchmark3.c | 10 +++-------
1 file changed, 3 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/tests/csrv14/benchmark3.c b/src/plugins/e-acsl/tests/csrv14/benchmark3.c
index 72f84cdce91..183b16212e8 100644
--- a/src/plugins/e-acsl/tests/csrv14/benchmark3.c
+++ b/src/plugins/e-acsl/tests/csrv14/benchmark3.c
@@ -13,7 +13,7 @@ void swap(int* array, int i, int j) {
array[j] = tmp;
}
-/*@ requires \valid(array+(left..right));
+/*@ requires \forall integer j; left <= j <= right ==> \valid(array+j);
@ assigns array[left..right];
@*/
int partition (int* array, int left, int right, int pivotIndex) {
@@ -33,7 +33,7 @@ int partition (int* array, int left, int right, int pivotIndex) {
return storeIndex;
}
-/*@ requires \valid(array+(left..right));
+/*@ requires \forall integer j; left <= j <= right ==> \valid(array+j);
@ assigns array[left..right];
@ ensures \forall int i; left <= i < right ==> array[i] <= array[i+1];
@*/
@@ -48,20 +48,16 @@ void quicksort(int* array, int left, int right) {
int main(void) {
int i;
- int arr_min[LEN]; // array of minimal elements
int arr[LEN]; // array to be sorted
int arr_max[LEN]; // array of maximal elements
arr[0] = 0;
- arr_min[0] = 0;
arr_max[0] = 9;
for(i = 1; i < LEN; i++){
arr[i] = (13 * arr[i-1] + i) % 10;
- arr_min[i] = 0;
arr_max[i] = 9;
}
-
-
+
printf("\n Array before quicksort:\n");
for (i=0; i < LEN; i++)
printf("%d, ",arr[i]);
--
GitLab