diff --git a/src/plugins/value/engine/mem_exec.ml b/src/plugins/value/engine/mem_exec.ml index b70a4bc3d015ad01a4e5352643c3195b5d489c56..423bf04634fc106dc9b6031581b6467363fdd28c 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 a27eebd316e8fecb8f2d31c42a25e208d17a468c..f24a2a45c795452a83ea810cc13ddf7495b4cd60 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}