diff --git a/src/plugins/value/vtests b/src/plugins/value/vtests new file mode 100755 index 0000000000000000000000000000000000000000..03d9e24b6d1cac7ccae188a0a6121b6150465f05 --- /dev/null +++ b/src/plugins/value/vtests @@ -0,0 +1,38 @@ +#!/bin/bash -eu + +DEFAULT_TESTS=(float value idct builtins) +CONFIGS=(apron equality bitwise symblocs gauges octagon) + +ARGS=("${@-}") + +# has_target returns 0 if at least one of the arguments is a target +# (i.e. not an option such as "-j 8"). If so, do not run tests +# for all default targets, only for the specified target(s) +has_target=0 +# sets has_target=0 +function has_target() { + local __has_target=1 + for f in $@; do + __re="\\b$f\\b" # match argument as whole word + if [[ "$f" =~ \.[ci]$ || \ + ( "$f" =~ ^[A-Za-z] && "${DEFAULT_TESTS[@]}" =~ $__re ) ]]; then + __has_target=0 + fi + done + return $__has_target +} + + +if has_target ${ARGS[@]}; then + TESTS=("${ARGS[@]}") +else + TESTS="${DEFAULT_TESTS[@]} ${ARGS[@]}" +fi + +echo Testing ${TESTS[@]} + +for A in ${CONFIGS[@]} +do + echo $A + ./bin/ptests.opt -config $A ${TESTS[@]} +done diff --git a/tests/builtins/oracle_equalities/alloc_weak.res.oracle b/tests/builtins/oracle_equality/alloc_weak.res.oracle similarity index 100% rename from tests/builtins/oracle_equalities/alloc_weak.res.oracle rename to tests/builtins/oracle_equality/alloc_weak.res.oracle diff --git a/tests/builtins/oracle_equalities/allocated.1.res.oracle b/tests/builtins/oracle_equality/allocated.1.res.oracle similarity index 100% rename from tests/builtins/oracle_equalities/allocated.1.res.oracle rename to tests/builtins/oracle_equality/allocated.1.res.oracle diff --git a/tests/builtins/oracle_equalities/imprecise.res.oracle b/tests/builtins/oracle_equality/imprecise.res.oracle similarity index 100% rename from tests/builtins/oracle_equalities/imprecise.res.oracle rename to tests/builtins/oracle_equality/imprecise.res.oracle diff --git a/tests/builtins/oracle_equalities/linked_list.1.res.oracle b/tests/builtins/oracle_equality/linked_list.1.res.oracle similarity index 100% rename from tests/builtins/oracle_equalities/linked_list.1.res.oracle rename to tests/builtins/oracle_equality/linked_list.1.res.oracle diff --git a/tests/builtins/oracle_equalities/malloc-optimistic.res.oracle b/tests/builtins/oracle_equality/malloc-optimistic.res.oracle similarity index 100% rename from tests/builtins/oracle_equalities/malloc-optimistic.res.oracle rename to tests/builtins/oracle_equality/malloc-optimistic.res.oracle diff --git a/tests/builtins/oracle_equalities/write-const.res.oracle b/tests/builtins/oracle_equality/write-const.res.oracle similarity index 100% rename from tests/builtins/oracle_equalities/write-const.res.oracle rename to tests/builtins/oracle_equality/write-const.res.oracle diff --git a/tests/builtins/oracle_octagons/allocated.0.res.oracle b/tests/builtins/oracle_octagon/allocated.0.res.oracle similarity index 100% rename from tests/builtins/oracle_octagons/allocated.0.res.oracle rename to tests/builtins/oracle_octagon/allocated.0.res.oracle diff --git a/tests/builtins/oracle_octagons/allocated.1.res.oracle b/tests/builtins/oracle_octagon/allocated.1.res.oracle similarity index 100% rename from tests/builtins/oracle_octagons/allocated.1.res.oracle rename to tests/builtins/oracle_octagon/allocated.1.res.oracle diff --git a/tests/builtins/oracle_octagons/imprecise.res.oracle b/tests/builtins/oracle_octagon/imprecise.res.oracle similarity index 100% rename from tests/builtins/oracle_octagons/imprecise.res.oracle rename to tests/builtins/oracle_octagon/imprecise.res.oracle diff --git a/tests/builtins/oracle_octagons/linked_list.1.res.oracle b/tests/builtins/oracle_octagon/linked_list.1.res.oracle similarity index 100% rename from tests/builtins/oracle_octagons/linked_list.1.res.oracle rename to tests/builtins/oracle_octagon/linked_list.1.res.oracle diff --git a/tests/builtins/oracle_octagons/malloc-optimistic.res.oracle b/tests/builtins/oracle_octagon/malloc-optimistic.res.oracle similarity index 100% rename from tests/builtins/oracle_octagons/malloc-optimistic.res.oracle rename to tests/builtins/oracle_octagon/malloc-optimistic.res.oracle diff --git a/tests/builtins/test_config_equalities b/tests/builtins/test_config_equality similarity index 100% rename from tests/builtins/test_config_equalities rename to tests/builtins/test_config_equality diff --git a/tests/builtins/test_config_octagons b/tests/builtins/test_config_octagon similarity index 100% rename from tests/builtins/test_config_octagons rename to tests/builtins/test_config_octagon diff --git a/tests/float/oracle_equalities/alarms.0.res.oracle b/tests/float/oracle_equality/alarms.0.res.oracle similarity index 100% rename from tests/float/oracle_equalities/alarms.0.res.oracle rename to tests/float/oracle_equality/alarms.0.res.oracle diff --git a/tests/float/oracle_equalities/alarms.1.res.oracle b/tests/float/oracle_equality/alarms.1.res.oracle similarity index 100% rename from tests/float/oracle_equalities/alarms.1.res.oracle rename to tests/float/oracle_equality/alarms.1.res.oracle diff --git a/tests/float/oracle_equalities/cond.res.oracle b/tests/float/oracle_equality/cond.res.oracle similarity index 100% rename from tests/float/oracle_equalities/cond.res.oracle rename to tests/float/oracle_equality/cond.res.oracle diff --git a/tests/float/oracle_equalities/const3.1.res.oracle b/tests/float/oracle_equality/const3.1.res.oracle similarity index 94% rename from tests/float/oracle_equalities/const3.1.res.oracle rename to tests/float/oracle_equality/const3.1.res.oracle index 412af6075b5e836804b4f3c7685e52ef6d66ba06..7de759db47189f2c50ea83d7845623fa5994f43e 100644 --- a/tests/float/oracle_equalities/const3.1.res.oracle +++ b/tests/float/oracle_equality/const3.1.res.oracle @@ -1,4 +1,4 @@ -23c23 +25c25 < d1 ∈ [0x1.16c2000000000p-133 .. 0x1.16c3000000000p-133] --- > d1 ∈ {0x1.16c2000000000p-133} diff --git a/tests/float/oracle_equalities/dr.2.res.oracle b/tests/float/oracle_equality/dr.2.res.oracle similarity index 93% rename from tests/float/oracle_equalities/dr.2.res.oracle rename to tests/float/oracle_equality/dr.2.res.oracle index a95f94eddaafab39b9466d93690939f6fbae3ec4..10fe6f869598523c6f022e1f593f9c0dfd617337 100644 --- a/tests/float/oracle_equalities/dr.2.res.oracle +++ b/tests/float/oracle_equality/dr.2.res.oracle @@ -1,8 +1,8 @@ -25c25 +27c27 < [eva] tests/float/dr.i:26: Frama_C_show_each: {0; 1}, {0; 1} --- > [eva] tests/float/dr.i:26: Frama_C_show_each: {1}, {0; 1} -30c30 +32c32 < e1 ∈ {0; 1} --- > e1 ∈ {1} diff --git a/tests/float/oracle_equalities/nonlin.1.res.oracle b/tests/float/oracle_equality/nonlin.1.res.oracle similarity index 100% rename from tests/float/oracle_equalities/nonlin.1.res.oracle rename to tests/float/oracle_equality/nonlin.1.res.oracle diff --git a/tests/float/oracle_equalities/nonlin.2.res.oracle b/tests/float/oracle_equality/nonlin.2.res.oracle similarity index 100% rename from tests/float/oracle_equalities/nonlin.2.res.oracle rename to tests/float/oracle_equality/nonlin.2.res.oracle diff --git a/tests/float/oracle_equalities/nonlin.4.res.oracle b/tests/float/oracle_equality/nonlin.4.res.oracle similarity index 100% rename from tests/float/oracle_equalities/nonlin.4.res.oracle rename to tests/float/oracle_equality/nonlin.4.res.oracle diff --git a/tests/float/oracle_equalities/nonlin.5.res.oracle b/tests/float/oracle_equality/nonlin.5.res.oracle similarity index 100% rename from tests/float/oracle_equalities/nonlin.5.res.oracle rename to tests/float/oracle_equality/nonlin.5.res.oracle diff --git a/tests/float/oracle_equalities/parse.res.oracle b/tests/float/oracle_equality/parse.res.oracle similarity index 100% rename from tests/float/oracle_equalities/parse.res.oracle rename to tests/float/oracle_equality/parse.res.oracle diff --git a/tests/float/oracle_octagons/nonlin.1.res.oracle b/tests/float/oracle_octagon/nonlin.1.res.oracle similarity index 100% rename from tests/float/oracle_octagons/nonlin.1.res.oracle rename to tests/float/oracle_octagon/nonlin.1.res.oracle diff --git a/tests/float/oracle_octagons/nonlin.2.res.oracle b/tests/float/oracle_octagon/nonlin.2.res.oracle similarity index 100% rename from tests/float/oracle_octagons/nonlin.2.res.oracle rename to tests/float/oracle_octagon/nonlin.2.res.oracle diff --git a/tests/float/oracle_octagons/nonlin.4.res.oracle b/tests/float/oracle_octagon/nonlin.4.res.oracle similarity index 100% rename from tests/float/oracle_octagons/nonlin.4.res.oracle rename to tests/float/oracle_octagon/nonlin.4.res.oracle diff --git a/tests/float/oracle_octagons/nonlin.5.res.oracle b/tests/float/oracle_octagon/nonlin.5.res.oracle similarity index 100% rename from tests/float/oracle_octagons/nonlin.5.res.oracle rename to tests/float/oracle_octagon/nonlin.5.res.oracle diff --git a/tests/idct/oracle_equalities/ieee_1180_1990.res.oracle b/tests/idct/oracle_equality/ieee_1180_1990.res.oracle similarity index 100% rename from tests/idct/oracle_equalities/ieee_1180_1990.res.oracle rename to tests/idct/oracle_equality/ieee_1180_1990.res.oracle diff --git a/tests/idct/oracle_octagons/ieee_1180_1990.res.oracle b/tests/idct/oracle_octagon/ieee_1180_1990.res.oracle similarity index 100% rename from tests/idct/oracle_octagons/ieee_1180_1990.res.oracle rename to tests/idct/oracle_octagon/ieee_1180_1990.res.oracle diff --git a/tests/value/audit-in.json b/tests/misc/audit-in.json similarity index 92% rename from tests/value/audit-in.json rename to tests/misc/audit-in.json index d6abf18d0ffb9f05e82b0d158058b8715f36f417..4278dcffc0935c685a650032aba687e7f8ba817a 100644 --- a/tests/value/audit-in.json +++ b/tests/misc/audit-in.json @@ -1,8 +1,8 @@ { "sources": { - "tests/value/audit.c": "01010101010101010101010101010101", - "tests/value/audit_included.h": "c2cc488143a476f69cf2ed04c3439e6e", - "tests/value/non_existing_file.h": "1234567890abcdef1234567890abcdef" + "tests/misc/audit.c": "01010101010101010101010101010101", + "tests/misc/audit_included.h": "c2cc488143a476f69cf2ed04c3439e6e", + "tests/misc/non_existing_file.h": "1234567890abcdef1234567890abcdef" }, "kernel": { "warning-categories": { diff --git a/tests/value/audit.c b/tests/misc/audit.c similarity index 78% rename from tests/value/audit.c rename to tests/misc/audit.c index 7b3e27c0eb13ce8bf3de6099b21131006f9de2be..094beded8fc1e0ed11bd9f1b31a8ffd134e870de 100644 --- a/tests/value/audit.c +++ b/tests/misc/audit.c @@ -1,6 +1,6 @@ /* run.config LOG: audit-out.json - STDOPT: #"-audit-check @PTEST_DIR@/audit-in.json -audit-prepare @PTEST_DIR@/result/audit-out.json -kernel-warn-key audit=active" + STDOPT: #"-audit-check @PTEST_DIR@/audit-in.json -audit-prepare @PTEST_RESULT@/audit-out.json -kernel-warn-key audit=active" */ #include "audit_included.h" diff --git a/tests/value/audit_included.h b/tests/misc/audit_included.h similarity index 100% rename from tests/value/audit_included.h rename to tests/misc/audit_included.h diff --git a/tests/value/audit_included_but_not_listed.h b/tests/misc/audit_included_but_not_listed.h similarity index 100% rename from tests/value/audit_included_but_not_listed.h rename to tests/misc/audit_included_but_not_listed.h diff --git a/tests/value/oracle/audit-out.json b/tests/misc/oracle/audit-out.json similarity index 93% rename from tests/value/oracle/audit-out.json rename to tests/misc/oracle/audit-out.json index 23aa305f9c0060058b4df8ce27fde23d0ebc4f5c..c12464699ba37e8bab645ecf123b3ca67f8bd9bd 100644 --- a/tests/value/oracle/audit-out.json +++ b/tests/misc/oracle/audit-out.json @@ -70,9 +70,9 @@ } }, "sources": { - "tests/value/audit.c": "08f73691217888d926a0ee15cbe18159", - "tests/value/audit_included.h": "c2cc488143a476f69cf2ed04c3439e6e", - "tests/value/audit_included_but_not_listed.h": + "tests/misc/audit.c": "aec49f030fcf92bc135bd75e7088194f", + "tests/misc/audit_included.h": "c2cc488143a476f69cf2ed04c3439e6e", + "tests/misc/audit_included_but_not_listed.h": "c2cc488143a476f69cf2ed04c3439e6e" } } diff --git a/tests/value/oracle/audit.res.oracle b/tests/misc/oracle/audit.res.oracle similarity index 64% rename from tests/value/oracle/audit.res.oracle rename to tests/misc/oracle/audit.res.oracle index 338a77c21a7297b49c9f9bf0e4c7faba157e6082..40464f54b363d2da4daa36ed357da2364c3f944e 100644 --- a/tests/value/oracle/audit.res.oracle +++ b/tests/misc/oracle/audit.res.oracle @@ -1,13 +1,13 @@ [kernel:audit] Warning: - different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 + different hashes for tests/misc/audit.c: got aec49f030fcf92bc135bd75e7088194f, expected 01010101010101010101010101010101 [kernel:audit] Warning: - different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) + different hashes for tests/misc/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) [kernel:audit] Warning: missing files: - tests/value/non_existing_file.h -[kernel] Audit: sources list written to: tests/value/result/audit-out.json -[kernel] Parsing tests/value/audit.c (with preprocessing) -[kernel:parser:decimal-float] tests/value/audit.c:10: Warning: + tests/misc/non_existing_file.h +[kernel] Audit: sources list written to: tests/misc/result/audit-out.json +[kernel] Parsing tests/misc/audit.c (with preprocessing) +[kernel:parser:decimal-float] tests/misc/audit.c:10: Warning: Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1. (warn-once: no further messages from category 'parser:decimal-float' will be emitted) [eva] Analyzing a complete application starting at main @@ -31,4 +31,4 @@ f [inout] Inputs for function main: \nothing -[kernel] Wrote: tests/value/result/audit-out.json +[kernel] Wrote: tests/misc/result/audit-out.json diff --git a/tests/test_config_equalities b/tests/test_config_equality similarity index 100% rename from tests/test_config_equalities rename to tests/test_config_equality diff --git a/tests/test_config_octagons b/tests/test_config_octagon similarity index 100% rename from tests/test_config_octagons rename to tests/test_config_octagon diff --git a/tests/value/auto_loop_unroll.c b/tests/value/auto_loop_unroll.c index 1d083a1c84154a7c112a4f25e84cdf468ac7bbbf..81e4f54353158d275b6387b5a97dd8447577d736 100644 --- a/tests/value/auto_loop_unroll.c +++ b/tests/value/auto_loop_unroll.c @@ -159,7 +159,19 @@ void complex_loops () { i = 0; while (i < 64) { for (int j = 0; j < i; j++) { - i++; + if (undet && i < 64) + i++; // The outer loop could be unrolled, as this speeds up convergence. + } + res++; + i++; + } + Frama_C_show_each_imprecise(res); + res = 0; + i = 0; + while (i < 64) { + for (int j = 0; j < i; j++) { + if (undet && i > 0) + i--; // The outer loop cannot be unrolled. } res++; i++; diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle index f34b2d3391c550082ac44d8e02e57b4b4b1e1dc7..485d1f41d3be3aba44e9b92bc38ab195c6ca6809 100644 --- a/tests/value/oracle/auto_loop_unroll.0.res.oracle +++ b/tests/value/oracle/auto_loop_unroll.0.res.oracle @@ -6,7 +6,7 @@ undet ∈ [--..--] g ∈ {0} [eva] computing for function simple_loops <- main. - Called from tests/value/auto_loop_unroll.c:416. + Called from tests/value/auto_loop_unroll.c:428. [eva] tests/value/auto_loop_unroll.c:24: starting to merge loop iterations [eva:alarm] tests/value/auto_loop_unroll.c:25: Warning: signed overflow. assert res + 1 ≤ 2147483647; @@ -27,7 +27,7 @@ [eva] Recording results for simple_loops [eva] Done for function simple_loops [eva] computing for function various_loops <- main. - Called from tests/value/auto_loop_unroll.c:417. + Called from tests/value/auto_loop_unroll.c:429. [eva] tests/value/auto_loop_unroll.c:57: starting to merge loop iterations [eva:alarm] tests/value/auto_loop_unroll.c:58: Warning: signed overflow. assert res + 1 ≤ 2147483647; @@ -146,7 +146,7 @@ [eva] Recording results for various_loops [eva] Done for function various_loops [eva] computing for function complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:418. + Called from tests/value/auto_loop_unroll.c:430. [eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations [eva:alarm] tests/value/auto_loop_unroll.c:154: Warning: signed overflow. assert res + 1 ≤ 2147483647; @@ -154,201 +154,203 @@ Frama_C_show_each_imprecise: [0..2147483647] [eva] tests/value/auto_loop_unroll.c:160: starting to merge loop iterations [eva] tests/value/auto_loop_unroll.c:161: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:162: Warning: - signed overflow. assert i + 1 ≤ 2147483647; [eva:alarm] tests/value/auto_loop_unroll.c:165: Warning: - signed overflow. assert i + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:164: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:167: +[eva] tests/value/auto_loop_unroll.c:168: Frama_C_show_each_imprecise: [0..2147483647] [eva] tests/value/auto_loop_unroll.c:171: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning: +[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:176: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:176: +[eva] tests/value/auto_loop_unroll.c:179: + Frama_C_show_each_imprecise: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:183: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:186: Warning: + signed overflow. assert res + 1 ≤ 2147483647; +[eva] tests/value/auto_loop_unroll.c:188: Frama_C_show_each_imprecise: [0..2147483647] [eva] computing for function incr_g <- complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:181. + Called from tests/value/auto_loop_unroll.c:193. [eva] Recording results for incr_g [eva] Done for function incr_g -[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations +[eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations [eva] computing for function incr_g <- complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:181. + Called from tests/value/auto_loop_unroll.c:193. [eva] Recording results for incr_g [eva] Done for function incr_g [eva] computing for function incr_g <- complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:181. + Called from tests/value/auto_loop_unroll.c:193. [eva] Recording results for incr_g [eva] Done for function incr_g [eva] computing for function incr_g <- complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:181. + Called from tests/value/auto_loop_unroll.c:193. [eva] Recording results for incr_g [eva] Done for function incr_g -[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g -[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g -[eva:alarm] tests/value/auto_loop_unroll.c:183: Warning: +[eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g +[eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g +[eva:alarm] tests/value/auto_loop_unroll.c:195: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:185: +[eva] tests/value/auto_loop_unroll.c:197: Frama_C_show_each_imprecise: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:190: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:192: Warning: +[eva] tests/value/auto_loop_unroll.c:202: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:194: +[eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:198: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:200: Warning: +[eva] tests/value/auto_loop_unroll.c:210: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:212: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:199: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:211: Warning: signed overflow. assert i + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:202: +[eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_imprecise: [0..2147483647] [eva] Recording results for complex_loops [eva] Done for function complex_loops [eva] computing for function various_conditions <- main. - Called from tests/value/auto_loop_unroll.c:419. -[eva] tests/value/auto_loop_unroll.c:211: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:212: Warning: + Called from tests/value/auto_loop_unroll.c:431. +[eva] tests/value/auto_loop_unroll.c:223: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:224: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:216: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:217: Warning: +[eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:228: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:229: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:222: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:223: Warning: +[eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:234: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:235: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:222: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:234: Warning: signed overflow. assert -2147483648 ≤ i_0 - 1; -[eva] tests/value/auto_loop_unroll.c:225: +[eva] tests/value/auto_loop_unroll.c:237: Frama_C_show_each_0_13: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:227: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:228: Warning: +[eva] tests/value/auto_loop_unroll.c:239: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:240: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:227: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:239: Warning: signed overflow. assert -2147483648 ≤ i_1 - 1; -[eva] tests/value/auto_loop_unroll.c:230: +[eva] tests/value/auto_loop_unroll.c:242: Frama_C_show_each_0_14: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:233: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:236: Warning: +[eva] tests/value/auto_loop_unroll.c:245: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:248: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:238: +[eva] tests/value/auto_loop_unroll.c:250: Frama_C_show_each_0_15: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:240: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:241: Warning: +[eva] tests/value/auto_loop_unroll.c:252: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:253: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:245: +[eva] tests/value/auto_loop_unroll.c:257: Frama_C_show_each_11_111: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:250: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:251: Warning: +[eva] tests/value/auto_loop_unroll.c:262: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:263: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [0..2147483647] [eva] Recording results for various_conditions [eva] Done for function various_conditions [eva] computing for function temporary_variables <- main. - Called from tests/value/auto_loop_unroll.c:420. -[eva] tests/value/auto_loop_unroll.c:262: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:262: Warning: + Called from tests/value/auto_loop_unroll.c:432. +[eva] tests/value/auto_loop_unroll.c:274: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:274: Warning: signed overflow. assert i + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:263: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:275: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:267: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:268: Warning: +[eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:279: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:280: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:267: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:279: Warning: signed overflow. assert -2147483648 ≤ i - 1; -[eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:272: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:274: Warning: +[eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:284: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:286: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:272: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning: signed overflow. assert i + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:276: Frama_C_show_each_22: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:279: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:282: Warning: +[eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_22: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:291: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:294: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:279: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:291: Warning: signed overflow. assert i + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:284: Frama_C_show_each_23: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:287: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:290: Warning: +[eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_23: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:299: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:302: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:287: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:299: Warning: signed overflow. assert i + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:292: Frama_C_show_each_top: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_top: [0..2147483647] [eva] Recording results for temporary_variables [eva] Done for function temporary_variables [eva] computing for function loops_with_goto <- main. - Called from tests/value/auto_loop_unroll.c:421. -[eva] tests/value/auto_loop_unroll.c:298: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:299: Warning: + Called from tests/value/auto_loop_unroll.c:433. +[eva] tests/value/auto_loop_unroll.c:310: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:311: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: [0..2147483647] -[eva:alarm] tests/value/auto_loop_unroll.c:308: Warning: +[eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: [0..2147483647] +[eva:alarm] tests/value/auto_loop_unroll.c:320: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations -[eva] tests/value/auto_loop_unroll.c:312: Frama_C_show_each_top: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:315: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:316: Warning: +[eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations +[eva] tests/value/auto_loop_unroll.c:324: Frama_C_show_each_top: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:327: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:328: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: [0..2147483647] -[eva:alarm] tests/value/auto_loop_unroll.c:325: Warning: +[eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: [0..2147483647] +[eva:alarm] tests/value/auto_loop_unroll.c:337: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:324: starting to merge loop iterations -[eva] tests/value/auto_loop_unroll.c:329: +[eva] tests/value/auto_loop_unroll.c:336: starting to merge loop iterations +[eva] tests/value/auto_loop_unroll.c:341: Frama_C_show_each_33_inf: [0..2147483647] -[eva:alarm] tests/value/auto_loop_unroll.c:333: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:345: Warning: signed overflow. assert i + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:332: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:332: Warning: +[eva] tests/value/auto_loop_unroll.c:344: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:344: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:337: Frama_C_show_each_top: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:340: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:343: Warning: +[eva] tests/value/auto_loop_unroll.c:349: Frama_C_show_each_top: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:352: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:355: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:345: +[eva] tests/value/auto_loop_unroll.c:357: Frama_C_show_each_0_35: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:348: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:348: Warning: +[eva] tests/value/auto_loop_unroll.c:360: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:360: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:348: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:360: Warning: signed overflow. assert -2147483648 ≤ i - 1; -[eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:355: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:358: Warning: +[eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:367: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:370: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:360: Frama_C_show_each_27: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:372: Frama_C_show_each_27: [0..2147483647] [eva] Recording results for loops_with_goto [eva] Done for function loops_with_goto [eva] computing for function non_natural_loops <- main. - Called from tests/value/auto_loop_unroll.c:422. -[eva:alarm] tests/value/auto_loop_unroll.c:371: Warning: + Called from tests/value/auto_loop_unroll.c:434. +[eva:alarm] tests/value/auto_loop_unroll.c:383: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: [1..2147483647] -[eva:alarm] tests/value/auto_loop_unroll.c:379: Warning: +[eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: [1..2147483647] +[eva:alarm] tests/value/auto_loop_unroll.c:391: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:380: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:392: Warning: signed overflow. assert -2147483648 ≤ i - 1; -[eva] tests/value/auto_loop_unroll.c:383: +[eva] tests/value/auto_loop_unroll.c:395: Frama_C_show_each_1_51: [1..2147483647] [eva] Recording results for non_natural_loops [eva] Done for function non_natural_loops [eva] computing for function following_loops <- main. - Called from tests/value/auto_loop_unroll.c:423. -[eva] tests/value/auto_loop_unroll.c:390: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:392: Warning: + Called from tests/value/auto_loop_unroll.c:435. +[eva] tests/value/auto_loop_unroll.c:402: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:404: Warning: signed overflow. assert j + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:396: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:408: Warning: signed overflow. assert j + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:394: starting to merge loop iterations -[eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:401: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:403: Warning: +[eva] tests/value/auto_loop_unroll.c:406: starting to merge loop iterations +[eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:413: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:415: Warning: signed overflow. assert j + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:407: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:419: Warning: signed overflow. assert j + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:405: starting to merge loop iterations -[eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:417: starting to merge loop iterations +[eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [0..2147483647] [eva] Recording results for following_loops [eva] Done for function following_loops [eva] Recording results for main @@ -471,7 +473,7 @@ [inout] Inputs for function incr_g: g [inout] Out (internal) for function complex_loops: - g; res; i; j; p; j_0; t[0..9] + g; res; i; j; p; j_0; j_1; t[0..9] [inout] Inputs for function complex_loops: undet; g [inout] Out (internal) for function loops_with_goto: diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle index 1826be4c45b15e28b686ca1477a15430deaba845..1a4b5f83bab11263da5a047cb211f4f69164591a 100644 --- a/tests/value/oracle/auto_loop_unroll.1.res.oracle +++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle @@ -6,7 +6,7 @@ undet ∈ [--..--] g ∈ {0} [eva] computing for function simple_loops <- main. - Called from tests/value/auto_loop_unroll.c:416. + Called from tests/value/auto_loop_unroll.c:428. [eva:loop-unroll] tests/value/auto_loop_unroll.c:24: Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:24: Trace partitioning superposing up to 100 states @@ -25,7 +25,7 @@ [eva] Recording results for simple_loops [eva] Done for function simple_loops [eva] computing for function various_loops <- main. - Called from tests/value/auto_loop_unroll.c:417. + Called from tests/value/auto_loop_unroll.c:429. [eva:loop-unroll] tests/value/auto_loop_unroll.c:57: Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: {64} [eva:loop-unroll] tests/value/auto_loop_unroll.c:62: Automatic loop unrolling. @@ -287,7 +287,7 @@ [eva] Recording results for various_loops [eva] Done for function various_loops [eva] computing for function complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:418. + Called from tests/value/auto_loop_unroll.c:430. [eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations [eva:alarm] tests/value/auto_loop_unroll.c:154: Warning: signed overflow. assert res + 1 ≤ 2147483647; @@ -295,143 +295,145 @@ Frama_C_show_each_imprecise: [0..2147483647] [eva] tests/value/auto_loop_unroll.c:160: starting to merge loop iterations [eva] tests/value/auto_loop_unroll.c:161: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:162: Warning: - signed overflow. assert i + 1 ≤ 2147483647; [eva:alarm] tests/value/auto_loop_unroll.c:165: Warning: - signed overflow. assert i + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:164: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:167: +[eva] tests/value/auto_loop_unroll.c:168: Frama_C_show_each_imprecise: [0..2147483647] [eva] tests/value/auto_loop_unroll.c:171: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning: +[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:176: Warning: + signed overflow. assert res + 1 ≤ 2147483647; +[eva] tests/value/auto_loop_unroll.c:179: + Frama_C_show_each_imprecise: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:183: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:186: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:176: +[eva] tests/value/auto_loop_unroll.c:188: Frama_C_show_each_imprecise: [0..2147483647] [eva] computing for function incr_g <- complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:181. + Called from tests/value/auto_loop_unroll.c:193. [eva] Recording results for incr_g [eva] Done for function incr_g -[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations +[eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations [eva] computing for function incr_g <- complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:181. + Called from tests/value/auto_loop_unroll.c:193. [eva] Recording results for incr_g [eva] Done for function incr_g [eva] computing for function incr_g <- complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:181. + Called from tests/value/auto_loop_unroll.c:193. [eva] Recording results for incr_g [eva] Done for function incr_g [eva] computing for function incr_g <- complex_loops <- main. - Called from tests/value/auto_loop_unroll.c:181. + Called from tests/value/auto_loop_unroll.c:193. [eva] Recording results for incr_g [eva] Done for function incr_g -[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g -[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g -[eva:alarm] tests/value/auto_loop_unroll.c:183: Warning: +[eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g +[eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g +[eva:alarm] tests/value/auto_loop_unroll.c:195: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:185: +[eva] tests/value/auto_loop_unroll.c:197: Frama_C_show_each_imprecise: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:190: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:192: Warning: +[eva] tests/value/auto_loop_unroll.c:202: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:194: +[eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:198: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:200: Warning: +[eva] tests/value/auto_loop_unroll.c:210: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:212: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:199: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:211: Warning: signed overflow. assert i + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:202: +[eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_imprecise: [0..2147483647] [eva] Recording results for complex_loops [eva] Done for function complex_loops [eva] computing for function various_conditions <- main. - Called from tests/value/auto_loop_unroll.c:419. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:211: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: {11} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:216: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: {12} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:222: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:225: Frama_C_show_each_0_13: [0..13] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:227: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:230: Frama_C_show_each_0_14: [0..14] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:233: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_0_15: [0..15] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:240: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:240: + Called from tests/value/auto_loop_unroll.c:431. +[eva:loop-unroll] tests/value/auto_loop_unroll.c:223: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: {11} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:228: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: {12} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:234: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:237: Frama_C_show_each_0_13: [0..13] +[eva:loop-unroll] tests/value/auto_loop_unroll.c:239: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:242: Frama_C_show_each_0_14: [0..14] +[eva:loop-unroll] tests/value/auto_loop_unroll.c:245: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:250: Frama_C_show_each_0_15: [0..15] +[eva:loop-unroll] tests/value/auto_loop_unroll.c:252: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:252: Trace partitioning superposing up to 100 states -[eva] tests/value/auto_loop_unroll.c:245: Frama_C_show_each_11_111: [11..111] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:250: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: {16} +[eva] tests/value/auto_loop_unroll.c:257: Frama_C_show_each_11_111: [11..111] +[eva:loop-unroll] tests/value/auto_loop_unroll.c:262: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: {16} [eva] Recording results for various_conditions [eva] Done for function various_conditions [eva] computing for function temporary_variables <- main. - Called from tests/value/auto_loop_unroll.c:420. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:262: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: {20} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:267: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: {21} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:272: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:276: Frama_C_show_each_22: {22} + Called from tests/value/auto_loop_unroll.c:432. +[eva:loop-unroll] tests/value/auto_loop_unroll.c:274: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: {20} [eva:loop-unroll] tests/value/auto_loop_unroll.c:279: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:284: Frama_C_show_each_23: {23} -[eva] tests/value/auto_loop_unroll.c:287: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:290: Warning: +[eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: {21} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:284: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_22: {22} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:291: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_23: {23} +[eva] tests/value/auto_loop_unroll.c:299: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:302: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:287: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:299: Warning: signed overflow. assert i + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:292: Frama_C_show_each_top: [0..2147483647] +[eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_top: [0..2147483647] [eva] Recording results for temporary_variables [eva] Done for function temporary_variables [eva] computing for function loops_with_goto <- main. - Called from tests/value/auto_loop_unroll.c:421. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:298: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: {30} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:307: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:308: Warning: + Called from tests/value/auto_loop_unroll.c:433. +[eva:loop-unroll] tests/value/auto_loop_unroll.c:310: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: {30} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:319: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:320: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:307: +[eva] tests/value/auto_loop_unroll.c:319: Trace partitioning superposing up to 100 states -[eva] tests/value/auto_loop_unroll.c:312: +[eva] tests/value/auto_loop_unroll.c:324: Frama_C_show_each_top: [31..2147483647] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:315: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: {32} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:324: Automatic loop unrolling. -[eva:alarm] tests/value/auto_loop_unroll.c:325: Warning: +[eva:loop-unroll] tests/value/auto_loop_unroll.c:327: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: {32} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:336: Automatic loop unrolling. +[eva:alarm] tests/value/auto_loop_unroll.c:337: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:329: +[eva] tests/value/auto_loop_unroll.c:341: Frama_C_show_each_33_inf: [33..2147483647] -[eva:alarm] tests/value/auto_loop_unroll.c:333: Warning: +[eva:alarm] tests/value/auto_loop_unroll.c:345: Warning: signed overflow. assert i + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:332: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:332: Warning: +[eva] tests/value/auto_loop_unroll.c:344: starting to merge loop iterations +[eva:alarm] tests/value/auto_loop_unroll.c:344: Warning: signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:337: Frama_C_show_each_top: [0..2147483647] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:340: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:345: Frama_C_show_each_0_35: [0..35] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:348: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: {36} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:355: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:360: Frama_C_show_each_27: {27} +[eva] tests/value/auto_loop_unroll.c:349: Frama_C_show_each_top: [0..2147483647] +[eva:loop-unroll] tests/value/auto_loop_unroll.c:352: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:357: Frama_C_show_each_0_35: [0..35] +[eva:loop-unroll] tests/value/auto_loop_unroll.c:360: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: {36} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:367: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:372: Frama_C_show_each_27: {27} [eva] Recording results for loops_with_goto [eva] Done for function loops_with_goto [eva] computing for function non_natural_loops <- main. - Called from tests/value/auto_loop_unroll.c:422. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:370: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: {50} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:379: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:383: Frama_C_show_each_1_51: [1..51] + Called from tests/value/auto_loop_unroll.c:434. +[eva:loop-unroll] tests/value/auto_loop_unroll.c:382: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: {50} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:391: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:395: Frama_C_show_each_1_51: [1..51] [eva] Recording results for non_natural_loops [eva] Done for function non_natural_loops [eva] computing for function following_loops <- main. - Called from tests/value/auto_loop_unroll.c:423. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:390: Automatic loop unrolling. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:394: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: {30} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:401: Automatic loop unrolling. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:405: Automatic loop unrolling. -[eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [15..45] + Called from tests/value/auto_loop_unroll.c:435. +[eva:loop-unroll] tests/value/auto_loop_unroll.c:402: Automatic loop unrolling. +[eva:loop-unroll] tests/value/auto_loop_unroll.c:406: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: {30} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:413: Automatic loop unrolling. +[eva:loop-unroll] tests/value/auto_loop_unroll.c:417: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [15..45] [eva] Recording results for following_loops [eva] Done for function following_loops [eva] Recording results for main @@ -554,7 +556,7 @@ [inout] Inputs for function incr_g: g [inout] Out (internal) for function complex_loops: - g; res; i; j; p; j_0; t[0..9] + g; res; i; j; p; j_0; j_1; t[0..9] [inout] Inputs for function complex_loops: undet; g [inout] Out (internal) for function loops_with_goto: diff --git a/tests/value/oracle_apron/audit.res.oracle b/tests/value/oracle_apron/audit.res.oracle deleted file mode 100644 index 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- a/tests/value/oracle_apron/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_apron/auto_loop_unroll.0.res.oracle b/tests/value/oracle_apron/auto_loop_unroll.0.res.oracle index a327adacc6b58b32c198364c25748edc883450ae..1fb1e4da2fc9a40d8f8e546dc3b3d7a33a9b9348 100644 --- a/tests/value/oracle_apron/auto_loop_unroll.0.res.oracle +++ b/tests/value/oracle_apron/auto_loop_unroll.0.res.oracle @@ -120,206 +120,214 @@ < [eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [0..2147483647] --- > [eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [3..2147483647] -161,162d145 -< [eva:alarm] tests/value/auto_loop_unroll.c:164: Warning: +157,160c142 +< [eva:alarm] tests/value/auto_loop_unroll.c:165: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -169c152 +< [eva] tests/value/auto_loop_unroll.c:168: +< Frama_C_show_each_imprecise: [0..2147483647] +--- +> [eva] tests/value/auto_loop_unroll.c:168: Frama_C_show_each_imprecise: [0..65] +166c148 +< Frama_C_show_each_imprecise: [0..2147483647] +--- +> Frama_C_show_each_imprecise: [64..2147483647] +171c153 < Frama_C_show_each_imprecise: [0..2147483647] --- > Frama_C_show_each_imprecise: [10..2147483647] -187,192c170,178 -< [eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g -< [eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g -< [eva:alarm] tests/value/auto_loop_unroll.c:183: Warning: +189,194c171,179 +< [eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g +< [eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g +< [eva:alarm] tests/value/auto_loop_unroll.c:195: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:185: +< [eva] tests/value/auto_loop_unroll.c:197: < Frama_C_show_each_imprecise: [0..2147483647] --- > [eva] computing for function incr_g <- complex_loops <- main. -> Called from tests/value/auto_loop_unroll.c:181. +> Called from tests/value/auto_loop_unroll.c:193. > [eva] Recording results for incr_g > [eva] Done for function incr_g > [eva] computing for function incr_g <- complex_loops <- main. -> Called from tests/value/auto_loop_unroll.c:181. +> Called from tests/value/auto_loop_unroll.c:193. > [eva] Recording results for incr_g > [eva] Done for function incr_g -> [eva] tests/value/auto_loop_unroll.c:185: Frama_C_show_each_imprecise: [0..64] -194,197c180 -< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning: +> [eva] tests/value/auto_loop_unroll.c:197: Frama_C_show_each_imprecise: [0..64] +196,199c181 +< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:194: +< [eva] tests/value/auto_loop_unroll.c:206: < Frama_C_show_each_imprecise: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [0..9] -199,200d181 -< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning: +> [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [0..9] +201,202d182 +< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -204c185 +206c186 < Frama_C_show_each_imprecise: [0..2147483647] --- > Frama_C_show_each_imprecise: [64..2147483647] -210,212c191 -< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning: +212,214c192 +< [eva:alarm] tests/value/auto_loop_unroll.c:224: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: {11} -214,216c193 -< [eva:alarm] tests/value/auto_loop_unroll.c:217: Warning: +> [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: {11} +216,218c194 +< [eva:alarm] tests/value/auto_loop_unroll.c:229: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: {12} -218,219d194 -< [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning: +> [eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: {12} +220,221d195 +< [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -221a197,198 -> [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning: +223a198,199 +> [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -225,226d201 -< [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning: +227,228d202 +< [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -228a204,205 -> [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning: +230a205,206 +> [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -232,233d208 -< [eva:alarm] tests/value/auto_loop_unroll.c:236: Warning: +234,235d209 +< [eva:alarm] tests/value/auto_loop_unroll.c:248: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -237,240c212 -< [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning: +239,242c213 +< [eva:alarm] tests/value/auto_loop_unroll.c:253: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:245: +< [eva] tests/value/auto_loop_unroll.c:257: < Frama_C_show_each_11_111: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:245: Frama_C_show_each_11_111: [11..111] -242,244c214 -< [eva:alarm] tests/value/auto_loop_unroll.c:251: Warning: +> [eva] tests/value/auto_loop_unroll.c:257: Frama_C_show_each_11_111: [11..111] +244,246c215 +< [eva:alarm] tests/value/auto_loop_unroll.c:263: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [16..2147483647] -252,254c222 -< [eva:alarm] tests/value/auto_loop_unroll.c:263: Warning: +> [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [16..2147483647] +254,256c223 +< [eva:alarm] tests/value/auto_loop_unroll.c:275: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [20..2147483646] -256,257d223 -< [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning: +> [eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [20..2147483646] +258,259d224 +< [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -260,262c226 -< [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: [0..2147483647] -< [eva] tests/value/auto_loop_unroll.c:272: starting to merge loop iterations -< [eva:alarm] tests/value/auto_loop_unroll.c:274: Warning: ---- -> [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning: -264,266c228,230 -< [eva:alarm] tests/value/auto_loop_unroll.c:272: Warning: +262,264c227 +< [eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:284: starting to merge loop iterations +< [eva:alarm] tests/value/auto_loop_unroll.c:286: Warning: +--- +> [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning: +266,268c229,231 +< [eva:alarm] tests/value/auto_loop_unroll.c:284: Warning: < signed overflow. assert i + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:276: Frama_C_show_each_22: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_22: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: {21} -> [eva] tests/value/auto_loop_unroll.c:272: starting to merge loop iterations -> [eva] tests/value/auto_loop_unroll.c:276: Frama_C_show_each_22: {21; 22} -268,272c232 -< [eva:alarm] tests/value/auto_loop_unroll.c:282: Warning: +> [eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: {21} +> [eva] tests/value/auto_loop_unroll.c:284: starting to merge loop iterations +> [eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_22: {21; 22} +270,274c233 +< [eva:alarm] tests/value/auto_loop_unroll.c:294: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva:alarm] tests/value/auto_loop_unroll.c:279: Warning: +< [eva:alarm] tests/value/auto_loop_unroll.c:291: Warning: < signed overflow. assert i + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:284: Frama_C_show_each_23: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_23: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:284: Frama_C_show_each_23: {22; 23} -276,278c236,237 -< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning: +> [eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_23: {22; 23} +278,280c237,238 +< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning: < signed overflow. assert i + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:292: Frama_C_show_each_top: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_top: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:292: +> [eva] tests/value/auto_loop_unroll.c:304: > Frama_C_show_each_top: [23..2147483647] -284,286c243,244 -< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning: +286,288c244,245 +< [eva:alarm] tests/value/auto_loop_unroll.c:311: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: {30} -> [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations -289,290c247,248 -< [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations -< [eva] tests/value/auto_loop_unroll.c:312: Frama_C_show_each_top: [0..2147483647] +> [eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: {30} +> [eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations +291,292c248,249 +< [eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations +< [eva] tests/value/auto_loop_unroll.c:324: Frama_C_show_each_top: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:312: +> [eva] tests/value/auto_loop_unroll.c:324: > Frama_C_show_each_top: [31..2147483647] -292,294c250 -< [eva:alarm] tests/value/auto_loop_unroll.c:316: Warning: +294,296c251 +< [eva:alarm] tests/value/auto_loop_unroll.c:328: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: {32} -299c255 +> [eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: {32} +301c256 < Frama_C_show_each_33_inf: [0..2147483647] --- > Frama_C_show_each_33_inf: [33..2147483647] -303,304d258 -< [eva:alarm] tests/value/auto_loop_unroll.c:332: Warning: +305,306d259 +< [eva:alarm] tests/value/auto_loop_unroll.c:344: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -307,310c261 -< [eva:alarm] tests/value/auto_loop_unroll.c:343: Warning: +309,312c262 +< [eva:alarm] tests/value/auto_loop_unroll.c:355: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:345: +< [eva] tests/value/auto_loop_unroll.c:357: < Frama_C_show_each_0_35: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:345: Frama_C_show_each_0_35: [0..35] -313,314d263 +> [eva] tests/value/auto_loop_unroll.c:357: Frama_C_show_each_0_35: [0..35] +315,316d264 < signed overflow. assert res + 1 ≤ 2147483647; -< [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning: -316,318c265 -< [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: [0..2147483647] -< [eva] tests/value/auto_loop_unroll.c:355: starting to merge loop iterations -< [eva:alarm] tests/value/auto_loop_unroll.c:358: Warning: ---- -> [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning: -320c267,269 -< [eva] tests/value/auto_loop_unroll.c:360: Frama_C_show_each_27: [0..2147483647] ---- -> [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: {36} -> [eva] tests/value/auto_loop_unroll.c:355: starting to merge loop iterations -> [eva] tests/value/auto_loop_unroll.c:360: Frama_C_show_each_27: [0..37] -325,327c274 -< [eva:alarm] tests/value/auto_loop_unroll.c:371: Warning: +< [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning: +318,320c266 +< [eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:367: starting to merge loop iterations +< [eva:alarm] tests/value/auto_loop_unroll.c:370: Warning: +--- +> [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning: +322c268,270 +< [eva] tests/value/auto_loop_unroll.c:372: Frama_C_show_each_27: [0..2147483647] +--- +> [eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: {36} +> [eva] tests/value/auto_loop_unroll.c:367: starting to merge loop iterations +> [eva] tests/value/auto_loop_unroll.c:372: Frama_C_show_each_27: [0..37] +327,329c275 +< [eva:alarm] tests/value/auto_loop_unroll.c:383: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: [1..2147483647] +< [eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: [1..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: {50} -330,331d276 -< [eva:alarm] tests/value/auto_loop_unroll.c:380: Warning: -< signed overflow. assert -2147483648 ≤ i - 1; -339,342d283 +> [eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: {50} +332,333d277 < [eva:alarm] tests/value/auto_loop_unroll.c:392: Warning: +< signed overflow. assert -2147483648 ≤ i - 1; +341,344d284 +< [eva:alarm] tests/value/auto_loop_unroll.c:404: Warning: < signed overflow. assert j + 1 ≤ 2147483647; -< [eva:alarm] tests/value/auto_loop_unroll.c:396: Warning: +< [eva:alarm] tests/value/auto_loop_unroll.c:408: Warning: < signed overflow. assert j + 1 ≤ 2147483647; -344c285 -< [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: [0..2147483647] +346c286 +< [eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: {30} -346,349d286 -< [eva:alarm] tests/value/auto_loop_unroll.c:403: Warning: +> [eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: {30} +348,351d287 +< [eva:alarm] tests/value/auto_loop_unroll.c:415: Warning: < signed overflow. assert j + 1 ≤ 2147483647; -< [eva:alarm] tests/value/auto_loop_unroll.c:407: Warning: +< [eva:alarm] tests/value/auto_loop_unroll.c:419: Warning: < signed overflow. assert j + 1 ≤ 2147483647; -351c288 -< [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [0..2147483647] +353c289 +< [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: {30} -361c298 +> [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: {30} +363c299 < __retres ∈ [1..2147483647] --- > __retres ∈ [1..25] -363c300 +365c301 < g ∈ [1..2147483647] --- > g ∈ [1..126] -391c328 +393c329 < k ∈ [22..2147483647] --- > k ∈ {22} diff --git a/tests/value/oracle_apron/auto_loop_unroll.1.res.oracle b/tests/value/oracle_apron/auto_loop_unroll.1.res.oracle index 702df814fedff678c3b0b1c0cf8476d6a588c359..6094367647e11eab9abe112c53a07a27ed4c8837 100644 --- a/tests/value/oracle_apron/auto_loop_unroll.1.res.oracle +++ b/tests/value/oracle_apron/auto_loop_unroll.1.res.oracle @@ -191,120 +191,128 @@ < [eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [0..2147483647] --- > [eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [3..2147483647] -302,303d370 -< [eva:alarm] tests/value/auto_loop_unroll.c:164: Warning: +298,301c367 +< [eva:alarm] tests/value/auto_loop_unroll.c:165: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -310c377 +< [eva] tests/value/auto_loop_unroll.c:168: +< Frama_C_show_each_imprecise: [0..2147483647] +--- +> [eva] tests/value/auto_loop_unroll.c:168: Frama_C_show_each_imprecise: [0..65] +307c373 +< Frama_C_show_each_imprecise: [0..2147483647] +--- +> Frama_C_show_each_imprecise: [64..2147483647] +312c378 < Frama_C_show_each_imprecise: [0..2147483647] --- > Frama_C_show_each_imprecise: [10..2147483647] -328,333c395,403 -< [eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g -< [eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g -< [eva:alarm] tests/value/auto_loop_unroll.c:183: Warning: +330,335c396,404 +< [eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g +< [eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g +< [eva:alarm] tests/value/auto_loop_unroll.c:195: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:185: +< [eva] tests/value/auto_loop_unroll.c:197: < Frama_C_show_each_imprecise: [0..2147483647] --- > [eva] computing for function incr_g <- complex_loops <- main. -> Called from tests/value/auto_loop_unroll.c:181. +> Called from tests/value/auto_loop_unroll.c:193. > [eva] Recording results for incr_g > [eva] Done for function incr_g > [eva] computing for function incr_g <- complex_loops <- main. -> Called from tests/value/auto_loop_unroll.c:181. +> Called from tests/value/auto_loop_unroll.c:193. > [eva] Recording results for incr_g > [eva] Done for function incr_g -> [eva] tests/value/auto_loop_unroll.c:185: Frama_C_show_each_imprecise: [0..64] -335,338c405 -< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning: +> [eva] tests/value/auto_loop_unroll.c:197: Frama_C_show_each_imprecise: [0..64] +337,340c406 +< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:194: +< [eva] tests/value/auto_loop_unroll.c:206: < Frama_C_show_each_imprecise: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [0..9] -340,341d406 -< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning: +> [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [0..9] +342,343d407 +< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -345c410 +347c411 < Frama_C_show_each_imprecise: [0..2147483647] --- > Frama_C_show_each_imprecise: [64..2147483647] -350c415 -< [eva:loop-unroll] tests/value/auto_loop_unroll.c:211: Automatic loop unrolling. ---- -> [eva] tests/value/auto_loop_unroll.c:211: starting to merge loop iterations -352c417 -< [eva:loop-unroll] tests/value/auto_loop_unroll.c:216: Automatic loop unrolling. ---- -> [eva] tests/value/auto_loop_unroll.c:216: starting to merge loop iterations -354,359c419,435 -< [eva:loop-unroll] tests/value/auto_loop_unroll.c:222: Automatic loop unrolling. -< [eva] tests/value/auto_loop_unroll.c:225: Frama_C_show_each_0_13: [0..13] -< [eva:loop-unroll] tests/value/auto_loop_unroll.c:227: Automatic loop unrolling. -< [eva] tests/value/auto_loop_unroll.c:230: Frama_C_show_each_0_14: [0..14] -< [eva:loop-unroll] tests/value/auto_loop_unroll.c:233: Automatic loop unrolling. -< [eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_0_15: [0..15] ---- -> [eva] tests/value/auto_loop_unroll.c:222: starting to merge loop iterations -> [eva:alarm] tests/value/auto_loop_unroll.c:222: Warning: +352c416 +< [eva:loop-unroll] tests/value/auto_loop_unroll.c:223: Automatic loop unrolling. +--- +> [eva] tests/value/auto_loop_unroll.c:223: starting to merge loop iterations +354c418 +< [eva:loop-unroll] tests/value/auto_loop_unroll.c:228: Automatic loop unrolling. +--- +> [eva] tests/value/auto_loop_unroll.c:228: starting to merge loop iterations +356,361c420,436 +< [eva:loop-unroll] tests/value/auto_loop_unroll.c:234: Automatic loop unrolling. +< [eva] tests/value/auto_loop_unroll.c:237: Frama_C_show_each_0_13: [0..13] +< [eva:loop-unroll] tests/value/auto_loop_unroll.c:239: Automatic loop unrolling. +< [eva] tests/value/auto_loop_unroll.c:242: Frama_C_show_each_0_14: [0..14] +< [eva:loop-unroll] tests/value/auto_loop_unroll.c:245: Automatic loop unrolling. +< [eva] tests/value/auto_loop_unroll.c:250: Frama_C_show_each_0_15: [0..15] +--- +> [eva] tests/value/auto_loop_unroll.c:234: starting to merge loop iterations +> [eva:alarm] tests/value/auto_loop_unroll.c:234: Warning: > signed overflow. assert -2147483648 ≤ i_0 - 1; -> [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning: +> [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -> [eva] tests/value/auto_loop_unroll.c:225: +> [eva] tests/value/auto_loop_unroll.c:237: > Frama_C_show_each_0_13: [0..2147483647] -> [eva] tests/value/auto_loop_unroll.c:227: starting to merge loop iterations -> [eva:alarm] tests/value/auto_loop_unroll.c:227: Warning: +> [eva] tests/value/auto_loop_unroll.c:239: starting to merge loop iterations +> [eva:alarm] tests/value/auto_loop_unroll.c:239: Warning: > signed overflow. assert -2147483648 ≤ i_1 - 1; -> [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning: +> [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -> [eva] tests/value/auto_loop_unroll.c:230: +> [eva] tests/value/auto_loop_unroll.c:242: > Frama_C_show_each_0_14: [0..2147483647] -> [eva] tests/value/auto_loop_unroll.c:233: starting to merge loop iterations -> [eva] tests/value/auto_loop_unroll.c:238: +> [eva] tests/value/auto_loop_unroll.c:245: starting to merge loop iterations +> [eva] tests/value/auto_loop_unroll.c:250: > Frama_C_show_each_0_15: [0..2147483647] -372c448,452 -< [eva:loop-unroll] tests/value/auto_loop_unroll.c:267: Automatic loop unrolling. +374c449,453 +< [eva:loop-unroll] tests/value/auto_loop_unroll.c:279: Automatic loop unrolling. --- -> [eva] tests/value/auto_loop_unroll.c:267: starting to merge loop iterations -> [eva:alarm] tests/value/auto_loop_unroll.c:267: Warning: +> [eva] tests/value/auto_loop_unroll.c:279: starting to merge loop iterations +> [eva:alarm] tests/value/auto_loop_unroll.c:279: Warning: > signed overflow. assert -2147483648 ≤ i - 1; -> [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning: +> [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -381,383c461,462 -< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning: +383,385c462,463 +< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning: < signed overflow. assert i + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:292: Frama_C_show_each_top: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_top: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:292: +> [eva] tests/value/auto_loop_unroll.c:304: > Frama_C_show_each_top: [23..2147483647] -408,409d486 -< [eva:alarm] tests/value/auto_loop_unroll.c:332: Warning: +410,411d487 +< [eva:alarm] tests/value/auto_loop_unroll.c:344: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -413c490,494 -< [eva:loop-unroll] tests/value/auto_loop_unroll.c:348: Automatic loop unrolling. +415c491,495 +< [eva:loop-unroll] tests/value/auto_loop_unroll.c:360: Automatic loop unrolling. --- -> [eva] tests/value/auto_loop_unroll.c:348: starting to merge loop iterations -> [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning: +> [eva] tests/value/auto_loop_unroll.c:360: starting to merge loop iterations +> [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning: > signed overflow. assert -2147483648 ≤ i - 1; -> [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning: +> [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -423,424c504,507 -< [eva:loop-unroll] tests/value/auto_loop_unroll.c:379: Automatic loop unrolling. -< [eva] tests/value/auto_loop_unroll.c:383: Frama_C_show_each_1_51: [1..51] +425,426c505,508 +< [eva:loop-unroll] tests/value/auto_loop_unroll.c:391: Automatic loop unrolling. +< [eva] tests/value/auto_loop_unroll.c:395: Frama_C_show_each_1_51: [1..51] --- -> [eva:alarm] tests/value/auto_loop_unroll.c:379: Warning: +> [eva:alarm] tests/value/auto_loop_unroll.c:391: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -> [eva] tests/value/auto_loop_unroll.c:383: +> [eva] tests/value/auto_loop_unroll.c:395: > Frama_C_show_each_1_51: [1..2147483647] -434c517 -< [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [15..45] +436c518 +< [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [15..45] --- -> [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: {30} -442c525 +> [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: {30} +444c526 < j ∈ [15..45] --- > j ∈ [15..30] -467c550 +469c551 < i ∈ [-1..50] --- > i ∈ [-2147483648..50] diff --git a/tests/value/oracle_bitwise/audit.res.oracle b/tests/value/oracle_bitwise/audit.res.oracle deleted file mode 100644 index 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- a/tests/value/oracle_bitwise/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_equalities/audit.res.oracle b/tests/value/oracle_equalities/audit.res.oracle deleted file mode 100644 index 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- a/tests/value/oracle_equalities/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_equalities/CruiseControl.res.oracle b/tests/value/oracle_equality/CruiseControl.res.oracle similarity index 100% rename from tests/value/oracle_equalities/CruiseControl.res.oracle rename to tests/value/oracle_equality/CruiseControl.res.oracle diff --git a/tests/value/oracle_equalities/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle similarity index 100% rename from tests/value/oracle_equalities/addition.res.oracle rename to tests/value/oracle_equality/addition.res.oracle diff --git a/tests/value/oracle_equalities/alias.0.res.oracle b/tests/value/oracle_equality/alias.0.res.oracle similarity index 100% rename from tests/value/oracle_equalities/alias.0.res.oracle rename to tests/value/oracle_equality/alias.0.res.oracle diff --git a/tests/value/oracle_equalities/alias.1.res.oracle b/tests/value/oracle_equality/alias.1.res.oracle similarity index 100% rename from tests/value/oracle_equalities/alias.1.res.oracle rename to tests/value/oracle_equality/alias.1.res.oracle diff --git a/tests/value/oracle_equalities/alias.2.res.oracle b/tests/value/oracle_equality/alias.2.res.oracle similarity index 100% rename from tests/value/oracle_equalities/alias.2.res.oracle rename to tests/value/oracle_equality/alias.2.res.oracle diff --git a/tests/value/oracle_equalities/alias.3.res.oracle b/tests/value/oracle_equality/alias.3.res.oracle similarity index 100% rename from tests/value/oracle_equalities/alias.3.res.oracle rename to tests/value/oracle_equality/alias.3.res.oracle diff --git a/tests/value/oracle_equalities/alias.4.res.oracle b/tests/value/oracle_equality/alias.4.res.oracle similarity index 100% rename from tests/value/oracle_equalities/alias.4.res.oracle rename to tests/value/oracle_equality/alias.4.res.oracle diff --git a/tests/value/oracle_equalities/alias.5.res.oracle b/tests/value/oracle_equality/alias.5.res.oracle similarity index 100% rename from tests/value/oracle_equalities/alias.5.res.oracle rename to tests/value/oracle_equality/alias.5.res.oracle diff --git a/tests/value/oracle_equalities/alias.6.res.oracle b/tests/value/oracle_equality/alias.6.res.oracle similarity index 100% rename from tests/value/oracle_equalities/alias.6.res.oracle rename to tests/value/oracle_equality/alias.6.res.oracle diff --git a/tests/value/oracle_equalities/auto_loop_unroll.0.res.oracle b/tests/value/oracle_equality/auto_loop_unroll.0.res.oracle similarity index 100% rename from tests/value/oracle_equalities/auto_loop_unroll.0.res.oracle rename to tests/value/oracle_equality/auto_loop_unroll.0.res.oracle diff --git a/tests/value/oracle_equalities/backward_add_ptr.res.oracle b/tests/value/oracle_equality/backward_add_ptr.res.oracle similarity index 100% rename from tests/value/oracle_equalities/backward_add_ptr.res.oracle rename to tests/value/oracle_equality/backward_add_ptr.res.oracle diff --git a/tests/value/oracle_equalities/bitfield.res.oracle b/tests/value/oracle_equality/bitfield.res.oracle similarity index 100% rename from tests/value/oracle_equalities/bitfield.res.oracle rename to tests/value/oracle_equality/bitfield.res.oracle diff --git a/tests/value/oracle_equalities/bitwise_pointer.res.oracle b/tests/value/oracle_equality/bitwise_pointer.res.oracle similarity index 100% rename from tests/value/oracle_equalities/bitwise_pointer.res.oracle rename to tests/value/oracle_equality/bitwise_pointer.res.oracle diff --git a/tests/value/oracle_equalities/call_simple.res.oracle b/tests/value/oracle_equality/call_simple.res.oracle similarity index 100% rename from tests/value/oracle_equalities/call_simple.res.oracle rename to tests/value/oracle_equality/call_simple.res.oracle diff --git a/tests/value/oracle_equalities/case_analysis.res.oracle b/tests/value/oracle_equality/case_analysis.res.oracle similarity index 100% rename from tests/value/oracle_equalities/case_analysis.res.oracle rename to tests/value/oracle_equality/case_analysis.res.oracle diff --git a/tests/value/oracle_equalities/descending.res.oracle b/tests/value/oracle_equality/descending.res.oracle similarity index 100% rename from tests/value/oracle_equalities/descending.res.oracle rename to tests/value/oracle_equality/descending.res.oracle diff --git a/tests/value/oracle_equalities/domains_function.res.oracle b/tests/value/oracle_equality/domains_function.res.oracle similarity index 100% rename from tests/value/oracle_equalities/domains_function.res.oracle rename to tests/value/oracle_equality/domains_function.res.oracle diff --git a/tests/value/oracle_equalities/downcast.2.res.oracle b/tests/value/oracle_equality/downcast.2.res.oracle similarity index 100% rename from tests/value/oracle_equalities/downcast.2.res.oracle rename to tests/value/oracle_equality/downcast.2.res.oracle diff --git a/tests/value/oracle_equalities/fptr.1.res.oracle b/tests/value/oracle_equality/fptr.1.res.oracle similarity index 100% rename from tests/value/oracle_equalities/fptr.1.res.oracle rename to tests/value/oracle_equality/fptr.1.res.oracle diff --git a/tests/value/oracle_equalities/from_call.0.res.oracle b/tests/value/oracle_equality/from_call.0.res.oracle similarity index 100% rename from tests/value/oracle_equalities/from_call.0.res.oracle rename to tests/value/oracle_equality/from_call.0.res.oracle diff --git a/tests/value/oracle_equalities/from_call.1.res.oracle b/tests/value/oracle_equality/from_call.1.res.oracle similarity index 100% rename from tests/value/oracle_equalities/from_call.1.res.oracle rename to tests/value/oracle_equality/from_call.1.res.oracle diff --git a/tests/value/oracle_equalities/from_termin.res.oracle b/tests/value/oracle_equality/from_termin.res.oracle similarity index 100% rename from tests/value/oracle_equalities/from_termin.res.oracle rename to tests/value/oracle_equality/from_termin.res.oracle diff --git a/tests/value/oracle_equalities/imprecise_invalid_write.res.oracle b/tests/value/oracle_equality/imprecise_invalid_write.res.oracle similarity index 100% rename from tests/value/oracle_equalities/imprecise_invalid_write.res.oracle rename to tests/value/oracle_equality/imprecise_invalid_write.res.oracle diff --git a/tests/value/oracle_equalities/incompatible_states.res.oracle b/tests/value/oracle_equality/incompatible_states.res.oracle similarity index 100% rename from tests/value/oracle_equalities/incompatible_states.res.oracle rename to tests/value/oracle_equality/incompatible_states.res.oracle diff --git a/tests/value/oracle_equalities/library.res.oracle b/tests/value/oracle_equality/library.res.oracle similarity index 100% rename from tests/value/oracle_equalities/library.res.oracle rename to tests/value/oracle_equality/library.res.oracle diff --git a/tests/value/oracle_equalities/long_const.0.res.oracle b/tests/value/oracle_equality/long_const.0.res.oracle similarity index 100% rename from tests/value/oracle_equalities/long_const.0.res.oracle rename to tests/value/oracle_equality/long_const.0.res.oracle diff --git a/tests/value/oracle_equalities/long_const.1.res.oracle b/tests/value/oracle_equality/long_const.1.res.oracle similarity index 100% rename from tests/value/oracle_equalities/long_const.1.res.oracle rename to tests/value/oracle_equality/long_const.1.res.oracle diff --git a/tests/value/oracle_equalities/modulo.res.oracle b/tests/value/oracle_equality/modulo.res.oracle similarity index 100% rename from tests/value/oracle_equalities/modulo.res.oracle rename to tests/value/oracle_equality/modulo.res.oracle diff --git a/tests/value/oracle_equalities/non_natural.res.oracle b/tests/value/oracle_equality/non_natural.res.oracle similarity index 100% rename from tests/value/oracle_equalities/non_natural.res.oracle rename to tests/value/oracle_equality/non_natural.res.oracle diff --git a/tests/value/oracle_equalities/nonlin.res.oracle b/tests/value/oracle_equality/nonlin.res.oracle similarity index 100% rename from tests/value/oracle_equalities/nonlin.res.oracle rename to tests/value/oracle_equality/nonlin.res.oracle diff --git a/tests/value/oracle_equalities/octagons.res.oracle b/tests/value/oracle_equality/octagons.res.oracle similarity index 100% rename from tests/value/oracle_equalities/octagons.res.oracle rename to tests/value/oracle_equality/octagons.res.oracle diff --git a/tests/value/oracle_equalities/offsetmap.0.res.oracle b/tests/value/oracle_equality/offsetmap.0.res.oracle similarity index 100% rename from tests/value/oracle_equalities/offsetmap.0.res.oracle rename to tests/value/oracle_equality/offsetmap.0.res.oracle diff --git a/tests/value/oracle_equalities/offsetmap.1.res.oracle b/tests/value/oracle_equality/offsetmap.1.res.oracle similarity index 100% rename from tests/value/oracle_equalities/offsetmap.1.res.oracle rename to tests/value/oracle_equality/offsetmap.1.res.oracle diff --git a/tests/value/oracle_equalities/origin.0.res.oracle b/tests/value/oracle_equality/origin.0.res.oracle similarity index 100% rename from tests/value/oracle_equalities/origin.0.res.oracle rename to tests/value/oracle_equality/origin.0.res.oracle diff --git a/tests/value/oracle_equalities/period.res.oracle b/tests/value/oracle_equality/period.res.oracle similarity index 100% rename from tests/value/oracle_equalities/period.res.oracle rename to tests/value/oracle_equality/period.res.oracle diff --git a/tests/value/oracle_equalities/plevel.res.oracle b/tests/value/oracle_equality/plevel.res.oracle similarity index 100% rename from tests/value/oracle_equalities/plevel.res.oracle rename to tests/value/oracle_equality/plevel.res.oracle diff --git a/tests/value/oracle_equalities/pointer_comp.res.oracle b/tests/value/oracle_equality/pointer_comp.res.oracle similarity index 100% rename from tests/value/oracle_equalities/pointer_comp.res.oracle rename to tests/value/oracle_equality/pointer_comp.res.oracle diff --git a/tests/value/oracle_equalities/ptr_relation.0.res.oracle b/tests/value/oracle_equality/ptr_relation.0.res.oracle similarity index 100% rename from tests/value/oracle_equalities/ptr_relation.0.res.oracle rename to tests/value/oracle_equality/ptr_relation.0.res.oracle diff --git a/tests/value/oracle_equalities/redundant_alarms.res.oracle b/tests/value/oracle_equality/redundant_alarms.res.oracle similarity index 100% rename from tests/value/oracle_equalities/redundant_alarms.res.oracle rename to tests/value/oracle_equality/redundant_alarms.res.oracle diff --git a/tests/value/oracle_equalities/relation_reduction.res.oracle b/tests/value/oracle_equality/relation_reduction.res.oracle similarity index 100% rename from tests/value/oracle_equalities/relation_reduction.res.oracle rename to tests/value/oracle_equality/relation_reduction.res.oracle diff --git a/tests/value/oracle_equalities/relation_shift.res.oracle b/tests/value/oracle_equality/relation_shift.res.oracle similarity index 100% rename from tests/value/oracle_equalities/relation_shift.res.oracle rename to tests/value/oracle_equality/relation_shift.res.oracle diff --git a/tests/value/oracle_equalities/relations.res.oracle b/tests/value/oracle_equality/relations.res.oracle similarity index 100% rename from tests/value/oracle_equalities/relations.res.oracle rename to tests/value/oracle_equality/relations.res.oracle diff --git a/tests/value/oracle_equalities/relations2.res.oracle b/tests/value/oracle_equality/relations2.res.oracle similarity index 100% rename from tests/value/oracle_equalities/relations2.res.oracle rename to tests/value/oracle_equality/relations2.res.oracle diff --git a/tests/value/oracle_equalities/struct2.res.oracle b/tests/value/oracle_equality/struct2.res.oracle similarity index 100% rename from tests/value/oracle_equalities/struct2.res.oracle rename to tests/value/oracle_equality/struct2.res.oracle diff --git a/tests/value/oracle_gauges/audit.res.oracle b/tests/value/oracle_gauges/audit.res.oracle deleted file mode 100644 index 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- a/tests/value/oracle_gauges/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle b/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle index b53899a72738a7c9f35605d4cba511a0cb611d45..acb3b936b41fb972ec550113fd21dcb346e961f3 100644 --- a/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle +++ b/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle @@ -57,139 +57,139 @@ < Frama_C_show_each_32_64: [0..2147483647] --- > [eva] tests/value/auto_loop_unroll.c:122: Frama_C_show_each_32_64: [32..65] -194,197c172 -< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning: +196,199c174 +< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:194: +< [eva] tests/value/auto_loop_unroll.c:206: < Frama_C_show_each_imprecise: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [1..9] -199,200d173 -< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning: +> [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [1..9] +201,202d175 +< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -204c177 +206c179 < Frama_C_show_each_imprecise: [0..2147483647] --- > Frama_C_show_each_imprecise: [64..2147483647] -210,212c183 -< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning: +212,214c185 +< [eva:alarm] tests/value/auto_loop_unroll.c:224: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: {11} -214,216c185 -< [eva:alarm] tests/value/auto_loop_unroll.c:217: Warning: +> [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: {11} +216,218c187 +< [eva:alarm] tests/value/auto_loop_unroll.c:229: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: {12} -218,219d186 -< [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning: +> [eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: {12} +220,221d188 +< [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -221a189,190 -> [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning: +223a191,192 +> [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -225,226d193 -< [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning: +227,228d195 +< [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -228a196,197 -> [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning: +230a198,199 +> [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -232,233d200 -< [eva:alarm] tests/value/auto_loop_unroll.c:236: Warning: +234,235d202 +< [eva:alarm] tests/value/auto_loop_unroll.c:248: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -237,240c204 -< [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning: +239,242c206 +< [eva:alarm] tests/value/auto_loop_unroll.c:253: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:245: +< [eva] tests/value/auto_loop_unroll.c:257: < Frama_C_show_each_11_111: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:245: Frama_C_show_each_11_111: [11..111] -242,244c206 -< [eva:alarm] tests/value/auto_loop_unroll.c:251: Warning: +> [eva] tests/value/auto_loop_unroll.c:257: Frama_C_show_each_11_111: [11..111] +244,246c208 +< [eva:alarm] tests/value/auto_loop_unroll.c:263: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [16..2147483647] -252,254c214 -< [eva:alarm] tests/value/auto_loop_unroll.c:263: Warning: +> [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [16..2147483647] +254,256c216 +< [eva:alarm] tests/value/auto_loop_unroll.c:275: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [20..2147483646] -256,257d215 -< [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning: +> [eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [20..2147483646] +258,259d217 +< [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -260c218,220 -< [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: [0..2147483647] +262c220,222 +< [eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: [0..2147483647] --- -> [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning: +> [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -> [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: {21} -264,265d223 -< [eva:alarm] tests/value/auto_loop_unroll.c:272: Warning: +> [eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: {21} +266,267d225 +< [eva:alarm] tests/value/auto_loop_unroll.c:284: Warning: < signed overflow. assert i + 1 ≤ 2147483647; -270,271d227 -< [eva:alarm] tests/value/auto_loop_unroll.c:279: Warning: +272,273d229 +< [eva:alarm] tests/value/auto_loop_unroll.c:291: Warning: < signed overflow. assert i + 1 ≤ 2147483647; -276,277d231 -< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning: -< signed overflow. assert i + 1 ≤ 2147483647; -284,286c238,239 +278,279d233 < [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning: +< signed overflow. assert i + 1 ≤ 2147483647; +286,288c240,241 +< [eva:alarm] tests/value/auto_loop_unroll.c:311: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: {30} -> [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations -289d241 -< [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations -292,294c244 -< [eva:alarm] tests/value/auto_loop_unroll.c:316: Warning: +> [eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: {30} +> [eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations +291d243 +< [eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations +294,296c246 +< [eva:alarm] tests/value/auto_loop_unroll.c:328: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: [0..2147483647] +< [eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: {32} -307,310c257 -< [eva:alarm] tests/value/auto_loop_unroll.c:343: Warning: +> [eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: {32} +309,312c259 +< [eva:alarm] tests/value/auto_loop_unroll.c:355: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:345: +< [eva] tests/value/auto_loop_unroll.c:357: < Frama_C_show_each_0_35: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:345: Frama_C_show_each_0_35: [0..35] -313,314d259 +> [eva] tests/value/auto_loop_unroll.c:357: Frama_C_show_each_0_35: [0..35] +315,316d261 < signed overflow. assert res + 1 ≤ 2147483647; -< [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning: -316c261,263 -< [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: [0..2147483647] +< [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning: +318c263,265 +< [eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: [0..2147483647] --- -> [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning: +> [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning: > signed overflow. assert res + 1 ≤ 2147483647; -> [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: {36} -325,327c272 -< [eva:alarm] tests/value/auto_loop_unroll.c:371: Warning: +> [eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: {36} +327,329c274 +< [eva:alarm] tests/value/auto_loop_unroll.c:383: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: [1..2147483647] +< [eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: [1..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: {50} -330,331d274 -< [eva:alarm] tests/value/auto_loop_unroll.c:380: Warning: -< signed overflow. assert -2147483648 ≤ i - 1; -339,342d281 +> [eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: {50} +332,333d276 < [eva:alarm] tests/value/auto_loop_unroll.c:392: Warning: +< signed overflow. assert -2147483648 ≤ i - 1; +341,344d283 +< [eva:alarm] tests/value/auto_loop_unroll.c:404: Warning: < signed overflow. assert j + 1 ≤ 2147483647; -< [eva:alarm] tests/value/auto_loop_unroll.c:396: Warning: +< [eva:alarm] tests/value/auto_loop_unroll.c:408: Warning: < signed overflow. assert j + 1 ≤ 2147483647; -344c283 -< [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: [0..2147483647] +346c285 +< [eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: {30} -346,349d284 -< [eva:alarm] tests/value/auto_loop_unroll.c:403: Warning: +> [eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: {30} +348,351d286 +< [eva:alarm] tests/value/auto_loop_unroll.c:415: Warning: < signed overflow. assert j + 1 ≤ 2147483647; -< [eva:alarm] tests/value/auto_loop_unroll.c:407: Warning: +< [eva:alarm] tests/value/auto_loop_unroll.c:419: Warning: < signed overflow. assert j + 1 ≤ 2147483647; -351c286 -< [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [0..2147483647] +353c288 +< [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [15..45] +> [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [15..45] diff --git a/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle b/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle index 69c5d75fdc9b168fb5e84a39b225b0e6a9ac2f9f..59ea5970bd9b665e9f627703a65474a83aeff80a 100644 --- a/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle +++ b/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle @@ -12,20 +12,20 @@ < Frama_C_show_each_imprecise: [0..2147483647] --- > [eva] tests/value/auto_loop_unroll.c:41: Frama_C_show_each_imprecise: {100} -335,338c329 -< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning: +337,340c331 +< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -< [eva] tests/value/auto_loop_unroll.c:194: +< [eva] tests/value/auto_loop_unroll.c:206: < Frama_C_show_each_imprecise: [0..2147483647] --- -> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [1..9] -340,341d330 -< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning: +> [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [1..9] +342,343d332 +< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning: < signed overflow. assert res + 1 ≤ 2147483647; -345c334 +347c336 < Frama_C_show_each_imprecise: [0..2147483647] --- > Frama_C_show_each_imprecise: [64..2147483647] -381,382d369 -< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning: +383,384d371 +< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning: < signed overflow. assert i + 1 ≤ 2147483647; diff --git a/tests/value/oracle_octagons/alias.1.res.oracle b/tests/value/oracle_octagon/alias.1.res.oracle similarity index 100% rename from tests/value/oracle_octagons/alias.1.res.oracle rename to tests/value/oracle_octagon/alias.1.res.oracle diff --git a/tests/value/oracle_octagons/alias.2.res.oracle b/tests/value/oracle_octagon/alias.2.res.oracle similarity index 100% rename from tests/value/oracle_octagons/alias.2.res.oracle rename to tests/value/oracle_octagon/alias.2.res.oracle diff --git a/tests/value/oracle_octagons/alias.3.res.oracle b/tests/value/oracle_octagon/alias.3.res.oracle similarity index 100% rename from tests/value/oracle_octagons/alias.3.res.oracle rename to tests/value/oracle_octagon/alias.3.res.oracle diff --git a/tests/value/oracle_octagons/alias.5.res.oracle b/tests/value/oracle_octagon/alias.5.res.oracle similarity index 100% rename from tests/value/oracle_octagons/alias.5.res.oracle rename to tests/value/oracle_octagon/alias.5.res.oracle diff --git a/tests/value/oracle_octagons/alias.6.res.oracle b/tests/value/oracle_octagon/alias.6.res.oracle similarity index 100% rename from tests/value/oracle_octagons/alias.6.res.oracle rename to tests/value/oracle_octagon/alias.6.res.oracle diff --git a/tests/value/oracle_octagons/auto_loop_unroll.0.res.oracle b/tests/value/oracle_octagon/auto_loop_unroll.0.res.oracle similarity index 55% rename from tests/value/oracle_octagons/auto_loop_unroll.0.res.oracle rename to tests/value/oracle_octagon/auto_loop_unroll.0.res.oracle index 88c7352194e032c8c77c2feede550015b0d8113a..04f9ac7adc919a19e2bc43d4dd89b823377227e3 100644 --- a/tests/value/oracle_octagons/auto_loop_unroll.0.res.oracle +++ b/tests/value/oracle_octagon/auto_loop_unroll.0.res.oracle @@ -1,23 +1,23 @@ -220,221d219 -< [eva:alarm] tests/value/auto_loop_unroll.c:222: Warning: +222,223d221 +< [eva:alarm] tests/value/auto_loop_unroll.c:234: Warning: < signed overflow. assert -2147483648 ≤ i_0 - 1; -227,228d224 -< [eva:alarm] tests/value/auto_loop_unroll.c:227: Warning: +229,230d226 +< [eva:alarm] tests/value/auto_loop_unroll.c:239: Warning: < signed overflow. assert -2147483648 ≤ i_1 - 1; -258,259d253 -< [eva:alarm] tests/value/auto_loop_unroll.c:267: Warning: +260,261d255 +< [eva:alarm] tests/value/auto_loop_unroll.c:279: Warning: < signed overflow. assert -2147483648 ≤ i - 1; -314,315d307 -< [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning: +316,317d309 +< [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning: < signed overflow. assert -2147483648 ≤ i - 1; -330,331d321 -< [eva:alarm] tests/value/auto_loop_unroll.c:380: Warning: +332,333d323 +< [eva:alarm] tests/value/auto_loop_unroll.c:392: Warning: < signed overflow. assert -2147483648 ≤ i - 1; -384c374 +386c376 < i ∈ [-2147483648..50] --- > i ∈ [-1..50] -389,391c379,381 +391,393c381,383 < i ∈ [0..2147483647] < j ∈ [23..2147483647] < k ∈ [22..2147483647] diff --git a/tests/value/oracle_octagons/auto_loop_unroll.1.res.oracle b/tests/value/oracle_octagon/auto_loop_unroll.1.res.oracle similarity index 87% rename from tests/value/oracle_octagons/auto_loop_unroll.1.res.oracle rename to tests/value/oracle_octagon/auto_loop_unroll.1.res.oracle index a4f29dd3292a4588e4f0cd036a44807e4997ff3b..43d97821cb3587d8876d9f2ed32b3ea55cdaca44 100644 --- a/tests/value/oracle_octagons/auto_loop_unroll.1.res.oracle +++ b/tests/value/oracle_octagon/auto_loop_unroll.1.res.oracle @@ -1,4 +1,4 @@ -472,473c472,473 +474,475c474,475 < i ∈ [0..2147483647] < j ∈ [23..2147483647] --- diff --git a/tests/value/oracle_octagons/bitfield.res.oracle b/tests/value/oracle_octagon/bitfield.res.oracle similarity index 100% rename from tests/value/oracle_octagons/bitfield.res.oracle rename to tests/value/oracle_octagon/bitfield.res.oracle diff --git a/tests/value/oracle_octagons/builtins_split.res.oracle b/tests/value/oracle_octagon/builtins_split.res.oracle similarity index 100% rename from tests/value/oracle_octagons/builtins_split.res.oracle rename to tests/value/oracle_octagon/builtins_split.res.oracle diff --git a/tests/value/oracle_octagons/call_simple.res.oracle b/tests/value/oracle_octagon/call_simple.res.oracle similarity index 100% rename from tests/value/oracle_octagons/call_simple.res.oracle rename to tests/value/oracle_octagon/call_simple.res.oracle diff --git a/tests/value/oracle_octagons/descending.res.oracle b/tests/value/oracle_octagon/descending.res.oracle similarity index 100% rename from tests/value/oracle_octagons/descending.res.oracle rename to tests/value/oracle_octagon/descending.res.oracle diff --git a/tests/value/oracle_octagons/downcast.1.res.oracle b/tests/value/oracle_octagon/downcast.1.res.oracle similarity index 100% rename from tests/value/oracle_octagons/downcast.1.res.oracle rename to tests/value/oracle_octagon/downcast.1.res.oracle diff --git a/tests/value/oracle_octagons/equality.res.oracle b/tests/value/oracle_octagon/equality.res.oracle similarity index 100% rename from tests/value/oracle_octagons/equality.res.oracle rename to tests/value/oracle_octagon/equality.res.oracle diff --git a/tests/value/oracle_octagons/find_ivaltop.res.oracle b/tests/value/oracle_octagon/find_ivaltop.res.oracle similarity index 100% rename from tests/value/oracle_octagons/find_ivaltop.res.oracle rename to tests/value/oracle_octagon/find_ivaltop.res.oracle diff --git a/tests/value/oracle_octagons/for_loops.3.res.oracle b/tests/value/oracle_octagon/for_loops.3.res.oracle similarity index 100% rename from tests/value/oracle_octagons/for_loops.3.res.oracle rename to tests/value/oracle_octagon/for_loops.3.res.oracle diff --git a/tests/value/oracle_octagons/gauges.res.oracle b/tests/value/oracle_octagon/gauges.res.oracle similarity index 100% rename from tests/value/oracle_octagons/gauges.res.oracle rename to tests/value/oracle_octagon/gauges.res.oracle diff --git a/tests/value/oracle_octagons/loop.res.oracle b/tests/value/oracle_octagon/loop.res.oracle similarity index 100% rename from tests/value/oracle_octagons/loop.res.oracle rename to tests/value/oracle_octagon/loop.res.oracle diff --git a/tests/value/oracle_octagons/loop_wvar.1.res.oracle b/tests/value/oracle_octagon/loop_wvar.1.res.oracle similarity index 100% rename from tests/value/oracle_octagons/loop_wvar.1.res.oracle rename to tests/value/oracle_octagon/loop_wvar.1.res.oracle diff --git a/tests/value/oracle_octagons/modulo.res.oracle b/tests/value/oracle_octagon/modulo.res.oracle similarity index 100% rename from tests/value/oracle_octagons/modulo.res.oracle rename to tests/value/oracle_octagon/modulo.res.oracle diff --git a/tests/value/oracle_octagons/non_natural.res.oracle b/tests/value/oracle_octagon/non_natural.res.oracle similarity index 100% rename from tests/value/oracle_octagons/non_natural.res.oracle rename to tests/value/oracle_octagon/non_natural.res.oracle diff --git a/tests/value/oracle_octagons/nonlin.res.oracle b/tests/value/oracle_octagon/nonlin.res.oracle similarity index 100% rename from tests/value/oracle_octagons/nonlin.res.oracle rename to tests/value/oracle_octagon/nonlin.res.oracle diff --git a/tests/value/oracle_octagons/plevel.res.oracle b/tests/value/oracle_octagon/plevel.res.oracle similarity index 100% rename from tests/value/oracle_octagons/plevel.res.oracle rename to tests/value/oracle_octagon/plevel.res.oracle diff --git a/tests/value/oracle_octagons/ptr_relation.1.res.oracle b/tests/value/oracle_octagon/ptr_relation.1.res.oracle similarity index 100% rename from tests/value/oracle_octagons/ptr_relation.1.res.oracle rename to tests/value/oracle_octagon/ptr_relation.1.res.oracle diff --git a/tests/value/oracle_octagons/relation_reduction.res.oracle b/tests/value/oracle_octagon/relation_reduction.res.oracle similarity index 100% rename from tests/value/oracle_octagons/relation_reduction.res.oracle rename to tests/value/oracle_octagon/relation_reduction.res.oracle diff --git a/tests/value/oracle_octagons/relation_shift.res.oracle b/tests/value/oracle_octagon/relation_shift.res.oracle similarity index 100% rename from tests/value/oracle_octagons/relation_shift.res.oracle rename to tests/value/oracle_octagon/relation_shift.res.oracle diff --git a/tests/value/oracle_octagons/relations.res.oracle b/tests/value/oracle_octagon/relations.res.oracle similarity index 100% rename from tests/value/oracle_octagons/relations.res.oracle rename to tests/value/oracle_octagon/relations.res.oracle diff --git a/tests/value/oracle_octagons/relations2.res.oracle b/tests/value/oracle_octagon/relations2.res.oracle similarity index 100% rename from tests/value/oracle_octagons/relations2.res.oracle rename to tests/value/oracle_octagon/relations2.res.oracle diff --git a/tests/value/oracle_octagons/semaphore.res.oracle b/tests/value/oracle_octagon/semaphore.res.oracle similarity index 100% rename from tests/value/oracle_octagons/semaphore.res.oracle rename to tests/value/oracle_octagon/semaphore.res.oracle diff --git a/tests/value/oracle_octagons/struct2.res.oracle b/tests/value/oracle_octagon/struct2.res.oracle similarity index 100% rename from tests/value/oracle_octagons/struct2.res.oracle rename to tests/value/oracle_octagon/struct2.res.oracle diff --git a/tests/value/oracle_octagons/test.0.res.oracle b/tests/value/oracle_octagon/test.0.res.oracle similarity index 100% rename from tests/value/oracle_octagons/test.0.res.oracle rename to tests/value/oracle_octagon/test.0.res.oracle diff --git a/tests/value/oracle_octagons/unroll.res.oracle b/tests/value/oracle_octagon/unroll.res.oracle similarity index 100% rename from tests/value/oracle_octagons/unroll.res.oracle rename to tests/value/oracle_octagon/unroll.res.oracle diff --git a/tests/value/oracle_octagons/unroll_simple.res.oracle b/tests/value/oracle_octagon/unroll_simple.res.oracle similarity index 100% rename from tests/value/oracle_octagons/unroll_simple.res.oracle rename to tests/value/oracle_octagon/unroll_simple.res.oracle diff --git a/tests/value/oracle_octagons/audit.res.oracle b/tests/value/oracle_octagons/audit.res.oracle deleted file mode 100644 index 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- a/tests/value/oracle_octagons/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json diff --git a/tests/value/oracle_symblocs/audit.res.oracle b/tests/value/oracle_symblocs/audit.res.oracle deleted file mode 100644 index 9ff41db248872519df6d5b9ea95483fc420a1ff1..0000000000000000000000000000000000000000 --- a/tests/value/oracle_symblocs/audit.res.oracle +++ /dev/null @@ -1,11 +0,0 @@ -1,8d0 -< [kernel:audit] Warning: -< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101 -< [kernel:audit] Warning: -< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) -< [kernel:audit] Warning: -< missing files: -< tests/value/non_existing_file.h -< [kernel] Audit: sources list written to: tests/value/result/audit-out.json -34d25 -< [kernel] Wrote: tests/value/result/audit-out.json