Merge branch 'mc++'

Conflicts:
	src/simgrid/sg_config.c
	src/xbt/mmalloc/mm_diff.c

diff --cc CMakeLists.txt
Simple merge

diff --cc buildtools/Cmake/AddTests.cmake
Simple merge

diff --cc buildtools/Cmake/CompleteInFiles.cmake
Simple merge

diff --cc buildtools/Cmake/DefinePackages.cmake
Simple merge

diff --cc buildtools/Cmake/MakeExe.cmake
Simple merge

diff --cc buildtools/Cmake/MakeLib.cmake
Simple merge

diff --cc src/include/mc/mc.h
Simple merge

diff --cc src/mc/mc_memory.c
Simple merge

diff --cc src/simgrid/sg_config.c
index fd2dfd2,4ebfb8e..9a97006
--- 1/src/simgrid/sg_config.c
--- 2/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@@ -595,9 -587,21 +595,21 @@@ void sg_config_init(int *argc, char **a
      /* do liveness model-checking */
      xbt_cfg_register(&_sg_cfg_set, "model-check/property",
                       "Specify the name of the file containing the property. It must be the result of the ltl2ba program.",
 -                     xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL);
 +                     xbt_cfgelm_string, 1, 1, _mc_cfg_cb_property, NULL);
      xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", "");
  
 -                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL);
+     /* do communications determinism model-checking */
+     xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism",
+                      "Enable/disable the detection of determinism in the communications schemes",
 -                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_send_determinism, NULL);
++                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_comms_determinism, NULL);
+     xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no");
+ 
+     /* do send determinism model-checking */
+     xbt_cfg_register(&_sg_cfg_set, "model-check/send_determinism",
+                      "Enable/disable the detection of send-determinism in the communications schemes",
++                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_send_determinism, NULL);
+     xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/send_determinism", "no");
+ 
      /* Specify the kind of model-checking reduction */
      xbt_cfg_register(&_sg_cfg_set, "model-check/reduction",
                       "Specify the kind of exploration reduction (either none or DPOR)",
@@@ -607,9 -611,15 +619,15 @@@
      /* Enable/disable timeout for wait requests with model-checking */
      xbt_cfg_register(&_sg_cfg_set, "model-check/timeout",
                       "Enable/Disable timeout for wait requests",
 -                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_timeout, NULL);
 +                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_timeout, NULL);
      xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/timeout", "no");
  
 -                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_hash, NULL);
+     /* Enable/disable global hash computation with model-checking */
+     xbt_cfg_register(&_sg_cfg_set, "model-check/hash",
+                      "Enable/Disable state hash for state comparison",
++                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_hash, NULL);
+     xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no");
+ 
      /* Set max depth exploration */
      xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth",
                       "Specify the max depth of exploration (default : 1000)",

diff --cc src/simix/smx_network.c
Simple merge

diff --cc src/smpi/smpi_base.c
Simple merge

diff --cc src/smpi/smpi_global.c
Simple merge

diff --cc src/xbt/mmalloc/mm_diff.c
index 39cd21c,a17a4a3..7258e6f
--- 1/src/xbt/mmalloc/mm_diff.c
--- 2/src/xbt/mmalloc/mm_diff.c
+++ b/src/xbt/mmalloc/mm_diff.c
@@@ -314,30 -345,30 +345,30 @@@ int init_heap_information(xbt_mheap_t h
  
    int i, j;
  
-   heaplimit = ((struct mdesc *)heap1)->heaplimit;
+   state->heaplimit = ((struct mdesc *)heap1)->heaplimit;
  
-   s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
 -  state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - getpagesize();
++  state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
  
-   heapbase1 = (char *)heap1 + BLOCKSIZE;
-   heapbase2 = (char *)heap2 + BLOCKSIZE;
+   state->heapbase1 = (char *)heap1 + BLOCKSIZE;
+   state->heapbase2 = (char *)heap2 + BLOCKSIZE;
  
-   heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)((struct mdesc *)heap1)->heapinfo - (char *)s_heap)));
-   heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)((struct mdesc *)heap2)->heapinfo - (char *)s_heap)));
+   state->heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)((struct mdesc *)heap1)->heapinfo - (char *)state->s_heap)));
+   state->heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)((struct mdesc *)heap2)->heapinfo - (char *)state->s_heap)));
  
-   heapsize1 = heap1->heapsize;
-   heapsize2 = heap2->heapsize;
+   state->heapsize1 = heap1->heapsize;
+   state->heapsize2 = heap2->heapsize;
  
-   to_ignore1 = i1;
-   to_ignore2 = i2;
+   state->to_ignore1 = i1;
+   state-> to_ignore2 = i2;
  
-   equals_to1 = malloc(heaplimit * sizeof(heap_area_t *));
-   types1 = malloc(heaplimit * sizeof(type_name *));
-   for(i=0; i<=heaplimit; i++){
-     equals_to1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(heap_area_t));
-     types1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(type_name));
+   state->equals_to1 = malloc(state->heaplimit * sizeof(heap_area_t *));
+   state->types1 = malloc(state->heaplimit * sizeof(type_name *));
+   for(i=0; i<=state->heaplimit; i++){
+     state->equals_to1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(heap_area_t));
+     state->types1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(type_name));
      for(j=0; j<MAX_FRAGMENT_PER_BLOCK; j++){
-       equals_to1[i][j] = NULL;
-       types1[i][j] = NULL;
+       state->equals_to1[i][j] = NULL;
+       state->types1[i][j] = NULL;
      }      
    }
  
@@@ -1370,18 -1433,18 +1433,18 @@@ int mmalloc_linear_compare_heap(xbt_mhe
    }
  
    /* Heap information */
-   heaplimit = ((struct mdesc *)heap1)->heaplimit;
+   state->heaplimit = ((struct mdesc *)heap1)->heaplimit;
  
-   s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
 -  state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - getpagesize();
++  state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
  
-   heapbase1 = (char *)heap1 + BLOCKSIZE;
-   heapbase2 = (char *)heap2 + BLOCKSIZE;
+   state->heapbase1 = (char *)heap1 + BLOCKSIZE;
+   state->heapbase2 = (char *)heap2 + BLOCKSIZE;
  
-   heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)heap1->heapinfo - (char *)s_heap)));
-   heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)heap2->heapinfo - (char *)s_heap)));
+   state->heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)heap1->heapinfo - (char *)state->s_heap)));
+   state->heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)heap2->heapinfo - (char *)state->s_heap)));
  
-   heapsize1 = heap1->heapsize;
-   heapsize2 = heap2->heapsize;
+   state->heapsize1 = heap1->heapsize;
+   state->heapsize2 = heap2->heapsize;
  
    /* Start comparison */
    size_t i, j, k;