[mc] Do not take NULL to mean 'the current address space' in dwarf expressions

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 897ff8f..6c787e1 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -404,12 +404,12 @@ static void mc_fill_local_variables_values(mc_stack_frame_t stack_frame,
       new_var->address = current_variable->address;
     } else if (current_variable->locations.size != 0) {
       s_mc_location_t location;
-      // FIXME, cross-process support
-      mc_dwarf_resolve_locations(&location, &current_variable->locations,
-                                              current_variable->object_info,
-                                              &(stack_frame->unw_cursor),
-                                              (void *) stack_frame->frame_base,
-                                              NULL, process_index);
+      mc_dwarf_resolve_locations(
+        &location, &current_variable->locations,
+        current_variable->object_info,
+        &(stack_frame->unw_cursor),
+        (void *) stack_frame->frame_base,
+        (mc_address_space_t) &mc_model_checker->process, process_index);
 
       switch(mc_get_location_type(&location)) {
       case MC_LOCATION_TYPE_ADDRESS:

diff --git a/src/mc/mc_dwarf_expression.c b/src/mc/mc_dwarf_expression.c
index 92e4e47..adcf360 100644 (file)
--- a/src/mc/mc_dwarf_expression.c
+++ b/src/mc/mc_dwarf_expression.c
@@ -399,19 +399,12 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
       {
         // Computed address:
         uintptr_t address = (uintptr_t) state->stack[state->stack_size - 1];
-        uintptr_t value;
-        if (state->address_space) {
-          uintptr_t temp;
-          const uintptr_t* res = (uintptr_t*) MC_address_space_read(
-            state->address_space, MC_ADDRESS_SPACE_READ_FLAGS_LAZY,
-            &temp, (const void*) address, sizeof(uintptr_t), state->process_index);
-          value = *res;
-        }
-        else {
-          // TODO, use a mc_process representing the current process instead of this
-          value = *(const uintptr_t*) address;
-        }
-        state->stack[state->stack_size - 1] = value;
+        if (!state->address_space)
+          xbt_die("Missing address space");
+        MC_address_space_read(
+          state->address_space, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
+          &state->stack[state->stack_size - 1], (const void*) address,
+          sizeof(uintptr_t), state->process_index);
       }
       break;
 

diff --git a/teshsuite/mc/dwarf_expression/dwarf_expression.c b/teshsuite/mc/dwarf_expression/dwarf_expression.c
index 998b779..a4dbb9a 100644 (file)
--- a/teshsuite/mc/dwarf_expression/dwarf_expression.c
+++ b/teshsuite/mc/dwarf_expression/dwarf_expression.c
@@ -15,6 +15,8 @@
 #include "../src/mc/mc_private.h"
 #include "../src/mc/mc_object_info.h"
 
+static s_mc_process_t process;
+
 static
 uintptr_t eval_binary_operation(mc_expression_state_t state, int op, uintptr_t a, uintptr_t b) {
   state->stack_size = 0;
@@ -113,8 +115,11 @@ void test_deref(mc_expression_state_t state) {
 }
 
 int main(int argc, char** argv) {
+  MC_process_init(&process, getpid(), -1);
+
   s_mc_expression_state_t state;
   memset(&state, 0, sizeof(s_mc_expression_state_t));
+  state.address_space = (mc_address_space_t) &process;
 
   basic_test(&state);