From d97c6f2f870da7d3d6ce6ebbc129842a82536a4f Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 8 Feb 2016 11:11:49 +0100
Subject: [PATCH] [tests] moving GMP-specific test files
---
.../e-acsl-runtime/oracle/array.0.res.oracle | 21 --
.../e-acsl-runtime/oracle/at.0.res.oracle | 34 ---
.../oracle/comparison.0.res.oracle | 14 --
.../e-acsl-runtime/oracle/gen_linear_search.c | 215 ++++++++++++++++++
.../oracle/quantif.0.res.oracle | 30 ---
.../tests/{e-acsl-runtime => gmp}/arith.i | 2 +-
.../tests/{e-acsl-runtime => gmp}/array.i | 2 +-
.../e-acsl/tests/{e-acsl-runtime => gmp}/at.i | 2 +-
.../tests/{e-acsl-runtime => gmp}/cast.i | 2 +-
.../{e-acsl-runtime => gmp}/comparison.i | 2 +-
.../integer_constant.i | 2 +-
.../tests/{e-acsl-runtime => gmp}/longlong.i | 2 +-
.../tests/{e-acsl-runtime => gmp}/not.i | 2 +-
.../oracle/arith.0.err.oracle | 0
.../tests/gmp/oracle/arith.0.res.oracle | 33 +++
.../oracle/arith.1.err.oracle | 0
.../oracle/arith.1.res.oracle | 0
.../oracle/array.0.err.oracle | 0
.../oracle/array.0.res.oracle} | 2 +
.../oracle/array.1.err.oracle | 0
.../oracle/array.1.res.oracle | 4 -
.../oracle/at.0.err.oracle | 0
.../e-acsl/tests/gmp/oracle/at.0.res.oracle | 43 ++++
.../oracle/at.1.err.oracle | 0
.../oracle/at.1.res.oracle | 0
.../oracle/cast.0.err.oracle | 0
.../oracle/cast.0.res.oracle | 0
.../oracle/cast.1.err.oracle | 0
.../oracle/cast.1.res.oracle | 0
.../oracle/comparison.0.err.oracle | 0
.../tests/gmp/oracle/comparison.0.res.oracle | 32 +++
.../oracle/comparison.1.err.oracle | 0
.../oracle/comparison.1.res.oracle | 0
.../oracle/gen_arith.c | 0
.../oracle/gen_arith2.c | 0
.../oracle/gen_array.c | 0
.../oracle/gen_array2.c | 0
.../{e-acsl-runtime => gmp}/oracle/gen_at.c | 0
.../{e-acsl-runtime => gmp}/oracle/gen_at2.c | 0
.../{e-acsl-runtime => gmp}/oracle/gen_cast.c | 0
.../oracle/gen_cast2.c | 0
.../oracle/gen_comparison.c | 0
.../oracle/gen_comparison2.c | 0
.../oracle/gen_integer_constant.c | 0
.../oracle/gen_integer_constant2.c | 0
.../oracle/gen_longlong.c | 0
.../oracle/gen_longlong2.c | 0
.../{e-acsl-runtime => gmp}/oracle/gen_not.c | 0
.../{e-acsl-runtime => gmp}/oracle/gen_not2.c | 0
.../oracle/gen_quantif.c | 0
.../oracle/gen_quantif2.c | 0
.../oracle/integer_constant.0.err.oracle | 0
.../oracle/integer_constant.0.res.oracle | 0
.../oracle/integer_constant.1.err.oracle | 0
.../oracle/integer_constant.1.res.oracle | 0
.../oracle/longlong.0.err.oracle | 0
.../oracle/longlong.0.res.oracle | 4 +-
.../oracle/longlong.1.err.oracle | 0
.../oracle/longlong.1.res.oracle | 4 +-
.../oracle/not.0.err.oracle | 0
.../oracle/not.0.res.oracle | 0
.../oracle/not.1.err.oracle | 0
.../oracle/not.1.res.oracle | 0
.../oracle/quantif.0.err.oracle | 0
.../tests/gmp/oracle/quantif.0.res.oracle | 31 +++
.../oracle/quantif.1.err.oracle | 0
.../oracle/quantif.1.res.oracle | 1 -
.../tests/{e-acsl-runtime => gmp}/quantif.i | 2 +-
68 files changed, 369 insertions(+), 117 deletions(-)
delete mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/arith.i (82%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/array.i (64%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/at.i (84%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/cast.i (73%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/comparison.i (77%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/integer_constant.i (64%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/longlong.i (70%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/not.i (54%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/arith.0.err.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/arith.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/arith.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/array.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime/oracle/arith.0.res.oracle => gmp/oracle/array.0.res.oracle} (93%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/array.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/array.1.res.oracle (73%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/at.0.err.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/at.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/at.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/cast.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/cast.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/cast.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/cast.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/comparison.0.err.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/comparison.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/comparison.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_arith.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_arith2.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_array.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_array2.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_at.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_at2.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_cast.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_cast2.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_comparison.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_comparison2.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_integer_constant.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_integer_constant2.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_longlong.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_longlong2.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_not.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_not2.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_quantif.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/gen_quantif2.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/integer_constant.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/integer_constant.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/integer_constant.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/integer_constant.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/longlong.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/longlong.0.res.oracle (90%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/longlong.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/longlong.1.res.oracle (90%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/not.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/not.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/not.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/not.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/quantif.0.err.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/quantif.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/oracle/quantif.1.res.oracle (96%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => gmp}/quantif.i (80%)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle
deleted file mode 100644
index 8f4a3d3b726..00000000000
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle
+++ /dev/null
@@ -1,21 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
- T1[0..2] ∈ {0}
- T2[0..3] ∈ {0}
-tests/e-acsl-runtime/array.i:12:[value] entering loop for the first time
-tests/e-acsl-runtime/array.i:13:[value] entering loop for the first time
-tests/e-acsl-runtime/array.i:15:[value] warning: assertion got status unknown.
-[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/array.i:16:[value] warning: assertion got status unknown.
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle
deleted file mode 100644
index 2f339588463..00000000000
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle
+++ /dev/null
@@ -1,34 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
- A ∈ {0}
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __delete_block
-[value] using specification for function e_acsl_assert
-tests/e-acsl-runtime/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:14:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/at.i:53:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:53:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/at.i:54:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:54:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/at.i:55:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:55:[value] warning: assertion got status unknown.
-[value] using specification for function __initialize
-[value] using specification for function __valid_read
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/at.i:32:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:32:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/at.i:34:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:34:[value] warning: assertion got status unknown.
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle
deleted file mode 100644
index f0d9dbf6c71..00000000000
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function e_acsl_assert
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 9526b80c620..20295c7ae73 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -1,2 +1,217 @@
/* Generated by Frama-C */
+int A[10];
+/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i+1];
+
+ behavior exists:
+ assumes ∃ ℤ j; 0 ≤ j < 10 ∧ A[j] ≡ elt;
+ ensures \result ≡ 1;
+
+ behavior not_exists:
+ assumes ∀ ℤ j; 0 ≤ j < 10 ⇒ A[j] ≢ elt;
+ ensures \result ≡ 0;
+ */
+int search(int elt)
+{
+ int __retres;
+ int k;
+ k = 0;
+ {
+ int __e_acsl_forall;
+ int __e_acsl_i;
+ int __e_acsl_and;
+ __e_acsl_forall = 1;
+ __e_acsl_i = 0;
+ while (1) {
+ if (__e_acsl_i < k) ; else break;
+ e_acsl_assert(__e_acsl_i < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __e_acsl_i < 10",20);
+ e_acsl_assert(0 <= __e_acsl_i,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __e_acsl_i",20);
+ if (A[__e_acsl_i] < elt) ;
+ else {
+ __e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ __e_acsl_i ++;
+ }
+ e_acsl_end_loop1: ;
+ e_acsl_assert(__e_acsl_forall,(char *)"Invariant",(char *)"search",
+ (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",20);
+ if (0 <= k) __e_acsl_and = k <= 10; else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"Invariant",(char *)"search",
+ (char *)"0 <= k <= 10",19);
+ /*@ loop invariant 0 ≤ k ≤ 10;
+ loop invariant ∀ ℤ i; 0 ≤ i < k ⇒ A[i] < elt;
+ */
+ while (k < 10) {
+ if (A[k] == elt) {
+ __retres = 1;
+ goto return_label;
+ }
+ else
+ if (A[k] > elt) {
+ __retres = 0;
+ goto return_label;
+ }
+ {
+ int __e_acsl_and_2;
+ int __e_acsl_forall_2;
+ int __e_acsl_i_2;
+ k ++;
+ if (0 <= k) __e_acsl_and_2 = k <= 10; else __e_acsl_and_2 = 0;
+ e_acsl_assert(__e_acsl_and_2,(char *)"Invariant",(char *)"search",
+ (char *)"0 <= k <= 10",19);
+ __e_acsl_forall_2 = 1;
+ __e_acsl_i_2 = 0;
+ while (1) {
+ if (__e_acsl_i_2 < k) ; else break;
+ e_acsl_assert(__e_acsl_i_2 < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __e_acsl_i_2 < 10",20);
+ e_acsl_assert(0 <= __e_acsl_i_2,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __e_acsl_i_2",20);
+ if (A[__e_acsl_i_2] < elt) ;
+ else {
+ __e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop2;
+ }
+ __e_acsl_i_2 ++;
+ }
+ e_acsl_end_loop2: ;
+ e_acsl_assert(__e_acsl_forall_2,(char *)"Invariant",(char *)"search",
+ (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",
+ 20);
+ }
+ }
+ }
+ __retres = 0;
+ return_label: return __retres;
+}
+
+/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i+1];
+
+ behavior exists:
+ assumes ∃ ℤ j; 0 ≤ j < 10 ∧ A[j] ≡ elt;
+ ensures \result ≡ 1;
+
+ behavior not_exists:
+ assumes ∀ ℤ j; 0 ≤ j < 10 ⇒ A[j] ≢ elt;
+ ensures \result ≡ 0;
+ */
+int __e_acsl_search(int elt)
+{
+ int __e_acsl_at_2;
+ int __e_acsl_at;
+ int __retres;
+ {
+ int __e_acsl_forall;
+ int __e_acsl_i;
+ __e_acsl_forall = 1;
+ __e_acsl_i = 0;
+ while (1) {
+ if (__e_acsl_i < 9) ; else break;
+ e_acsl_assert(__e_acsl_i + 1 < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: (int)(__e_acsl_i+1) < 10",9);
+ e_acsl_assert(0 <= __e_acsl_i + 1,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= (int)(__e_acsl_i+1)",9);
+ e_acsl_assert(__e_acsl_i < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __e_acsl_i < 10",9);
+ e_acsl_assert(0 <= __e_acsl_i,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __e_acsl_i",9);
+ if (A[__e_acsl_i] <= A[__e_acsl_i + 1]) ;
+ else {
+ __e_acsl_forall = 0;
+ goto e_acsl_end_loop3;
+ }
+ __e_acsl_i ++;
+ }
+ e_acsl_end_loop3: ;
+ e_acsl_assert(__e_acsl_forall,(char *)"Precondition",(char *)"search",
+ (char *)"\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i+1]",
+ 9);
+ {
+ int __e_acsl_forall_2;
+ int __e_acsl_j_2;
+ __e_acsl_forall_2 = 1;
+ __e_acsl_j_2 = 0;
+ while (1) {
+ if (__e_acsl_j_2 < 10) ; else break;
+ e_acsl_assert(__e_acsl_j_2 < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __e_acsl_j_2 < 10",14);
+ e_acsl_assert(0 <= __e_acsl_j_2,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __e_acsl_j_2",14);
+ if (A[__e_acsl_j_2] != elt) ;
+ else {
+ __e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop5;
+ }
+ __e_acsl_j_2 ++;
+ }
+ e_acsl_end_loop5: ;
+ __e_acsl_at_2 = __e_acsl_forall_2;
+ }
+ {
+ int __e_acsl_exists;
+ int __e_acsl_j;
+ __e_acsl_exists = 0;
+ __e_acsl_j = 0;
+ while (1) {
+ if (__e_acsl_j < 10) ; else break;
+ e_acsl_assert(__e_acsl_j < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __e_acsl_j < 10",11);
+ e_acsl_assert(0 <= __e_acsl_j,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __e_acsl_j",11);
+ if (! (A[__e_acsl_j] == elt)) ;
+ else {
+ __e_acsl_exists = 1;
+ goto e_acsl_end_loop4;
+ }
+ __e_acsl_j ++;
+ }
+ e_acsl_end_loop4: ;
+ __e_acsl_at = __e_acsl_exists;
+ }
+ __retres = search(elt);
+ }
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) __e_acsl_implies = 1;
+ else __e_acsl_implies = __retres == 1;
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"search",
+ (char *)"\\old(\\exists integer j; 0 <= j < 10 && A[j] == elt) ==> \\result == 1",
+ 12);
+ if (! __e_acsl_at_2) __e_acsl_implies_2 = 1;
+ else __e_acsl_implies_2 = __retres == 0;
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"search",
+ (char *)"\\old(\\forall integer j; 0 <= j < 10 ==> A[j] != elt) ==> \\result == 0",
+ 15);
+ return __retres;
+ }
+}
+
+int main(void)
+{
+ int __retres;
+ int found;
+ {
+ int i;
+ i = 0;
+ while (i < 10) {
+ A[i] = i * i;
+ i ++;
+ }
+ }
+ found = __e_acsl_search(36);
+ /*@ assert found ≡ 1; */
+ e_acsl_assert(found == 1,(char *)"Assertion",(char *)"main",
+ (char *)"found == 1",33);
+ found = __e_acsl_search(5);
+ /*@ assert found ≡ 0; */
+ e_acsl_assert(found == 0,(char *)"Assertion",(char *)"main",
+ (char *)"found == 0",36);
+ __retres = 0;
+ return __retres;
+}
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle
deleted file mode 100644
index e0ebf45e128..00000000000
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle
+++ /dev/null
@@ -1,30 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-tests/e-acsl-runtime/quantif.i:11:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/quantif.i:11:[value] entering loop for the first time
-[value] using specification for function e_acsl_assert
-tests/e-acsl-runtime/quantif.i:12:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/quantif.i:12:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:13:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/quantif.i:13:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:14:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/quantif.i:14:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:18:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/quantif.i:18:[value] entering loop for the first time
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/quantif.i:23:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/quantif.i:23:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:27:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/quantif.i:27:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:28:[value] entering loop for the first time
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i b/src/plugins/e-acsl/tests/gmp/arith.i
similarity index 82%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
rename to src/plugins/e-acsl/tests/gmp/arith.i
index 91954d6142d..b58f25a24e5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
+++ b/src/plugins/e-acsl/tests/gmp/arith.i
@@ -2,7 +2,7 @@
COMMENT: arithmetic operations
COMMENT: add the last assertion when fixing BTS #751
COMMENT: no diff
- EXECNOW: LOG gen_arith2.c BIN gen_arith2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/arith.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith2.c > /dev/null && ./gcc_runtime.sh arith2
+ EXECNOW: LOG gen_arith2.c BIN gen_arith2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/gmp/arith.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/gmp/result/gen_arith2.c > /dev/null && ./gcc_runtime.sh arith2
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/array.i b/src/plugins/e-acsl/tests/gmp/array.i
similarity index 64%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/array.i
rename to src/plugins/e-acsl/tests/gmp/array.i
index 2bd785a6135..9474ac288c8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/array.i
+++ b/src/plugins/e-acsl/tests/gmp/array.i
@@ -2,7 +2,7 @@
COMMENT: arrays
STDOPT: #"-slevel 5"
COMMENT: no diff
- EXECNOW: LOG gen_array2.c BIN gen_array2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/array.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array2.c > /dev/null && ./gcc_runtime.sh array2
+ EXECNOW: LOG gen_array2.c BIN gen_array2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/gmp/array.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/gmp/result/gen_array2.c > /dev/null && ./gcc_runtime.sh array2
*/
int T1[3],T2[4];
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/at.i b/src/plugins/e-acsl/tests/gmp/at.i
similarity index 84%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/at.i
rename to src/plugins/e-acsl/tests/gmp/at.i
index 45d8548caec..1dade3f0c1d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
+++ b/src/plugins/e-acsl/tests/gmp/at.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: \at
COMMENT: no diff
- EXECNOW: LOG gen_at2.c BIN gen_at2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/at.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at2.c > /dev/null && ./gcc_runtime.sh at2 -Wno-unused-label
+ EXECNOW: LOG gen_at2.c BIN gen_at2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/gmp/at.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/gmp/result/gen_at2.c > /dev/null && ./gcc_runtime.sh at2 -Wno-unused-label
*/
int A = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i b/src/plugins/e-acsl/tests/gmp/cast.i
similarity index 73%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
rename to src/plugins/e-acsl/tests/gmp/cast.i
index 7e4c94d3a8a..485648bf9fb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
+++ b/src/plugins/e-acsl/tests/gmp/cast.i
@@ -2,7 +2,7 @@
COMMENT: cast
STDOPT: #"-no-warn-signed-downcast" #"-no-warn-unsigned-downcast"
COMMENT: no diff
- EXECNOW: LOG gen_cast2.c BIN gen_cast2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/cast.i -e-acsl-gmp-only -no-warn-signed-downcast -no-warn-unsigned-downcast -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast2.c > /dev/null && ./gcc_runtime.sh cast2
+ EXECNOW: LOG gen_cast2.c BIN gen_cast2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/gmp/cast.i -e-acsl-gmp-only -no-warn-signed-downcast -no-warn-unsigned-downcast -e-acsl -then-on e-acsl -print -ocode ./tests/gmp/result/gen_cast2.c > /dev/null && ./gcc_runtime.sh cast2
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i b/src/plugins/e-acsl/tests/gmp/comparison.i
similarity index 77%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
rename to src/plugins/e-acsl/tests/gmp/comparison.i
index 9ee270ac380..216a98c5224 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
+++ b/src/plugins/e-acsl/tests/gmp/comparison.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: comparison operators
COMMENT: no diff
- EXECNOW: LOG gen_comparison2.c BIN gen_comparison2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/comparison.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_comparison2.c > /dev/null && ./gcc_runtime.sh comparison2
+ EXECNOW: LOG gen_comparison2.c BIN gen_comparison2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/gmp/comparison.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/gmp/result/gen_comparison2.c > /dev/null && ./gcc_runtime.sh comparison2
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i b/src/plugins/e-acsl/tests/gmp/integer_constant.i
similarity index 64%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
rename to src/plugins/e-acsl/tests/gmp/integer_constant.i
index 08c82dcb45f..2b3c0715012 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
+++ b/src/plugins/e-acsl/tests/gmp/integer_constant.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: integer constant + a stmt after the assertion
COMMENT: no diff
- EXECNOW: LOG gen_integer_constant2.c BIN gen_integer_constant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant2.c > /dev/null && ./gcc_runtime.sh integer_constant2
+ EXECNOW: LOG gen_integer_constant2.c BIN gen_integer_constant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/gmp/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/gmp/result/gen_integer_constant2.c > /dev/null && ./gcc_runtime.sh integer_constant2
*/
int main(void) {
int x;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i b/src/plugins/e-acsl/tests/gmp/longlong.i
similarity index 70%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
rename to src/plugins/e-acsl/tests/gmp/longlong.i
index b1e87e04fbf..8bf4d0c1a95 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
+++ b/src/plugins/e-acsl/tests/gmp/longlong.i
@@ -2,7 +2,7 @@
COMMENT: upgrading longlong to GMP
STDOPT: +"-no-eva -val-ignore-recursive-calls"
COMMENT: no diff
- EXECNOW: LOG gen_longlong2.c BIN gen_longlong2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/longlong.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_longlong2.c > /dev/null && ./gcc_runtime.sh longlong2
+ EXECNOW: LOG gen_longlong2.c BIN gen_longlong2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/gmp/longlong.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/gmp/result/gen_longlong2.c > /dev/null && ./gcc_runtime.sh longlong2
*/
unsigned long long my_pow(unsigned int x, unsigned int n) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i b/src/plugins/e-acsl/tests/gmp/not.i
similarity index 54%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/not.i
rename to src/plugins/e-acsl/tests/gmp/not.i
index ceb89ce41c9..aaec6975f59 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
+++ b/src/plugins/e-acsl/tests/gmp/not.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: predicate [!p]
COMMENT: no diff
- EXECNOW: LOG gen_not2.c BIN gen_not2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/not.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_not2.c > /dev/null && ./gcc_runtime.sh not2
+ EXECNOW: LOG gen_not2.c BIN gen_not2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/gmp/not.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/gmp/result/gen_not2.c > /dev/null && ./gcc_runtime.sh not2
*/
int main(void) {
int x = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/arith.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
new file mode 100644
index 00000000000..570b475bf07
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
@@ -0,0 +1,33 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+tests/gmp/arith.i:12:[value] Assertion got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/gmp/arith.i:13:[value] Assertion got status valid.
+tests/gmp/arith.i:14:[value] Assertion got status valid.
+tests/gmp/arith.i:16:[value] Assertion got status valid.
+tests/gmp/arith.i:17:[value] Assertion got status valid.
+tests/gmp/arith.i:18:[value] Assertion got status valid.
+tests/gmp/arith.i:19:[value] Assertion got status valid.
+tests/gmp/arith.i:20:[value] Assertion got status valid.
+tests/gmp/arith.i:21:[value] Assertion got status valid.
+tests/gmp/arith.i:22:[value] Assertion got status valid.
+tests/gmp/arith.i:23:[value] Assertion got status valid.
+tests/gmp/arith.i:25:[value] Assertion got status valid.
+tests/gmp/arith.i:27:[value] Assertion got status valid.
+tests/gmp/arith.i:28:[value] Assertion got status valid.
+tests/gmp/arith.i:29:[value] Assertion got status valid.
+tests/gmp/arith.i:30:[value] Assertion got status valid.
+tests/gmp/arith.i:32:[value] Assertion got status valid.
+tests/gmp/arith.i:33:[value] Assertion got status valid.
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/arith.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/array.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
similarity index 93%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
index f0d9dbf6c71..6a3662a24f1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
@@ -10,5 +10,7 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
+ T1[0..2] ∈ {0}
+ T2[0..3] ∈ {0}
[value] using specification for function e_acsl_assert
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/array.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
similarity index 73%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
index eb2477f723c..84e54776a15 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
@@ -12,13 +12,9 @@
__memory_size ∈ [--..--]
T1[0..2] ∈ {0}
T2[0..3] ∈ {0}
-tests/e-acsl-runtime/array.i:12:[value] entering loop for the first time
-tests/e-acsl-runtime/array.i:13:[value] entering loop for the first time
-tests/e-acsl-runtime/array.i:15:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-tests/e-acsl-runtime/array.i:16:[value] warning: assertion got status unknown.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/at.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
new file mode 100644
index 00000000000..64260f42a32
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
@@ -0,0 +1,43 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ A ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __delete_block
+tests/gmp/at.i:40:[value] Function h: postcondition got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/gmp/at.i:40:[value] Function __e_acsl_h: postcondition got status valid.
+tests/gmp/at.i:48:[value] Assertion got status valid.
+tests/gmp/at.i:13:[value] Assertion got status valid.
+tests/gmp/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
+tests/gmp/at.i:14:[value] Assertion got status unknown.
+tests/gmp/at.i:15:[value] Assertion got status valid.
+tests/gmp/at.i:16:[value] Assertion got status valid.
+tests/gmp/at.i:9:[value] Function f: postcondition got status valid.
+tests/gmp/at.i:9:[value] Function __e_acsl_f: postcondition got status valid.
+tests/gmp/at.i:53:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
+tests/gmp/at.i:53:[value] Assertion got status unknown.
+tests/gmp/at.i:54:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
+tests/gmp/at.i:54:[value] Assertion got status unknown.
+tests/gmp/at.i:55:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
+tests/gmp/at.i:55:[value] Assertion got status unknown.
+[value] using specification for function __initialize
+[value] using specification for function __valid_read
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:32:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
+tests/gmp/at.i:32:[value] Assertion got status unknown.
+tests/gmp/at.i:34:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
+tests/gmp/at.i:34:[value] Assertion got status unknown.
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/at.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/cast.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/cast.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/comparison.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
new file mode 100644
index 00000000000..6afe4e90f3b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
@@ -0,0 +1,32 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+tests/gmp/comparison.i:9:[value] Assertion got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/gmp/comparison.i:10:[value] Assertion got status valid.
+tests/gmp/comparison.i:11:[value] Assertion got status valid.
+tests/gmp/comparison.i:12:[value] Assertion got status valid.
+tests/gmp/comparison.i:14:[value] Assertion got status valid.
+tests/gmp/comparison.i:17:[value] Assertion got status valid.
+tests/gmp/comparison.i:18:[value] Assertion got status valid.
+tests/gmp/comparison.i:19:[value] Assertion got status valid.
+tests/gmp/comparison.i:20:[value] Assertion got status valid.
+tests/gmp/comparison.i:21:[value] Assertion got status valid.
+tests/gmp/comparison.i:22:[value] Assertion got status valid.
+tests/gmp/comparison.i:24:[value] Assertion got status valid.
+tests/gmp/comparison.i:25:[value] Assertion got status valid.
+tests/gmp/comparison.i:26:[value] Assertion got status valid.
+tests/gmp/comparison.i:27:[value] Assertion got status valid.
+tests/gmp/comparison.i:28:[value] Assertion got status valid.
+tests/gmp/comparison.i:29:[value] Assertion got status valid.
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/comparison.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_array.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_array.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
rename to src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/longlong.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
similarity index 90%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 05f59d98e5e..2e7040fe69e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -10,8 +10,8 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/longlong.i:11:[value] warning: recursive call during value analysis
- of my_pow (my_pow <- my_pow :: tests/e-acsl-runtime/longlong.i:18 <- main).
+tests/gmp/longlong.i:11:[value] warning: recursive call during value analysis
+ of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:18 <- main).
Using specification of my_pow.
[value] user error: Recursive call on an unspecified function. Using potentially invalid
inferred assigns 'assigns \result \from x, n;'
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/longlong.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
similarity index 90%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index 382e1ff4d99..c491aab0b76 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -10,8 +10,8 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/longlong.i:11:[value] warning: recursive call during value analysis
- of my_pow (my_pow <- my_pow :: tests/e-acsl-runtime/longlong.i:18 <- main).
+tests/gmp/longlong.i:11:[value] warning: recursive call during value analysis
+ of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:18 <- main).
Using specification of my_pow.
[value] user error: Recursive call on an unspecified function. Using potentially invalid
inferred assigns 'assigns \result \from x, n;'
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/not.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/not.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/quantif.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
new file mode 100644
index 00000000000..bcba84153e8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
@@ -0,0 +1,31 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+tests/gmp/quantif.i:11:[value] Assertion got status unknown.
+tests/gmp/quantif.i:11:[value] entering loop for the first time
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/gmp/quantif.i:12:[value] Assertion got status unknown.
+tests/gmp/quantif.i:12:[value] entering loop for the first time
+tests/gmp/quantif.i:13:[value] Assertion got status unknown.
+tests/gmp/quantif.i:13:[value] entering loop for the first time
+tests/gmp/quantif.i:14:[value] Assertion got status unknown.
+tests/gmp/quantif.i:14:[value] entering loop for the first time
+tests/gmp/quantif.i:18:[value] Assertion got status unknown.
+tests/gmp/quantif.i:18:[value] entering loop for the first time
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/gmp/quantif.i:23:[value] Assertion got status unknown.
+tests/gmp/quantif.i:23:[value] entering loop for the first time
+tests/gmp/quantif.i:27:[value] Assertion got status unknown.
+tests/gmp/quantif.i:27:[value] entering loop for the first time
+tests/gmp/quantif.i:28:[value] entering loop for the first time
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.err.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.err.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/quantif.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
similarity index 96%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
rename to src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
index 5f380012785..4603d120f85 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
@@ -10,7 +10,6 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/quantif.i:11:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_set
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/quantif.i b/src/plugins/e-acsl/tests/gmp/quantif.i
similarity index 80%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/quantif.i
rename to src/plugins/e-acsl/tests/gmp/quantif.i
index afcac4ef3cd..852243ee71e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/quantif.i
+++ b/src/plugins/e-acsl/tests/gmp/quantif.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: quantifiers
COMMENT: no diff
- EXECNOW: LOG gen_quantif2.c BIN gen_quantif2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/quantif.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_quantif2.c > /dev/null && ./gcc_runtime.sh quantif2
+ EXECNOW: LOG gen_quantif2.c BIN gen_quantif2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/gmp/quantif.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/gmp/result/gen_quantif2.c > /dev/null && ./gcc_runtime.sh quantif2
*/
int main(void) {
--
GitLab