[Eva] Reverts a change in the comparison function between partition keys.

[Datatype.Option] defines a different order than [Stdlib.Option.compare].

Type ['state partition] is a map from partition keys to states.
Such maps are converted into lists to be propagated through statements.
Changes in [Key.compare] impact the list order.
The list order impacts the heuristics used to remove redundant states before
propagating them (see Partitioning_index): redundant states may be propagated
or not depending of the list order.
This impacts the number of states propagated at some statements, and thus the
consumed slevel, and the precision of the analysis afterwards.

This commit reverts the change in the comparison of keys only to minimize
changes in the behavior of the analysis partitioning.

src/plugins/value/partitioning/partition.ml

@@ -210,7 +210,7 @@ struct
         let (<?>) c (cmp,x,y) =
           if c = 0 then cmp x y else c
         in
-        Stamp.compare k1.ration_stamp k2.ration_stamp
+        Stdlib.Option.compare IntPair.compare k1.ration_stamp k2.ration_stamp
         <?> (LoopList.compare, k1.loops, k2.loops)
         <?> (Splits.compare, k1.splits, k2.splits)
         (* Ignore monitors in comparison *)

tests/value/oracle/split_return.0.res.oracle

@@ -32,8 +32,8 @@
   Called from tests/value/split_return.i:51.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
 [eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
 [eva] tests/value/split_return.i:54: assertion got status valid.
 [eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
 [eva] tests/value/split_return.i:57: assertion got status valid.
@@ -72,8 +72,8 @@
   Called from tests/value/split_return.i:120.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:123: assertion got status valid.
 [eva] tests/value/split_return.i:125: assertion got status valid.
 [eva] Recording results for main5

tests/value/oracle/split_return.1.res.oracle

@@ -34,8 +34,8 @@
   Called from tests/value/split_return.i:51.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
 [eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
 [eva] tests/value/split_return.i:54: assertion got status valid.
 [eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
 [eva] tests/value/split_return.i:57: assertion got status valid.
@@ -47,8 +47,8 @@
   Called from tests/value/split_return.i:76.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:79: assertion got status valid.
 [eva] tests/value/split_return.i:81: assertion got status valid.
 [eva] Recording results for main3
@@ -59,8 +59,8 @@
   Called from tests/value/split_return.i:97.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
 [eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
 [eva] tests/value/split_return.i:100: assertion got status valid.
 [eva] tests/value/split_return.i:102: assertion got status valid.
 [eva] Recording results for main4
@@ -71,8 +71,8 @@
   Called from tests/value/split_return.i:120.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:123: assertion got status valid.
 [eva] tests/value/split_return.i:125: assertion got status valid.
 [eva] Recording results for main5
@@ -104,8 +104,8 @@
   Called from tests/value/split_return.i:174.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.

tests/value/oracle/split_return.4.res.oracle

@@ -472,8 +472,8 @@
   Called from tests/value/split_return.i:51.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
 [eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
 [eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
 [eva] Recording results for main2
 [eva] Done for function main2