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 8f4a3d3b726e4de70a64a83ff6d2a86ac9758b36..0000000000000000000000000000000000000000
--- 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 2f339588463bc8f05aa1bf2ebac8874f03c071ed..0000000000000000000000000000000000000000
--- 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 f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9..0000000000000000000000000000000000000000
--- 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 9526b80c6209b5f42bb516e568b9589c7aa27a78..20295c7ae73c027b14901bead80dab16d14f6402 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 e0ebf45e128eca822961123d7e337097f902e58f..0000000000000000000000000000000000000000
--- 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 91954d6142dbba12e1cb847ce2b3588d4df79e9a..b58f25a24e5ed061a2f2e13a2f9797b62b2fd7b3 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 2bd785a61358906e21937a63fa69b60f28752c26..9474ac288c869a4b9f7573afc6cb96424a3dff7d 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 45d8548caec24ad8ba987cf0d9058df925a643b6..1dade3f0c1df29c3f6f3710c3645e8bb1fa4f3cd 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 7e4c94d3a8ae2977ad5e464847d5995c8c0011e7..485648bf9fb0a736b317bd983a66dac9464afdca 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 9ee270ac380137148390a1583b7cb95769ae08f7..216a98c522462b188927dc0fcae381cf820462df 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 08c82dcb45fd314f6633b52f098cab4308fdfe18..2b3c07150121f4d46d8514fa09fbcdae5b3f9e3b 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 b1e87e04fbf7431e6d5d181f90e81de0f58bc6b3..8bf4d0c1a9599d11b4c182989e6932dc2d6d0b58 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 ceb89ce41c9f67936f0e13a3e086e748bfe9b7c5..aaec6975f5918464473ba6f31eadf9e39a6e5acc 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 0000000000000000000000000000000000000000..570b475bf0797b1f8ef7a0798d0acb276ffff465
--- /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 f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9..6a3662a24f1c6d1fdb4b3f9bd72a67a1ae4be418 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 eb2477f723cb8c2dc008e03316844225964c80e3..84e54776a151ce574449f61a543884e5f6fbea92 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 0000000000000000000000000000000000000000..64260f42a32b9a6a98911571c35651999e3360d4
--- /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 0000000000000000000000000000000000000000..6afe4e90f3b78c987eff45e9407f6c67948cb676
--- /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 05f59d98e5e0b32f63057a2314f237804f7c5d52..2e7040fe69e707c7233f96eed46c8b8d931eb3f9 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 382e1ff4d9982a73481965743000bb0828c5a82b..c491aab0b764734d866183a889e7234bd12ac2e4 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 0000000000000000000000000000000000000000..bcba84153e85bfe08e70a2a7c50d6fdf8896c759
--- /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 5f380012785867d1870e6f42134ee0204da33a35..4603d120f8554dfbb879f97768d1faffdbce243a 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 afcac4ef3cda6a9d9f5033edfff9c32736023790..852243ee71e5f84b3d53a2328328ca1e35251264 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) {