Skip to content
Snippets Groups Projects
Commit 21d13d05 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

[Eva] update oracles

- for imprecise.i, the equality domain does not keep an equality with
  sizeof since the sizeof is now normalized to it's constant equivalent;
  the dependency to a variable of an incomplete type disapear
- for the other tests only the order of string bases changes
parent 333eff76
No related branches found
No related tags found
No related merge requests found
98a99,100
> [kernel] imprecise.c:51:
> imprecise size for variable v3 (abstract type 'struct u')
220a223,224
220a221,222
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
228a233,234
228a231,232
> [kernel] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
237,240d242
237,240d240
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
< [kernel] imprecise.c:114:
......
......@@ -41,8 +41,8 @@
x FROM \nothing
y FROM \nothing
S___fc_stdout[0].__fc_FILE_data
FROM S___fc_stdout[0]; "%d\n"; "%d\n"; "%d\n"; "%d\n";
"%d,%d\n"[bits 0 to 55] (and SELF)
FROM S___fc_stdout[0]; "%d\n"; "%d\n";
"%d,%d\n"[bits 0 to 55]; "%d\n"; "%d\n" (and SELF)
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function f:
......@@ -52,5 +52,5 @@
[inout] Out (internal) for function main:
x; y; S___fc_stdout[0].__fc_FILE_data
[inout] Inputs for function main:
x; y; S___fc_stdout[0]; "%d\n"; "%d\n"; "%d\n"; "%d\n";
"%d,%d\n"[bits 0 to 55]
x; y; S___fc_stdout[0]; "%d\n"; "%d\n"; "%d,%d\n"[bits 0 to 55]; "%d\n";
"%d\n"
......@@ -33,11 +33,11 @@
[eva:alarm] nonlin.c:38: Warning:
signed overflow.
assert (int)((int)z + 17817) * (int)((int)z + 17817) ≤ 2147483647;
[eva:nonlin] nonlin.c:45: non-linear 'i1 * i1', lv 'i1'
[eva:nonlin] nonlin.c:45:
non-linear '(i2 + (long long)3) * (i2 + (long long)3)', lv 'i2'
[eva:nonlin] nonlin.c:45: non-linear 'i1 * i1', lv 'i1'
[eva:nonlin] nonlin.c:45: subdividing on i2
[eva:nonlin] nonlin.c:45: subdividing on i1
[eva:nonlin] nonlin.c:45: subdividing on i2
[eva:alarm] nonlin.c:49: Warning: assertion got status unknown.
[eva:nonlin] nonlin.c:50: non-linear '(int)idx * (int)idx', lv 'idx'
[eva:nonlin] nonlin.c:50: subdividing on idx
......
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