Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : ignore variable about time used with tracing
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 25 Mar 2013 21:37:39 +0000 (22:37 +0100)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 25 Mar 2013 22:11:00 +0000 (23:11 +0100)
src/mc/mc_global.c

index 38118a9..025dfe0 100644 (file)
@@ -216,6 +216,9 @@ void MC_init(){
   MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
   MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
 
   MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
   MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
 
+  /* Ignore local variable about time used for tracing */
+  MC_ignore_stack("start_time", "*"); 
+
   MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
   MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time)); 
   MC_ignore_data_bss(&mc_time, sizeof(mc_time));
   MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
   MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time)); 
   MC_ignore_data_bss(&mc_time, sizeof(mc_time));