diff --git a/tests/misc/eva_annot.c b/tests/misc/eva_annot.c
new file mode 100644
index 0000000000000000000000000000000000000000..b444bf6eb0afd75487443da6bbfacb9525654ae9
--- /dev/null
+++ b/tests/misc/eva_annot.c
@@ -0,0 +1,29 @@
+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+ OPT: -eva -eva-precision 2 -eva-annot main -print
+*/
+
+/* -------------------------------------------------------------------------- */
+/* --- Testing EVA Annotations --- */
+/* -------------------------------------------------------------------------- */
+
+//@ ghost int world;
+int a[20];
+
+/*@
+ ensures 0 <= \result <= 100;
+ assigns \result,world \from world;
+*/
+int value(void);
+
+int main(void) {
+ int s = 0;
+ for (int i = 0; i < 20; i++) {
+ int v = value();
+ a[i] = v;
+ s += v;
+ }
+ return s;
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/tests/misc/eva_annot_float.c b/tests/misc/eva_annot_float.c
new file mode 100644
index 0000000000000000000000000000000000000000..31fd27f8bb30d553ad6f55d2c8e35de1147ca306
--- /dev/null
+++ b/tests/misc/eva_annot_float.c
@@ -0,0 +1,30 @@
+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+ OPT: -eva -eva-precision 2 -eva-annot main -print
+*/
+
+/* -------------------------------------------------------------------------- */
+/* --- Testing EVA Annotations --- */
+/* -------------------------------------------------------------------------- */
+
+//@ ghost int world;
+double a[20];
+
+/*@
+ ensures \is_finite(\result);
+ ensures 0.0 <= \result <= 100.0;
+ assigns \result,world \from world;
+*/
+double value(void);
+
+double main(void) {
+ double s = 0;
+ for (int i = 0; i < 20; i++) {
+ double v = value();
+ a[i] = v;
+ s += v;
+ }
+ return s;
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/tests/misc/eva_annot_range.c b/tests/misc/eva_annot_range.c
new file mode 100644
index 0000000000000000000000000000000000000000..a997339e15256aea762f1dfc967c9ae9bba5c68b
--- /dev/null
+++ b/tests/misc/eva_annot_range.c
@@ -0,0 +1,29 @@
+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+ OPT: -eva -eva-precision 2 -eva-annot main -print
+*/
+
+/* -------------------------------------------------------------------------- */
+/* --- Testing EVA Annotations --- */
+/* -------------------------------------------------------------------------- */
+
+//@ ghost int world;
+int a[20];
+
+/*@
+ ensures 0 <= \result <= 100;
+ assigns \result,world \from world;
+*/
+int value(void);
+
+int main(void) {
+ int s = 0;
+ for (int i = 0; i < 20; i+=2) {
+ int v = value();
+ a[i] = v;
+ s += v;
+ }
+ return s;
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/tests/misc/oracle/eva_annot.res.oracle b/tests/misc/oracle/eva_annot.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..30a1431306a486f23147309b7473fef7f9fb0806
--- /dev/null
+++ b/tests/misc/oracle/eva_annot.res.oracle
@@ -0,0 +1,74 @@
+[kernel] Parsing eva_annot.c (with preprocessing)
+[eva] Option -eva-precision 2 detected, automatic configuration of the analysis:
+ option -eva-min-loop-unroll set to 0 (default value).
+ option -eva-auto-loop-unroll set to 32.
+ option -eva-widening-delay set to 2.
+ option -eva-partition-history set to 0 (default value).
+ option -eva-slevel set to 20.
+ option -eva-ilevel set to 16.
+ option -eva-plevel set to 40.
+ option -eva-subdivide-non-linear set to 40.
+ option -eva-remove-redundant-alarms set to true (default value).
+ option -eva-domains set to 'cvalue,equality,symbolic-locations'.
+ option -eva-split-return set to '' (default value).
+ option -eva-equality-through-calls set to 'none'.
+ option -eva-octagon-through-calls set to false (default value).
+[eva] Analyzing a complete application starting at main
+[eva:initial-state] Values of globals at initialization
+ world ∈ {0}
+ a[0..19] ∈ {0}
+[eva:loop-unroll:auto] eva_annot.c:21: Automatic loop unrolling.
+[eva] using specification for function value
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ world ∈ [--..--]
+ a[0..19] ∈ [0..100]
+ s ∈ [0..2000]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[eva] Annotate main
+/* Generated by Frama-C */
+/*@ ghost int world; */
+int a[20];
+/*@ ensures 0 ≤ \result ≤ 100;
+ assigns \result, world;
+ assigns \result \from world;
+ assigns world \from world;
+ */
+int value(void);
+
+int main(void)
+{
+ int s = 0;
+ {
+ int i = 0;
+ while (1) {
+ /*@ assert Eva_domain: 0 ≤ i ≤ 20; */
+ if (! (i < 20)) break;
+ {
+ int v = value();
+ /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
+ /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
+ a[i] = v;
+ /*@ assert Eva_domain: 0 ≤ s ≤ 1900; */
+ /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
+ s += v;
+ }
+ /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
+ i ++;
+ }
+ }
+ /*@ assert Eva_domain: 0 ≤ s ≤ 2000; */
+ return s;
+}
+
+
diff --git a/tests/misc/oracle/eva_annot_float.res.oracle b/tests/misc/oracle/eva_annot_float.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d7f9900478e1ecf60972366b82ea17e92ec868eb
--- /dev/null
+++ b/tests/misc/oracle/eva_annot_float.res.oracle
@@ -0,0 +1,86 @@
+[kernel] Parsing eva_annot_float.c (with preprocessing)
+[eva] Option -eva-precision 2 detected, automatic configuration of the analysis:
+ option -eva-min-loop-unroll set to 0 (default value).
+ option -eva-auto-loop-unroll set to 32.
+ option -eva-widening-delay set to 2.
+ option -eva-partition-history set to 0 (default value).
+ option -eva-slevel set to 20.
+ option -eva-ilevel set to 16.
+ option -eva-plevel set to 40.
+ option -eva-subdivide-non-linear set to 40.
+ option -eva-remove-redundant-alarms set to true (default value).
+ option -eva-domains set to 'cvalue,equality,symbolic-locations'.
+ option -eva-split-return set to '' (default value).
+ option -eva-equality-through-calls set to 'none'.
+ option -eva-octagon-through-calls set to false (default value).
+[eva] Analyzing a complete application starting at main
+[eva:initial-state] Values of globals at initialization
+ world ∈ {0}
+ a[0..19] ∈ {0}
+[eva:loop-unroll:auto] eva_annot_float.c:22: Automatic loop unrolling.
+[eva] using specification for function value
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ world ∈ [--..--]
+ a[0..19] ∈ [-0. .. 100.]
+ s ∈ [0. .. 2000.]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[eva] Annotate main
+/* Generated by Frama-C */
+/*@ ghost int world; */
+double a[20];
+/*@ ensures \is_finite(\result);
+ ensures 0.0 ≤ \result ≤ 100.0;
+ assigns \result, world;
+ assigns \result \from world;
+ assigns world \from world;
+ */
+double value(void);
+
+double main(void)
+{
+ double s = (double)0;
+ {
+ int i = 0;
+ while (1) {
+ /*@ assert Eva_domain: 0 ≤ i ≤ 20; */
+ if (! (i < 20)) break;
+ {
+ double v = value();
+ /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
+ /*@ assert
+ Eva_domain:
+ -0.0000000000000000e+00d ≤ v ≤ 1.0000000000000000e+02d;
+ */
+ a[i] = v;
+ /*@ assert
+ Eva_domain:
+ 0.0000000000000000e+00d ≤ s ≤ 1.9000000000000000e+03d;
+ */
+ /*@ assert
+ Eva_domain:
+ -0.0000000000000000e+00d ≤ v ≤ 1.0000000000000000e+02d;
+ */
+ s += v;
+ }
+ /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
+ i ++;
+ }
+ }
+ /*@ assert
+ Eva_domain: 0.0000000000000000e+00d ≤ s ≤ 2.0000000000000000e+03d;
+ */
+ return s;
+}
+
+
diff --git a/tests/misc/oracle/eva_annot_range.res.oracle b/tests/misc/oracle/eva_annot_range.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..883c0bbe5c11b597c3957bb175fbced3ca0bacaf
--- /dev/null
+++ b/tests/misc/oracle/eva_annot_range.res.oracle
@@ -0,0 +1,106 @@
+[kernel] Parsing eva_annot_range.c (with preprocessing)
+[eva] Option -eva-precision 2 detected, automatic configuration of the analysis:
+ option -eva-min-loop-unroll set to 0 (default value).
+ option -eva-auto-loop-unroll set to 32.
+ option -eva-widening-delay set to 2.
+ option -eva-partition-history set to 0 (default value).
+ option -eva-slevel set to 20.
+ option -eva-ilevel set to 16.
+ option -eva-plevel set to 40.
+ option -eva-subdivide-non-linear set to 40.
+ option -eva-remove-redundant-alarms set to true (default value).
+ option -eva-domains set to 'cvalue,equality,symbolic-locations'.
+ option -eva-split-return set to '' (default value).
+ option -eva-equality-through-calls set to 'none'.
+ option -eva-octagon-through-calls set to false (default value).
+[eva] Analyzing a complete application starting at main
+[eva:initial-state] Values of globals at initialization
+ world ∈ {0}
+ a[0..19] ∈ {0}
+[eva:loop-unroll:auto] eva_annot_range.c:21: Automatic loop unrolling.
+[eva] using specification for function value
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ world ∈ [--..--]
+ a[0] ∈ [0..100]
+ [1] ∈ {0}
+ [2] ∈ [0..100]
+ [3] ∈ {0}
+ [4] ∈ [0..100]
+ [5] ∈ {0}
+ [6] ∈ [0..100]
+ [7] ∈ {0}
+ [8] ∈ [0..100]
+ [9] ∈ {0}
+ [10] ∈ [0..100]
+ [11] ∈ {0}
+ [12] ∈ [0..100]
+ [13] ∈ {0}
+ [14] ∈ [0..100]
+ [15] ∈ {0}
+ [16] ∈ [0..100]
+ [17] ∈ {0}
+ [18] ∈ [0..100]
+ [19] ∈ {0}
+ s ∈ [0..1000]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[eva] Annotate main
+/* Generated by Frama-C */
+/*@ ghost int world; */
+int a[20];
+/*@ ensures 0 ≤ \result ≤ 100;
+ assigns \result, world;
+ assigns \result \from world;
+ assigns world \from world;
+ */
+int value(void);
+
+int main(void)
+{
+ int s = 0;
+ {
+ int i = 0;
+ while (1) {
+ /*@ assert
+ Eva_domain:
+ i ≡ 0 ∨ i ≡ 2 ∨ i ≡ 4 ∨ i ≡ 6 ∨ i ≡ 8 ∨
+ i ≡ 10 ∨ i ≡ 12 ∨ i ≡ 14 ∨ i ≡ 16 ∨ i ≡ 18 ∨
+ i ≡ 20;
+ */
+ if (! (i < 20)) break;
+ {
+ int v = value();
+ /*@ assert
+ Eva_domain:
+ i ≡ 0 ∨ i ≡ 2 ∨ i ≡ 4 ∨ i ≡ 6 ∨ i ≡ 8 ∨
+ i ≡ 10 ∨ i ≡ 12 ∨ i ≡ 14 ∨ i ≡ 16 ∨ i ≡ 18;
+ */
+ /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
+ a[i] = v;
+ /*@ assert Eva_domain: 0 ≤ s ≤ 900; */
+ /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
+ s += v;
+ }
+ /*@ assert
+ Eva_domain:
+ i ≡ 0 ∨ i ≡ 2 ∨ i ≡ 4 ∨ i ≡ 6 ∨ i ≡ 8 ∨
+ i ≡ 10 ∨ i ≡ 12 ∨ i ≡ 14 ∨ i ≡ 16 ∨ i ≡ 18;
+ */
+ i += 2;
+ }
+ }
+ /*@ assert Eva_domain: 0 ≤ s ≤ 1000; */
+ return s;
+}
+
+