model-checker : change printf for size_t variables

diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt
index 3a9eb3e..f330a04 100644 (file)
--- a/examples/msg/mc/CMakeLists.txt
+++ b/examples/msg/mc/CMakeLists.txt
@@ -14,6 +14,10 @@ automatonparse_promela.c example_liveness_without_cycle.c)
 add_executable(example2_liveness_without_cycle automaton.c
 automatonparse_promela.c
 example2_liveness_without_cycle.c)
+add_executable(example_liveness_with_cycle automaton.c
+automatonparse_promela.c example_liveness_with_cycle.c)
+
+
 
 
 target_link_libraries(centralized simgrid m )
@@ -24,4 +28,5 @@ target_link_libraries(bugged2     simgrid m )
 target_link_libraries(bugged3     simgrid m )
 target_link_libraries(random_test     simgrid m )
 target_link_libraries(example_liveness_without_cycle     simgrid m )
-target_link_libraries(example2_liveness_without_cycle     simgrid m )
\ No newline at end of file
+target_link_libraries(example2_liveness_without_cycle     simgrid m )
+target_link_libraries(example_liveness_with_cycle     simgrid m )

diff --git a/examples/msg/mc/bugged3.c b/examples/msg/mc/bugged3.c
index a398f0f..8e33b31 100644 (file)
--- a/examples/msg/mc/bugged3.c
+++ b/examples/msg/mc/bugged3.c
@@ -29,7 +29,7 @@ int server(int argc, char *argv[])
   val1 = (long) MSG_task_get_data(task1);
   XBT_INFO("Received %lu", val1);
 
-  //MC_assert(val1 == 2);
+  MC_assert(val1 == 2);
 
   XBT_INFO("OK");
   return 0;

diff --git a/examples/msg/mc/example2_liveness_without_cycle.c b/examples/msg/mc/example2_liveness_without_cycle.c
index 14c54b0..519933c 100644 (file)
--- a/examples/msg/mc/example2_liveness_without_cycle.c
+++ b/examples/msg/mc/example2_liveness_without_cycle.c
@@ -20,7 +20,7 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "Example liveness with
 extern xbt_automaton_t automaton;
 
 
-int p=1;
+int p=0;
 int q=0;
 
 
@@ -51,7 +51,7 @@ int server(int argc, char *argv[])
   val1 = (long) MSG_task_get_data(task1);
   XBT_INFO("Received %lu", val1);
 
-  //MC_assert_pair_stateless(val1 == 2);
+  MC_assert_pair_stateless(val1 == 2);
 
   /*if(val1 == 2)
     q = 1;

diff --git a/examples/msg/mc/example_liveness_with_cycle.c b/examples/msg/mc/example_liveness_with_cycle.c
index 42ef27d..09deb12 100644 (file)
--- a/examples/msg/mc/example_liveness_with_cycle.c
+++ b/examples/msg/mc/example_liveness_with_cycle.c
@@ -12,7 +12,7 @@
 #include "y.tab.c"
 
 #define AMOUNT_OF_CLIENTS 2
-#define CS_PER_PROCESS 1
+#define CS_PER_PROCESS 2
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages");
 
@@ -27,6 +27,10 @@ int predQ(){
   return q;
 }
 
+
+//xbt_dynar_t listeVars -> { void *ptr; int size (nb octets); } => liste de structures 
+//=> parcourir la liste et comparer les contenus de chaque pointeur
+
 int coordinator(int argc, char *argv[])
 {
   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);   // dynamic vector storing requests (which are char*)
@@ -48,23 +52,21 @@ int coordinator(int argc, char *argv[])
          m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
          MSG_task_send(answer, req);
          CS_used = 1;
-         }else{
+       }else{
          m_task_t answer = MSG_task_create("notgrant", 0, 1000, NULL);
          MSG_task_send(answer, req);
        }
-       
       }
     } else {                    // that's a release. Check if someone was waiting for the lock
       if (xbt_dynar_length(requests) > 0) {
         XBT_INFO("CS release. Grant to queued requests (queue size: %lu)",
               xbt_dynar_length(requests));
-        char *req;
+        char *req ;
+       xbt_dynar_pop(requests, &req);
        if(strcmp(req, "1") == 0){
-         xbt_dynar_pop(requests, &req);
          MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
          todo--;
        }else{
-         xbt_dynar_pop(requests, &req);
          MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req);
          todo--;
        }
@@ -88,12 +90,10 @@ int client(int argc, char *argv[])
   // request the CS 2 times, sleeping a bit in between
   int i;
   for (i = 0; i < CS_PER_PROCESS; i++) {
-    p = 1;
-    q = 0;
     XBT_INFO("Ask the request");
     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox),
                   "coordinator");
-    if(strcmp(my_mailbox, "1") == 0){
+    if(strcmp(my_mailbox, "2") == 0){
       p = 1;
       q = 0;
     }
@@ -112,12 +112,6 @@ int client(int argc, char *argv[])
       MSG_process_sleep(1);
       MSG_task_send(MSG_task_create("release", 0, 1000,NULL ),
                    "coordinator");
-    }else{
-      MSG_task_destroy(grant);
-      XBT_INFO("Negative answer");
-      MSG_process_sleep(1);
-      MSG_task_send(MSG_task_create("notrelease", 0, 1000,NULL ),
-                   "coordinator");
     }
     
     MSG_process_sleep(my_pid);

diff --git a/examples/msg/mc/example_liveness_without_cycle.c b/examples/msg/mc/example_liveness_without_cycle.c
index a6e998c..a43f7c8 100644 (file)
--- a/examples/msg/mc/example_liveness_without_cycle.c
+++ b/examples/msg/mc/example_liveness_without_cycle.c
@@ -12,32 +12,18 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_without_cycle, "Example liveness w
 
 extern xbt_automaton_t automaton;
 
-
-int p=1;
 int r=1;
-int q=1;
 int e=1;
 int d=1;
 
-
-int predP(){
-  return p;
-}
-
 int predR(){
   return r;
 }
 
-int predQ(){
-  return q;
-}
-
-
 int predD(){
   return d;
 }
 
-
 int predE(){
   return e;
 }
@@ -59,7 +45,7 @@ int server(int argc, char *argv[])
     //XBT_INFO("r (server) = %d", r);
      
   }
-  MC_assert_pair_stateless(atoi(MSG_task_get_name(task)) == 3);
+  //MC_assert_pair_stateless(atoi(MSG_task_get_name(task)) == 3);
 
   XBT_INFO("OK");
   return 0;
@@ -76,7 +62,7 @@ int client(int argc, char *argv[])
   
   XBT_INFO("Sent!");
   
-  //r=(r+1)%3;
+  r=(r+1)%2;
   //XBT_INFO("r (client) = %d", r);
   
   return 0;
@@ -88,9 +74,7 @@ int main(int argc, char **argv){
   init();
   yyparse();
   automaton = get_automaton();
-  xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP); 
-  ps = xbt_new_propositional_symbol(automaton,"q", &predQ); 
-  ps = xbt_new_propositional_symbol(automaton,"r", &predR); 
+  xbt_propositional_symbol_t ps =  xbt_new_propositional_symbol(automaton,"r", &predR); 
   ps = xbt_new_propositional_symbol(automaton,"e", &predE);
   ps = xbt_new_propositional_symbol(automaton,"d", &predD);
       

diff --git a/examples/msg/mc/example_liveness_without_cycle.h b/examples/msg/mc/example_liveness_without_cycle.h
index 1ff4c99..1667c45 100644 (file)
--- a/examples/msg/mc/example_liveness_without_cycle.h
+++ b/examples/msg/mc/example_liveness_without_cycle.h
@@ -1,5 +1,5 @@
-#ifndef _EXAMPLE_AUTOMATON_H
-#define _EXAMPLE_AUTOMATON_H
+#ifndef _EXAMPLE_LIVENESS_WITHOUT_CYCLE_H
+#define _EXAMPLE_LIVENESS_WITHOUT_CYCLE_H
 
 int yyparse(void);
 int yywrap(void);

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 60adc47..480358f 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -82,10 +82,11 @@ int reached(xbt_automaton_t a, mc_snapshot_t s){
     
     cursor = 0;
     mc_pair_reached_t pair_test;
+    int (*compare_dynar)(const void*; const void*) = propositional_symbols_compare;
     
     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
       if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-       if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, propositional_symbols_compare_value) == 0){
+       if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, compare_dynar) == 0){
          if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){
            MC_UNSET_RAW_MEM;
            return 1;

diff --git a/src/xbt/automaton.c b/src/xbt/automaton.c
index 46d06fa..e9f4f02 100644 (file)
--- a/src/xbt/automaton.c
+++ b/src/xbt/automaton.c
@@ -343,6 +343,6 @@ int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
 
 int propositional_symbols_compare_value(const void *s1, const void *s2){
 
-  return (!((int)s1 == (int)s2));
+  return (!(s1 == s2));
 
 }

diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c
index b2814b3..6c72b25 100644 (file)
--- a/src/xbt/mmalloc/mm_legacy.c
+++ b/src/xbt/mmalloc/mm_legacy.c
@@ -298,7 +298,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
 
  
   size_t block_free1, start1, block_free2 , start2, block_busy1, block_busy2 ;
-  unsigned int i;
+  size_t i;
   void *addr_block1, *addr_block2;
   struct mdesc* mdp;
 
@@ -307,7 +307,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
   block_busy1 = start1 + mdp1->heapinfo[start1].free.size;
   block_busy2 = start2 + mdp2->heapinfo[start2].free.size;
 
-  XBT_DEBUG("Block busy : %d - %d", block_busy1, block_busy2);
+  XBT_DEBUG("Block busy : %Zu - %Zu", block_busy1, block_busy2);
 
 
   if(mdp1->heapinfo[start1].free.size != mdp2->heapinfo[start2].free.size){ // <=> check block_busy
@@ -326,12 +326,12 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
    
       i=block_busy1 ;
 
-      XBT_DEBUG("Next free : %d", mdp1->heapinfo[start1].free.next);
+      XBT_DEBUG("Next free : %Zu", mdp1->heapinfo[start1].free.next);
 
 
       while(i<mdp1->heapinfo[start1].free.next){
 
-       XBT_DEBUG("i (block busy) : %d", i);
+       XBT_DEBUG("i (block busy) : %Zu", i);
 
        if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
          XBT_DEBUG("Different type of busy block");
@@ -347,9 +347,9 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
              XBT_DEBUG("Different size of a large cluster");
              return 1;
            }else{
-             XBT_DEBUG("Blocks %d : %p - %p / Data size : %d (%d blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size );       
+             XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu (%Zu blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size );    
              if(memcmp(addr_block1, addr_block2, mdp1->heapinfo[i].busy.info.size * BLOCKSIZE) != 0){
-               XBT_DEBUG("Different data in block %d", i);
+               XBT_DEBUG("Different data in block %Zu", i);
                return 1;
              } 
            }
@@ -365,7 +365,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
                return 1; 
              }else{
                if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){
-                 XBT_DEBUG("Different data in block %d", i);
+                 XBT_DEBUG("Different data in block %Zu", i);
                  return 1;
                } 
              }
@@ -392,14 +392,14 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
          return 1;
        }else{
 
-         XBT_DEBUG("Index of next busy block : %d - %d", block_busy1, block_busy2);
-         XBT_DEBUG("Index of next free cluster : %d", mdp1->heapinfo[block_free1].free.next);
+         XBT_DEBUG("Index of next busy block : %Zu - %Zu", block_busy1, block_busy2);
+         XBT_DEBUG("Index of next free cluster : %Zu", mdp1->heapinfo[block_free1].free.next);
        
          i = block_busy1;
 
          while(i<mdp1->heapinfo[block_free1].free.next){
 
-           XBT_DEBUG("i (block busy) : %d", i);
+           XBT_DEBUG("i (block busy) : %Zu", i);
 
            if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
              XBT_DEBUG("Different type of busy block");
@@ -415,10 +415,10 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
                  XBT_DEBUG("Different size of a large cluster");
                  return 1;
                }else{
-                 XBT_DEBUG("Blocks %d : %p - %p / Data size : %d", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE));                
+                 XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE));              
                  //XBT_DEBUG("Size of large cluster %d", mdp->heapinfo[i].busy.info.size);
                  if(memcmp(addr_block1, addr_block2, (mdp1->heapinfo[i].busy.info.size * BLOCKSIZE)) != 0){
-                   XBT_DEBUG("Different data in block %d", i);
+                   XBT_DEBUG("Different data in block %Zu", i);
                    return 1;
                  } 
                }
@@ -434,7 +434,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
                    return 1; 
                  }else{
                    if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){
-                     XBT_DEBUG("Different data in fragmented block %d", i);
+                     XBT_DEBUG("Different data in fragmented block %Zu", i);
                      return 1;
                    } 
                  }