From f26cf0afb3989622991543b02897ba0b07157109 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 22 Oct 2019 13:24:53 +0200
Subject: [PATCH] [Eva] New test file for the automatic loop unrolling
heuristic.
---
tests/value/auto_loop_unroll.c | 192 ++++++++
.../oracle/auto_loop_unroll.0.res.oracle | 297 ++++++++++++
.../oracle/auto_loop_unroll.1.res.oracle | 431 ++++++++++++++++++
3 files changed, 920 insertions(+)
create mode 100644 tests/value/auto_loop_unroll.c
create mode 100644 tests/value/oracle/auto_loop_unroll.0.res.oracle
create mode 100644 tests/value/oracle/auto_loop_unroll.1.res.oracle
diff --git a/tests/value/auto_loop_unroll.c b/tests/value/auto_loop_unroll.c
new file mode 100644
index 00000000000..d3a1a1ce141
--- /dev/null
+++ b/tests/value/auto_loop_unroll.c
@@ -0,0 +1,192 @@
+/* run.config*
+ STDOPT: +"-eva-auto-loop-unroll 10"
+ STDOPT: +"-eva-auto-loop-unroll 128"
+*/
+
+/* Tests the automatic loop unrolling heuristic. */
+
+#include <__fc_builtin.h>
+
+volatile int undet;
+
+int g = 0;
+void incr_g () {
+ g++;
+}
+
+int incr (int i) {
+ return i+1;
+}
+
+void simple_loops () {
+ int res = 0;
+ /* This loop should be automatically unrolled on the second run. */
+ for (int i = 0; i < 100; i++) {
+ res++;
+ }
+ Frama_C_show_each_auto(res);
+ res = 0;
+ /* This loop should not be automatically unrolled. */
+ for (int i = 0; i < 1000; i++) {
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ /* The annotation has priority over the automatic loop unrolling:
+ this loop should never be unrolled. */
+ /*@ loop unroll 0; */
+ for (int i = 0; i < 100; i++) {
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ /* The annnotation has priority over the automatic loop unrolling:
+ this loop should always be unrolled. */
+ /*@ loop unroll 100; */
+ for (int i = 0; i < 100; i++) {
+ res++;
+ }
+ Frama_C_show_each_singleton(res);
+}
+
+/* Examples of various loops that should be automatically unrolled
+ on the second run, but not on the first. */
+void various_loops () {
+ int res = 0;
+ /* Decreasing loop counter. */
+ for (int i = 64; i > 0; i--)
+ res++;
+ Frama_C_show_each_64(res);
+ res = 0;
+ /* Decrements the loop counter by 3. */
+ for (int i = 120; i > 0; i -= 3)
+ res++;
+ Frama_C_show_each_40(res);
+ res = 0;
+ /* Several increments of the loop counter. */
+ for (int i = 0; i < 160; i++) {
+ i += 2;
+ res++;
+ i--;
+ }
+ Frama_C_show_each_80(res);
+ res = 0;
+ /* Random increments of the loop counter. */
+ for (int i = 0; i < 160;) {
+ res++;
+ if (undet)
+ i += 2;
+ else
+ i += 5;
+ }
+ Frama_C_show_each_32_80(res);
+ res = 0;
+ /* Other loop breaking condition. */
+ for (int i = 0; i < 111; i++) {
+ res++;
+ if (undet && res > 10)
+ break;
+ }
+ Frama_C_show_each_11_111(res);
+ res = 0;
+ /* More complex loop condition. */
+ int x = 24;
+ int k = Frama_C_interval(0, 10);
+ for (int i = 75; i + x > 2 * k; i -= 2)
+ res++;
+ Frama_C_show_each_40_50(res);
+ res = 0;
+ /* Loop calling some functions that do not modify the loop counter. */
+ for (int i = 0; i < 25; i++) {
+ incr_g();
+ int t = incr(i);
+ res = incr(res);
+ }
+ Frama_C_show_each_25(res);
+ res = 0;
+ /* Nested loops. */
+ res = 0;
+ for (int i = 0; i < 16; i++) {
+ for (int j = 0; j < i; j++) {
+ res++;
+ }
+ }
+ Frama_C_show_each_120(res);
+ res = 0;
+}
+
+/* Loops that cannot be unrolled. */
+void complex_loops () {
+ /* Loop counter modified through a pointer. */
+ int res = 0;
+ int i = 0;
+ int *p = &i;
+ while (i < 64) {
+ (*p)++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ /* Loop counter modified within a nested loop. */
+ res = 0;
+ i = 0;
+ while (i < 64) {
+ for (int j = 0; j < i; j++) {
+ i++;
+ }
+ res++;
+ i++;
+ }
+ Frama_C_show_each_imprecise(res);
+ /* Loop counter incremented under a condition. */
+ res = 0;
+ i = 0;
+ while (i < 10) {
+ if (undet)
+ i++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ i = 0;
+ while (i < 10) {
+ if (undet)
+ i++;
+ else
+ i++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ /* Loop counter modified by a function. */
+ res = 0;
+ g = 0;
+ while (g < 64) {
+ incr_g();
+ g++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ /* Too complex loop condition. */
+ int t[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+ i = 0;
+ while (t[i] < 6) {
+ i++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ /* Random loop condition. */
+ i = 0;
+ while (i < 64 && undet) {
+ i++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+}
+
+
+void main () {
+ simple_loops ();
+ various_loops ();
+ complex_loops ();
+}
diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle
new file mode 100644
index 00000000000..359bdb60f2f
--- /dev/null
+++ b/tests/value/oracle/auto_loop_unroll.0.res.oracle
@@ -0,0 +1,297 @@
+[kernel] Parsing tests/value/auto_loop_unroll.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ undet ∈ [--..--]
+ g ∈ {0}
+[eva] computing for function simple_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:189.
+[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;
+[eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:30: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:33:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:38: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:41:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:46:
+ Trace partitioning superposing up to 100 states
+[eva] tests/value/auto_loop_unroll.c:49: Frama_C_show_each_singleton: {100}
+[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:190.
+[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;
+[eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:62: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:63: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:67: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:69: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:75: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:76: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:82:
+ Frama_C_show_each_32_80: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:85: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:86: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:90:
+ Frama_C_show_each_11_111: [0..2147483647]
+[eva] computing for function Frama_C_interval <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:94.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/auto_loop_unroll.c:94:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/auto_loop_unroll.c:95: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:96: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:97:
+ Frama_C_show_each_40_50: [0..2147483647]
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:100: starting to merge loop iterations
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva:alarm] tests/value/auto_loop_unroll.c:14: Warning:
+ signed overflow. assert g + 1 ≤ 2147483647;
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva:alarm] tests/value/auto_loop_unroll.c:18: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:105: Frama_C_show_each_25: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:110: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:109: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:110: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:111: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:114: Frama_C_show_each_120: [0..2147483647]
+[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:191.
+[eva] tests/value/auto_loop_unroll.c:124: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:126: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:128:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:132: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:134: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:137: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:136: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:139:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:143: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:146: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:148:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:151: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:156: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:158:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:162: starting to merge loop iterations
+[eva] computing for function incr_g <- complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:163.
+[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:163.
+[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:163.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:167:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:176:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:182: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:184:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] Recording results for complex_loops
+[eva] Done for function complex_loops
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function incr:
+ __retres ∈ [1..2147483647]
+[eva:final-states] Values at end of function incr_g:
+ g ∈ [1..2147483647]
+[eva:final-states] Values at end of function complex_loops:
+ g ∈ {64}
+ res ∈ [0..2147483647]
+ i ∈ [0..64]
+ p ∈ {{ &i }}
+ t[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {2}
+ [3] ∈ {3}
+ [4] ∈ {4}
+ [5] ∈ {5}
+ [6] ∈ {6}
+ [7] ∈ {7}
+ [8] ∈ {8}
+ [9] ∈ {9}
+[eva:final-states] Values at end of function simple_loops:
+ res ∈ {100}
+[eva:final-states] Values at end of function various_loops:
+ Frama_C_entropy_source ∈ [--..--]
+ g ∈ [0..2147483647]
+ res ∈ {0}
+ x ∈ {24}
+ k ∈ [0..10]
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ g ∈ {64}
+[from] Computing for function incr
+[from] Done for function incr
+[from] Computing for function incr_g
+[from] Done for function incr_g
+[from] Computing for function complex_loops
+[from] Done for function complex_loops
+[from] Computing for function simple_loops
+[from] Done for function simple_loops
+[from] Computing for function various_loops
+[from] Computing for function Frama_C_interval <-various_loops
+[from] Done for function Frama_C_interval
+[from] Done for function various_loops
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function incr:
+ \result FROM i
+[from] Function incr_g:
+ g FROM g
+[from] Function complex_loops:
+ g FROM \nothing
+[from] Function simple_loops:
+ NO EFFECTS
+[from] Function various_loops:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ g FROM g (and SELF)
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ g FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function incr:
+ __retres
+[inout] Inputs for function incr:
+ \nothing
+[inout] Out (internal) for function incr_g:
+ g
+[inout] Inputs for function incr_g:
+ g
+[inout] Out (internal) for function complex_loops:
+ g; res; i; p; j; t[0..9]
+[inout] Inputs for function complex_loops:
+ undet; g
+[inout] Out (internal) for function simple_loops:
+ res; i; i_0; i_1; i_2
+[inout] Inputs for function simple_loops:
+ \nothing
+[inout] Out (internal) for function various_loops:
+ Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; i_3; x; k; i_4; i_5;
+ t; i_6; j
+[inout] Inputs for function various_loops:
+ Frama_C_entropy_source; undet; g
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; g
+[inout] Inputs for function main:
+ Frama_C_entropy_source; undet; g
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
new file mode 100644
index 00000000000..775a7323bf9
--- /dev/null
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -0,0 +1,431 @@
+[kernel] Parsing tests/value/auto_loop_unroll.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ undet ∈ [--..--]
+ g ∈ {0}
+[eva] computing for function simple_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:189.
+[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
+[eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: {100}
+[eva] tests/value/auto_loop_unroll.c:30: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:33:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:38: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:41:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:49: Frama_C_show_each_singleton: {100}
+[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:190.
+[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.
+[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] 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] 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]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:85: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:90: Frama_C_show_each_11_111: [11..111]
+[eva] computing for function Frama_C_interval <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:94.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/auto_loop_unroll.c:94:
+ 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:95: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:97: Frama_C_show_each_40_50: [40..50]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:100: Automatic loop unrolling.
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:105: Frama_C_show_each_25: {25}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:109: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:110: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:114: Frama_C_show_each_120: {120}
+[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:191.
+[eva] tests/value/auto_loop_unroll.c:124: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:126: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:128:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:132: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:134: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:137: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:136: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:139:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:143: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:146: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:148:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:151: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:156: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:158:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:162: starting to merge loop iterations
+[eva] computing for function incr_g <- complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:163.
+[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:163.
+[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:163.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:167:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:176:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:182: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:184:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] Recording results for complex_loops
+[eva] Done for function complex_loops
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function incr:
+ __retres ∈ [1..25]
+[eva:final-states] Values at end of function incr_g:
+ g ∈ [1..63]
+[eva:final-states] Values at end of function complex_loops:
+ g ∈ {64}
+ res ∈ [0..2147483647]
+ i ∈ [0..64]
+ p ∈ {{ &i }}
+ t[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {2}
+ [3] ∈ {3}
+ [4] ∈ {4}
+ [5] ∈ {5}
+ [6] ∈ {6}
+ [7] ∈ {7}
+ [8] ∈ {8}
+ [9] ∈ {9}
+[eva:final-states] Values at end of function simple_loops:
+ res ∈ {100}
+[eva:final-states] Values at end of function various_loops:
+ Frama_C_entropy_source ∈ [--..--]
+ g ∈ {25}
+ res ∈ {0}
+ x ∈ {24}
+ k ∈ [0..10]
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ g ∈ {64}
+[from] Computing for function incr
+[from] Done for function incr
+[from] Computing for function incr_g
+[from] Done for function incr_g
+[from] Computing for function complex_loops
+[from] Done for function complex_loops
+[from] Computing for function simple_loops
+[from] Done for function simple_loops
+[from] Computing for function various_loops
+[from] Computing for function Frama_C_interval <-various_loops
+[from] Done for function Frama_C_interval
+[from] Done for function various_loops
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function incr:
+ \result FROM i
+[from] Function incr_g:
+ g FROM g
+[from] Function complex_loops:
+ g FROM \nothing
+[from] Function simple_loops:
+ NO EFFECTS
+[from] Function various_loops:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ g FROM g (and SELF)
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ g FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function incr:
+ __retres
+[inout] Inputs for function incr:
+ \nothing
+[inout] Out (internal) for function incr_g:
+ g
+[inout] Inputs for function incr_g:
+ g
+[inout] Out (internal) for function complex_loops:
+ g; res; i; p; j; t[0..9]
+[inout] Inputs for function complex_loops:
+ undet; g
+[inout] Out (internal) for function simple_loops:
+ res; i; i_0; i_1; i_2
+[inout] Inputs for function simple_loops:
+ \nothing
+[inout] Out (internal) for function various_loops:
+ Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; i_3; x; k; i_4; i_5;
+ t; i_6; j
+[inout] Inputs for function various_loops:
+ Frama_C_entropy_source; undet; g
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; g
+[inout] Inputs for function main:
+ Frama_C_entropy_source; undet; g
--
GitLab