From 046f27f07bc99a6dc3541086a063eb1c2e60130b Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 10 Apr 2020 13:34:07 +0200
Subject: [PATCH] [Eva] Make memexec also consider logic inputs as input bases.
---
src/plugins/value/engine/mem_exec.ml | 8 ++++++--
tests/value/oracle/memexec.res.oracle | 7 +++----
2 files changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/plugins/value/engine/mem_exec.ml b/src/plugins/value/engine/mem_exec.ml
index b70a4bc3d01..423bf04634f 100644
--- a/src/plugins/value/engine/mem_exec.ml
+++ b/src/plugins/value/engine/mem_exec.ml
@@ -156,8 +156,12 @@ module Make
| None -> ()
| Some inout ->
try
- let output_bases = bases inout.Inout_type.over_outputs_if_termination
- and input_bases = bases inout.Inout_type.over_inputs in
+ let output_bases = bases inout.Inout_type.over_outputs_if_termination in
+ let input_bases =
+ let input_bases = bases inout.Inout_type.over_inputs in
+ let logic_input_bases = bases inout.Inout_type.over_logic_inputs in
+ Base.Hptset.union input_bases logic_input_bases
+ in
(* There are two strategies to compute the 'inputs' for a memexec
function: either we take all inputs_bases+outputs_bases
(outputs_bases are important because of weak updates), or we
diff --git a/tests/value/oracle/memexec.res.oracle b/tests/value/oracle/memexec.res.oracle
index a27eebd316e..f24a2a45c79 100644
--- a/tests/value/oracle/memexec.res.oracle
+++ b/tests/value/oracle/memexec.res.oracle
@@ -103,8 +103,7 @@
Frama_C_show_each_f5: [9..2147483647], [-2147483648..6], [-2147483648..7]
[eva] tests/value/memexec.c:113: Reusing old results for call to f5_aux
[eva] tests/value/memexec.c:114:
- Frama_C_show_each_f5:
- [9..2147483647], [-2147483648..2147483647], [-2147483648..7]
+ Frama_C_show_each_f5: [9..2147483647], [-2147483648..6], [-2147483648..7]
[eva] Recording results for f5
[eva] Done for function f5
[eva] computing for function f6 <- main.
@@ -192,7 +191,7 @@
[eva:final-states] Values at end of function f5_aux:
v ∈ [--..--]
[eva:final-states] Values at end of function f5:
- g_f5_1 ∈ [--..--]
+ g_f5_1 ∈ [-2147483648..6]
g_f5_2 ∈ [-2147483648..7]
arg ∈ [9..2147483647]
[eva:final-states] Values at end of function f6_1:
@@ -228,7 +227,7 @@
S[0..7] ∈ {0}
[8].i ∈ {0; 6}
[9] ∈ {0}
- g_f5_1 ∈ [--..--]
+ g_f5_1 ∈ [-2147483648..6]
g_f5_2 ∈ [-2147483648..7]
two_fields.x ∈ {1}
.y ∈ {3}
--
GitLab