From 0c86eeaaf91a728374642f5721821ce617bc90f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Mon, 12 Apr 2021 12:10:16 +0200 Subject: [PATCH] [Eva] Updates alternative test oracles. --- tests/float/oracle_equalities/const3.1.res.oracle | 2 +- tests/float/oracle_equalities/dr.2.res.oracle | 4 ++-- tests/value/oracle_apron/audit.res.oracle | 11 ----------- tests/value/oracle_bitwise/audit.res.oracle | 11 ----------- tests/value/oracle_equalities/audit.res.oracle | 11 ----------- tests/value/oracle_gauges/audit.res.oracle | 11 ----------- tests/value/oracle_octagons/audit.res.oracle | 11 ----------- tests/value/oracle_symblocs/audit.res.oracle | 11 ----------- 8 files changed, 3 insertions(+), 69 deletions(-) delete mode 100644 tests/value/oracle_apron/audit.res.oracle delete mode 100644 tests/value/oracle_bitwise/audit.res.oracle delete mode 100644 tests/value/oracle_equalities/audit.res.oracle delete mode 100644 tests/value/oracle_gauges/audit.res.oracle delete mode 100644 tests/value/oracle_octagons/audit.res.oracle delete mode 100644 tests/value/oracle_symblocs/audit.res.oracle diff --git a/tests/float/oracle_equalities/const3.1.res.oracle b/tests/float/oracle_equalities/const3.1.res.oracle index 412af6075b5..7de759db471 100644 --- a/tests/float/oracle_equalities/const3.1.res.oracle +++ b/tests/float/oracle_equalities/const3.1.res.oracle @@ -1,4 +1,4 @@ -23c23 +25c25 < d1 ∈ [0x1.16c2000000000p-133 .. 0x1.16c3000000000p-133] --- > d1 ∈ {0x1.16c2000000000p-133} diff --git a/tests/float/oracle_equalities/dr.2.res.oracle b/tests/float/oracle_equalities/dr.2.res.oracle index a95f94eddaa..10fe6f86959 100644 --- a/tests/float/oracle_equalities/dr.2.res.oracle +++ b/tests/float/oracle_equalities/dr.2.res.oracle @@ -1,8 +1,8 @@ -25c25 +27c27 < [eva] tests/float/dr.i:26: Frama_C_show_each: {0; 1}, {0; 1} --- > [eva] tests/float/dr.i:26: Frama_C_show_each: {1}, {0; 1} -30c30 +32c32 < e1 ∈ {0; 1} --- > e1 ∈ {1} diff --git a/tests/value/oracle_apron/audit.res.oracle b/tests/value/oracle_apron/audit.res.oracle deleted file mode 100644 index 9ff41db2488..00000000000 --- a/tests/value/oracle_apron/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_bitwise/audit.res.oracle b/tests/value/oracle_bitwise/audit.res.oracle deleted file mode 100644 index 9ff41db2488..00000000000 --- a/tests/value/oracle_bitwise/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_equalities/audit.res.oracle b/tests/value/oracle_equalities/audit.res.oracle deleted file mode 100644 index 9ff41db2488..00000000000 --- a/tests/value/oracle_equalities/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_gauges/audit.res.oracle b/tests/value/oracle_gauges/audit.res.oracle deleted file mode 100644 index 9ff41db2488..00000000000 --- a/tests/value/oracle_gauges/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_octagons/audit.res.oracle b/tests/value/oracle_octagons/audit.res.oracle deleted file mode 100644 index 9ff41db2488..00000000000 --- a/tests/value/oracle_octagons/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_symblocs/audit.res.oracle b/tests/value/oracle_symblocs/audit.res.oracle deleted file mode 100644 index 9ff41db2488..00000000000 --- a/tests/value/oracle_symblocs/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json -- GitLab