From 7587f3c01e47072af996640c397655d4267d9774 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 20 May 2014 10:01:46 +0200
Subject: [PATCH] [csrv'14] improve benchmark 3
---
src/plugins/e-acsl/tests/csrv14/benchmark3.c | 61 +++++++-------
.../e-acsl/tests/csrv14/benchmark3.solution.c | 82 +++++++++----------
2 files changed, 70 insertions(+), 73 deletions(-)
diff --git a/src/plugins/e-acsl/tests/csrv14/benchmark3.c b/src/plugins/e-acsl/tests/csrv14/benchmark3.c
index c0280eef2cc..9ba866170c1 100644
--- a/src/plugins/e-acsl/tests/csrv14/benchmark3.c
+++ b/src/plugins/e-acsl/tests/csrv14/benchmark3.c
@@ -2,21 +2,13 @@
/* instructions */
/* ************************************************************************** */
/*
-
- Detect an out-of-bounds access to arr[LEN] due to the call from main()
- quicksort(arr, 0, LEN);
- instead of
- quicksort(arr, 0, LEN-1);
- Here this out-of-bounds access does not provoke a segmentation fault by chance
- since it happens to access another array. Moreover, this access may
- not provoke a sorting error by chance like in this example where the
- accessed element arr[LEN] is equal to the maximal element of the array arr.
-
+ Check that each call to the function [quicksort] is performed on an array
+ correctly allocated for each cell array[i], with left <= i <= right.
*/
/* ************************************************************************** */
-#include<stdio.h>
-#define LEN 2048
+//#include<stdio.h>
+#define LEN 10000
void swap(int* array, int i, int j) {
int tmp = array[i];
@@ -46,28 +38,41 @@ void quicksort(int* array, int left, int right) {
}
}
-int main(void) {
+void init(int* arr1, int* arr2) {
int i;
- int arr[LEN]; // array to be sorted
- int arr_max[LEN]; // array of maximal elements
-// filling arrays
- arr[0] = 0;
- arr_max[0] = 9;
+ // filling arrays
+ arr1[0] = 0;
+ arr2[0] = 9;
for(i = 1; i < LEN; i++){
- arr[i] = (13 * arr[i-1] + i) % 10;
- arr_max[i] = 9;
+ arr1[i] = (13 * arr1[i-1] + i) % 10;
+ arr2[i] = 9;
}
+}
+
+int main(void) {
+ int i;
+ int arr[LEN]; // array to be sorted
+ int arr_max[LEN]; // array of maximal elements
- printf("\n Array before quicksort:\n");
- for (i=0; i < LEN; i++)
- printf("%d, ",arr[i]);
-
- quicksort(arr, 0, LEN); // error ! must be: quicksort(arr, 0, LEN-1);
+ init(arr, arr_max);
+
+ /* printf("\n Array before quicksort:\n"); */
+ /* for (i=0; i < LEN; i++) */
+ /* printf("%d, ",arr[i]); */
+
+ quicksort(arr, 0, LEN-1);
- printf("\n Array after quicksort:\n");
- for (i=0; i < LEN; i++)
- printf("%d, ",arr[i]);
+ /* printf("\n Array after quicksort:\n"); */
+ /* for (i=0; i < LEN; i++) */
+ /* printf("%d, ",arr[i]); */
+
+ init(arr, arr_max);
+
+ /* error to be detected on the next function call.
+ Should be: quicksort(arr, 0, LEN-1)
+ to prevent an out-of-bound access to arr[LEN] */
+ quicksort(arr, 0, LEN);
return 0;
}
diff --git a/src/plugins/e-acsl/tests/csrv14/benchmark3.solution.c b/src/plugins/e-acsl/tests/csrv14/benchmark3.solution.c
index 22c0559c035..67667f2bd03 100644
--- a/src/plugins/e-acsl/tests/csrv14/benchmark3.solution.c
+++ b/src/plugins/e-acsl/tests/csrv14/benchmark3.solution.c
@@ -2,44 +2,26 @@
/* instructions */
/* ************************************************************************** */
/*
-
- Detect an out-of-bounds access to arr[LEN] due to the call from main()
- quicksort(arr, 0, LEN);
- instead of
- quicksort(arr, 0, LEN-1);
- Here this out-of-bounds access does not provoke a segmentation fault by chance
- since it happens to access another array. Moreover, this access may
- not provoke a sorting error by chance like in this example where the
- accessed element arr[LEN] is equal to the maximal element of the array arr.
-
+ Check that each call to the function [quicksort] is performed on an array
+ correctly allocated for each cell array[i], with left <= i <= right.
*/
/* ************************************************************************** */
-#include<stdio.h>
-#define LEN 2048
+//#include<stdio.h>
+#define LEN 10000
-/*@ requires \valid(array+i);
- @ requires \valid(array+j);
- @ assigns array[i], array[j];
- @ ensures array[i] == \old(array[j]);
- @ ensures array[j] == \old(array[i]);
- @*/
+/* /\*@ requires \valid(array+i); */
+/* @ requires \valid(array+j); *\/ */
void swap(int* array, int i, int j) {
int tmp = array[i];
array[i] = array[j];
array[j] = tmp;
}
-/*@ requires \forall integer j; left <= j <= right ==> \valid(array+j);
- @ assigns array[left..right];
- @*/
+///*@ requires \forall integer j; left <= j <= right ==> \valid(array+j); */
int partition (int* array, int left, int right, int pivotIndex) {
int pivotValue = array[pivotIndex], storeIndex = left, i;
swap(array, pivotIndex, right);
- /*@ loop invariant left <= i <= right;
- @ loop assigns i, storeIndex, array[left..right];
- @ loop variant right-i;
- @*/
for(i = left; i < right; i++) {
if(array[i] <= pivotValue) {
swap(array, i, storeIndex);
@@ -50,10 +32,7 @@ int partition (int* array, int left, int right, int pivotIndex) {
return storeIndex;
}
-/*@ 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];
- @*/
+/*@ requires \forall integer j; left <= j <= right ==> \valid(array+j); */
void quicksort(int* array, int left, int right) {
if(left < right) {
int pivotIndex = (left+right)/2;
@@ -63,28 +42,41 @@ void quicksort(int* array, int left, int right) {
}
}
-int main(void) {
+void init(int* arr1, int* arr2) {
int i;
- int arr[LEN]; // array to be sorted
- int arr_max[LEN]; // array of maximal elements
-// filling arrays
- arr[0] = 0;
- arr_max[0] = 9;
+ // filling arrays
+ arr1[0] = 0;
+ arr2[0] = 9;
for(i = 1; i < LEN; i++){
- arr[i] = (13 * arr[i-1] + i) % 10;
- arr_max[i] = 9;
+ arr1[i] = (13 * arr1[i-1] + i) % 10;
+ arr2[i] = 9;
}
+}
+
+int main(void) {
+ int i;
+ int arr[LEN]; // array to be sorted
+ int arr_max[LEN]; // array of maximal elements
- printf("\n Array before quicksort:\n");
- for (i=0; i < LEN; i++)
- printf("%d, ",arr[i]);
-
- quicksort(arr, 0, LEN); // error ! must be: quicksort(arr, 0, LEN-1);
+ init(arr, arr_max);
+
+ /* printf("\n Array before quicksort:\n"); */
+ /* for (i=0; i < LEN; i++) */
+ /* printf("%d, ",arr[i]); */
+
+ quicksort(arr, 0, LEN-1);
- printf("\n Array after quicksort:\n");
- for (i=0; i < LEN; i++)
- printf("%d, ",arr[i]);
+ /* printf("\n Array after quicksort:\n"); */
+ /* for (i=0; i < LEN; i++) */
+ /* printf("%d, ",arr[i]); */
+
+ init(arr, arr_max);
+
+ /* error to be detected on the next function call.
+ Should be: quicksort(arr, 0, LEN-1)
+ to prevent an out-of-bound access to arr[LEN] */
+ quicksort(arr, 0, LEN);
return 0;
}
--
GitLab