Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : fix std_heap address for heap comparison algorithm
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Wed, 13 Jun 2012 15:21:29 +0000 (17:21 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Thu, 14 Jun 2012 07:32:47 +0000 (09:32 +0200)
src/include/mc/mc.h
src/mc/mc_private.h
src/xbt/mmalloc/mm_diff.c

index 3073498..4b34fd6 100644 (file)
@@ -15,6 +15,7 @@
 #include "simgrid/modelchecker.h" /* our public interface (and definition of HAVE_MC) */
 #include "xbt/automaton.h"
 
+#define STD_HEAP_SIZE   20480000        /* Maximum size of the system's heap */
 
 SG_BEGIN_DECL()
 
index a64ca64..b088e88 100644 (file)
@@ -137,7 +137,7 @@ void MC_print_statistics_pairs(mc_stats_pair_t);
 
 extern void *std_heap;
 extern void *raw_heap;
-#define STD_HEAP_SIZE   20480000        /* Maximum size of the system's heap */
+
 
 /* FIXME: Horrible hack! because the mmalloc library doesn't provide yet of */
 /* an API to query about the status of a heap, we simply call mmstats and */
index 6e54a5d..4c37c9e 100644 (file)
@@ -7,6 +7,7 @@
 
 #include "xbt/ex_interface.h" /* internals of backtrace setup */
 #include "xbt/str.h"
+#include "mc/mc.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt,
                                 "Logging specific to mm_diff in mmalloc");
@@ -197,7 +198,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
   //void* heapbase1 = (char *)mdp1 + ((char *)mdp1->heapbase - (char *)s_heap);
   //void* heapbase2 = (char *)mdp2 + ((char *)mdp2->heapbase - (char *)s_heap);
 
-  xbt_mheap_t s_heap = mmalloc_get_current_heap();
+  void* s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - getpagesize();
     
   void *heapbase1 = (char *)mdp1 + BLOCKSIZE;
   void *heapbase2 = (char *)mdp2 + BLOCKSIZE;