benchmark3 and solution (quicksort)

src/plugins/e-acsl/tests/csrv14/benchmark3.c

+/* ************************************************************************** */
+/* 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.
+
+*/
+/* ************************************************************************** */
+
 #include<stdio.h>
 #define LEN 2048 
 
-/*@ 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]);
-  @*/
 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];
-  @*/
 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);
@@ -33,10 +37,6 @@ 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];
-  @*/
 void quicksort(int* array, int left, int right) {
   if(left < right) {
     int pivotIndex = (left+right)/2;
@@ -51,6 +51,7 @@ int main(void) {
   int arr[LEN];     // array to be sorted
   int arr_max[LEN]; // array of maximal elements
 
+// filling arrays
   arr[0] = 0; 
   arr_max[0] = 9;
   for(i = 1; i < LEN; i++){

src/plugins/e-acsl/tests/csrv14/benchmark3.solution.c

+/* ************************************************************************** */
+/* 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.
+
+*/
+/* ************************************************************************** */
+
+#include<stdio.h>
+#define LEN 2048 
+
+/*@ 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]);
+  @*/
+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];
+  @*/
+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);
+      storeIndex++;
+    }
+  }
+  swap(array, storeIndex, right);
+  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];
+  @*/
+void quicksort(int* array, int left, int right) {
+  if(left < right) {
+    int pivotIndex = (left+right)/2;
+    int pivotNewIndex = partition(array, left, right, pivotIndex);
+    quicksort(array, left, pivotNewIndex-1);
+    quicksort(array, pivotNewIndex+1, right);
+  }
+}
+
+int main(void) {
+  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;
+  for(i = 1; i < LEN; i++){
+    arr[i] = (13 * arr[i-1] + i) % 10; 
+    arr_max[i] = 9;
+  }
+    
+  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); 
+  
+  printf("\n Array after quicksort:\n");
+  for (i=0; i < LEN; i++) 
+    printf("%d, ",arr[i]);
+
+  return 0;
+}