[Eva] Updates alternative test oracles for the octagon domain.

tests/builtins/oracle_octagon/realloc.res.oracle

-627a628,630
-> [eva] realloc.c:152: Call to builtin realloc
-> [eva:malloc] bases_to_realloc: {__realloc_w_main10_l152}
-> [eva:malloc] realloc.c:152: weak free on bases: {__realloc_w_main10_l152}

tests/value/oracle_octagon/CruiseControl.res.oracle

+979c979
+<        [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1}
+---
+>        [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1}
+1217c1217
+<        [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1}
+---
+>        [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1}

tests/value/oracle_octagon/builtins_split.res.oracle

@@ -6,7 +6,8 @@
 > [eva] builtins_split.c:104: Call to builtin Frama_C_builtin_split_all
 > [eva] builtins_split.c:104: Call to builtin Frama_C_builtin_split_all
 > [eva] builtins_split.c:104: Call to builtin Frama_C_builtin_split_all
-75a83,89
+75a83,90
+> [eva] builtins_split.c:112: Call to builtin Frama_C_builtin_split_all
 > [eva] builtins_split.c:112: Call to builtin Frama_C_builtin_split_all
 > [eva] builtins_split.c:112: Call to builtin Frama_C_builtin_split_all
 > [eva] builtins_split.c:112: Call to builtin Frama_C_builtin_split_all

tests/value/oracle_octagon/equality.res.oracle

-42,43c42,43
-< [eva:alarm] equality.c:57: Warning: 
-<   function sqrtf: precondition 'arg_positive' got status unknown.
+60c60
+< [eva] equality.c:99: Frama_C_show_each_10_19: [10..42]
 ---
-> [eva] equality.c:57: 
->   function sqrtf: precondition 'arg_positive' got status valid.
+> [eva] equality.c:99: Frama_C_show_each_10_19: [10..19]
 75,76c75,76
 <   y ∈ [0..42] or UNINITIALIZED
 <   w ∈ [0..42] or UNINITIALIZED
 ---
 >   y ∈ [0..42]
 >   w ∈ [0..42]
-87c87
-<   res ∈ [-0. .. 3.16227769852] or UNINITIALIZED
----
->   res ∈ [3.74339206651e-23 .. 3.16227769852] or UNINITIALIZED

tests/value/oracle_octagon/from_termin.res.oracle

+9a10
+> [eva] from_termin.i:8: starting to merge loop iterations

tests/value/oracle_octagon/gauges.res.oracle

-196,197d195
-< [eva:alarm] gauges.c:156: Warning: 
-<   signed overflow. assert -2147483648 ≤ toCopy - 1;
-259,260d256
+259,260d258
 < [eva:alarm] gauges.c:201: Warning: 
 <   signed overflow. assert -2147483648 ≤ numNonZero - 1;
-282,286d277
+282,286d279
 < [eva] gauges.c:218: Frama_C_show_each:
 < [eva] gauges.c:218: Frama_C_show_each:
 < [eva] gauges.c:218: Frama_C_show_each:
 < [eva:alarm] gauges.c:220: Warning: 
 <   signed overflow. assert -2147483648 ≤ n - 1;
-767c758
+767c760
 <   numNonZero ∈ [-2147483648..8]
 ---
 >   numNonZero ∈ {-1}
-778c769
+778c771
 <   n ∈ [-2147483648..99]
 ---
 >   n ∈ {-1}
-839c830
-<   toCopy ∈ [-2147483648..99]
----
->   toCopy ∈ {-1}

tests/value/oracle_octagon/incompatible_states.res.oracle

+58c58
+<   t[0] ∈ {0; 1}
+---
+>   t[0] ∈ {0}

tests/value/oracle_octagon/redundant_alarms.res.oracle

+46a47
+> [eva] redundant_alarms.c:39: starting to merge loop iterations

tests/value/oracle_octagon/relations.res.oracle

-38,41d37
+34,49d33
+< [eva:alarm] relations.i:41: Warning: 
+<   signed overflow. assert -2147483648 ≤ u[5] - u[0];
+< [eva:alarm] relations.i:41: Warning: 
+<   signed overflow. assert u[5] - u[0] ≤ 2147483647;
 < [eva:alarm] relations.i:46: Warning: 
 <   signed overflow. assert -2147483648 ≤ u[10] - u[11];
 < [eva:alarm] relations.i:46: Warning: 
 <   signed overflow. assert u[10] - u[11] ≤ 2147483647;
-72c68
+< [eva:alarm] relations.i:48: Warning: 
+<   signed overflow. assert -2147483648 ≤ u[1] - u[0];
+< [eva:alarm] relations.i:48: Warning: 
+<   signed overflow. assert u[1] - u[0] ≤ 2147483647;
+< [eva:alarm] relations.i:52: Warning: 
+<   signed overflow. assert -2147483648 ≤ u[5] - u[1];
+< [eva:alarm] relations.i:52: Warning: 
+<   signed overflow. assert u[5] - u[1] ≤ 2147483647;
+60,61c44
+<   u[0] ∈ [-2147483648..2147483646]
+<    [1] ∈ [--..--]
+---
+>   u[0..1] ∈ [-2147483648..2147483646]
+67,78c50,60
+<   R1 ∈ [--..--]
+<   R2 ∈ [--..--]
+<   R3 ∈ [-2147483648..2147483646]
+<   R4 ∈ [--..--]
+<   R5 ∈ [--..--]
 <   R6 ∈ [--..--]
+<   R7 ∈ {0; 1}
+<   A7 ∈ [--..--]
+<   R8 ∈ {0; 1}
+<   A8 ∈ [--..--]
+<   S1 ∈ {-1; 0; 1}
+<   S2 ∈ {0; 1}
 ---
+>   R1 ∈ {0; 3}
+>   R2 ∈ {0; 3}
+>   R3 ∈ {0; 2}
+>   R4 ∈ {0; 2}
+>   R5 ∈ {1}
 >   R6 ∈ {0}
-80,81c76,78
+>   R7 ∈ {1}
+>   A7 ∈ {0}
+>   A8 ∈ {1}
+>   S1 ∈ {0}
+>   S2 ∈ {1}
+80,81c62,64
 <   e ∈ [--..--]
 <   f ∈ [--..--]
 ---
 >   e ∈ {1}
 >   f[bits 0 to 7] ∈ {1; 4}
 >    [bits 8 to 31] ∈ [--..--]
+102c85
+<   R7 FROM g (and SELF)
+---
+>   R7 FROM g
+104d86
+<   R8 FROM g (and SELF)
+107c89
+<   S2 FROM pCs; S_pCs[0]{.L0; .L1} (and SELF)
+---
+>   S2 FROM pCs; S_pCs[0]{.L0; .L1}
+112c94
+<     A7; R8; A8; S1; S2; c; e; f; tmp; tmp_0; S_pCs[0]{.T13; .T; .L8}
+---
+>     A7; A8; S1; S2; c; e; f; tmp; tmp_0; S_pCs[0]{.T13; .T; .L8}

tests/value/oracle_octagon/struct2.res.oracle

-77,80d76
-<   accessing out of bounds index. assert 0 ≤ (int)(i + j);
-< [eva:alarm] struct2.i:185: Warning: 
-<   accessing out of bounds index. assert (int)(i + j) < 2;
-< [eva:alarm] struct2.i:185: Warning: 
-98d93
-< [scope:rm_asserts] removing 2 assertion(s)

tests/value/oracle_octagon/taint.res.oracle

@@ -10,22 +10,3 @@
 <   y ∈ [2..11]
 ---
 >   y ∈ {3; 5; 7; 9; 11}
-229,232c229
-<   Frama_C_entropy_source ∈ [--..--]
-<   tainted ∈ {2; 4; 6; 8; 10}
-<   l ∈ {0}
-<   __retres ∈ {0}
----
->   NON TERMINATING FUNCTION
-255a253
-> [from] Non-terminating function main (no dependencies)
-284,286c282
-<   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-<   tainted FROM Frama_C_entropy_source
-<   \result FROM \nothing
----
->   NON TERMINATING - NO EFFECTS
-325c321
-<     Frama_C_entropy_source; tainted; l; __retres
----
->     Frama_C_entropy_source; tainted; l

tests/value/oracle_octagon/unroll.res.oracle

-20c20
+14a15
+> [eva] unroll.i:39: starting to merge loop iterations
+20c21
 <   G ∈ [17739..2147483647]
 ---
 >   G ∈ [17854..2147483647]

tests/value/oracle_octagon/unroll_simple.res.oracle

-17c17
+11a12
+> [eva] unroll_simple.i:16: starting to merge loop iterations
+17c18
 <   G ∈ [8772..2147483647]
 ---
 >   G ∈ [8896..2147483647]