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

[Eva] Updates test oracles.

parent ae7a94b1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/value/oracle/addition.res.oracle
+ 0
− 34
View file @ ce1b5d31
...@@ -148,23 +148,6 @@ ...@@ -148,23 +148,6 @@
[eva] addition.i:88: assertion got status valid. [eva] addition.i:88: assertion got status valid.
[eva] Recording results for main [eva] Recording results for main
[eva] Done for function main [eva] Done for function main
[eva:garbled-mix:summary] Warning:
Garbled mix generated during analysis:
{{ garbled mix of &{p3} (origin: Arithmetic {addition.i:34}) }}
{{ garbled mix of &{p2} (origin: Arithmetic {addition.i:34}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:36}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:38}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:40}) }}
{{ garbled mix of &{p2} (origin: Arithmetic {addition.i:42}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:42}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:44}) }}
{{ garbled mix of &{p2} (origin: Arithmetic {addition.i:46}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:50}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
{{ garbled mix of &{p2} (origin: Arithmetic {addition.i:56}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:56}) }}
{{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
{{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
[scope:rm_asserts] removing 9 assertion(s) [scope:rm_asserts] removing 9 assertion(s)
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
...@@ -390,23 +373,6 @@ ...@@ -390,23 +373,6 @@
[eva] addition.i:87: Frama_C_show_each_1: [-10..15] [eva] addition.i:87: Frama_C_show_each_1: [-10..15]
[eva] Recording results for main [eva] Recording results for main
[eva] Done for function main [eva] Done for function main
[eva:garbled-mix:summary] Warning:
Garbled mix generated during analysis:
{{ garbled mix of &{p3} (origin: Arithmetic {addition.i:34}) }}
{{ garbled mix of &{p2} (origin: Arithmetic {addition.i:34}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:36}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:38}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:40}) }}
{{ garbled mix of &{p2} (origin: Arithmetic {addition.i:42}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:42}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:44}) }}
{{ garbled mix of &{p2} (origin: Arithmetic {addition.i:46}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:50}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
{{ garbled mix of &{p2} (origin: Arithmetic {addition.i:56}) }}
{{ garbled mix of &{p1} (origin: Arithmetic {addition.i:56}) }}
{{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
{{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
[scope:rm_asserts] removing 9 assertion(s) [scope:rm_asserts] removing 9 assertion(s)
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
......
tests/value/oracle/backward_add_ptr.res.oracle
+ 3
− 25
View file @ ce1b5d31
...@@ -182,31 +182,9 @@ ...@@ -182,31 +182,9 @@
[eva] Recording results for main [eva] Recording results for main
[eva] Done for function main [eva] Done for function main
[eva:garbled-mix:summary] Warning: [eva:garbled-mix:summary] Warning:
Garbled mix generated during analysis: Origins of garbled mix generated during analysis:
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:25}) }} backward_add_ptr.c:68: arithmetic operation on addresses
{{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:25}) }} (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:32}) }}
{{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:32}) }}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:38}) }}
{{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:38}) }}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:54}) }}
{{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:54}) }}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:60}) }}
{{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:60}) }}
{{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:68}) }}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:81}) }}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:87}) }}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:96}) }}
{{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:68}) }}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:106}) }}
{{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:115}) }}
{{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:115}) }}
{{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:121}) }}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:130}) }}
{{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:136}) }}
{{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:68}) }}
{{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:68}) }}
{{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:68}) }}
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function gm: [eva:final-states] Values at end of function gm:
__retres ∈ __retres ∈
......
tests/value/oracle/join_misaligned.res.oracle
+ 0
− 4
View file @ ce1b5d31
...@@ -20,10 +20,6 @@ ...@@ -20,10 +20,6 @@
pointer downcast. assert (unsigned int)(&u) ≤ 2147483647; pointer downcast. assert (unsigned int)(&u) ≤ 2147483647;
[eva] Recording results for main [eva] Recording results for main
[eva] Done for function main [eva] Done for function main
[eva:garbled-mix:summary] Warning:
Garbled mix generated during analysis:
{{ garbled mix of &{t} (origin: Merge {join_misaligned.i:42}) }}
{{ garbled mix of &{u} (origin: Merge {join_misaligned.i:42}) }}
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
t{[0]; [1][bits 0 to 15]} ∈ {0} t{[0]; [1][bits 0 to 15]} ∈ {0}
......
tests/value/oracle/struct3.res.oracle
+ 0
− 3
View file @ ce1b5d31
...@@ -28,9 +28,6 @@ ...@@ -28,9 +28,6 @@
The imprecision originates from Arithmetic {struct3.i:46} The imprecision originates from Arithmetic {struct3.i:46}
[eva] Recording results for main [eva] Recording results for main
[eva] Done for function main [eva] Done for function main
[eva:garbled-mix:summary] Warning:
Garbled mix generated during analysis:
{{ garbled mix of &{s1} (origin: Arithmetic {struct3.i:46}) }}
[eva] struct3.i:42: assertion 'Eva,index_bound' got final status invalid. [eva] struct3.i:42: assertion 'Eva,index_bound' got final status invalid.
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment