From 9e997242747f259b75fbded23c061917ece30f13 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 25 Apr 2023 21:55:10 +0200
Subject: [PATCH] [Eva] Updates alternative test oracles for the octagon
domain.
---
.../oracle_octagon/realloc.res.oracle | 4 --
.../oracle_octagon/CruiseControl.res.oracle | 8 +++
.../oracle_octagon/builtins_split.res.oracle | 3 +-
.../value/oracle_octagon/equality.res.oracle | 12 +---
.../oracle_octagon/from_termin.res.oracle | 2 +
tests/value/oracle_octagon/gauges.res.oracle | 15 ++---
.../incompatible_states.res.oracle | 4 ++
.../redundant_alarms.res.oracle | 2 +
.../value/oracle_octagon/relations.res.oracle | 58 ++++++++++++++++++-
tests/value/oracle_octagon/struct2.res.oracle | 7 ---
tests/value/oracle_octagon/taint.res.oracle | 19 ------
tests/value/oracle_octagon/unroll.res.oracle | 4 +-
.../oracle_octagon/unroll_simple.res.oracle | 4 +-
13 files changed, 86 insertions(+), 56 deletions(-)
delete mode 100644 tests/builtins/oracle_octagon/realloc.res.oracle
create mode 100644 tests/value/oracle_octagon/CruiseControl.res.oracle
create mode 100644 tests/value/oracle_octagon/from_termin.res.oracle
create mode 100644 tests/value/oracle_octagon/incompatible_states.res.oracle
create mode 100644 tests/value/oracle_octagon/redundant_alarms.res.oracle
diff --git a/tests/builtins/oracle_octagon/realloc.res.oracle b/tests/builtins/oracle_octagon/realloc.res.oracle
deleted file mode 100644
index c6980b05984..00000000000
--- a/tests/builtins/oracle_octagon/realloc.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-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}
diff --git a/tests/value/oracle_octagon/CruiseControl.res.oracle b/tests/value/oracle_octagon/CruiseControl.res.oracle
new file mode 100644
index 00000000000..7c3d8d711cf
--- /dev/null
+++ b/tests/value/oracle_octagon/CruiseControl.res.oracle
@@ -0,0 +1,8 @@
+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}
diff --git a/tests/value/oracle_octagon/builtins_split.res.oracle b/tests/value/oracle_octagon/builtins_split.res.oracle
index 4f5a68d6cdb..09146749136 100644
--- a/tests/value/oracle_octagon/builtins_split.res.oracle
+++ b/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
diff --git a/tests/value/oracle_octagon/equality.res.oracle b/tests/value/oracle_octagon/equality.res.oracle
index 05c8486c527..24564fbdf14 100644
--- a/tests/value/oracle_octagon/equality.res.oracle
+++ b/tests/value/oracle_octagon/equality.res.oracle
@@ -1,16 +1,10 @@
-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
diff --git a/tests/value/oracle_octagon/from_termin.res.oracle b/tests/value/oracle_octagon/from_termin.res.oracle
new file mode 100644
index 00000000000..d03d84f92d5
--- /dev/null
+++ b/tests/value/oracle_octagon/from_termin.res.oracle
@@ -0,0 +1,2 @@
+9a10
+> [eva] from_termin.i:8: starting to merge loop iterations
diff --git a/tests/value/oracle_octagon/gauges.res.oracle b/tests/value/oracle_octagon/gauges.res.oracle
index 3bd3c265780..a5e47e28258 100644
--- a/tests/value/oracle_octagon/gauges.res.oracle
+++ b/tests/value/oracle_octagon/gauges.res.oracle
@@ -1,24 +1,17 @@
-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}
diff --git a/tests/value/oracle_octagon/incompatible_states.res.oracle b/tests/value/oracle_octagon/incompatible_states.res.oracle
new file mode 100644
index 00000000000..426fe5da2c9
--- /dev/null
+++ b/tests/value/oracle_octagon/incompatible_states.res.oracle
@@ -0,0 +1,4 @@
+58c58
+< t[0] ∈ {0; 1}
+---
+> t[0] ∈ {0}
diff --git a/tests/value/oracle_octagon/redundant_alarms.res.oracle b/tests/value/oracle_octagon/redundant_alarms.res.oracle
new file mode 100644
index 00000000000..913f8ab9f77
--- /dev/null
+++ b/tests/value/oracle_octagon/redundant_alarms.res.oracle
@@ -0,0 +1,2 @@
+46a47
+> [eva] redundant_alarms.c:39: starting to merge loop iterations
diff --git a/tests/value/oracle_octagon/relations.res.oracle b/tests/value/oracle_octagon/relations.res.oracle
index d629b85b3f6..1aba9b820f8 100644
--- a/tests/value/oracle_octagon/relations.res.oracle
+++ b/tests/value/oracle_octagon/relations.res.oracle
@@ -1,16 +1,68 @@
-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}
diff --git a/tests/value/oracle_octagon/struct2.res.oracle b/tests/value/oracle_octagon/struct2.res.oracle
index 0422f2e21dd..e69de29bb2d 100644
--- a/tests/value/oracle_octagon/struct2.res.oracle
+++ b/tests/value/oracle_octagon/struct2.res.oracle
@@ -1,7 +0,0 @@
-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)
diff --git a/tests/value/oracle_octagon/taint.res.oracle b/tests/value/oracle_octagon/taint.res.oracle
index 20cde282911..0fc62dbb2d3 100644
--- a/tests/value/oracle_octagon/taint.res.oracle
+++ b/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
diff --git a/tests/value/oracle_octagon/unroll.res.oracle b/tests/value/oracle_octagon/unroll.res.oracle
index c82ddd4f318..b0b04dfe12a 100644
--- a/tests/value/oracle_octagon/unroll.res.oracle
+++ b/tests/value/oracle_octagon/unroll.res.oracle
@@ -1,4 +1,6 @@
-20c20
+14a15
+> [eva] unroll.i:39: starting to merge loop iterations
+20c21
< G ∈ [17739..2147483647]
---
> G ∈ [17854..2147483647]
diff --git a/tests/value/oracle_octagon/unroll_simple.res.oracle b/tests/value/oracle_octagon/unroll_simple.res.oracle
index 8a48c42f84b..0aead1b2497 100644
--- a/tests/value/oracle_octagon/unroll_simple.res.oracle
+++ b/tests/value/oracle_octagon/unroll_simple.res.oracle
@@ -1,4 +1,6 @@
-17c17
+11a12
+> [eva] unroll_simple.i:16: starting to merge loop iterations
+17c18
< G ∈ [8772..2147483647]
---
> G ∈ [8896..2147483647]
--
GitLab