From 1d4fe906559daf4c6221a91bbb7ee7baf8ba3f76 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 1 Oct 2021 10:46:22 +0200
Subject: [PATCH] [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 | 2 +-
tests/value/oracle/split_return.0.res.oracle | 4 ++--
tests/value/oracle/split_return.1.res.oracle | 10 +++++-----
tests/value/oracle/split_return.4.res.oracle | 2 +-
4 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index 32ea6246dbd..440e24747d4 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 7606908946d..3c39daac772 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 7410bd57efb..e161e8a2114 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 cbcd6482358..9751f1d7147 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
--
GitLab