From 0ab8d09d4cf1530bfb1e15cbd525413a931acb5f Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 24 Apr 2014 09:55:19 +0200
Subject: [PATCH] [E-ACSL] preparing CSRV'14

---
 src/plugins/e-acsl/gcc.sh                     |  2 +-
 src/plugins/e-acsl/tests/csrv14/benchmark1.c  | 45 +++++++++++++++
 .../e-acsl/tests/csrv14/benchmark1.solution.c | 57 +++++++++++++++++++
 3 files changed, 103 insertions(+), 1 deletion(-)
 create mode 100644 src/plugins/e-acsl/tests/csrv14/benchmark1.c
 create mode 100644 src/plugins/e-acsl/tests/csrv14/benchmark1.solution.c

diff --git a/src/plugins/e-acsl/gcc.sh b/src/plugins/e-acsl/gcc.sh
index 181990bf960..8184fbdd06a 100755
--- a/src/plugins/e-acsl/gcc.sh
+++ b/src/plugins/e-acsl/gcc.sh
@@ -7,4 +7,4 @@ echo compiling $1
 gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o $1.out $SHARE/e-acsl/e_acsl.c $SHARE/e-acsl/memory_model/e_acsl_bittree.c $SHARE/e-acsl/memory_model/e_acsl_mmodel.c $1 -lgmp
 
 echo executing $1
-./$1.out
+time ./$1.out
diff --git a/src/plugins/e-acsl/tests/csrv14/benchmark1.c b/src/plugins/e-acsl/tests/csrv14/benchmark1.c
new file mode 100644
index 00000000000..7cb7c28c00f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/csrv14/benchmark1.c
@@ -0,0 +1,45 @@
+/* ************************************************************************** */
+/* instructions */
+/* ************************************************************************** */
+/*
+   check that each call to [binary_search]:
+   o takes as argument:
+     - a [length] >= 0; and
+     - a fully-allocated and sorted array [a] of (at least) [length] elements
+   o returns:
+     - either an index [i] s.t. a[i] == key;
+     - or -1 if there is no such index
+*/
+/* ************************************************************************** */
+
+#define LEN 2000000
+
+int binary_search(int* a, int length, int key) {
+  int low = 0, high = length - 1;
+  while (low<=high) {
+    int mid = low + (high - low) / 2;
+    if (a[mid] == key) return mid;
+    if (a[mid] < key) { low = mid + 1; }
+    else { high = mid - 1; }
+  }
+  return -1;
+}
+
+int main(void) {
+  int t[LEN];
+  int res, i;
+
+  for(i = 0; i < LEN; i++)
+    t[i] = 2 * i + 1;
+  res = binary_search(t, LEN, 10101);
+  if (res != 5050) return 1;
+  res = binary_search(t, LEN, 10100);
+  if (res != -1) return 2;
+
+  t[LEN / 4] = t[0];
+  // an error must be detected on the next function call
+  res = binary_search(t, LEN, 101);
+  if (res != -1) return 3;
+
+  return 0;
+}
diff --git a/src/plugins/e-acsl/tests/csrv14/benchmark1.solution.c b/src/plugins/e-acsl/tests/csrv14/benchmark1.solution.c
new file mode 100644
index 00000000000..a4e838327cc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/csrv14/benchmark1.solution.c
@@ -0,0 +1,57 @@
+/* ************************************************************************** */
+/* instructions */
+/* ************************************************************************** */
+/*
+   check that each call to [binary_search]:
+   o takes as argument:
+     - a [length] >= 0; and
+     - a fully-allocated and sorted array [a] of (at least) [length] elements
+   o returns:
+     - either an index [i] s.t. a[i] == key;
+     - or -1 if there is no such index
+*/
+/* ************************************************************************** */
+
+#define LEN 2000000
+
+/*@ requires \valid(a+(0..length-1));
+    requires \forall integer i; 0 <= i < length - 1 ==> a[i] <= a[i+1];
+    requires length >=0;
+
+    behavior exists:
+      assumes \exists integer i; 0 <= i < length && a[i] == key;
+      ensures 0 <= \result < length && a[\result] == key;
+
+    behavior not_exists:
+      assumes \forall integer i; 0 <= i < length ==> a[i] != key;
+      ensures \result == -1;
+*/
+int binary_search(int* a, int length, int key) {
+  int low = 0, high = length - 1;
+  while (low<=high) {
+    int mid = low + (high - low) / 2;
+    if (a[mid] == key) return mid;
+    if (a[mid] < key) { low = mid + 1; }
+    else { high = mid - 1; }
+  }
+  return -1;
+}
+
+int main(void) {
+  int t[LEN];
+  int res, i;
+
+  for(i = 0; i < LEN; i++)
+    t[i] = 2 * i + 1;
+  res = binary_search(t, LEN, 10101);
+  if (res != 5050) return 1;
+  res = binary_search(t, LEN, 10100);
+  if (res != -1) return 2;
+
+  t[LEN / 4] = t[0];
+  // an error must be detected on the next function call
+  res = binary_search(t, LEN, 101);
+  if (res != -1) return 3;
+
+  return 0;
+}
-- 
GitLab