diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json index 37b15f621160b41164b54a6e7a12dfb98166efaf..8cdec560c40031b74821a19934281e6acab08674 100644 --- a/tests/misc/oracle/audit-out.json +++ b/tests/misc/oracle/audit-out.json @@ -43,8 +43,8 @@ "taint" ], "disabled": [ - "garbled-mix", "invalid-assigns", "loop-unroll", "malloc:weak", - "missing-loop-unroll", "missing-loop-unroll:for" + "garbled-mix", "invalid-assigns", "loop-unroll", "loop-unroll:auto", + "malloc:weak", "missing-loop-unroll", "missing-loop-unroll:for" ] } }, diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle index 485d1f41d3be3aba44e9b92bc38ab195c6ca6809..f68ab995441dfd4f14bdd14cc8f3c5da96b8f70a 100644 --- a/tests/value/oracle/auto_loop_unroll.0.res.oracle +++ b/tests/value/oracle/auto_loop_unroll.0.res.oracle @@ -123,7 +123,8 @@ [eva] Recording results for incr [eva] Done for function incr [eva] tests/value/auto_loop_unroll.c:103: Frama_C_show_each_25: [0..2147483647] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:108: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:108: + Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:107: starting to merge loop iterations [eva] tests/value/auto_loop_unroll.c:108: starting to merge loop iterations [eva:alarm] tests/value/auto_loop_unroll.c:109: Warning: diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle index 1a4b5f83bab11263da5a047cb211f4f69164591a..3d5a7ef165f5f6eee6530b78ceb2c30ea4f63646 100644 --- a/tests/value/oracle/auto_loop_unroll.1.res.oracle +++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle @@ -7,7 +7,8 @@ g ∈ {0} [eva] computing for function simple_loops <- main. Called from tests/value/auto_loop_unroll.c:428. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:24: Automatic loop unrolling. +[eva:loop-unroll:auto] 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 [eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: {100} @@ -26,13 +27,17 @@ [eva] Done for function simple_loops [eva] computing for function various_loops <- main. Called from tests/value/auto_loop_unroll.c:429. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:57: Automatic loop unrolling. +[eva:loop-unroll:auto] 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. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:62: + Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: {40} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:67: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:67: + Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: {80} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:75: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:75: + Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:75: Trace partitioning superposing up to 100 states [eva] tests/value/auto_loop_unroll.c:82: Frama_C_show_each_32_80: [32..80] @@ -42,11 +47,14 @@ [eva] tests/value/auto_loop_unroll.c:86: function Frama_C_interval: precondition 'order' got status valid. [eva] Done for function Frama_C_interval -[eva:loop-unroll] tests/value/auto_loop_unroll.c:87: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:87: + Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:89: Frama_C_show_each_40_50: [40..50] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:92: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:92: + Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:95: Frama_C_show_each_101: {101} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:98: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:98: + Automatic loop unrolling. [eva] computing for function incr_g <- various_loops <- main. Called from tests/value/auto_loop_unroll.c:99. [eva] Recording results for incr_g @@ -273,12 +281,16 @@ [eva] Done for function incr [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr [eva] tests/value/auto_loop_unroll.c:103: Frama_C_show_each_25: {25} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:107: Automatic loop unrolling. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:108: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:107: + Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:108: + Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:112: Frama_C_show_each_120: {120} -[eva:loop-unroll] tests/value/auto_loop_unroll.c:115: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:115: + Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:122: Frama_C_show_each_32_64: [32..64] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:125: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/auto_loop_unroll.c:125: + Automatic loop unrolling. [eva] tests/value/auto_loop_unroll.c:132: Frama_C_show_each_1_28: [1..28] [eva] tests/value/auto_loop_unroll.c:134: starting to merge loop iterations [eva:alarm] tests/value/auto_loop_unroll.c:139: Warning: @@ -349,33 +361,44 @@ [eva] Done for function complex_loops [eva] computing for function various_conditions <- main. Called from tests/value/auto_loop_unroll.c:431. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:223: Automatic loop unrolling. +[eva:loop-unroll:auto] 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:loop-unroll:auto] 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:loop-unroll:auto] 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:loop-unroll:auto] 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:loop-unroll:auto] 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:loop-unroll:auto] 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:257: Frama_C_show_each_11_111: [11..111] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:262: Automatic loop unrolling. +[eva:loop-unroll:auto] 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:432. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:274: Automatic loop unrolling. +[eva:loop-unroll:auto] 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:loop-unroll:auto] tests/value/auto_loop_unroll.c:279: + Automatic loop unrolling. [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:loop-unroll:auto] 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:loop-unroll:auto] 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: @@ -387,9 +410,11 @@ [eva] Done for function temporary_variables [eva] computing for function loops_with_goto <- main. Called from tests/value/auto_loop_unroll.c:433. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:310: Automatic loop unrolling. +[eva:loop-unroll:auto] 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:loop-unroll:auto] 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; @@ -397,9 +422,11 @@ Trace partitioning superposing up to 100 states [eva] tests/value/auto_loop_unroll.c:324: Frama_C_show_each_top: [31..2147483647] -[eva:loop-unroll] tests/value/auto_loop_unroll.c:327: Automatic loop unrolling. +[eva:loop-unroll:auto] 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:loop-unroll:auto] 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:341: @@ -410,29 +437,38 @@ [eva:alarm] tests/value/auto_loop_unroll.c:344: Warning: signed overflow. assert res + 1 ≤ 2147483647; [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:loop-unroll:auto] 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:loop-unroll:auto] 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:loop-unroll:auto] 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:434. -[eva:loop-unroll] tests/value/auto_loop_unroll.c:382: Automatic loop unrolling. +[eva:loop-unroll:auto] 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:loop-unroll:auto] 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: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:loop-unroll:auto] tests/value/auto_loop_unroll.c:402: + Automatic loop unrolling. +[eva:loop-unroll:auto] 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:loop-unroll:auto] tests/value/auto_loop_unroll.c:413: + Automatic loop unrolling. +[eva:loop-unroll:auto] 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 diff --git a/tests/value/oracle/taint.res.oracle b/tests/value/oracle/taint.res.oracle index 75144a86df8e788522f2d412ea7bc785dd0b8981..111c04d6d53643435bbb7f63aba2ba67ce3985d8 100644 --- a/tests/value/oracle/taint.res.oracle +++ b/tests/value/oracle/taint.res.oracle @@ -20,7 +20,7 @@ [eva] Done for function taint_basic [eva] computing for function taint_assume_1 <- main. Called from tests/value/taint.c:146. -[eva:loop-unroll] tests/value/taint.c:47: Automatic loop unrolling. +[eva:loop-unroll:auto] tests/value/taint.c:47: Automatic loop unrolling. [eva] tests/value/taint.c:48: Frama_C_dump_each: # taint: