diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index b020de87b292080cf85983ecf88a0e87698bf39d..14af242908ead4186f697795717423c67e0a1b7f 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -1593,15 +1593,15 @@ module Make
let typ = Cil.typeOf expr in
let eval acc state =
match fst (evaluate state expr) with
- | `Bottom -> acc
+ | `Bottom -> (state, `Bottom, false) :: acc
| `Value (_cache, value) ->
let zero_or_one = Cvalue.V.cardinal_zero_or_one (get value) in
- (state, value, zero_or_one) :: acc
+ (state, `Value value, zero_or_one) :: acc
in
let eval_states = List.fold_left eval [] states in
let match_expected_value expected_value states =
let process_one_state (eq, mess, neq) (s, v, zero_or_one as current) =
- if Value.is_included expected_value v then
+ if Bottom.is_included Value.is_included expected_value v then
(* The integer on which we split is part of the result *)
if zero_or_one then
(s :: eq, mess, neq) (* Clean split *)
@@ -1613,7 +1613,7 @@ module Make
List.fold_left process_one_state ([], false, []) states
in
let process_one_value (acc, states) i =
- let value = Value.reduce (Value.inject_int typ i) in
+ let value = `Value (Value.reduce (Value.inject_int typ i)) in
let eq, mess, neq = match_expected_value value states in
(i, eq, mess) :: acc, neq
in
diff --git a/tests/value/oracle/split_return.0.res.oracle b/tests/value/oracle/split_return.0.res.oracle
index e0a0991d0ef1539d7b0127334b596f71da4d8416..342033647fd5610389bc72b57770adf8ebfe9147 100644
--- a/tests/value/oracle/split_return.0.res.oracle
+++ b/tests/value/oracle/split_return.0.res.oracle
@@ -5,6 +5,8 @@
\return(f3) == -2, -4 (user)
\return(f4) == 4 (user)
\return(f5) == -2 (user)
+ \return(uninit) == 0 (user)
+ \return(escaping) == 0 (user)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -15,8 +17,9 @@
i5 ∈ [--..--]
v ∈ [--..--]
v7 ∈ {0}
+ rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:176.
+ Called from tests/value/split_return.i:204.
[eva] computing for function init <- main1 <- main.
Called from tests/value/split_return.i:17.
[eva] using specification for function init
@@ -24,7 +27,7 @@
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:177.
+ Called from tests/value/split_return.i:205.
[eva] computing for function f2 <- main2 <- main.
Called from tests/value/split_return.i:48.
[eva] Recording results for f2
@@ -37,7 +40,7 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:178.
+ Called from tests/value/split_return.i:206.
[eva] computing for function f3 <- main3 <- main.
Called from tests/value/split_return.i:73.
[eva] tests/value/split_return.i:69: f3: cannot properly split on \result == -2
@@ -51,7 +54,7 @@
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -64,7 +67,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:180.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f5 <- main5 <- main.
Called from tests/value/split_return.i:117.
[eva] Recording results for f5
@@ -76,7 +79,7 @@
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:181.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f6 <- main6 <- main.
Called from tests/value/split_return.i:135.
[eva:alarm] tests/value/split_return.i:130: Warning:
@@ -86,7 +89,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:182.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f7 <- main7 <- main.
Called from tests/value/split_return.i:148.
[eva] Recording results for f7
@@ -96,7 +99,7 @@
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -105,9 +108,29 @@
Frama_C_show_each_then8: {-1; 4}, {{ NULL ; &x }}
[eva] Recording results for main8
[eva] Done for function main8
+[eva] computing for function main9 <- main.
+ Called from tests/value/split_return.i:212.
+[eva] computing for function uninit <- main9 <- main.
+ Called from tests/value/split_return.i:199.
+[eva] Recording results for uninit
+[eva] Done for function uninit
+[eva] computing for function escaping <- main9 <- main.
+ Called from tests/value/split_return.i:200.
+[eva:locals-escaping] tests/value/split_return.i:192: Warning:
+ locals {x} escaping the scope of a block of escaping through p
+[eva] Recording results for escaping
+[eva] Done for function escaping
+[eva] computing for function escaping <- main9 <- main.
+ Called from tests/value/split_return.i:200.
+[eva] Recording results for escaping
+[eva] Done for function escaping
+[eva] Recording results for main9
+[eva] Done for function main9
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function escaping:
+ p ∈ ESCAPINGADDR
[eva:final-states] Values at end of function f2:
i2 ∈ {0; 5}
__retres ∈ {0; 5; 7}
@@ -153,12 +176,19 @@
x ∈ {-1; 4}
pf ∈ {{ &f8 }}
p ∈ {{ NULL ; &x }}
+[eva:final-states] Values at end of function uninit:
+ x ∈ {0} or UNINITIALIZED
+[eva:final-states] Values at end of function main9:
+ y ∈ {0} or UNINITIALIZED
+ q ∈ ESCAPINGADDR
[eva:final-states] Values at end of function main:
i2 ∈ {0; 5}
i3 ∈ {0; 5}
i4 ∈ {0; 5}
i5 ∈ {0; 5}
v7 ∈ {0; 1}
+[from] Computing for function escaping
+[from] Done for function escaping
[from] Computing for function f2
[from] Done for function f2
[from] Computing for function f3
@@ -191,10 +221,16 @@
[from] Done for function main7
[from] Computing for function main8
[from] Done for function main8
+[from] Computing for function uninit
+[from] Done for function uninit
+[from] Computing for function main9
+[from] Done for function main9
[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 escaping:
+ \result FROM \nothing
[from] Function f2:
i2 FROM i2
\result FROM i2
@@ -234,6 +270,10 @@
v7 FROM v
[from] Function main8:
NO EFFECTS
+[from] Function uninit:
+ \result FROM rand
+[from] Function main9:
+ NO EFFECTS
[from] Function main:
i2 FROM i2
i3 FROM i3
@@ -241,6 +281,10 @@
i5 FROM i5
v7 FROM v
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function escaping:
+ p
+[inout] Inputs for function escaping:
+ \nothing
[inout] Out (internal) for function f2:
i2; __retres
[inout] Inputs for function f2:
@@ -301,10 +345,18 @@
x; pf; p; tmp
[inout] Inputs for function main8:
v
+[inout] Out (internal) for function uninit:
+ x
+[inout] Inputs for function uninit:
+ rand
+[inout] Out (internal) for function main9:
+ y; q
+[inout] Inputs for function main9:
+ rand
[inout] Out (internal) for function main:
i2; i3; i4; i5; v7
[inout] Inputs for function main:
- i2; i3; i4; i5; v; v7
+ i2; i3; i4; i5; v; v7; rand
[report] Computing properties status...
--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/split_return.1.res.oracle b/tests/value/oracle/split_return.1.res.oracle
index 0dd5a8d1cdf2e75536b0cb84f3d82f3e56f36c68..ff8657d99c46823571074bfd6f7f425bc04b59ed 100644
--- a/tests/value/oracle/split_return.1.res.oracle
+++ b/tests/value/oracle/split_return.1.res.oracle
@@ -8,6 +8,7 @@
\return(f5) == -2 (auto)
\return(f6) == 0 (auto)
\return(f8) == 0 (auto)
+ \return(escaping) == 0 (auto)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -18,8 +19,9 @@
i5 ∈ [--..--]
v ∈ [--..--]
v7 ∈ {0}
+ rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:176.
+ Called from tests/value/split_return.i:204.
[eva] computing for function init <- main1 <- main.
Called from tests/value/split_return.i:17.
[eva] using specification for function init
@@ -27,7 +29,7 @@
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:177.
+ Called from tests/value/split_return.i:205.
[eva] computing for function f2 <- main2 <- main.
Called from tests/value/split_return.i:48.
[eva] Recording results for f2
@@ -40,7 +42,7 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:178.
+ Called from tests/value/split_return.i:206.
[eva] computing for function f3 <- main3 <- main.
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
@@ -52,7 +54,7 @@
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -64,7 +66,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:180.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f5 <- main5 <- main.
Called from tests/value/split_return.i:117.
[eva] Recording results for f5
@@ -76,7 +78,7 @@
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:181.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f6 <- main6 <- main.
Called from tests/value/split_return.i:135.
[eva:alarm] tests/value/split_return.i:130: Warning:
@@ -87,7 +89,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:182.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f7 <- main7 <- main.
Called from tests/value/split_return.i:148.
[eva] Recording results for f7
@@ -97,7 +99,7 @@
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -106,9 +108,25 @@
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
+[eva] computing for function main9 <- main.
+ Called from tests/value/split_return.i:212.
+[eva] computing for function uninit <- main9 <- main.
+ Called from tests/value/split_return.i:199.
+[eva] Recording results for uninit
+[eva] Done for function uninit
+[eva] computing for function escaping <- main9 <- main.
+ Called from tests/value/split_return.i:200.
+[eva:locals-escaping] tests/value/split_return.i:192: Warning:
+ locals {x} escaping the scope of a block of escaping through p
+[eva] Recording results for escaping
+[eva] Done for function escaping
+[eva] Recording results for main9
+[eva] Done for function main9
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function escaping:
+ p ∈ ESCAPINGADDR
[eva:final-states] Values at end of function f2:
i2 ∈ {0; 5}
__retres ∈ {0; 5; 7}
@@ -154,12 +172,19 @@
x ∈ {-1; 4}
pf ∈ {{ &f8 }}
p ∈ {{ NULL ; &x }}
+[eva:final-states] Values at end of function uninit:
+ x ∈ {0} or UNINITIALIZED
+[eva:final-states] Values at end of function main9:
+ y ∈ {0} or UNINITIALIZED
+ q ∈ ESCAPINGADDR
[eva:final-states] Values at end of function main:
i2 ∈ {0; 5}
i3 ∈ {0; 5}
i4 ∈ {0; 5}
i5 ∈ {0; 5}
v7 ∈ {0; 1}
+[from] Computing for function escaping
+[from] Done for function escaping
[from] Computing for function f2
[from] Done for function f2
[from] Computing for function f3
@@ -192,10 +217,16 @@
[from] Done for function main7
[from] Computing for function main8
[from] Done for function main8
+[from] Computing for function uninit
+[from] Done for function uninit
+[from] Computing for function main9
+[from] Done for function main9
[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 escaping:
+ \result FROM \nothing
[from] Function f2:
i2 FROM i2
\result FROM i2
@@ -235,6 +266,10 @@
v7 FROM v
[from] Function main8:
NO EFFECTS
+[from] Function uninit:
+ \result FROM rand
+[from] Function main9:
+ NO EFFECTS
[from] Function main:
i2 FROM i2
i3 FROM i3
@@ -242,6 +277,10 @@
i5 FROM i5
v7 FROM v
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function escaping:
+ p
+[inout] Inputs for function escaping:
+ \nothing
[inout] Out (internal) for function f2:
i2; __retres
[inout] Inputs for function f2:
@@ -302,10 +341,18 @@
x; pf; p; tmp
[inout] Inputs for function main8:
v
+[inout] Out (internal) for function uninit:
+ x
+[inout] Inputs for function uninit:
+ rand
+[inout] Out (internal) for function main9:
+ y; q
+[inout] Inputs for function main9:
+ rand
[inout] Out (internal) for function main:
i2; i3; i4; i5; v7
[inout] Inputs for function main:
- i2; i3; i4; i5; v; v7
+ i2; i3; i4; i5; v; v7; rand
[report] Computing properties status...
--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/split_return.3.res.oracle b/tests/value/oracle/split_return.3.res.oracle
index c33284f92cc95fbd1c46cc04906e08cc03a05bcc..1ad5a6b949801e802041412d0870ce55b97cb0da 100644
--- a/tests/value/oracle/split_return.3.res.oracle
+++ b/tests/value/oracle/split_return.3.res.oracle
@@ -11,8 +11,9 @@
i5 ∈ [--..--]
v ∈ [--..--]
v7 ∈ {0}
+ rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:176.
+ Called from tests/value/split_return.i:204.
[eva] computing for function init <- main1 <- main.
Called from tests/value/split_return.i:17.
[eva] using specification for function init
@@ -20,7 +21,7 @@
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:177.
+ Called from tests/value/split_return.i:205.
[eva] computing for function f2 <- main2 <- main.
Called from tests/value/split_return.i:48.
[eva] Recording results for f2
@@ -35,7 +36,7 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:178.
+ Called from tests/value/split_return.i:206.
[eva] computing for function f3 <- main3 <- main.
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
@@ -47,7 +48,7 @@
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:178.
+ Called from tests/value/split_return.i:206.
[eva] computing for function f3 <- main3 <- main.
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
@@ -57,7 +58,7 @@
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -69,7 +70,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -79,7 +80,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -89,7 +90,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -99,7 +100,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:180.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f5 <- main5 <- main.
Called from tests/value/split_return.i:117.
[eva] Recording results for f5
@@ -111,7 +112,7 @@
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:181.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f6 <- main6 <- main.
Called from tests/value/split_return.i:135.
[eva:alarm] tests/value/split_return.i:130: Warning:
@@ -121,7 +122,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:181.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f6 <- main6 <- main.
Called from tests/value/split_return.i:135.
[eva] Recording results for f6
@@ -129,7 +130,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:182.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f7 <- main7 <- main.
Called from tests/value/split_return.i:148.
[eva] Recording results for f7
@@ -139,7 +140,7 @@
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:182.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f7 <- main7 <- main.
Called from tests/value/split_return.i:148.
[eva] Recording results for f7
@@ -149,7 +150,7 @@
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -159,7 +160,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -169,7 +170,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -179,7 +180,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -188,9 +189,29 @@
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
+[eva] computing for function main9 <- main.
+ Called from tests/value/split_return.i:212.
+[eva] computing for function uninit <- main9 <- main.
+ Called from tests/value/split_return.i:199.
+[eva] Recording results for uninit
+[eva] Done for function uninit
+[eva] computing for function escaping <- main9 <- main.
+ Called from tests/value/split_return.i:200.
+[eva:locals-escaping] tests/value/split_return.i:192: Warning:
+ locals {x} escaping the scope of a block of escaping through p
+[eva] Recording results for escaping
+[eva] Done for function escaping
+[eva] computing for function escaping <- main9 <- main.
+ Called from tests/value/split_return.i:200.
+[eva] Recording results for escaping
+[eva] Done for function escaping
+[eva] Recording results for main9
+[eva] Done for function main9
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function escaping:
+ p ∈ ESCAPINGADDR
[eva:final-states] Values at end of function f2:
i2 ∈ {0; 5}
__retres ∈ {0; 5; 7}
@@ -236,12 +257,19 @@
x ∈ {-1; 4}
pf ∈ {{ &f8 }}
p ∈ {{ NULL ; &x }}
+[eva:final-states] Values at end of function uninit:
+ x ∈ {0} or UNINITIALIZED
+[eva:final-states] Values at end of function main9:
+ y ∈ {0} or UNINITIALIZED
+ q ∈ ESCAPINGADDR
[eva:final-states] Values at end of function main:
i2 ∈ {0; 5}
i3 ∈ {0; 5}
i4 ∈ {0; 5}
i5 ∈ {0; 5}
v7 ∈ {0; 1}
+[from] Computing for function escaping
+[from] Done for function escaping
[from] Computing for function f2
[from] Done for function f2
[from] Computing for function f3
@@ -274,10 +302,16 @@
[from] Done for function main7
[from] Computing for function main8
[from] Done for function main8
+[from] Computing for function uninit
+[from] Done for function uninit
+[from] Computing for function main9
+[from] Done for function main9
[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 escaping:
+ \result FROM \nothing
[from] Function f2:
i2 FROM i2
\result FROM i2
@@ -317,6 +351,10 @@
v7 FROM v
[from] Function main8:
NO EFFECTS
+[from] Function uninit:
+ \result FROM rand
+[from] Function main9:
+ NO EFFECTS
[from] Function main:
i2 FROM i2
i3 FROM i3
@@ -324,6 +362,10 @@
i5 FROM i5
v7 FROM v
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function escaping:
+ p
+[inout] Inputs for function escaping:
+ \nothing
[inout] Out (internal) for function f2:
i2; __retres
[inout] Inputs for function f2:
@@ -384,7 +426,15 @@
x; pf; p; tmp
[inout] Inputs for function main8:
v
+[inout] Out (internal) for function uninit:
+ x
+[inout] Inputs for function uninit:
+ rand
+[inout] Out (internal) for function main9:
+ y; q
+[inout] Inputs for function main9:
+ rand
[inout] Out (internal) for function main:
i2; i3; i4; i5; v7
[inout] Inputs for function main:
- i2; i3; i4; i5; v; v7
+ i2; i3; i4; i5; v; v7; rand
diff --git a/tests/value/oracle/split_return.4.res.oracle b/tests/value/oracle/split_return.4.res.oracle
index 6985eb6c49e28b7cb25f2f343621a1a79b9b2a47..46c3281323efa5dbd6f217ae060050721529854c 100644
--- a/tests/value/oracle/split_return.4.res.oracle
+++ b/tests/value/oracle/split_return.4.res.oracle
@@ -14,8 +14,9 @@
i5 ∈ [--..--]
v ∈ [--..--]
v7 ∈ {0}
+ rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:176.
+ Called from tests/value/split_return.i:204.
[eva] computing for function init <- main1 <- main.
Called from tests/value/split_return.i:17.
[eva] using specification for function init
@@ -23,7 +24,7 @@
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:177.
+ Called from tests/value/split_return.i:205.
[eva] computing for function f2 <- main2 <- main.
Called from tests/value/split_return.i:48.
[eva] Recording results for f2
@@ -38,7 +39,7 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:178.
+ Called from tests/value/split_return.i:206.
[eva] computing for function f3 <- main3 <- main.
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
@@ -50,7 +51,7 @@
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:178.
+ Called from tests/value/split_return.i:206.
[eva] computing for function f3 <- main3 <- main.
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
@@ -60,7 +61,7 @@
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -72,7 +73,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -82,7 +83,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -92,7 +93,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -102,7 +103,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:180.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f5 <- main5 <- main.
Called from tests/value/split_return.i:117.
[eva] Recording results for f5
@@ -114,7 +115,7 @@
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:181.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f6 <- main6 <- main.
Called from tests/value/split_return.i:135.
[eva:alarm] tests/value/split_return.i:130: Warning:
@@ -124,7 +125,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:181.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f6 <- main6 <- main.
Called from tests/value/split_return.i:135.
[eva] Recording results for f6
@@ -132,7 +133,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:182.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f7 <- main7 <- main.
Called from tests/value/split_return.i:148.
[eva] Recording results for f7
@@ -142,7 +143,7 @@
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:182.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f7 <- main7 <- main.
Called from tests/value/split_return.i:148.
[eva] Recording results for f7
@@ -152,7 +153,7 @@
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -162,7 +163,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -172,7 +173,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -182,7 +183,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -191,9 +192,29 @@
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
+[eva] computing for function main9 <- main.
+ Called from tests/value/split_return.i:212.
+[eva] computing for function uninit <- main9 <- main.
+ Called from tests/value/split_return.i:199.
+[eva] Recording results for uninit
+[eva] Done for function uninit
+[eva] computing for function escaping <- main9 <- main.
+ Called from tests/value/split_return.i:200.
+[eva:locals-escaping] tests/value/split_return.i:192: Warning:
+ locals {x} escaping the scope of a block of escaping through p
+[eva] Recording results for escaping
+[eva] Done for function escaping
+[eva] computing for function escaping <- main9 <- main.
+ Called from tests/value/split_return.i:200.
+[eva] Recording results for escaping
+[eva] Done for function escaping
+[eva] Recording results for main9
+[eva] Done for function main9
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function escaping:
+ p ∈ ESCAPINGADDR
[eva:final-states] Values at end of function f2:
i2 ∈ {0; 5}
__retres ∈ {0; 5; 7}
@@ -239,12 +260,19 @@
x ∈ {-1; 4}
pf ∈ {{ &f8 }}
p ∈ {{ NULL ; &x }}
+[eva:final-states] Values at end of function uninit:
+ x ∈ {0} or UNINITIALIZED
+[eva:final-states] Values at end of function main9:
+ y ∈ {0} or UNINITIALIZED
+ q ∈ ESCAPINGADDR
[eva:final-states] Values at end of function main:
i2 ∈ {0; 5}
i3 ∈ {0; 5}
i4 ∈ {0; 5}
i5 ∈ {0; 5}
v7 ∈ {0; 1}
+[from] Computing for function escaping
+[from] Done for function escaping
[from] Computing for function f2
[from] Done for function f2
[from] Computing for function f3
@@ -277,10 +305,16 @@
[from] Done for function main7
[from] Computing for function main8
[from] Done for function main8
+[from] Computing for function uninit
+[from] Done for function uninit
+[from] Computing for function main9
+[from] Done for function main9
[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 escaping:
+ \result FROM \nothing
[from] Function f2:
i2 FROM i2
\result FROM i2
@@ -320,6 +354,10 @@
v7 FROM v
[from] Function main8:
NO EFFECTS
+[from] Function uninit:
+ \result FROM rand
+[from] Function main9:
+ NO EFFECTS
[from] Function main:
i2 FROM i2
i3 FROM i3
@@ -327,6 +365,10 @@
i5 FROM i5
v7 FROM v
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function escaping:
+ p
+[inout] Inputs for function escaping:
+ \nothing
[inout] Out (internal) for function f2:
i2; __retres
[inout] Inputs for function f2:
@@ -387,10 +429,18 @@
x; pf; p; tmp
[inout] Inputs for function main8:
v
+[inout] Out (internal) for function uninit:
+ x
+[inout] Inputs for function uninit:
+ rand
+[inout] Out (internal) for function main9:
+ y; q
+[inout] Inputs for function main9:
+ rand
[inout] Out (internal) for function main:
i2; i3; i4; i5; v7
[inout] Inputs for function main:
- i2; i3; i4; i5; v; v7
+ i2; i3; i4; i5; v; v7; rand
[eva] Warning: option -eva-split-return-function: 'f2' previously bound to 'full split';
now bound to 'auto split'.
[eva] Splitting return states on:
@@ -408,15 +458,16 @@
i5 ∈ [--..--]
v ∈ [--..--]
v7 ∈ {0}
+ rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:176.
+ Called from tests/value/split_return.i:204.
[eva] computing for function init <- main1 <- main.
Called from tests/value/split_return.i:17.
[eva] Done for function init
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:177.
+ Called from tests/value/split_return.i:205.
[eva] computing for function f2 <- main2 <- main.
Called from tests/value/split_return.i:48.
[eva] Recording results for f2
@@ -427,7 +478,7 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:178.
+ Called from tests/value/split_return.i:206.
[eva] computing for function f3 <- main3 <- main.
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
@@ -437,7 +488,7 @@
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:178.
+ Called from tests/value/split_return.i:206.
[eva] computing for function f3 <- main3 <- main.
Called from tests/value/split_return.i:73.
[eva] Recording results for f3
@@ -447,7 +498,7 @@
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -457,7 +508,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -467,7 +518,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -477,7 +528,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:179.
+ Called from tests/value/split_return.i:207.
[eva] computing for function f4 <- main4 <- main.
Called from tests/value/split_return.i:94.
[eva] Recording results for f4
@@ -487,7 +538,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:180.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f5 <- main5 <- main.
Called from tests/value/split_return.i:117.
[eva] Recording results for f5
@@ -497,7 +548,7 @@
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:181.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f6 <- main6 <- main.
Called from tests/value/split_return.i:135.
[eva] Recording results for f6
@@ -505,7 +556,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:181.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f6 <- main6 <- main.
Called from tests/value/split_return.i:135.
[eva] Recording results for f6
@@ -513,7 +564,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:182.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f7 <- main7 <- main.
Called from tests/value/split_return.i:148.
[eva] Recording results for f7
@@ -523,7 +574,7 @@
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:182.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f7 <- main7 <- main.
Called from tests/value/split_return.i:148.
[eva] Recording results for f7
@@ -533,7 +584,7 @@
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -543,7 +594,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -553,7 +604,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -563,7 +614,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:183.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f8 <- main8 <- main.
Called from tests/value/split_return.i:171.
[eva] Recording results for f8
@@ -572,9 +623,27 @@
[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
+[eva] computing for function main9 <- main.
+ Called from tests/value/split_return.i:212.
+[eva] computing for function uninit <- main9 <- main.
+ Called from tests/value/split_return.i:199.
+[eva] Recording results for uninit
+[eva] Done for function uninit
+[eva] computing for function escaping <- main9 <- main.
+ Called from tests/value/split_return.i:200.
+[eva] Recording results for escaping
+[eva] Done for function escaping
+[eva] computing for function escaping <- main9 <- main.
+ Called from tests/value/split_return.i:200.
+[eva] Recording results for escaping
+[eva] Done for function escaping
+[eva] Recording results for main9
+[eva] Done for function main9
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function escaping:
+ p ∈ ESCAPINGADDR
[eva:final-states] Values at end of function f2:
i2 ∈ {0; 5}
__retres ∈ {0; 5; 7}
@@ -620,12 +689,19 @@
x ∈ {-1; 4}
pf ∈ {{ &f8 }}
p ∈ {{ NULL ; &x }}
+[eva:final-states] Values at end of function uninit:
+ x ∈ {0} or UNINITIALIZED
+[eva:final-states] Values at end of function main9:
+ y ∈ {0} or UNINITIALIZED
+ q ∈ ESCAPINGADDR
[eva:final-states] Values at end of function main:
i2 ∈ {0; 5}
i3 ∈ {0; 5}
i4 ∈ {0; 5}
i5 ∈ {0; 5}
v7 ∈ {0; 1}
+[from] Computing for function escaping
+[from] Done for function escaping
[from] Computing for function f2
[from] Done for function f2
[from] Computing for function f3
@@ -658,10 +734,16 @@
[from] Done for function main7
[from] Computing for function main8
[from] Done for function main8
+[from] Computing for function uninit
+[from] Done for function uninit
+[from] Computing for function main9
+[from] Done for function main9
[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 escaping:
+ \result FROM \nothing
[from] Function f2:
i2 FROM i2
\result FROM i2
@@ -701,6 +783,10 @@
v7 FROM v
[from] Function main8:
NO EFFECTS
+[from] Function uninit:
+ \result FROM rand
+[from] Function main9:
+ NO EFFECTS
[from] Function main:
i2 FROM i2
i3 FROM i3
@@ -708,6 +794,10 @@
i5 FROM i5
v7 FROM v
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function escaping:
+ p
+[inout] Inputs for function escaping:
+ \nothing
[inout] Out (internal) for function f2:
i2; __retres
[inout] Inputs for function f2:
@@ -768,7 +858,15 @@
x; pf; p; tmp
[inout] Inputs for function main8:
v
+[inout] Out (internal) for function uninit:
+ x
+[inout] Inputs for function uninit:
+ rand
+[inout] Out (internal) for function main9:
+ y; q
+[inout] Inputs for function main9:
+ rand
[inout] Out (internal) for function main:
i2; i3; i4; i5; v7
[inout] Inputs for function main:
- i2; i3; i4; i5; v; v7
+ i2; i3; i4; i5; v; v7; rand
diff --git a/tests/value/split_return.i b/tests/value/split_return.i
index 35b3df0bc703b749b97514f35dcde38db13bedbf..4437a236ec1defd15006b4432304a51b7fc8d42c 100644
--- a/tests/value/split_return.i
+++ b/tests/value/split_return.i
@@ -1,10 +1,10 @@
/* run.config*
- STDOPT: +"-deterministic -eva-no-memexec -slevel-function init:3,main1:3,f2:4,main2:4,f4:3,main5:3 -val-split-return-function f2:0,f3:-2:-4,f4:4,f5:-2,NON_EXISTING:4 -permissive -then -load-module report -report"
- STDOPT: +"-deterministic -eva-no-memexec -val -journal-disable -out -input -deps -slevel 6 -val-split-return auto -val-split-return-function f7:0:3 -then -load-module report -report"
+ STDOPT: +"-deterministic -eva-no-memexec -slevel-function init:3,main1:3,f2:4,main2:4,f4:3,main5:3,uninit:2,main9:2 -val-split-return-function f2:0,f3:-2:-4,f4:4,f5:-2,NON_EXISTING:4,uninit:0,escaping:0 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -permissive -then -load-module report -report"
+ STDOPT: +"-deterministic -eva-no-memexec -val -journal-disable -out -input -deps -slevel 6 -val-split-return auto -val-split-return-function f7:0:3 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -load-module report -report"
COMMENT: below command must fail, as -permissive is not set
- STDOPT: +"-deterministic -eva-no-memexec -val -slevel-function NON_EXISTING:4"
- STDOPT: +"-deterministic -eva-no-memexec -val -journal-disable -out -input -deps -slevel 6 -val-split-return full"
- STDOPT: +"-deterministic -eva-no-memexec -val -journal-disable -out -input -deps -slevel 6 -val-split-return full -val-split-return-function f7:0:3 -val-split-return-function f2:full -then -val-split-return-function f2:auto"
+ STDOPT: +"-deterministic -eva-no-memexec -val -slevel-function NON_EXISTING:4 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
+ STDOPT: +"-deterministic -eva-no-memexec -val -journal-disable -out -input -deps -slevel 6 -val-split-return full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
+ STDOPT: +"-deterministic -eva-no-memexec -val -journal-disable -out -input -deps -slevel 6 -val-split-return full -val-split-return-function f7:0:3 -val-split-return-function f2:full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -val-split-return-function f2:auto"
*/
/*@ assigns \result \from \nothing;
@@ -172,6 +172,34 @@ void main8() {
Frama_C_show_each_then8(x, p);
}
+/* [main9] checks that -split-return does not remove states in which the result
+ is an escaping pointer or an uninitialized variable (and thus evaluates to
+ bottom) when -eva-warn-copy-indeterminate is disabled. */
+
+volatile int rand;
+
+int uninit () {
+ int x;
+ if (rand)
+ x = 0;
+ return x;
+}
+
+int *escaping () {
+ int *p;
+ {
+ int x;
+ p = &x;
+ }
+ return p;
+}
+
+/* At the end, [y] may be uninitialized and [q] is a dangling pointer. */
+void main9 () {
+ int y = uninit();
+ int *q = escaping();
+}
+
void main() {
main1();
main2();
@@ -181,4 +209,5 @@ void main() {
main6();
main7();
main8();
+ main9();
}