typedef struct s_stack_region{
void *address;
- char *process_name;
void *context;
size_t size;
int block;
static void stack_region_free(stack_region_t s)
{
if (s) {
- xbt_free(s->process_name);
xbt_free(s);
}
}
}
+void MC_stack_area_add(stack_region_t stack_area)
+{
+ if (stacks_areas == NULL)
+ stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
+ xbt_dynar_push(stacks_areas, &stack_area);
+}
+
/** @brief Register a stack in the model checker
*
* The stacks are allocated in the heap. The MC handle them especially
{
int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
MC_SET_MC_HEAP;
- if (stacks_areas == NULL)
- stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
-
- stack_region_t region = NULL;
- region = xbt_new0(s_stack_region_t, 1);
+ stack_region_t region = xbt_new0(s_stack_region_t, 1);
region->address = stack;
- region->process_name = process && process->name ? strdup(process->name) : NULL;
region->context = context;
region->size = size;
region->block =
#endif
region->process_index = -1;
- xbt_dynar_push(stacks_areas, ®ion);
+ if (mc_mode == MC_MODE_CLIENT) {
+ s_mc_stack_region_message_t message;
+ message.type = MC_MESSAGE_STACK_REGION;
+ message.stack_region = *region;
+ MC_client_send_message(&message, sizeof(message));
+ }
+
+ MC_stack_area_add(region);
if (!raw_mem_set)
MC_SET_STD_HEAP;
void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
void MC_heap_region_ignore_send(mc_heap_ignore_region_t region);
void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size);
+void MC_stack_area_add(stack_region_t stack_area);
xbt_dynar_t MC_checkpoint_ignore_new(void);
+
SG_END_DECL();
MC_MESSAGE_IGNORE_HEAP,
MC_MESSAGE_UNIGNORE_HEAP,
MC_MESSAGE_IGNORE_MEMORY,
+ MC_MESSAGE_STACK_REGION,
} e_mc_message_type;
#define MC_MESSAGE_LENGTH 512
size_t size;
} s_mc_ignore_memory_message_t, *mc_ignore_memory_message_t;
+typedef struct s_mc_stack_region_message {
+ e_mc_message_type type;
+ s_stack_region_t stack_region;
+} s_mc_stack_region_message_t, *mc_stack_region_message_t;
+
int MC_protocol_send(int socket, void* message, size_t size);
int MC_protocol_send_simple_message(int socket, int type);
int MC_protocol_hello(int socket);
}
break;
+ case MC_MESSAGE_STACK_REGION:
+ {
+ XBT_DEBUG("Received stack area");
+ s_mc_stack_region_message_t message;
+ if (size != sizeof(message))
+ xbt_die("Broken messsage");
+ memcpy(&message, buffer, sizeof(message));
+ stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
+ *stack_region = message.stack_region;
+ MC_stack_area_add(stack_region);
+ }
+ break;
+
default:
xbt_die("Unexpected message from model-checked application");