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

[Eva] Updates alternative oracles.

parent 2dc27a4a
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
tests/builtins/diff_apron
+ 6
− 19
View file @ 9a647053
......@@ -8,27 +8,14 @@ diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_a
---
> tests/builtins/result_apron/Longinit_sequencer.sav
diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_apron/allocated.0.res.oracle
243c243
< [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]
250c250
< [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]
257c257
< [eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..9]
---
> [eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
276c276
260a261,263
> [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
273c276
< j ∈ [1..2147483647]
---
> j ∈ [1..12]
282,283c282
< __malloc_w_main_l82[0..1] ∈ [7..2147483647] or UNINITIALIZED
< [2] ∈ [7..27] or UNINITIALIZED
---
> __malloc_w_main_l82[0..2] ∈ [7..27] or UNINITIALIZED
> j ∈ [1..10]
diff tests/builtins/oracle/memexec-malloc.res.oracle tests/builtins/oracle_apron/memexec-malloc.res.oracle
20c20,23
< [eva] tests/builtins/memexec-malloc.c:25: Reusing old results for call to f
......
tests/idct/diff_apron
+ 501
− 338
View file @ 9a647053
This diff is collapsed.
tests/idct/diff_equalities
+ 53
− 57
View file @ 9a647053
diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_equalities/ieee_1180_1990.res.oracle
331a332,333
355a356,357
> [eva] tests/idct/ieee_1180_1990.c:219: Warning:
> 2's complement assumed for overflow
335a338,339
359a362,363
> [eva] tests/idct/ieee_1180_1990.c:220: Warning:
> 2's complement assumed for overflow
341,342d344
365,366d368
< [eva] tests/idct/ieee_1180_1990.c:219: Warning:
< 2's complement assumed for overflow
365a368,369
391a394,395
> [eva] tests/idct/ieee_1180_1990.c:243: Warning:
> 2's complement assumed for overflow
369a374,375
395a400,401
> [eva] tests/idct/ieee_1180_1990.c:244: Warning:
> 2's complement assumed for overflow
375,376d380
401,402d406
< [eva] tests/idct/ieee_1180_1990.c:243: Warning:
< 2's complement assumed for overflow
397a402,405
423a428,435
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
410a419,420
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
436a449,450
> [eva] tests/idct/ieee_1180_1990.c:265: Warning:
> 2's complement assumed for overflow
414a425,426
440a455,456
> [eva] tests/idct/ieee_1180_1990.c:266: Warning:
> 2's complement assumed for overflow
420,421d431
446,447d461
< [eva] tests/idct/ieee_1180_1990.c:265: Warning:
< 2's complement assumed for overflow
437a448,449
465a480,481
> [eva] tests/idct/ieee_1180_1990.c:289: Warning:
> 2's complement assumed for overflow
441a454,455
469a486,487
> [eva] tests/idct/ieee_1180_1990.c:290: Warning:
> 2's complement assumed for overflow
447,448d460
475,476d492
< [eva] tests/idct/ieee_1180_1990.c:289: Warning:
< 2's complement assumed for overflow
469a482,485
497a514,521
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
482a499,500
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
510a535,536
> [eva] tests/idct/ieee_1180_1990.c:311: Warning:
> 2's complement assumed for overflow
486a505,506
514a541,542
> [eva] tests/idct/ieee_1180_1990.c:312: Warning:
> 2's complement assumed for overflow
492,493d511
520,521d547
< [eva] tests/idct/ieee_1180_1990.c:311: Warning:
< 2's complement assumed for overflow
509a528,529
539a566,567
> [eva] tests/idct/ieee_1180_1990.c:335: Warning:
> 2's complement assumed for overflow
513a534,535
543a572,573
> [eva] tests/idct/ieee_1180_1990.c:336: Warning:
> 2's complement assumed for overflow
519,520d540
549,550d578
< [eva] tests/idct/ieee_1180_1990.c:335: Warning:
< 2's complement assumed for overflow
540a561,564
570a599,606
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
548a573,578
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
578a615,632
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:101:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
550a581,582
> [eva] tests/idct/ieee_1180_1990.c:101:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
552a585,590
> [eva] tests/idct/ieee_1180_1990.c:101:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:101:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
574a613,618
580a635,636
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
582a639,640
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
604a663,676
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:141:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
576a621,622
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
578a625,630
> [eva] tests/idct/ieee_1180_1990.c:141:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:141:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
620a673,676
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
650a707,710
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
680a741,744
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
688a753,754
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
690a757,762
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:101:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:100:
606a679,680
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
692a765,770
> [eva] tests/idct/ieee_1180_1990.c:100:
608a683,688
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:101:
> [eva] tests/idct/ieee_1180_1990.c:141:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:100:
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
tests/idct/diff_gauges
+ 2
− 63
View file @ 9a647053
diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_gauges/ieee_1180_1990.res.oracle
51a52,55
> [eva] tests/idct/idct.c:90: Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/idct.c:91: Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/idct.c:90: Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/idct.c:91: Call to builtin Frama_C_cos for function cos
150a155,158
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
198a207,214
578a579,580
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:101:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:101:
> Call to builtin Frama_C_cos for function cos
280a297,304
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:141:
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:141:
> Call to builtin Frama_C_cos for function cos
548a573,574
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
574a601,602
604a607,608
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
688a717,718
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
891a922,950
> [eva] tests/idct/ieee_1180_1990.c:236:
> Reusing old results for call to IEEE_1180_1990_dctf
> [eva] tests/idct/ieee_1180_1990.c:237:
> Reusing old results for call to IEEE_1180_1990_idctf
> [eva] tests/idct/ieee_1180_1990.c:238: Reusing old results for call to idct
> [eva] tests/idct/ieee_1180_1990.c:257:
> Reusing old results for call to IEEE_1180_1990_mkbk
> [eva] tests/idct/ieee_1180_1990.c:258:
> Reusing old results for call to IEEE_1180_1990_dctf
> [eva] tests/idct/ieee_1180_1990.c:259:
> Reusing old results for call to IEEE_1180_1990_idctf
> [eva] tests/idct/ieee_1180_1990.c:260: Reusing old results for call to idct
> [eva] tests/idct/ieee_1180_1990.c:282:
> Reusing old results for call to IEEE_1180_1990_dctf
> [eva] tests/idct/ieee_1180_1990.c:283:
> Reusing old results for call to IEEE_1180_1990_idctf
> [eva] tests/idct/ieee_1180_1990.c:284: Reusing old results for call to idct
> [eva] tests/idct/ieee_1180_1990.c:303:
> Reusing old results for call to IEEE_1180_1990_mkbk
> [eva] tests/idct/ieee_1180_1990.c:304:
> Reusing old results for call to IEEE_1180_1990_dctf
> [eva] tests/idct/ieee_1180_1990.c:305:
> Reusing old results for call to IEEE_1180_1990_idctf
> [eva] tests/idct/ieee_1180_1990.c:306: Reusing old results for call to idct
> [eva] tests/idct/ieee_1180_1990.c:328:
> Reusing old results for call to IEEE_1180_1990_dctf
> [eva] tests/idct/ieee_1180_1990.c:329:
> Reusing old results for call to IEEE_1180_1990_idctf
> [eva] tests/idct/ieee_1180_1990.c:330: Reusing old results for call to idct
tests/value/diff_apron
+ 52
− 90
View file @ 9a647053
......@@ -265,91 +265,80 @@ diff tests/value/oracle/fun_ptr.1.res.oracle tests/value/oracle_apron/fun_ptr.1.
> [eva] Recording results for f
> [eva] Done for function f
diff tests/value/oracle/gauges.res.oracle tests/value/oracle_apron/gauges.res.oracle
32,35d31
< [eva] tests/value/gauges.c:19: Frama_C_show_each_0: {{ "in" }}
< [eva] tests/value/gauges.c:21: Frama_C_show_each_1: {{ "in" }}
38,39d37
< [eva:alarm] tests/value/gauges.c:26: Warning:
< signed overflow. assert l + 1 ≤ 2147483647;
60,63d55
< [eva] tests/value/gauges.c:41: Frama_C_show_each_0: {{ "in" }}
< [eva] tests/value/gauges.c:43: Frama_C_show_each_1: {{ "in" }}
70,71d67
< [eva:alarm] tests/value/gauges.c:48: Warning:
< signed overflow. assert l + 1 ≤ 2147483647;
104a97,99
> [eva] tests/value/gauges.c:83: Frama_C_show_each: {{ "outer" }}
> [eva] tests/value/gauges.c:78: starting to merge loop iterations
> [eva] tests/value/gauges.c:80: Frama_C_show_each: {{ "inner" }}
110,114d104
< [eva] tests/value/gauges.c:78: starting to merge loop iterations
< [eva] tests/value/gauges.c:80: Frama_C_show_each: {{ "inner" }}
< [eva] tests/value/gauges.c:83: Frama_C_show_each: {{ "outer" }}
< [eva] tests/value/gauges.c:80: Frama_C_show_each: {{ "inner" }}
< [eva] tests/value/gauges.c:83: Frama_C_show_each: {{ "outer" }}
117c107
113,114d108
< [eva:alarm] tests/value/gauges.c:81: Warning:
< signed overflow. assert k + 1 ≤ 2147483647;
116,117d109
< [eva:alarm] tests/value/gauges.c:84: Warning:
< signed overflow. assert k + 1 ≤ 2147483647;
123a116,117
> [eva:alarm] tests/value/gauges.c:81: Warning:
> signed overflow. assert k + 1 ≤ 2147483647;
125c119,121
< [eva] tests/value/gauges.c:86: Frama_C_show_each: [0..2147483647]
---
> [eva:alarm] tests/value/gauges.c:84: Warning:
> signed overflow. assert k + 1 ≤ 2147483647;
> [eva] tests/value/gauges.c:86: Frama_C_show_each: [15..2147483647]
131,132d120
139,140d134
< [eva:alarm] tests/value/gauges.c:99: Warning:
< signed overflow. assert c + 1 ≤ 2147483647;
179,180d166
187,188d180
< [eva:alarm] tests/value/gauges.c:140: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
291,292d276
299,300d290
< [eva:alarm] tests/value/gauges.c:220: Warning:
< signed overflow. assert -2147483648 ≤ n - 1;
307,308d290
315,316d304
< [eva:alarm] tests/value/gauges.c:240: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
310c292
318c306
< Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..2147483647]
---
> Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..46]
316,317d297
324,325d311
< [eva:alarm] tests/value/gauges.c:251: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
319c299
327c313
< Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..2147483647]
---
> Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..49]
325,326d304
333,334d318
< [eva:alarm] tests/value/gauges.c:263: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
328c306
336c320
< Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..2147483647]
---
> Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..65]
334,335d311
342,343d325
< [eva:alarm] tests/value/gauges.c:274: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
337c313
345c327
< Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..2147483647]
---
> Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..70]
345,346d320
353,354d334
< [eva:alarm] tests/value/gauges.c:293: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
348c322
356c336
< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
---
> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..598]
716c690
< l ∈ [4..2147483647]
---
> l ∈ [4..101]
721c695
< l ∈ [4..2147483647]
---
> l ∈ [4..101]
772c746
780c760
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
775c749
783c763
< i ∈ [0..2147483647]
---
> i ∈ [10..2147483647]
811c785
819c799
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
......@@ -748,7 +737,9 @@ diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_apron/pr
> Called from tests/value/precise_locations.i:39.
> [eva] Recording results for ct
> [eva] Done for function ct
37,40c49,64
37,42c49,72
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
......@@ -770,14 +761,17 @@ diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_apron/pr
> Called from tests/value/precise_locations.i:39.
> [eva] Recording results for ct
> [eva] Done for function ct
193,198d216
< [eva] Done for function f
< [eva] computing for function g <- main.
< Called from tests/value/precise_locations.i:49.
< [eva] Done for function g
< [eva] computing for function f <- main.
< Called from tests/value/precise_locations.i:48.
518,525c536,567
> [eva] computing for function ct <- main.
> Called from tests/value/precise_locations.i:39.
> [eva] Recording results for ct
> [eva] Done for function ct
> [eva] computing for function ct <- main.
> Called from tests/value/precise_locations.i:39.
> [eva] Recording results for ct
> [eva] Done for function ct
520,529c550,589
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
......@@ -819,13 +813,14 @@ diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_apron/pr
> Called from tests/value/precise_locations.i:39.
> [eva] Recording results for ct
> [eva] Done for function ct
736,741d777
< [eva] computing for function f <- main.
< Called from tests/value/precise_locations.i:48.
< [eva] Done for function f
< [eva] computing for function g <- main.
< Called from tests/value/precise_locations.i:49.
< [eva] Done for function g
> [eva] computing for function ct <- main.
> Called from tests/value/precise_locations.i:39.
> [eva] Recording results for ct
> [eva] Done for function ct
> [eva] computing for function ct <- main.
> Called from tests/value/precise_locations.i:39.
> [eva] Recording results for ct
> [eva] Done for function ct
diff tests/value/oracle/precond.res.oracle tests/value/oracle_apron/precond.res.oracle
49a50,51
> [eva] computing for function f <- main.
......@@ -977,39 +972,6 @@ diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_apron/unroll
< j ∈ [-2147483648..-126]
---
> j ∈ {-250}
diff tests/value/oracle/widen_non_constant.res.oracle tests/value/oracle_apron/widen_non_constant.res.oracle
25c25
< Frama_C_show_each_in: {0; 1; 2}, [1..23]
---
> Frama_C_show_each_in: [0..22], [1..23]
27,28d26
< [eva] tests/value/widen_non_constant.i:13:
< Frama_C_show_each_in: [0..23], [1..23]
44c42
< Frama_C_show_each_in: {0; 1; 2}, [1..23]
---
> Frama_C_show_each_in: [0..22], [1..23]
46,47d43
< [eva] tests/value/widen_non_constant.i:29:
< Frama_C_show_each_in: [0..25], [1..23]
63c59
< Frama_C_show_each_in: {0; 1; 2}, [1..23]
---
> Frama_C_show_each_in: [0..22], [1..23]
65,70d60
< [eva] tests/value/widen_non_constant.i:48:
< Frama_C_show_each_in: [0..2147483647], [1..23]
< [eva:alarm] tests/value/widen_non_constant.i:49: Warning:
< out of bounds read. assert \valid_read(p + j);
< [eva:alarm] tests/value/widen_non_constant.i:45: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
91c81
< j ∈ {23; 24; 25; 26}
---
> j ∈ {23; 24; 25}
diff tests/value/oracle/widen_on_non_monotonic.res.oracle tests/value/oracle_apron/widen_on_non_monotonic.res.oracle
22a23
> [eva] tests/value/widen_on_non_monotonic.i:26: starting to merge loop iterations
diff tests/value/oracle/with_comment.res.oracle tests/value/oracle_apron/with_comment.res.oracle
9,10d8
< [eva:alarm] tests/value/with_comment.i:21: Warning:
......
tests/value/diff_gauges
+ 42
− 89
View file @ 9a647053
......@@ -38,10 +38,6 @@ diff tests/value/oracle/for_loops.2.res.oracle tests/value/oracle_gauges/for_loo
< [eva] tests/value/for_loops.c:43: Frama_C_show_each: [0..2147483647]
---
> [eva] tests/value/for_loops.c:43: Frama_C_show_each: [0..1000]
diff tests/value/oracle/for_loops.3.res.oracle tests/value/oracle_gauges/for_loops.3.res.oracle
11a12,13
> Frama_C_show_each_F: {0; 1; 2}, [0..2147483647]
> [eva] tests/value/for_loops.c:55:
diff tests/value/oracle/from_termin.res.oracle tests/value/oracle_gauges/from_termin.res.oracle
9a10
> [eva] tests/value/from_termin.i:8: starting to merge loop iterations
......@@ -49,41 +45,41 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
25,26d24
< [eva:alarm] tests/value/gauges.c:23: Warning:
< signed overflow. assert -2147483648 ≤ j - 4;
34,35d31
38,39d35
< [eva:alarm] tests/value/gauges.c:26: Warning:
< signed overflow. assert l + 1 ≤ 2147483647;
53,54d48
57,58d52
< [eva:alarm] tests/value/gauges.c:45: Warning:
< signed overflow. assert -2147483648 ≤ j - 4;
57a52,53
61a56,57
> [eva:alarm] tests/value/gauges.c:45: Warning:
> signed overflow. assert -2147483648 ≤ j - 4;
62,63d57
70,71d65
< [eva:alarm] tests/value/gauges.c:48: Warning:
< signed overflow. assert l + 1 ≤ 2147483647;
75,76d68
83,84d76
< [eva:alarm] tests/value/gauges.c:58: Warning:
< accessing out of bounds index. assert j < 38;
89,93d80
97,101d88
< [eva:alarm] tests/value/gauges.c:71: Warning:
< out of bounds write. assert \valid(tmp);
< (tmp from p++)
< [eva] tests/value/gauges.c:72: Frama_C_show_each:
< [eva] tests/value/gauges.c:72: Frama_C_show_each:
105,106d91
113,114d99
< [eva:alarm] tests/value/gauges.c:81: Warning:
< signed overflow. assert k + 1 ≤ 2147483647;
108,109d92
116,117d100
< [eva:alarm] tests/value/gauges.c:84: Warning:
< signed overflow. assert k + 1 ≤ 2147483647;
117c100
125c108
< [eva] tests/value/gauges.c:86: Frama_C_show_each: [0..2147483647]
---
> [eva] tests/value/gauges.c:86: Frama_C_show_each: {390}
131,132d113
139,140d121
< [eva:alarm] tests/value/gauges.c:99: Warning:
< signed overflow. assert c + 1 ≤ 2147483647;
170,173c151,154
178,181c159,162
< [eva] tests/value/gauges.c:129: Frama_C_show_each: {{ &y + [4..36],0%4 }}
< [eva] tests/value/gauges.c:129: Frama_C_show_each: {{ &y + [4..40],0%4 }}
< [eva:alarm] tests/value/gauges.c:130: Warning:
......@@ -93,93 +89,93 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
> Frama_C_show_each: {{ &y + {4; 8; 12; 16; 20; 24} }}
> [eva] tests/value/gauges.c:129:
> Frama_C_show_each: {{ &y + {4; 8; 12; 16; 20; 24} }}
179,180d159
187,188d167
< [eva:alarm] tests/value/gauges.c:140: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
198,200d176
206,208d184
< [eva:alarm] tests/value/gauges.c:158: Warning:
< out of bounds write. assert \valid(tmp);
< (tmp from p--)
247,250d222
255,258d230
< [eva:alarm] tests/value/gauges.c:192: Warning:
< out of bounds write. assert \valid(p);
< [eva:alarm] tests/value/gauges.c:193: Warning:
< out of bounds write. assert \valid(q);
258,263d229
266,271d237
< [eva:alarm] tests/value/gauges.c:202: Warning:
< out of bounds read. assert \valid_read(tmp);
< (tmp from A++)
< [eva:alarm] tests/value/gauges.c:202: Warning:
< out of bounds read. assert \valid_read(tmp_0);
< (tmp_0 from B++)
307,310c273
315,318c281
< [eva:alarm] tests/value/gauges.c:240: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
< [eva] tests/value/gauges.c:242:
< Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..2147483647]
---
> [eva] tests/value/gauges.c:242: Frama_C_show_each: {47; 48}, {6}
316,317d278
324,325d286
< [eva:alarm] tests/value/gauges.c:251: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
319c280
327c288
< Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..2147483647]
---
> Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, {6; 7}
325,328c286
333,336c294
< [eva:alarm] tests/value/gauges.c:263: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
< [eva] tests/value/gauges.c:265:
< Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..2147483647]
---
> [eva] tests/value/gauges.c:265: Frama_C_show_each: {-58; -57}, {9}
334,335d291
342,343d299
< [eva:alarm] tests/value/gauges.c:274: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
337c293
345c301
< Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..2147483647]
---
> Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, {9; 10}
345,346d300
353,354d308
< [eva:alarm] tests/value/gauges.c:293: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
348c302
356c310
< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
---
> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [99..119]
407a362,365
415a370,373
> # Gauges domain:
> V: [{[ p -> {{ &x }}
> i -> {1} ]}]
> s395: λ(0)
464a423,426
472a431,434
> # Gauges domain:
> V: [{[ i -> {1} ]}]
> s395: λ([0 .. 1])
> {[ i -> {1} ]}
520a483,486
528a491,494
> # Gauges domain:
> V: [{[ i -> {1} ]}]
> s395: λ([0 .. 2])
> {[ i -> {1} ]}
576a543,546
584a551,554
> # Gauges domain:
> V: [{[ i -> {1} ]}]
> s395: λ([0 .. 10])
> {[ i -> {1} ]}
638a609,613
646a617,621
> # Gauges domain:
> V: [{[ p -> {{ &a }}
> i -> {2} ]}]
> s409: λ(0)
> s408: λ(0)
696a672,676
704a680,684
> # Gauges domain:
> V: [{[ i -> {2} ]}]
> s409: λ(0)
> s408: λ([0 .. 1])
> {[ i -> {0} ]}
698a679,800
706a687,808
> [eva] tests/value/gauges.c:325:
> Frama_C_dump_each:
> # Cvalue domain:
......@@ -302,61 +298,53 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
> s408: λ([0 .. +oo])
> {[ i -> {0} ]}
> ==END OF DUMP==
706a809,810
714a817,818
> [eva] tests/value/gauges.c:343: Call to builtin malloc
> [eva] tests/value/gauges.c:343: Call to builtin malloc
716c820
< l ∈ [4..2147483647]
---
> l ∈ [4..53]
721c825
< l ∈ [4..2147483647]
---
> l ∈ [4..53]
759,760c863,864
767,768c871,872
< A ∈ {{ &A + [0..--],0%4 }}
< B ∈ {{ &B + [0..--],0%4 }}
---
> A ∈ {{ &A + [0..36],0%4 }}
> B ∈ {{ &B + [0..36],0%4 }}
778c882
786c890
< i ∈ {45; 46; 47; 48; 49; 50; 51}
---
> i ∈ {45; 46; 47; 48}
784c888
792c896
< i ∈ {-59; -58; -57; -56; -55; -54; -53}
---
> i ∈ {-58; -57; -56; -55; -54; -53}
804c908
812c916
< p ∈ {{ &u + [0..--],0%4 }}
---
> p ∈ {{ &u + [0..400],0%4 }}
806c910
814c918
< k ∈ [0..2147483647]
---
> k ∈ [0..390]
811c915
819c923
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
822,823c926,928
830,831c934,936
< [1..9] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
< p ∈ {{ &y + [4..40],0%4 }}
---
> [1..6] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
> [7..9] ∈ UNINITIALIZED
> p ∈ {{ &y[7] }}
834c939
842c947
< p ∈ {{ &T + [--..396],0%4 }}
---
> p ∈ {{ &T + [-4..396],0%4 }}
969,970c1074,1075
977,978c1082,1083
< p FROM p; A; B; n; p; A[0..9]; B[0..9] (and SELF)
< \result FROM p; A; B; n; p; A[0..9]; B[0..9]
---
> p FROM p; A; B; n; p; A[0..8]; B[0..8] (and SELF)
> \result FROM p; A; B; n; p; A[0..8]; B[0..8]
1048c1153
1056c1161
< p; A[0..9]; B[0..9]
---
> p; A[0..8]; B[0..8]
......@@ -850,11 +838,6 @@ diff tests/value/oracle/noreturn.res.oracle tests/value/oracle_gauges/noreturn.r
> [eva] tests/value/noreturn.i:7: starting to merge loop iterations
36a40
> [eva] tests/value/noreturn.i:13: starting to merge loop iterations
diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_gauges/precise_locations.res.oracle
40a41
> [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
517a519
> [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
diff tests/value/oracle/reduce_formals.res.oracle tests/value/oracle_gauges/reduce_formals.res.oracle
10a11
> [eva] tests/value/reduce_formals.i:5: starting to merge loop iterations
......@@ -901,10 +884,6 @@ diff tests/value/oracle/semaphore.res.oracle tests/value/oracle_gauges/semaphore
diff tests/value/oracle/symbolic_locs.res.oracle tests/value/oracle_gauges/symbolic_locs.res.oracle
133a134
> [eva] tests/value/symbolic_locs.i:93: starting to merge loop iterations
diff tests/value/oracle/test.0.res.oracle tests/value/oracle_gauges/test.0.res.oracle
18a19,20
> [eva:alarm] tests/value/test.i:10: Warning:
> signed overflow. assert i + 1 ≤ 2147483647;
diff tests/value/oracle/undefined_sequence.0.res.oracle tests/value/oracle_gauges/undefined_sequence.0.res.oracle
97a98
> [eva] tests/value/undefined_sequence.i:43: starting to merge loop iterations
......@@ -952,33 +931,7 @@ diff tests/value/oracle/va_list2.1.res.oracle tests/value/oracle_gauges/va_list2
> [eva] computing for function __builtin_va_arg <- main.
> Called from tests/value/va_list2.c:20.
> [eva] Done for function __builtin_va_arg
diff tests/value/oracle/widen_non_constant.res.oracle tests/value/oracle_gauges/widen_non_constant.res.oracle
28c28
< Frama_C_show_each_in: [0..23], [1..23]
---
> Frama_C_show_each_in: [0..22], [1..23]
47c47
< Frama_C_show_each_in: [0..25], [1..23]
---
> Frama_C_show_each_in: [0..22], [1..23]
66,70c66
< Frama_C_show_each_in: [0..2147483647], [1..23]
< [eva:alarm] tests/value/widen_non_constant.i:49: Warning:
< out of bounds read. assert \valid_read(p + j);
< [eva:alarm] tests/value/widen_non_constant.i:45: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
---
> Frama_C_show_each_in: [0..22], [1..23]
88c84
< j ∈ {23; 24}
---
> j ∈ {23}
91c87
< j ∈ {23; 24; 25; 26}
---
> j ∈ {23; 24; 25}
diff tests/value/oracle/widen_on_non_monotonic.res.oracle tests/value/oracle_gauges/widen_on_non_monotonic.res.oracle
24a25,27
> [eva] tests/value/widen_on_non_monotonic.i:26: starting to merge loop iterations
25a26,27
> [eva] tests/value/widen_on_non_monotonic.i:21: starting to merge loop iterations
> [eva] tests/value/widen_on_non_monotonic.i:18: starting to merge loop iterations
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