From 21fce2eda21e3c3bea7a19630948ccd6ec64145f Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Fri, 29 Jun 2012 10:17:29 +0200 Subject: [PATCH] model-checker : move functions about snapshot comparison from mc_liveness to mc_checkpoint and declare them static --- src/mc/mc_checkpoint.c | 104 +++++++++++++++++++++++++++++++++++++++++ src/mc/mc_liveness.c | 102 ---------------------------------------- src/mc/mc_private.h | 3 +- 3 files changed, 105 insertions(+), 104 deletions(-) diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 31927b84b5..0839f6787c 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -182,4 +182,108 @@ void MC_free_snapshot(mc_snapshot_t snapshot) xbt_free(snapshot); } +static int data_program_region_compare(void *d1, void *d2, size_t size); +static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size); + +static int data_program_region_compare(void *d1, void *d2, size_t size){ + int distance = 0; + int i; + + for(i=0; inum_reg != s2->num_reg){ + XBT_INFO("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg); + return 1; + } + + int i; + int errors = 0; + + for(i=0 ; i< s1->num_reg ; i++){ + + if(s1->regions[i]->type != s2->regions[i]->type){ + XBT_INFO("Different type of region"); + errors++; + } + + switch(s1->regions[i]->type){ + case 0: + if(s1->regions[i]->size != s2->regions[i]->size){ + XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; + } + if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ + XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; + } + if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){ + XBT_INFO("Different heap (mmalloc_compare)"); + errors++; + } + break; + case 1 : + if(s1->regions[i]->size != s2->regions[i]->size){ + XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; + } + if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ + XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; + } + if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ + XBT_INFO("Different memcmp for data in libsimgrid"); + errors++; + } + break; + case 2 : + if(s1->regions[i]->size != s2->regions[i]->size){ + XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; + } + if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ + XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; + } + if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ + XBT_INFO("Different memcmp for data in program"); + errors++; + } + break; + default: + break; + } + } + + return (errors > 0); + +} diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 1b05a14c13..b0877f6707 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -33,108 +33,6 @@ unsigned int hash_region(char *str, int str_len){ } -int data_program_region_compare(void *d1, void *d2, size_t size){ - int distance = 0; - int i; - - for(i=0; inum_reg != s2->num_reg){ - XBT_INFO("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg); - return 1; - } - - int i; - int errors = 0; - - for(i=0 ; i< s1->num_reg ; i++){ - - if(s1->regions[i]->type != s2->regions[i]->type){ - XBT_INFO("Different type of region"); - errors++; - } - - switch(s1->regions[i]->type){ - case 0: - if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - } - if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - } - if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){ - XBT_INFO("Different heap (mmalloc_compare)"); - errors++; - } - break; - case 1 : - if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - } - if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - } - if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - XBT_INFO("Different memcmp for data in libsimgrid"); - errors++; - } - break; - case 2 : - if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - } - if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - } - if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - XBT_INFO("Different memcmp for data in program"); - errors++; - } - break; - default: - break; - } - } - - return (errors > 0); - -} - int reached(xbt_state_t st){ raw_mem_set = (mmalloc_get_current_heap() == raw_heap); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 01ad368609..d9b9f7f5d8 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -41,6 +41,7 @@ void MC_take_snapshot_liveness(mc_snapshot_t s); void MC_restore_snapshot(mc_snapshot_t); void MC_free_snapshot(mc_snapshot_t); + /********************************* MC Global **********************************/ extern double *mc_time; @@ -246,8 +247,6 @@ void set_pair_reached(xbt_state_t st); int reached_hash(xbt_state_t st); void set_pair_reached_hash(xbt_state_t st); int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2); -int data_program_region_compare(void *d1, void *d2, size_t size); -int data_libsimgrid_region_compare(void *d1, void *d2, size_t size); void MC_pair_delete(mc_pair_t pair); void MC_exit_liveness(void); mc_state_t MC_state_pair_new(void); -- 2.20.1