From 7b46f86075584d520c6fdfe2fac91dff5303c833 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Thu, 20 Dec 2018 16:24:37 +0100 Subject: [PATCH] [Eva] Updates alternative test oracles. The bitwise domain is less useful since the ival bitwise operators are more precise. --- tests/idct/diff_bitwise | 5 ----- tests/value/diff_bitwise | 28 ++-------------------------- 2 files changed, 2 insertions(+), 31 deletions(-) diff --git a/tests/idct/diff_bitwise b/tests/idct/diff_bitwise index 19f21ca2757..e69de29bb2d 100644 --- a/tests/idct/diff_bitwise +++ b/tests/idct/diff_bitwise @@ -1,5 +0,0 @@ -diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_bitwise/ieee_1180_1990.res.oracle -920c920 -< i ∈ [0..2147483646] ---- -> i ∈ [0..2147483646],0%2 diff --git a/tests/value/diff_bitwise b/tests/value/diff_bitwise index 29219259f93..be860471315 100644 --- a/tests/value/diff_bitwise +++ b/tests/value/diff_bitwise @@ -9,35 +9,20 @@ diff tests/value/oracle/addition.res.oracle tests/value/oracle_bitwise/addition. > {{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:52}) }} 130a130 > {{ garbled mix of &{p2} (origin: Misaligned {tests/value/addition.i:56}) }} -166,169c166,167 +166,168c166 < p10 ∈ < {{ garbled mix of &{p1} < (origin: Arithmetic {tests/value/addition.i:52}) }} -< p11 ∈ [-2147483648..0] --- > p10 ∈ {{ garbled mix of &{p1} }} -> p11 ∈ [-2147483648..0],0%4 358a357 > {{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:52}) }} -397,400c396,397 +397,399c396 < p10 ∈ < {{ garbled mix of &{p1} < (origin: Arithmetic {tests/value/addition.i:52}) }} -< p11 ∈ [-2147483648..0] --- > p10 ∈ {{ garbled mix of &{p1} }} -> p11 ∈ [-2147483648..0],0%4 -diff tests/value/oracle/bitwise_or.res.oracle tests/value/oracle_bitwise/bitwise_or.res.oracle -57c57 -< uand4 ∈ [8..24] ---- -> uand4 ∈ {8; 16; 24} -63,64c63,64 -< v1 ∈ [0..0x1FFFE],0%2 -< v2 ∈ [0..0x3FFFF] ---- -> v1 ∈ [0..0x1FFFC],0%4 -> v2 ∈ [0..0x3FFFE],0%2 diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_bitwise/bitwise_pointer.res.oracle 32,34c32 < [eva] tests/value/bitwise_pointer.i:18: @@ -51,15 +36,6 @@ diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_bitwise/bi < The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:22} --- > [eva] tests/value/bitwise_pointer.i:22: Assigning imprecise value to p1. -diff tests/value/oracle/cast.res.oracle tests/value/oracle_bitwise/cast.res.oracle -71c71 -< G ∈ [0..12] ---- -> G ∈ [2..12] -89c89 -< G ∈ [0..12] ---- -> G ∈ [2..12] diff tests/value/oracle/logic_ptr_cast.res.oracle tests/value/oracle_bitwise/logic_ptr_cast.res.oracle 8,10c8 < [eva] tests/value/logic_ptr_cast.i:8: -- GitLab