[csrv'14] improve benchmark 3

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;
 }

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;
 }