[Eva] improve Export test coverage

tests/misc/eva_annot_float.c

 /* run.config
    PLUGIN: @EVA_PLUGINS@
-   OPT: -eva -eva-precision 2 -eva-annot main -print
+   OPT: -eva -eva-precision 2 -warn-special-float none -eva-annot main1,main2,main3 -print
 */
 
 /* -------------------------------------------------------------------------- */
-/* --- Testing EVA Annotations                                            --- */
+/* --- Testing EVA exported annotations                                   --- */
 /* -------------------------------------------------------------------------- */
 
 //@ ghost int world;
@@ -17,7 +17,7 @@ double a[20];
 */
 double value(void);
 
-double main(void) {
+double main1(void) {
   double s = 0;
   for (int i = 0; i < 20; i++) {
     double v = value();
@@ -27,4 +27,36 @@ double main(void) {
   return s;
 }
 
+/*@
+  ensures (\is_finite(\result) ∧ 0.0 <= \result <= 100.0) ∨ \is_NaN(\result);
+  assigns \result,world \from world;
+*/
+double value_or_nan(void);
+
+void main2(void) {
+  for (int i = 0; i < 20; i++) {
+    double v = value_or_nan();
+    a[i] = v;
+  }
+}
+
+/*@
+  ensures \is_NaN(\result);
+  assigns \result,world \from world;
+*/
+double nan(void);
+
+void main3(void) {
+  for (int i = 0; i < 20; i++) {
+    double v = nan();
+    a[i] = v;
+  }
+}
+
+void main(void) {
+  main1();
+  main2();
+  main3();
+}
+
 /* -------------------------------------------------------------------------- */

tests/misc/oracle/eva_annot_float.res.oracle

@@ -19,15 +19,30 @@
   a[0..19] ∈ {0}
 [eva:loop-unroll:auto] eva_annot_float.c:22: Automatic loop unrolling.
 [eva] using specification for function value
+[eva:loop-unroll:auto] eva_annot_float.c:37: Automatic loop unrolling.
+[eva] using specification for function value_or_nan
+[eva:loop-unroll:auto] eva_annot_float.c:50: Automatic loop unrolling.
+[eva] using specification for function nan
 [eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
+[eva:final-states] Values at end of function main3:
+  world ∈ [--..--]
+  a[0..19] ∈ NaN
+  i ∈ {20}
+[eva:final-states] Values at end of function main1:
   world ∈ [--..--]
   a[0..19] ∈ [-0. .. 100.]
   s ∈ [0. .. 2000.]
+[eva:final-states] Values at end of function main2:
+  world ∈ [--..--]
+  a[0..19] ∈ [-0. .. 100.] ∪ {NaN}
+  i ∈ {20}
+[eva:final-states] Values at end of function main:
+  world ∈ [--..--]
+  a[0..19] ∈ NaN
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
-  1 function analyzed (out of 1): 100% coverage.
-  In this function, 12 statements reached (out of 12): 100% coverage.
+  4 functions analyzed (out of 4): 100% coverage.
+  In these functions, 34 statements reached (out of 34): 100% coverage.
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
   ----------------------------------------------------------------------------
@@ -35,7 +50,9 @@
   ----------------------------------------------------------------------------
   No logical properties have been reached by the analysis.
   ----------------------------------------------------------------------------
-[eva] Annotate main
+[eva] Annotate main1
+[eva] Annotate main2
+[eva] Annotate main3
 /* Generated by Frama-C */
 /*@ ghost int world; */
 double a[20];
@@ -47,7 +64,7 @@ double a[20];
  */
 double value(void);
 
-double main(void)
+double main1(void)
 {
   double s = (double)0;
   {
@@ -83,4 +100,68 @@ double main(void)
   return s;
 }
 
+/*@ ensures
+      (\is_finite(\result) ∧ 0.0 ≤ \result ≤ 100.0) ∨
+      \is_NaN(\result);
+    assigns \result, world;
+    assigns \result \from world;
+    assigns world \from world;
+ */
+double value_or_nan(void);
+
+void main2(void)
+{
+  int i = 0;
+  while (1) {
+    /*@ assert Eva_export: 0 ≤ i ≤ 20; */
+    if (! (i < 20)) break;
+    {
+      double v = value_or_nan();
+      /*@ assert Eva_export: 0 ≤ i ≤ 19; */
+      /*@ assert
+          Eva_export:
+            \is_NaN(v) ∨
+            (-0.0000000000000000e+00d ≤ v ≤ 1.0000000000000000e+02d);
+      */
+      a[i] = v;
+    }
+    /*@ assert Eva_export: 0 ≤ i ≤ 19; */
+    i ++;
+  }
+  return;
+}
+
+/*@ ensures \is_NaN(\result);
+    assigns \result, world;
+    assigns \result \from world;
+    assigns world \from world;
+ */
+double nan(void);
+
+void main3(void)
+{
+  int i = 0;
+  while (1) {
+    /*@ assert Eva_export: 0 ≤ i ≤ 20; */
+    if (! (i < 20)) break;
+    {
+      double v = nan();
+      /*@ assert Eva_export: 0 ≤ i ≤ 19; */
+      /*@ assert Eva_export: \is_NaN(v); */
+      a[i] = v;
+    }
+    /*@ assert Eva_export: 0 ≤ i ≤ 19; */
+    i ++;
+  }
+  return;
+}
+
+void main(void)
+{
+  main1();
+  main2();
+  main3();
+  return;
+}
+