From 7921d9b6768a585ac3c1a55bb0b87c26909fc66b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 16 May 2014 17:48:57 +0200
Subject: [PATCH] [csrv'14] benchmark2 (merge of sorted arrays)
---
.../e-acsl/tests/csrv14/benchmark1.solution.c | 2 +-
src/plugins/e-acsl/tests/csrv14/benchmark2.c | 85 ++++++++++++++
.../e-acsl/tests/csrv14/benchmark2.solution.c | 111 ++++++++++++++++++
3 files changed, 197 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/e-acsl/tests/csrv14/benchmark2.c
create mode 100644 src/plugins/e-acsl/tests/csrv14/benchmark2.solution.c
diff --git a/src/plugins/e-acsl/tests/csrv14/benchmark1.solution.c b/src/plugins/e-acsl/tests/csrv14/benchmark1.solution.c
index a4e838327cc..b838cc8a9f3 100644
--- a/src/plugins/e-acsl/tests/csrv14/benchmark1.solution.c
+++ b/src/plugins/e-acsl/tests/csrv14/benchmark1.solution.c
@@ -28,7 +28,7 @@
*/
int binary_search(int* a, int length, int key) {
int low = 0, high = length - 1;
- while (low<=high) {
+ while (low <= high) {
int mid = low + (high - low) / 2;
if (a[mid] == key) return mid;
if (a[mid] < key) { low = mid + 1; }
diff --git a/src/plugins/e-acsl/tests/csrv14/benchmark2.c b/src/plugins/e-acsl/tests/csrv14/benchmark2.c
new file mode 100644
index 00000000000..84cd132a9f0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/csrv14/benchmark2.c
@@ -0,0 +1,85 @@
+/* ************************************************************************** */
+/* instructions */
+/* ************************************************************************** */
+/*
+ check that each call to both functions [*_merge]:
+ o takes as argument:
+ - [l1] >= 0; and
+ - [l2] >= 0; and
+ - 2 sorted arrays [t1] and [t2] of length [l1] and [l2] respectively
+ o modifies [t3] such that:
+ - [t3] is a sorted array of length [l1+l2];
+ - each element of [t1] and [t3] belongs to [t3];
+ - each element of [t3] belongs to either [t1] or [t2];
+*/
+/* ************************************************************************** */
+
+void correct_merge(int t1[], int t2[], int t3[], int l1, int l2) {
+ int i = 0, j = 0, k = 0 ;
+
+ while (i < l1 && j < l2) {
+ if (t1[i] < t2[j]) {
+ t3[k] = t1[i];
+ i++;
+ } else {
+ t3[k] = t2[j];
+ j++;
+ }
+ k++;
+ }
+ while (i < l1) {
+ t3[k] = t1[i];
+ i++;
+ k++;
+ }
+ while (j < l2) {
+ t3[k] = t2[j];
+ j++;
+ k++;
+ }
+}
+
+void wrong_merge(int t1[], int t2[], int t3[], int l1, int l2) {
+ int i = 0, j = 0, k = 0 ;
+
+ while (i < l1 && j < l2) {
+ if (t1[i] < t2[j]) {
+ t3[k] = t1[i];
+ i++;
+ } else {
+ t3[k] = t2[j];
+ j++;
+ }
+ k++;
+ }
+ while (i < l1) {
+ t3[k] = t1[i];
+ i++;
+ // k++; // missing instruction
+ }
+ while (j < l2) {
+ t3[k] = t2[j];
+ j++;
+ k++;
+ }
+}
+
+#define LEN1 6000
+#define LEN2 4000
+
+int main(void) {
+ int t1[LEN1], t2[LEN2], t3[LEN1+LEN2], i;
+
+ for(i = 0; i < LEN1; i++)
+ t1[i] = 4 * i + 1;
+
+ for(i = 0; i < LEN2; i++)
+ t2[i] = 3 * i + 1;
+
+ correct_merge(t1, t2, t3, LEN1, LEN2);
+
+ // an error must be detected on the next function call
+ wrong_merge(t1, t2, t3, LEN1, LEN2);
+
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/csrv14/benchmark2.solution.c b/src/plugins/e-acsl/tests/csrv14/benchmark2.solution.c
new file mode 100644
index 00000000000..9fce75ec313
--- /dev/null
+++ b/src/plugins/e-acsl/tests/csrv14/benchmark2.solution.c
@@ -0,0 +1,111 @@
+/* ************************************************************************** */
+/* instructions */
+/* ************************************************************************** */
+/*
+ check that each call to both functions [*_merge]:
+ o takes as argument:
+ - [l1] >= 0; and
+ - [l2] >= 0; and
+ - 2 sorted arrays [t1] and [t2] of length [l1] and [l2] respectively
+ o modifies [t3] such that:
+ - [t3] is a sorted array of length [l1+l2];
+ - each element of [t1] and [t3] belongs to [t3];
+ - each element of [t3] belongs to either [t1] or [t2];
+*/
+/* ************************************************************************** */
+
+/*@ requires l1 >= 0;
+ @ requires l2 >= 0;
+ @ requires \forall integer i; 0 <= i < l1 - 1 ==> t1[i] <= t1[i+1];
+ @ requires \forall integer i; 0 <= i < l2 - 1 ==> t2[i] <= t2[i+1];
+ @ ensures \forall integer i; 0 <= i < l1 + l2 - 1 ==> t3[i] <= t3[i+1];
+ @ ensures \forall integer i; 0 <= i < l1 ==>
+ \exists integer j; 0 <= j < l1 + l2 && t1[i] == t3[j];
+ @ ensures \forall integer i; 0 <= i < l2 ==>
+ \exists integer j; 0 <= j < l1 + l2 && t2[i] == t3[j];
+ @ ensures \forall integer i; 0 <= i < l1 + l2 ==>
+ ((\exists integer j; 0 <= j < l1 && t3[i] == t1[j])
+ || \exists integer j; 0 <= j < l2 && t3[i] == t2[j]);
+ @ */
+void correct_merge(int t1[], int t2[], int t3[], int l1, int l2) {
+ int i = 0, j = 0, k = 0 ;
+
+ while (i < l1 && j < l2) {
+ if (t1[i] < t2[j]) {
+ t3[k] = t1[i];
+ i++;
+ } else {
+ t3[k] = t2[j];
+ j++;
+ }
+ k++;
+ }
+ while (i < l1) {
+ t3[k] = t1[i];
+ i++;
+ k++;
+ }
+ while (j < l2) {
+ t3[k] = t2[j];
+ j++;
+ k++;
+ }
+}
+
+/*@ requires l1 >= 0;
+ @ requires l2 >= 0;
+ @ requires \forall integer i; 0 <= i < l1 - 1 ==> t1[i] <= t1[i+1];
+ @ requires \forall integer i; 0 <= i < l2 - 1 ==> t2[i] <= t2[i+1];
+ @ ensures \forall integer i; 0 <= i < l1 + l2 - 1 ==> t3[i] <= t3[i+1];
+ @ ensures \forall integer i; 0 <= i < l1 ==>
+ \exists integer j; 0 <= j < l1 + l2 && t1[i] == t3[j];
+ @ ensures \forall integer i; 0 <= i < l2 ==>
+ \exists integer j; 0 <= j < l1 + l2 && t2[i] == t3[j];
+ @ ensures \forall integer i; 0 <= i < l1 + l2 ==>
+ ((\exists integer j; 0 <= j < l1 && t3[i] == t1[j])
+ || \exists integer j; 0 <= j < l2 && t3[i] == t2[j]);
+ @ */
+void wrong_merge(int t1[], int t2[], int t3[], int l1, int l2) {
+ int i = 0, j = 0, k = 0 ;
+
+ while (i < l1 && j < l2) {
+ if (t1[i] < t2[j]) {
+ t3[k] = t1[i];
+ i++;
+ } else {
+ t3[k] = t2[j];
+ j++;
+ }
+ k++;
+ }
+ while (i < l1) {
+ t3[k] = t1[i];
+ i++;
+ // k++; // missing instruction
+ }
+ while (j < l2) {
+ t3[k] = t2[j];
+ j++;
+ k++;
+ }
+}
+
+#define LEN1 6000
+#define LEN2 4000
+
+int main(void) {
+ int t1[LEN1], t2[LEN2], t3[LEN1+LEN2], i;
+
+ for(i = 0; i < LEN1; i++)
+ t1[i] = 4 * i + 1;
+
+ for(i = 0; i < LEN2; i++)
+ t2[i] = 3 * i + 1;
+
+ correct_merge(t1, t2, t3, LEN1, LEN2);
+
+ // an error must be detected on the next function call
+ wrong_merge(t1, t2, t3, LEN1, LEN2);
+
+ return 0;
+}
--
GitLab