improve the documentation for the MSG_task_[send|receive]_* functions

[simgrid.git] / src / mc / mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 00a2eb9..c7b280f 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -1,5 +1,10 @@
-#include "private.h"
-#include "unistd.h"
+/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "mc_private.h"
+#include <unistd.h>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
@@ -32,7 +37,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
   
   if(s1->num_reg != s2->num_reg){
-    XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
+    XBT_DEBUG("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg);
     return 1;
   }
 
@@ -68,7 +73,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
          return 1;
        }
       }
-      if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data, std_heap)){
+      if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
        if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
          XBT_DEBUG("Different heap (mmalloc_compare)");
          errors++; 
@@ -130,13 +135,13 @@ int reached(xbt_state_t st){
     
     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
     int res;
-    int (*f)();
+    int_f_void_t f;
 
     /* Get values of propositional symbols */
     unsigned int cursor = 0;
     xbt_propositional_symbol_t ps = NULL;
     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
-      f = ps->function;
+      f = (int_f_void_t)ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
     }
@@ -147,7 +152,7 @@ int reached(xbt_state_t st){
     //xbt_dict_t current_rdv_points = SIMIX_get_rdv_points();
      
     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
-      XBT_DEBUG("Pair reached #%d", cursor+1);
+      XBT_DEBUG("Pair reached #%u", cursor+1);
       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
        if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
          //XBT_DEBUG("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
@@ -190,7 +195,7 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu
    xbt_fifo_item_t item1, item2;
    smx_action_t action1, action2;
    xbt_fifo_item_t item_req1, item_req2;
-   smx_req_t req1, req2;
+   smx_simcall_t req1, req2;
    int i=0;
    int j=0;
 
@@ -225,25 +230,25 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu
             return 1;
           }
 
-          if(xbt_fifo_size(action1->request_list) != xbt_fifo_size(action2->request_list)){
-            XBT_DEBUG("Different size of request list (%d - %d", xbt_fifo_size(action1->request_list), xbt_fifo_size(action2->request_list));
+          if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
+            XBT_DEBUG("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
             return 1;
           }else{
 
-            item_req1 = xbt_fifo_get_first_item(action1->request_list);        
-            item_req2 = xbt_fifo_get_first_item(action2->request_list);
+            item_req1 = xbt_fifo_get_first_item(action1->simcalls);    
+            item_req2 = xbt_fifo_get_first_item(action2->simcalls);
 
-            while(j<xbt_fifo_size(action1->request_list)){
+            while(j<xbt_fifo_size(action1->simcalls)){
 
-              req1 = (smx_req_t) xbt_fifo_get_item_content(item_req1);
-              req2 = (smx_req_t) xbt_fifo_get_item_content(item_req2);
+              req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
+              req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);
               
               if(req1->call != req2->call){
-                XBT_DEBUG("Different request call in request_list of action (%d - %d)", req1->call, req2->call);
+                XBT_DEBUG("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call);
                 return 1;
               }
               if(req1->issuer->pid != req2->issuer->pid){
-                XBT_DEBUG("Different request issuer in request_list of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
+                XBT_DEBUG("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
                 return 1;
               }
 
@@ -359,10 +364,10 @@ void set_pair_reached(xbt_state_t st){
   unsigned int cursor = 0;
   xbt_propositional_symbol_t ps = NULL;
   int res;
-  int (*f)(); 
+  int_f_void_t f;
 
   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
-    f = ps->function;
+    f = (int_f_void_t)ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
@@ -424,10 +429,10 @@ int reached_hash(xbt_state_t st){
     unsigned int cursor = 0;
     xbt_propositional_symbol_t ps = NULL;
     int res;
-    int (*f)();
+    int_f_void_t f;
 
     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
-      f = ps->function;
+      f = (int_f_void_t)ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
     }
@@ -498,10 +503,10 @@ void set_pair_reached_hash(xbt_state_t st){
   unsigned int cursor = 0;
   xbt_propositional_symbol_t ps = NULL;
   int res;
-  int (*f)();
+  int_f_void_t f;
 
   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
-    f = ps->function;
+    f = (int_f_void_t)ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
@@ -535,10 +540,10 @@ int visited(xbt_state_t st, int sc){
     unsigned int cursor = 0;
     xbt_propositional_symbol_t ps = NULL;
     int res;
-    int (*f)();
+    int_f_void_t f;
 
     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
-      f = ps->function;
+      f = (int_f_void_t)ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
     }
@@ -610,10 +615,10 @@ int visited_hash(xbt_state_t st, int sc){
     unsigned int cursor = 0;
     xbt_propositional_symbol_t ps = NULL;
     int res;
-    int (*f)();
+    int_f_void_t f;
 
     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
-      f = ps->function;
+      f = (int_f_void_t)ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
     }
@@ -688,10 +693,10 @@ void set_pair_visited_hash(xbt_state_t st, int sc){
   unsigned int cursor = 0;
   xbt_propositional_symbol_t ps = NULL;
   int res;
-  int (*f)();
+  int_f_void_t f;
 
   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
-    f = ps->function;
+    f = (int_f_void_t)ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
@@ -722,10 +727,10 @@ void set_pair_visited(xbt_state_t st, int sc){
   unsigned int cursor = 0;
   xbt_propositional_symbol_t ps = NULL;
   int res;
-  int (*f)();
+  int_f_void_t f;
 
   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
-    f = ps->function;
+    f = (int_f_void_t)ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
@@ -752,39 +757,33 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
     return (left_res || right_res);
-    break;
   }
   case 1 : {
     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
     return (left_res && right_res);
-    break;
   }
   case 2 : {
     int res = MC_automaton_evaluate_label(l->u.exp_not);
     return (!res);
-    break;
   }
   case 3 : { 
     unsigned int cursor = 0;
     xbt_propositional_symbol_t p = NULL;
-    int (*f)();
+    int_f_void_t f;
     xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){
-       f = p->function;
+       f = (int_f_void_t)p->function;
        return (*f)();
       }
     }
     return -1;
-    break;
   }
   case 4 : {
     return 2;
-    break;
   }
   default : 
     return -1;
-    break;
   }
 }
 
@@ -836,7 +835,7 @@ void MC_ddfs_init(void){
 
   /* Save the initial state */
   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness);
+  MC_take_snapshot_liveness(initial_snapshot_liveness);
 
   MC_UNSET_RAW_MEM; 
 
@@ -1003,7 +1002,7 @@ void MC_ddfs(int search_cycle){
              if(reached(pair_succ->automaton_state)){
                //if(reached_hash(pair_succ->automaton_state)){
              
-               XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
+               XBT_DEBUG("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
 
                XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
                XBT_INFO("|             ACCEPTANCE CYCLE            |");
@@ -1093,7 +1092,7 @@ void MC_ddfs(int search_cycle){
        }
 
        if(MC_state_interleave_size(current_pair->graph_state) > 0){
-         XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness));
+         XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
          MC_replay_liveness(mc_stack_liveness, 0);
        }
       }
@@ -1246,9 +1245,9 @@ void MC_ddfs(int search_cycle){
   }
 
   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
-    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
+    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
   }else{
-    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
+    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
   }