diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml index 32ea6246dbdaa5f561516fa9770f632980e6e9f7..440e24747d47f9c99ded7fb976553dc588986062 100644 --- a/src/plugins/value/partitioning/partition.ml +++ b/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 *) diff --git a/tests/value/oracle/split_return.0.res.oracle b/tests/value/oracle/split_return.0.res.oracle index 7606908946d52c53b2f5115012bec52daf02a0d6..3c39daac7720985d50738ccf8f1157084f82ae0b 100644 --- a/tests/value/oracle/split_return.0.res.oracle +++ b/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 diff --git a/tests/value/oracle/split_return.1.res.oracle b/tests/value/oracle/split_return.1.res.oracle index 7410bd57efb3df63e156880cf497ae249a41fbac..e161e8a21148dd6de625f47fd1cd8b0935903ee8 100644 --- a/tests/value/oracle/split_return.1.res.oracle +++ b/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. diff --git a/tests/value/oracle/split_return.4.res.oracle b/tests/value/oracle/split_return.4.res.oracle index cbcd6482358dd1db27e7dbf6051450b1f17124d3..9751f1d714782c4f4f5c41324c7050e3690dd387 100644 --- a/tests/value/oracle/split_return.4.res.oracle +++ b/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