From 21410a365f9f61be1385eb6a59b956ce64ceb278 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 11 Nov 2020 11:31:15 +0100
Subject: [PATCH] [Eva] Add new test cases for the automatic loop unrolling.
---
tests/value/auto_loop_unroll.c | 59 +++++++++-
.../oracle/auto_loop_unroll.0.res.oracle | 109 +++++++++++++-----
.../oracle/auto_loop_unroll.1.res.oracle | 105 ++++++++++++-----
3 files changed, 209 insertions(+), 64 deletions(-)
diff --git a/tests/value/auto_loop_unroll.c b/tests/value/auto_loop_unroll.c
index c713c76af25..5695f8cd18b 100644
--- a/tests/value/auto_loop_unroll.c
+++ b/tests/value/auto_loop_unroll.c
@@ -225,6 +225,14 @@ void various_conditions () {
}
Frama_C_show_each_11_111(res);
res = 0;
+ /* Exit conditions using pointers. */
+ int x = 16;
+ int *p = &x;
+ for (int i = 0 ; i < *p ; ++i) {
+ res++;
+ }
+ Frama_C_show_each_16(res);
+ res = 0;
}
/* Examples of loops where temporary variables are introduced by Frama-C.
@@ -243,7 +251,7 @@ void temporary_variables () {
Frama_C_show_each_21(res);
}
-/* Examples of loops with goto statements. */
+/* Examples of natural loops with goto or continue statements. */
void loops_with_goto () {
int i, res = 0;
for (i = 0; i < 30; i++) {
@@ -254,7 +262,7 @@ void loops_with_goto () {
Frama_C_show_each_30(res);
res = 0;
middle: ;
- /* Should never be unrolled. */
+ /* Can be unrolled, but [res] should still be imprecise. */
for (i = 0; i < 31; i++) {
res++;
if (undet)
@@ -287,6 +295,52 @@ void loops_with_goto () {
}
Frama_C_show_each_top(res);
res = 0;
+ /* Should be unrolled, and [res] should be precise. */
+ for (i = 0; i < 35; i++) {
+ if (undet)
+ continue;
+ res++;
+ }
+ Frama_C_show_each_0_35(res);
+ res = 0;
+ /* Should be unrolled, and [res] should be precise. */
+ for (i = 36; i--; res++) {
+ if (undet)
+ continue;
+ }
+ Frama_C_show_each_36(res);
+ res = 0;
+ /* Should be unrolled, and [res] should be precise. */
+ for (i = 0; i < 37; i++) {
+ if (i < 10)
+ continue;
+ res++;
+ }
+ Frama_C_show_each_27(res);
+ res = 0;
+}
+
+/* Examples of loops formed by goto statements. */
+void non_natural_loops () {
+ int i, res;
+ res = 0;
+ i = 0;
+ loop1:
+ i++;
+ res++;
+ if (i < 50) {
+ goto loop1;
+ }
+ Frama_C_show_each_50(res);
+ res = 0;
+ i = 50;
+ loop2:
+ res++;
+ if (undet && i--) {
+ goto loop2;
+ }
+ Frama_C_show_each_1_51(res);
+ res = 0;
}
void main () {
@@ -296,4 +350,5 @@ void main () {
various_conditions ();
temporary_variables ();
loops_with_goto ();
+ non_natural_loops ();
}
diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle
index 6f274e90fbf..23c479e7089 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:293.
+ Called from tests/value/auto_loop_unroll.c:347.
[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:294.
+ Called from tests/value/auto_loop_unroll.c:348.
[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;
@@ -137,7 +137,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:295.
+ Called from tests/value/auto_loop_unroll.c:349.
[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:135: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -196,7 +196,7 @@
[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:296.
+ Called from tests/value/auto_loop_unroll.c:350.
[eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:193: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -229,51 +229,83 @@
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:226:
Frama_C_show_each_11_111: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:231: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:232: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:234: 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:297.
-[eva] tests/value/auto_loop_unroll.c:235: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:235: Warning:
+ Called from tests/value/auto_loop_unroll.c:351.
+[eva] tests/value/auto_loop_unroll.c:243: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:243: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:236: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:244: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [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:246: Frama_C_show_each_20: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:248: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:249: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:248: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
-[eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:251: Frama_C_show_each_21: [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:298.
-[eva] tests/value/auto_loop_unroll.c:249: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:250: Warning:
+ Called from tests/value/auto_loop_unroll.c:352.
+[eva] tests/value/auto_loop_unroll.c:257: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:258: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: [0..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:259: Warning:
+[eva] tests/value/auto_loop_unroll.c:262: Frama_C_show_each_30: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
-[eva] tests/value/auto_loop_unroll.c:263: Frama_C_show_each_top: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:266: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
+[eva] tests/value/auto_loop_unroll.c:271: Frama_C_show_each_top: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:274: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:275: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: [0..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:276: Warning:
+[eva] tests/value/auto_loop_unroll.c:280: Frama_C_show_each_32: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:275: starting to merge loop iterations
-[eva] tests/value/auto_loop_unroll.c:280:
+[eva] tests/value/auto_loop_unroll.c:283: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:288:
Frama_C_show_each_33_inf: [0..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:292: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:283: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:283: Warning:
+[eva] tests/value/auto_loop_unroll.c:291: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:291: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_top: [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] tests/value/auto_loop_unroll.c:304:
+ Frama_C_show_each_0_35: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_top: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning:
+ signed overflow. assert -2147483648 ≤ i - 1;
+[eva] tests/value/auto_loop_unroll.c:311: Frama_C_show_each_36: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:314: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:317: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:319: 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:353.
+[eva:alarm] tests/value/auto_loop_unroll.c:330: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:334: Frama_C_show_each_50: [1..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:338: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:339: Warning:
+ signed overflow. assert -2147483648 ≤ i - 1;
+[eva] tests/value/auto_loop_unroll.c:342:
+ Frama_C_show_each_1_51: [1..2147483647]
+[eva] Recording results for non_natural_loops
+[eva] Done for function non_natural_loops
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -298,7 +330,10 @@
[8] ∈ {8}
[9] ∈ {9}
[eva:final-states] Values at end of function loops_with_goto:
- i ∈ [34..2147483647]
+ i ∈ {37}
+ res ∈ {0}
+[eva:final-states] Values at end of function non_natural_loops:
+ i ∈ [-2147483648..50]
res ∈ {0}
[eva:final-states] Values at end of function simple_loops:
res ∈ {100}
@@ -308,6 +343,8 @@
[eva:final-states] Values at end of function various_conditions:
i ∈ {12}
res ∈ {0}
+ x ∈ {16}
+ p ∈ {{ &x }}
[eva:final-states] Values at end of function various_loops:
Frama_C_entropy_source ∈ [--..--]
g ∈ [101..2147483647]
@@ -325,6 +362,8 @@
[from] Done for function complex_loops
[from] Computing for function loops_with_goto
[from] Done for function loops_with_goto
+[from] Computing for function non_natural_loops
+[from] Done for function non_natural_loops
[from] Computing for function simple_loops
[from] Done for function simple_loops
[from] Computing for function temporary_variables
@@ -350,6 +389,8 @@
g FROM \nothing
[from] Function loops_with_goto:
NO EFFECTS
+[from] Function non_natural_loops:
+ NO EFFECTS
[from] Function simple_loops:
NO EFFECTS
[from] Function temporary_variables:
@@ -376,9 +417,13 @@
[inout] Inputs for function complex_loops:
undet; g
[inout] Out (internal) for function loops_with_goto:
- i; res
+ i; res; tmp
[inout] Inputs for function loops_with_goto:
undet
+[inout] Out (internal) for function non_natural_loops:
+ i; res; tmp
+[inout] Inputs for function non_natural_loops:
+ undet
[inout] Out (internal) for function simple_loops:
res; i; i_0; i_1; i_2
[inout] Inputs for function simple_loops:
@@ -388,7 +433,7 @@
[inout] Inputs for function temporary_variables:
\nothing
[inout] Out (internal) for function various_conditions:
- i; res; i_0; tmp; i_1; tmp_0; i_2; i_3
+ i; res; i_0; tmp; i_1; tmp_0; i_2; i_3; x; p; i_4
[inout] Inputs for function various_conditions:
undet
[inout] Out (internal) for function various_loops:
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index f743d1ef27e..8ab0e3b6790 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:293.
+ Called from tests/value/auto_loop_unroll.c:347.
[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:294.
+ Called from tests/value/auto_loop_unroll.c:348.
[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.
@@ -281,7 +281,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:295.
+ Called from tests/value/auto_loop_unroll.c:349.
[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:135: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -340,7 +340,7 @@
[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:296.
+ Called from tests/value/auto_loop_unroll.c:350.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:192: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: {11}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:197: Automatic loop unrolling.
@@ -355,44 +355,76 @@
[eva] tests/value/auto_loop_unroll.c:221:
Trace partitioning superposing up to 100 states
[eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11_111: [11..111]
+[eva] tests/value/auto_loop_unroll.c:231: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:232: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:234: 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:297.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:235: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: {20}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:240: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: {21}
+ Called from tests/value/auto_loop_unroll.c:351.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:243: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:246: Frama_C_show_each_20: {20}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:248: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:251: Frama_C_show_each_21: {21}
[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:298.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:249: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: {30}
-[eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:259: Warning:
+ Called from tests/value/auto_loop_unroll.c:352.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:257: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:262: Frama_C_show_each_30: {30}
+[eva] tests/value/auto_loop_unroll.c:266: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:263: Frama_C_show_each_top: [0..2147483647]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:266: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: {32}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:275: Automatic loop unrolling.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:276: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:276:
+[eva] tests/value/auto_loop_unroll.c:271: Frama_C_show_each_top: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:274: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:280: Frama_C_show_each_32: {32}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:283: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:284: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:284:
Trace partitioning superposing up to 100 states
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:278:
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:286:
loop not completely unrolled
-[eva:alarm] tests/value/auto_loop_unroll.c:276: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:280:
+[eva] tests/value/auto_loop_unroll.c:288:
Frama_C_show_each_33_inf: [33..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:292: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:283: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:283: Warning:
+[eva] tests/value/auto_loop_unroll.c:291: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:291: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_top: [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] tests/value/auto_loop_unroll.c:304:
+ Frama_C_show_each_0_35: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning:
+ signed overflow. assert -2147483648 ≤ i - 1;
+[eva] tests/value/auto_loop_unroll.c:311: Frama_C_show_each_36: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:314: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:317: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_top: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:319: 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:353.
+[eva:alarm] tests/value/auto_loop_unroll.c:330: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:334: Frama_C_show_each_50: [1..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:338: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:339: Warning:
+ signed overflow. assert -2147483648 ≤ i - 1;
+[eva] tests/value/auto_loop_unroll.c:342:
+ Frama_C_show_each_1_51: [1..2147483647]
+[eva] Recording results for non_natural_loops
+[eva] Done for function non_natural_loops
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -417,7 +449,10 @@
[8] ∈ {8}
[9] ∈ {9}
[eva:final-states] Values at end of function loops_with_goto:
- i ∈ [34..2147483647]
+ i ∈ {37}
+ res ∈ {0}
+[eva:final-states] Values at end of function non_natural_loops:
+ i ∈ [-2147483648..50]
res ∈ {0}
[eva:final-states] Values at end of function simple_loops:
res ∈ {100}
@@ -427,6 +462,8 @@
[eva:final-states] Values at end of function various_conditions:
i ∈ {12}
res ∈ {0}
+ x ∈ {16}
+ p ∈ {{ &x }}
[eva:final-states] Values at end of function various_loops:
Frama_C_entropy_source ∈ [--..--]
g ∈ {126}
@@ -444,6 +481,8 @@
[from] Done for function complex_loops
[from] Computing for function loops_with_goto
[from] Done for function loops_with_goto
+[from] Computing for function non_natural_loops
+[from] Done for function non_natural_loops
[from] Computing for function simple_loops
[from] Done for function simple_loops
[from] Computing for function temporary_variables
@@ -469,6 +508,8 @@
g FROM \nothing
[from] Function loops_with_goto:
NO EFFECTS
+[from] Function non_natural_loops:
+ NO EFFECTS
[from] Function simple_loops:
NO EFFECTS
[from] Function temporary_variables:
@@ -495,9 +536,13 @@
[inout] Inputs for function complex_loops:
undet; g
[inout] Out (internal) for function loops_with_goto:
- i; res
+ i; res; tmp
[inout] Inputs for function loops_with_goto:
undet
+[inout] Out (internal) for function non_natural_loops:
+ i; res; tmp
+[inout] Inputs for function non_natural_loops:
+ undet
[inout] Out (internal) for function simple_loops:
res; i; i_0; i_1; i_2
[inout] Inputs for function simple_loops:
@@ -507,7 +552,7 @@
[inout] Inputs for function temporary_variables:
\nothing
[inout] Out (internal) for function various_conditions:
- i; res; i_0; tmp; i_1; tmp_0; i_2; i_3
+ i; res; i_0; tmp; i_1; tmp_0; i_2; i_3; x; p; i_4
[inout] Inputs for function various_conditions:
undet
[inout] Out (internal) for function various_loops:
--
GitLab