From ae875544804c85d0015636d6b61d4d4d9de2f06f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 25 Apr 2023 18:47:19 +0200
Subject: [PATCH] [Eva] Updates alternative test oracles on octagon tests.
---
.../octagons-pointers-simple.res.oracle | 38 ++++-----
.../oracle_apron/octagons-pointers.res.oracle | 57 -------------
tests/value/oracle_apron/octagons.res.oracle | 76 +----------------
.../value/oracle_equality/octagons.res.oracle | 48 +----------
.../octagons-pointers-intermediate.res.oracle | 17 ++--
.../octagons-pointers-simple.res.oracle | 29 +++----
.../octagons-pointers.res.oracle | 85 ++-----------------
tests/value/oracle_gauges/octagons.res.oracle | 4 +-
.../octagons-pointers.res.oracle | 6 --
9 files changed, 47 insertions(+), 313 deletions(-)
delete mode 100644 tests/value/oracle_apron/octagons-pointers.res.oracle
delete mode 100644 tests/value/oracle_symblocs/octagons-pointers.res.oracle
diff --git a/tests/value/oracle_apron/octagons-pointers-simple.res.oracle b/tests/value/oracle_apron/octagons-pointers-simple.res.oracle
index ff90c5f6bbd..c976f8080e0 100644
--- a/tests/value/oracle_apron/octagons-pointers-simple.res.oracle
+++ b/tests/value/oracle_apron/octagons-pointers-simple.res.oracle
@@ -1,23 +1,15 @@
-18c18
-< size - index ∈ [3..--]
----
-> size - index ∈ {433}
-19a20
-> size + cmdLen ∈ [--..867]
-21a23
-> index - cmdLen ∈ [-428..--]
-33a36
-> size + index ∈ [442..872]
-35a39
-> size + cmdLen ∈ [--..864]
-36a41,42
-> index + cmdLen ∈ [--..864]
-> index - cmdLen ∈ [-422..--]
-38c44
-< size - index ∈ [3..--]
----
-> size - index ∈ [3..430]
-39a46,48
-> index - cmdLen ∈ [-422..--]
-> index + index ∈ [12..869]
-> index - index ∈ [--..430]
+39a40,53
+> [eva] octagons-pointers-simple.c:43: starting to merge loop iterations
+> [eva] octagons-pointers-simple.c:46:
+> Frama_C_dump_each:
+> # octagon:
+> {[ buffer - cmd ∈ [-436..-6]
+> cmd->cmdLen - cmdLen ∈ {0}
+> index + cmdLen ∈ [--..434]
+> cmd->cmdLen + index ∈ [--..434]
+> ]}
+> ==END OF DUMP==
+> [eva] computing for function cmdRead <- main.
+> Called from octagons-pointers-simple.c:47.
+> [eva] Recording results for cmdRead
+> [eva] Done for function cmdRead
diff --git a/tests/value/oracle_apron/octagons-pointers.res.oracle b/tests/value/oracle_apron/octagons-pointers.res.oracle
deleted file mode 100644
index 92808f6680b..00000000000
--- a/tests/value/oracle_apron/octagons-pointers.res.oracle
+++ /dev/null
@@ -1,57 +0,0 @@
-18c18,19
-< size - index ∈ [3..--]
----
-> size - index ∈ {433}
-> size + cmd->cmdLen ∈ [--..867]
-20a22
-> index - cmd->cmdLen ∈ [-428..--]
-29c31,32
-< size - index ∈ [3..--]
----
-> size - index ∈ {433}
-> size + cmd->cmdLen ∈ [--..867]
-31a35
-> index - cmd->cmdLen ∈ [-428..--]
-46a51
-> size + index ∈ [--..872]
-47a53
-> size + cmd->cmdLen ∈ [--..864]
-49c55,58
-< size - index ∈ [3..--]
----
-> index + cmd->cmdLen ∈ [--..864]
-> size - index ∈ [3..430]
-> index + index ∈ [--..869]
-> index - index ∈ [--..430]
-50a60
-> cmd->cmdLen - index ∈ [--..422]
-58a69
-> size + index ∈ [--..872]
-59a71
-> size + cmd->cmdLen ∈ [--..864]
-60a73
-> index + cmd->cmdLen ∈ [--..864]
-63c76,78
-< size - index ∈ [3..--]
----
-> size - index ∈ [3..430]
-> index + index ∈ [--..869]
-> index - index ∈ [--..430]
-64a80
-> cmd->cmdLen - index ∈ [--..422]
-105a122
-> size + cmd->cmdLen ∈ [--..864]
-107c124
-< size - index ∈ [3..--]
----
-> size - index ∈ [3..430]
-108a126
-> cmd->cmdLen - index ∈ [--..422]
-116a135
-> size + cmd->cmdLen ∈ [--..864]
-120c139
-< size - index ∈ [3..--]
----
-> size - index ∈ [3..430]
-121a141
-> cmd->cmdLen - index ∈ [--..422]
diff --git a/tests/value/oracle_apron/octagons.res.oracle b/tests/value/oracle_apron/octagons.res.oracle
index 75df605d471..1c3d2499681 100644
--- a/tests/value/oracle_apron/octagons.res.oracle
+++ b/tests/value/oracle_apron/octagons.res.oracle
@@ -1,78 +1,4 @@
-239a240
-> a - neg_a ∈ [-24..39]
-240a242
-> b - neg_b ∈ [-23..40]
-242,256c244,265
-< a + r1 ∈ [-4..--]
-< a - r1 ∈ [--..12]
-< b + r1 ∈ [-4..--]
-< b - r1 ∈ [--..12]
-< neg_a + r1 ∈ [-12..--]
-< neg_a - r1 ∈ [--..4]
-< neg_b + r1 ∈ [-12..--]
-< neg_b - r1 ∈ [--..4]
-< a + r2 ∈ [-4..--]
-< a - r2 ∈ [--..12]
-< neg_b + r2 ∈ [-12..--]
-< neg_b - r2 ∈ [--..20]
-< b + r2 ∈ [-4..--]
-< b - r2 ∈ [--..12]
-< r1 + r2 ∈ [-16..--]
----
-> a - b ∈ [-16..16]
-> b + neg_a ∈ [-16..16]
-> a + neg_b ∈ [-16..16]
-> a + r1 ∈ [-4..28]
-> a - r1 ∈ [-20..12]
-> b + r1 ∈ [-4..28]
-> b - r1 ∈ [-20..12]
-> neg_a + r1 ∈ [-12..20]
-> neg_a - r1 ∈ [-28..4]
-> neg_b + r1 ∈ [-12..20]
-> neg_b - r1 ∈ [-28..4]
-> neg_a + neg_b ∈ [-40..24]
-> neg_a - neg_b ∈ [-16..16]
-> a + r2 ∈ [-4..28]
-> a - r2 ∈ [-20..12]
-> neg_b + r2 ∈ [-12..20]
-> neg_b - r2 ∈ [-28..4]
-> b + r2 ∈ [-4..28]
-> b - r2 ∈ [-20..12]
-> neg_a + r2 ∈ [-12..20]
-> neg_a - r2 ∈ [-28..4]
-> r1 + r2 ∈ [-16..32]
-258,268c267,275
-< neg_a + r2 ∈ [-12..--]
-< neg_a - r2 ∈ [--..17]
-< a + r3 ∈ [-4..--]
-< a - r3 ∈ [--..12]
-< b + r3 ∈ [-4..--]
-< b - r3 ∈ [--..12]
-< neg_a + r3 ∈ [-12..--]
-< neg_a - r3 ∈ [--..4]
-< neg_b + r3 ∈ [-12..--]
-< neg_b - r3 ∈ [--..4]
-< r1 + r3 ∈ [-16..--]
----
-> a + r3 ∈ [-4..28]
-> a - r3 ∈ [-20..12]
-> b + r3 ∈ [-4..28]
-> b - r3 ∈ [-20..12]
-> neg_a + r3 ∈ [-12..20]
-> neg_a - r3 ∈ [-28..4]
-> neg_b + r3 ∈ [-12..20]
-> neg_b - r3 ∈ [-28..4]
-> r1 + r3 ∈ [-16..32]
-270c277
-< r2 + r3 ∈ [-16..--]
----
-> r2 + r3 ∈ [-16..32]
-297c304,305
-< {[ k - tmp ∈ {0}
----
-> {[ k + tmp ∈ [-256..272]
-> k - tmp ∈ {0}
-417,420c425,428
+371,374c371,374
< a ∈ [-1024..2147483647]
< b ∈ [-1023..2147483647]
< c ∈ [-1023..2147483647]
diff --git a/tests/value/oracle_equality/octagons.res.oracle b/tests/value/oracle_equality/octagons.res.oracle
index b9c6fb2faa8..3b1ca3ecba8 100644
--- a/tests/value/oracle_equality/octagons.res.oracle
+++ b/tests/value/oracle_equality/octagons.res.oracle
@@ -2,53 +2,7 @@
< [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-128..127], [-128..127]
---
> [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-118..114], [6..127]
-239a240
-> a - neg_a ∈ [-24..--]
-240a242
-> b - neg_b ∈ [-23..--]
-242,245c244,252
-< a + r1 ∈ [-4..--]
-< a - r1 ∈ [--..12]
-< b + r1 ∈ [-4..--]
-< b - r1 ∈ [--..12]
----
-> a - b ∈ [-16..16]
-> b + neg_a ∈ [-16..16]
-> b - neg_a ∈ [-22..--]
-> a + neg_b ∈ [-16..16]
-> a - neg_b ∈ [-24..--]
-> a + r1 ∈ [-4..28]
-> a - r1 ∈ [-20..12]
-> b + r1 ∈ [-4..28]
-> b - r1 ∈ [-20..12]
-250,251c257,258
-< a + r2 ∈ [-4..--]
-< a - r2 ∈ [--..12]
----
-> a + r2 ∈ [-4..28]
-> a - r2 ∈ [-20..12]
-254,255c261,262
-< b + r2 ∈ [-4..--]
-< b - r2 ∈ [--..12]
----
-> b + r2 ∈ [-4..28]
-> b - r2 ∈ [-20..12]
-260,263c267,270
-< a + r3 ∈ [-4..--]
-< a - r3 ∈ [--..12]
-< b + r3 ∈ [-4..--]
-< b - r3 ∈ [--..12]
----
-> a + r3 ∈ [-4..28]
-> a - r3 ∈ [-20..12]
-> b + r3 ∈ [-4..28]
-> b - r3 ∈ [-20..12]
-297c304,305
-< {[ k - tmp ∈ {0}
----
-> {[ k + tmp ∈ [-256..272]
-> k - tmp ∈ {0}
-404c412
+358c358
< ct ∈ [--..--] or UNINITIALIZED
---
> ct ∈ [6..127] or UNINITIALIZED
diff --git a/tests/value/oracle_gauges/octagons-pointers-intermediate.res.oracle b/tests/value/oracle_gauges/octagons-pointers-intermediate.res.oracle
index e925f647f0e..993825158c7 100644
--- a/tests/value/oracle_gauges/octagons-pointers-intermediate.res.oracle
+++ b/tests/value/oracle_gauges/octagons-pointers-intermediate.res.oracle
@@ -1,9 +1,8 @@
-28a29,36
-> [eva] computing for function cmdRead <- main.
-> Called from octagons-pointers-intermediate.c:45.
-> [eva] Recording results for cmdRead
-> [eva] Done for function cmdRead
-> [eva] computing for function cmdRead <- main.
-> Called from octagons-pointers-intermediate.c:45.
-> [eva] Recording results for cmdRead
-> [eva] Done for function cmdRead
+23a24,30
+> [eva] octagons-pointers-intermediate.c:42: starting to merge loop iterations
+> [eva] octagons-pointers-intermediate.c:45:
+> Reusing old results for call to cmdRead
+> [eva] octagons-pointers-intermediate.c:45:
+> Reusing old results for call to cmdRead
+> [eva] octagons-pointers-intermediate.c:45:
+> Reusing old results for call to cmdRead
diff --git a/tests/value/oracle_gauges/octagons-pointers-simple.res.oracle b/tests/value/oracle_gauges/octagons-pointers-simple.res.oracle
index 6fd730a78a6..1f0784eedc6 100644
--- a/tests/value/oracle_gauges/octagons-pointers-simple.res.oracle
+++ b/tests/value/oracle_gauges/octagons-pointers-simple.res.oracle
@@ -1,33 +1,32 @@
-65a66,97
+39a40,70
+> [eva] octagons-pointers-simple.c:43: starting to merge loop iterations
> [eva] octagons-pointers-simple.c:46:
> Frama_C_dump_each:
> # octagon:
> {[ buffer - cmd ∈ [-436..-6]
> cmd->cmdLen - cmdLen ∈ {0}
-> size - cmdLen ∈ [8..--]
-> size - cmd->cmdLen ∈ [8..--]
-> size - index ∈ [3..--]
> index + cmdLen ∈ [--..434]
> cmd->cmdLen + index ∈ [--..434]
> ]}
> ==END OF DUMP==
-> [eva] computing for function cmdRead <- main.
-> Called from octagons-pointers-simple.c:47.
-> [eva] Recording results for cmdRead
-> [eva] Done for function cmdRead
+> [eva] octagons-pointers-simple.c:47: Reusing old results for call to cmdRead
> [eva] octagons-pointers-simple.c:46:
> Frama_C_dump_each:
> # octagon:
> {[ buffer - cmd ∈ [-436..-6]
> cmd->cmdLen - cmdLen ∈ {0}
-> size - cmdLen ∈ [8..--]
-> size - cmd->cmdLen ∈ [8..--]
-> size - index ∈ [3..--]
> index + cmdLen ∈ [--..434]
> cmd->cmdLen + index ∈ [--..434]
> ]}
> ==END OF DUMP==
-> [eva] computing for function cmdRead <- main.
-> Called from octagons-pointers-simple.c:47.
-> [eva] Recording results for cmdRead
-> [eva] Done for function cmdRead
+> [eva] octagons-pointers-simple.c:47: Reusing old results for call to cmdRead
+> [eva] octagons-pointers-simple.c:46:
+> Frama_C_dump_each:
+> # octagon:
+> {[ buffer - cmd ∈ [-436..-6]
+> cmd->cmdLen - cmdLen ∈ {0}
+> index + cmdLen ∈ [--..434]
+> cmd->cmdLen + index ∈ [--..434]
+> ]}
+> ==END OF DUMP==
+> [eva] octagons-pointers-simple.c:47: Reusing old results for call to cmdRead
diff --git a/tests/value/oracle_gauges/octagons-pointers.res.oracle b/tests/value/oracle_gauges/octagons-pointers.res.oracle
index 7d34f511670..2c58a7bd206 100644
--- a/tests/value/oracle_gauges/octagons-pointers.res.oracle
+++ b/tests/value/oracle_gauges/octagons-pointers.res.oracle
@@ -1,99 +1,26 @@
-150a151,248
+83a84,108
+> [eva] octagons-pointers.c:43: starting to merge loop iterations
> [eva] octagons-pointers.c:46:
> Frama_C_dump_each:
> # octagon:
> {[ buffer - cmd ∈ [-436..-6]
-> size - cmd->cmdLen ∈ [8..--]
-> size - index ∈ [3..--]
> cmd->cmdLen + index ∈ [--..434]
> ]}
> ==END OF DUMP==
-> [eva] computing for function cmdRead <- main.
-> Called from octagons-pointers.c:47.
-> [eva] octagons-pointers.c:31:
-> Frama_C_dump_each:
-> # octagon:
-> {[ buffer - cmd ∈ [-436..-6]
-> size - cmd->cmdLen ∈ [8..--]
-> buffer - cmd ∈ [-433..-6]
-> cmd - cmd ∈ [-430..427]
-> size - index ∈ [3..--]
-> cmd->cmdLen + index ∈ [--..434]
-> cmd - len ∈ {0}
-> len - cmd ∈ [-430..427]
-> buffer - len ∈ [-433..-6]
-> len - code ∈ {-2}
-> cmd - code ∈ {-2}
-> code - cmd ∈ [-428..429]
-> buffer - code ∈ [-435..-8]
-> code - elt1 ∈ {-1}
-> cmd - elt1 ∈ {-3}
-> len - elt1 ∈ {-3}
-> elt1 - cmd ∈ [-427..430]
-> buffer - elt1 ∈ [-436..-9]
-> elt1 - elt2 ∈ {-4}
-> cmd - elt2 ∈ {-7}
-> len - elt2 ∈ {-7}
-> code - elt2 ∈ {-5}
-> elt2 - cmd ∈ [-423..434]
-> buffer - elt2 ∈ [-440..-13]
-> elt2 - elt3 ∈ {-2}
-> cmd - elt3 ∈ {-9}
-> len - elt3 ∈ {-9}
-> code - elt3 ∈ {-7}
-> elt1 - elt3 ∈ {-6}
-> elt3 - cmd ∈ [-421..436]
-> buffer - elt3 ∈ [-442..-15]
-> ]}
-> ==END OF DUMP==
-> [eva] Recording results for cmdRead
-> [eva] Done for function cmdRead
+> [eva] octagons-pointers.c:47: Reusing old results for call to cmdRead
> [eva] octagons-pointers.c:46:
> Frama_C_dump_each:
> # octagon:
> {[ buffer - cmd ∈ [-436..-6]
-> size - cmd->cmdLen ∈ [8..--]
-> size - index ∈ [3..--]
> cmd->cmdLen + index ∈ [--..434]
> ]}
> ==END OF DUMP==
-> [eva] computing for function cmdRead <- main.
-> Called from octagons-pointers.c:47.
-> [eva] octagons-pointers.c:31:
+> [eva] octagons-pointers.c:47: Reusing old results for call to cmdRead
+> [eva] octagons-pointers.c:46:
> Frama_C_dump_each:
> # octagon:
> {[ buffer - cmd ∈ [-436..-6]
-> size - cmd->cmdLen ∈ [8..--]
-> buffer - cmd ∈ [-433..-6]
-> cmd - cmd ∈ [-430..427]
-> size - index ∈ [3..--]
> cmd->cmdLen + index ∈ [--..434]
-> cmd - len ∈ {0}
-> len - cmd ∈ [-430..427]
-> buffer - len ∈ [-433..-6]
-> len - code ∈ {-2}
-> cmd - code ∈ {-2}
-> code - cmd ∈ [-428..429]
-> buffer - code ∈ [-435..-8]
-> code - elt1 ∈ {-1}
-> cmd - elt1 ∈ {-3}
-> len - elt1 ∈ {-3}
-> elt1 - cmd ∈ [-427..430]
-> buffer - elt1 ∈ [-436..-9]
-> elt1 - elt2 ∈ {-4}
-> cmd - elt2 ∈ {-7}
-> len - elt2 ∈ {-7}
-> code - elt2 ∈ {-5}
-> elt2 - cmd ∈ [-423..434]
-> buffer - elt2 ∈ [-440..-13]
-> elt2 - elt3 ∈ {-2}
-> cmd - elt3 ∈ {-9}
-> len - elt3 ∈ {-9}
-> code - elt3 ∈ {-7}
-> elt1 - elt3 ∈ {-6}
-> elt3 - cmd ∈ [-421..436]
-> buffer - elt3 ∈ [-442..-15]
> ]}
> ==END OF DUMP==
-> [eva] Recording results for cmdRead
-> [eva] Done for function cmdRead
+> [eva] octagons-pointers.c:47: Reusing old results for call to cmdRead
diff --git a/tests/value/oracle_gauges/octagons.res.oracle b/tests/value/oracle_gauges/octagons.res.oracle
index 59771def423..f07f5b7d9bc 100644
--- a/tests/value/oracle_gauges/octagons.res.oracle
+++ b/tests/value/oracle_gauges/octagons.res.oracle
@@ -11,7 +11,7 @@
< [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2147483648..1]
---
> [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2468..1]
-417,420c409,412
+371,374c363,366
< a ∈ [-1024..2147483647]
< b ∈ [-1023..2147483647]
< c ∈ [-1023..2147483647]
@@ -21,7 +21,7 @@
> b ∈ [-181..1867]
> c ∈ [-602..1446]
> d ∈ [-190..1874]
-422c414
+376c368
< d2 ∈ [-2147483648..1]
---
> d2 ∈ [-2468..1]
diff --git a/tests/value/oracle_symblocs/octagons-pointers.res.oracle b/tests/value/oracle_symblocs/octagons-pointers.res.oracle
deleted file mode 100644
index 9dafd7775e8..00000000000
--- a/tests/value/oracle_symblocs/octagons-pointers.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-34,35c34,35
-< cmd - len ∈ {0}
-< len - code ∈ {-2}
----
-> len - cmd ∈ {0}
-> code - len ∈ {2}
--
GitLab