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, ¤t_variable->locations,
- current_variable->object_info,
- &(stack_frame->unw_cursor),
- (void *) stack_frame->frame_base,
- NULL, process_index);
+ mc_dwarf_resolve_locations(
+ &location, ¤t_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:
{
// 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;
#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;
}
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);