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

[Eva] Fixes tests and updates test oracles.

parent 61cbcef3
No related branches found
No related tags found
No related merge requests found
......@@ -233,34 +233,31 @@
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
[eva:malloc] tests/builtins/allocated.c:127:
resizing variable `__malloc_main_l127' (0..31/95) to fit 0..63/127
[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3}
[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] tests/builtins/allocated.c:127:
strong free on bases: {__malloc_main_l127}
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
[eva:malloc] tests/builtins/allocated.c:127:
resizing variable `__malloc_main_l127' (0..31/127) to fit 0..63/159
[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4}
[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] tests/builtins/allocated.c:127:
strong free on bases: {__malloc_main_l127}
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
[eva:malloc] tests/builtins/allocated.c:127:
resizing variable `__malloc_main_l127' (0..31/159) to fit 0..63/191
[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4; 5}
[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] tests/builtins/allocated.c:127:
strong free on bases: {__malloc_main_l127}
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
[eva:malloc] tests/builtins/allocated.c:127:
resizing variable `__malloc_main_l127' (0..31/191) to fit 0..63/319
[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..9]
[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] tests/builtins/allocated.c:127:
strong free on bases: {__malloc_main_l127}
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
[eva:malloc] tests/builtins/allocated.c:127:
resizing variable `__malloc_main_l127' (0..31/319) to fit 0..63/319
[eva] Recording results for main
[eva] done for function main
[eva] tests/builtins/allocated.c:27:
......@@ -279,7 +276,8 @@
size ∈ [1..100]
pb ∈ ESCAPINGADDR
__retres ∈ {0}
__malloc_w_main_l82[0..2] ∈ [7..27] or UNINITIALIZED
__malloc_w_main_l82[0..1] ∈ [7..2147483647] or UNINITIALIZED
[2] ∈ [7..27] or UNINITIALIZED
[from] Computing for function main
[from] Computing for function malloc <-main
[from] Done for function malloc
......
......@@ -369,6 +369,8 @@
[eva] tests/idct/ieee_1180_1990.c:215: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:234: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:233: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:235: Warning:
2's complement assumed for overflow
[eva] computing for function IEEE_1180_1990_dctf <- main.
Called from tests/idct/ieee_1180_1990.c:236.
[eva] Recording results for IEEE_1180_1990_dctf
......@@ -446,6 +448,8 @@
[eva] tests/idct/ieee_1180_1990.c:277: Warning:
2's complement assumed for overflow
[eva] tests/idct/ieee_1180_1990.c:261: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:281: Warning:
2's complement assumed for overflow
[eva] tests/idct/ieee_1180_1990.c:280: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:279: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:282:
......@@ -518,6 +522,8 @@
[eva] tests/idct/ieee_1180_1990.c:323: Warning:
2's complement assumed for overflow
[eva] tests/idct/ieee_1180_1990.c:307: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:327: Warning:
2's complement assumed for overflow
[eva] tests/idct/ieee_1180_1990.c:326: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:325: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:328:
......@@ -898,7 +904,7 @@
[eva:final-states] Values at end of function IEEE_1180_1990_mkbk:
i ∈ {8}
j ∈ {8} or UNINITIALIZED
M1[0..7][0..7] ∈ [-2147483647..2147483647]
M1[0..7][0..7] ∈ [--..--]
IEEE_1180_1990_rand_randx ∈ [--..--]
[eva:final-states] Values at end of function IEEE_1180_1990_dctf:
i ∈ {8}
......@@ -951,7 +957,7 @@
omse ∈ [--..--] or UNINITIALIZED
ome ∈ [--..--] or UNINITIALIZED
err ∈ [--..--] or UNINITIALIZED
M1[0..7][0..7] ∈ [-2147483647..2147483647]
M1[0..7][0..7] ∈ [--..--]
IEEE_1180_1990_rand_randx ∈ [--..--]
IEEE_1180_1990_dctf_mcos[0..7][0..7] ∈
[-1.0000000000000000*2^-1 .. 1.0000000000000000*2^-1]
......
/* run.config*
STDOPT: +"-then -wlevel 4"
STDOPT: +"-then -eva-widening-delay 4 -eva-widening-period 3"
*/
int T[3] = {3,1,2};
......
......@@ -21,7 +21,7 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
G ∈ {5; 7; 15; 99}
G ∈ [5..99],1%2
i ∈ {3}
j ∈ {1; 2; 3; 4; 77}
[from] Computing for function main
......
/* run.config*
STDOPT: +"-then -inout -load-module report -report -then -plevel 250"
STDOPT: +"-eva-widening-period 3 -then -inout -load-module report -report -then -plevel 250"
*/
struct s {
......
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