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

[Eva] Updates test oracles.

parent 00ac995c
No related branches found
No related tags found
No related merge requests found
...@@ -228,16 +228,16 @@ ...@@ -228,16 +228,16 @@
[kernel] imprecise.c:114: approximating value to write. [kernel] imprecise.c:114: approximating value to write.
[eva:alarm] imprecise.c:116: Warning: assertion got status unknown. [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
[eva] Recording results for many_writes [eva] Recording results for many_writes
[kernel] imprecise.c:111:
more than 200(300) elements to enumerate. Approximating.
[kernel] imprecise.c:114:
more than 200(300) elements to enumerate. Approximating.
[from] Computing for function many_writes [from] Computing for function many_writes
[kernel] imprecise.c:111: [kernel] imprecise.c:111:
more than 200(300) dependencies to update. Approximating. more than 200(300) dependencies to update. Approximating.
[kernel] imprecise.c:114: [kernel] imprecise.c:114:
more than 200(300) dependencies to update. Approximating. more than 200(300) dependencies to update. Approximating.
[from] Done for function many_writes [from] Done for function many_writes
[kernel] imprecise.c:111:
more than 200(300) elements to enumerate. Approximating.
[kernel] imprecise.c:114:
more than 200(300) elements to enumerate. Approximating.
[eva] Done for function many_writes [eva] Done for function many_writes
[eva] computing for function overlap <- main. [eva] computing for function overlap <- main.
Called from imprecise.c:151. Called from imprecise.c:151.
......
...@@ -6,10 +6,10 @@ ...@@ -6,10 +6,10 @@
x ∈ {0} x ∈ {0}
[eva] replace_by_show_each.c:23: Frama_C_show_each_2: [eva] replace_by_show_each.c:23: Frama_C_show_each_2:
[eva] replace_by_show_each.c:25: Frama_C_show_each_1: [eva] replace_by_show_each.c:25: Frama_C_show_each_1:
[inout] Warning: no assigns clauses for function Frama_C_show_each_1.
Results will be imprecise.
[from] Warning: no assigns clauses for function Frama_C_show_each_1. [from] Warning: no assigns clauses for function Frama_C_show_each_1.
Results will be imprecise. Results will be imprecise.
[inout] Warning: no assigns clauses for function Frama_C_show_each_1.
Results will be imprecise.
[eva:alarm] replace_by_show_each.c:26: Warning: [eva:alarm] replace_by_show_each.c:26: Warning:
signed overflow. assert j + 1 ≤ 2147483647; signed overflow. assert j + 1 ≤ 2147483647;
[eva] Recording results for main [eva] Recording results for main
......
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