diff --git a/tests/float/oracle_equalities/const3.1.res.oracle b/tests/float/oracle_equalities/const3.1.res.oracle index 412af6075b5e836804b4f3c7685e52ef6d66ba06..7de759db47189f2c50ea83d7845623fa5994f43e 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 a95f94eddaafab39b9466d93690939f6fbae3ec4..10fe6f869598523c6f022e1f593f9c0dfd617337 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 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- 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 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- 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 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- 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 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- 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 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- 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 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- 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