[Eva] Make memexec also consider logic inputs as input bases.

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

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}