A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model-checker : remove variable from mc_local_variables if ignored
[simgrid.git]
/
src
/
mc
/
mc_global.c
diff --git
a/src/mc/mc_global.c
b/src/mc/mc_global.c
index
f9f2ad1
..
c3c6539
100644
(file)
--- a/
src/mc/mc_global.c
+++ b/
src/mc/mc_global.c
@@
-303,11
+303,16
@@
void MC_exit(void)
xbt_abort();
}
xbt_abort();
}
+int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
+
+ return simcall->mc_value;
+}
+
int MC_random(int min, int max)
{
/*FIXME: return mc_current_state->executed_transition->random.value;*/
int MC_random(int min, int max)
{
/*FIXME: return mc_current_state->executed_transition->random.value;*/
- return
0
;
+ return
simcall_mc_random(min, max)
;
}
/**
}
/**
@@
-744,8
+749,7
@@
void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
/************ MC_ignore ***********/
void heap_ignore_region_free(mc_heap_ignore_region_t r){
/************ MC_ignore ***********/
void heap_ignore_region_free(mc_heap_ignore_region_t r){
- if(r)
- xbt_free(r);
+ xbt_free(r);
}
void heap_ignore_region_free_voidp(void *r){
}
void heap_ignore_region_free_voidp(void *r){
@@
-961,7
+965,7
@@
static size_t data_bss_ignore_size(void *address){
-void MC_ignore_stack(const char *var_name, const char *frame){
+void MC_ignore_stack(const char *var_name, const char *frame
_name
){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@
-975,7
+979,7
@@
void MC_ignore_stack(const char *var_name, const char *frame){
mc_stack_ignore_variable_t var = NULL;
var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
var->var_name = strdup(var_name);
mc_stack_ignore_variable_t var = NULL;
var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
var->var_name = strdup(var_name);
- var->frame = strdup(frame);
+ var->frame = strdup(frame
_name
);
xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
@@
-989,7
+993,7
@@
void MC_ignore_stack(const char *var_name, const char *frame){
while(start <= end){
cursor = (start + end) / 2;
current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
while(start <= end){
cursor = (start + end) / 2;
current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
- if(strcmp(current_var->frame, frame) == 0){
+ if(strcmp(current_var->frame, frame
_name
) == 0){
if(strcmp(current_var->var_name, var_name) == 0){
MC_UNSET_RAW_MEM;
if(raw_mem_set)
if(strcmp(current_var->var_name, var_name) == 0){
MC_UNSET_RAW_MEM;
if(raw_mem_set)
@@
-1001,24
+1005,34
@@
void MC_ignore_stack(const char *var_name, const char *frame){
if(strcmp(current_var->var_name, var_name) > 0)
end = cursor - 1;
}
if(strcmp(current_var->var_name, var_name) > 0)
end = cursor - 1;
}
- if(strcmp(current_var->frame, frame) < 0)
+ if(strcmp(current_var->frame, frame
_name
) < 0)
start = cursor + 1;
start = cursor + 1;
- if(strcmp(current_var->frame, frame) > 0)
+ if(strcmp(current_var->frame, frame
_name
) > 0)
end = cursor - 1;
}
mc_stack_ignore_variable_t var = NULL;
var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
var->var_name = strdup(var_name);
end = cursor - 1;
}
mc_stack_ignore_variable_t var = NULL;
var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
var->var_name = strdup(var_name);
- var->frame = strdup(frame);
+ var->frame = strdup(frame
_name
);
- if(strcmp(current_var->frame, frame) < 0)
+ if(strcmp(current_var->frame, frame
_name
) < 0)
xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
else
xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
}
xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
else
xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
}
+ /* Remove variable from mc_local_variables */
+
+ if(mc_local_variables != NULL){
+
+ dw_frame_t frame = xbt_dict_get_or_null(mc_local_variables, frame_name);
+ if(frame != NULL)
+ xbt_dict_remove(frame->variables, var_name);
+
+ }
+
MC_UNSET_RAW_MEM;
if(raw_mem_set)
MC_UNSET_RAW_MEM;
if(raw_mem_set)
@@
-1342,10
+1356,8
@@
void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
}
xbt_free(subprogram_start);
}
xbt_free(subprogram_start);
- if(subprogram_end != NULL){
- xbt_free(subprogram_end);
- subprogram_end = NULL;
- }
+ xbt_free(subprogram_end);
+ subprogram_end = NULL;
}else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
}else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */