[Eva] Adds a test of printing large integer sets.

tests/value/ilevel.c

 /* run.config*
    PLUGIN: @EVA_MAIN_PLUGINS@ inout,slicing
    OPT: -eva @EVA_CONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48
-
+   STDOPT: +"-eva-ilevel 400 -main large_ilevel"
 */
 
 // Test in particular that ilevel is by-project, even though it is an ocaml ref
@@ -31,3 +31,18 @@ int main () {
 
   return i+j+k+l;
 }
+
+/* Tests printing large integer sets. */
+void large_ilevel (void) {
+  int i = Frama_C_interval(0, 10);
+  int j = nondet ? i : i - 25;
+  int k = Frama_C_interval(100, 200);
+  if (k == 128) return;
+
+  int a[11] = {53, 17, 64, 99, 25, 12, 72, 81, 404, 303, -101};
+
+  int s2 = nondet ? 40 : (nondet ? 41 : 42);
+  int s1 = a[i];
+
+  int x = nondet ? (nondet ? j : k) : (nondet ? s1 : s2);
+}

tests/value/oracle/ilevel.1.res.oracle

+[kernel] Parsing ilevel.c (with preprocessing)
+[eva] Analyzing a complete application starting at large_ilevel
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  nondet ∈ [--..--]
+  i ∈ {0}
+  j ∈ {0}
+  k ∈ {0}
+  l ∈ {0}
+[eva] computing for function Frama_C_interval <- large_ilevel.
+  Called from ilevel.c:37.
+[eva] using specification for function Frama_C_interval
+[eva] ilevel.c:37: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- large_ilevel.
+  Called from ilevel.c:39.
+[eva] ilevel.c:39: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] Recording results for large_ilevel
+[eva] done for function large_ilevel
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function large_ilevel:
+  Frama_C_entropy_source ∈ [--..--]
+  i_0 ∈ [0..10]
+  j_0 ∈ [-25..-15] ∪ [0..10]
+  k_0 ∈ [100..200]
+  a[0] ∈ {53}
+   [1] ∈ {17}
+   [2] ∈ {64}
+   [3] ∈ {99}
+   [4] ∈ {25}
+   [5] ∈ {12}
+   [6] ∈ {72}
+   [7] ∈ {81}
+   [8] ∈ {404}
+   [9] ∈ {303}
+   [10] ∈ {-101}
+  s2 ∈ {40; 41; 42}
+  s1 ∈ {-101; 12; 17; 25; 53; 64; 72; 81; 99; 303; 404}
+  x ∈
+   {-101} ∪ [-25..-15] ∪ [0..10]
+    ∪ {12; 17; 25; 40; 41; 42; 53; 64; 72; 81} ∪ [99..127] ∪ [129..200]
+    ∪ {303; 404}
+[from] Computing for function large_ilevel
+[from] Computing for function Frama_C_interval <-large_ilevel
+[from] Done for function Frama_C_interval
+[from] Done for function large_ilevel
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  \result FROM Frama_C_entropy_source; min; max
+[from] Function large_ilevel:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function large_ilevel:
+    Frama_C_entropy_source; i_0; j_0; tmp_0; k_0; a[0..10]; s2; tmp_2; 
+    tmp_3; s1; x; tmp_4; tmp_5; tmp_6
+[inout] Inputs for function large_ilevel:
+    Frama_C_entropy_source; nondet