Skip to content
Snippets Groups Projects
Commit 7b46f860 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Updates alternative test oracles.

The bitwise domain is less useful since the ival bitwise operators are more
precise.
parent 1597211b
No related branches found
No related tags found
No related merge requests found
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
......@@ -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:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment