correction compile warnings

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 688eab9..d3e4051 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -406,8 +406,8 @@ set(headers_to_install
        include/xbt/mmalloc.h
        include/xbt/replay_trace_reader.h
        include/xbt/parmap.h
-       include/xbt/automatonparse_promela.h
        include/xbt/automaton.h
+       include/xbt/automatonparse_promela.h
        include/mc/modelchecker.h
        include/msg/msg.h
        include/msg/datatypes.h

diff --git a/examples/msg/mc/automaton.c b/examples/msg/mc/automaton.c
index 475b8ca..f8bb337 100644 (file)
--- a/examples/msg/mc/automaton.c
+++ b/examples/msg/mc/automaton.c
@@ -268,7 +268,7 @@ xbt_state_t xbt_automaton_get_current_state(xbt_automaton_t a){
   return a->current_state;
 }
 
-xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, char* id, void* fct){
+xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct){
   xbt_propositional_symbol_t prop_symb = NULL;
   prop_symb = xbt_new0(struct xbt_propositional_symbol, 1);
   prop_symb->pred = strdup(id);

diff --git a/examples/msg/mc/automaton.h b/examples/msg/mc/automaton.h
index b7d5b4e..d1568c1 100644 (file)
--- a/examples/msg/mc/automaton.h
+++ b/examples/msg/mc/automaton.h
@@ -5,6 +5,7 @@
 #include <string.h>
 #include <xbt/dynar.h>
 #include <xbt/sysdep.h>
+#include <xbt/graph.h>
 
 SG_BEGIN_DECL()
 
@@ -58,7 +59,7 @@ typedef struct xbt_propositional_symbol{
 typedef struct xbt_propositional_symbol* xbt_propositional_symbol_t;
 
 
-XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new_automaton();
+XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new_automaton(void);
 
 XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id);
 
@@ -96,7 +97,9 @@ XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a);
 
 XBT_PUBLIC(void) xbt_automaton_display_exp(xbt_exp_label_t l);
 
-XBT_PUBLIC(xbt_propositional_symbol_t) xbt_new_propositional_symbol(xbt_automaton_t a, char* id, void* fct);
+XBT_PUBLIC(xbt_propositional_symbol_t) xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct);
+
+XBT_PUBLIC(xbt_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
 
 SG_END_DECL()
 

diff --git a/examples/msg/mc/automatonparse_promela.h b/examples/msg/mc/automatonparse_promela.h
index 739492a..ece387f 100644 (file)
--- a/examples/msg/mc/automatonparse_promela.h
+++ b/examples/msg/mc/automatonparse_promela.h
@@ -9,7 +9,7 @@ xbt_automaton_t automaton;
 
 SG_BEGIN_DECL()
 
-XBT_PUBLIC(void) init();
+XBT_PUBLIC(void) init(void);
 
 XBT_PUBLIC(void) new_state(char* id, int src);
 
@@ -17,9 +17,9 @@ XBT_PUBLIC(void) new_transition(char* id, xbt_exp_label_t label);
 
 XBT_PUBLIC(xbt_exp_label_t) new_label(int type, ...);
 
-XBT_PUBLIC(xbt_automaton_t) get_automaton();
+XBT_PUBLIC(xbt_automaton_t) get_automaton(void);
 
-XBT_PUBLIC(void) display_automaton();
+XBT_PUBLIC(void) display_automaton(void);
 
 SG_END_DECL()
 

diff --git a/examples/msg/mc/example_automaton.h b/examples/msg/mc/example_automaton.h
index 9ff9cfc..745762c 100644 (file)
--- a/examples/msg/mc/example_automaton.h
+++ b/examples/msg/mc/example_automaton.h
@@ -5,9 +5,11 @@ int yyparse(void);
 int yywrap(void);
 int yylex(void);
 
+int predD(void);
+int predR(void);
+int predE(void);
 
-int predD();
-int predR();
-int predE();
+int server(int argc, char *argv[]);
+int client(int argc, char *argv[]);
 
 #endif 

diff --git a/examples/msg/mc/parserPromela.yacc b/examples/msg/mc/parserPromela.yacc
index 558ea1a..f018f80 100644 (file)
--- a/examples/msg/mc/parserPromela.yacc
+++ b/examples/msg/mc/parserPromela.yacc
@@ -4,6 +4,8 @@
 #include "automatonparse_promela.h"
 #include "lex.yy.c"
 
+void yyerror(const char *s);
+
 %}
 
 %union{
@@ -64,9 +66,11 @@ exp : LEFT_PAR exp RIGHT_PAR { $$ = $2; }
  
 %%
 
-int yyerror(char *s) {
-  fprintf(stderr, "%s\n", s);
-  return 0;
+
+
+void yyerror(const char *s){
+  fprintf (stderr, "%s\n", s);
 }
 
 
+

diff --git a/examples/msg/mc/y.tab.c b/examples/msg/mc/y.tab.c
index 6a87e3f..d2cd6cb 100644 (file)
--- a/examples/msg/mc/y.tab.c
+++ b/examples/msg/mc/y.tab.c
@@ -75,10 +75,12 @@
 #include "automatonparse_promela.h"
 #include "lex.yy.c"
 
+void yyerror(const char *s);
+
 
 
 /* Line 189 of yacc.c  */
-#line 82 "y.tab.c"
+#line 84 "y.tab.c"
 
 /* Enabling traces.  */
 #ifndef YYDEBUG
@@ -157,7 +159,7 @@ typedef union YYSTYPE
 {
 
 /* Line 214 of yacc.c  */
-#line 9 "parserPromela.yacc"
+#line 11 "parserPromela.yacc"
 
   double real;
   int integer;
@@ -167,7 +169,7 @@ typedef union YYSTYPE
 
 
 /* Line 214 of yacc.c  */
-#line 171 "y.tab.c"
+#line 173 "y.tab.c"
 } YYSTYPE;
 # define YYSTYPE_IS_TRIVIAL 1
 # define yystype YYSTYPE /* obsolescent; will be withdrawn */
@@ -179,7 +181,7 @@ typedef union YYSTYPE
 
 
 /* Line 264 of yacc.c  */
-#line 183 "y.tab.c"
+#line 185 "y.tab.c"
 
 #ifdef short
 # undef short
@@ -467,8 +469,8 @@ static const yytype_int8 yyrhs[] =
 /* YYRLINE[YYN] -- source line where rule number YYN was defined.  */
 static const yytype_uint8 yyrline[] =
 {
-       0,    46,    46,    49,    50,    50,    53,    54,    57,    58,
-      59,    60,    61,    62
+       0,    48,    48,    51,    52,    52,    55,    56,    59,    60,
+      61,    62,    63,    64
 };
 #endif
 
@@ -1384,63 +1386,63 @@ yyreduce:
         case 4:
 
 /* Line 1455 of yacc.c  */
-#line 50 "parserPromela.yacc"
+#line 52 "parserPromela.yacc"
     { new_state((yyvsp[(1) - (2)].string), 1);}
     break;
 
   case 7:
 
 /* Line 1455 of yacc.c  */
-#line 54 "parserPromela.yacc"
+#line 56 "parserPromela.yacc"
     { new_transition((yyvsp[(5) - (6)].string), (yyvsp[(2) - (6)].label));}
     break;
 
   case 8:
 
 /* Line 1455 of yacc.c  */
-#line 57 "parserPromela.yacc"
+#line 59 "parserPromela.yacc"
     { (yyval.label) = (yyvsp[(2) - (3)].label); }
     break;
 
   case 9:
 
 /* Line 1455 of yacc.c  */
-#line 58 "parserPromela.yacc"
+#line 60 "parserPromela.yacc"
     { (yyval.label) = new_label(0, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
     break;
 
   case 10:
 
 /* Line 1455 of yacc.c  */
-#line 59 "parserPromela.yacc"
+#line 61 "parserPromela.yacc"
     { (yyval.label) = new_label(1, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
     break;
 
   case 11:
 
 /* Line 1455 of yacc.c  */
-#line 60 "parserPromela.yacc"
+#line 62 "parserPromela.yacc"
     { (yyval.label) = new_label(2, (yyvsp[(2) - (2)].label)); }
     break;
 
   case 12:
 
 /* Line 1455 of yacc.c  */
-#line 61 "parserPromela.yacc"
+#line 63 "parserPromela.yacc"
     { (yyval.label) = new_label(4); }
     break;
 
   case 13:
 
 /* Line 1455 of yacc.c  */
-#line 62 "parserPromela.yacc"
+#line 64 "parserPromela.yacc"
     { (yyval.label) = new_label(3, (yyvsp[(1) - (1)].string)); }
     break;
 
 
 
 /* Line 1455 of yacc.c  */
-#line 1444 "y.tab.c"
+#line 1446 "y.tab.c"
       default: break;
     }
   YY_SYMBOL_PRINT ("-> $$ =", yyr1[yyn], &yyval, &yyloc);
@@ -1652,13 +1654,15 @@ yyreturn:
 
 
 /* Line 1675 of yacc.c  */
-#line 65 "parserPromela.yacc"
+#line 67 "parserPromela.yacc"
 
 
-int yyerror(char *s) {
-  fprintf(stderr, "%s\n", s);
-  return 0;
+
+
+void yyerror(const char *s){
+  fprintf (stderr, "%s\n", s);
 }
 
 
 
+

diff --git a/examples/msg/mc/y.tab.h b/examples/msg/mc/y.tab.h
index 8ea5344..22bb813 100644 (file)
--- a/examples/msg/mc/y.tab.h
+++ b/examples/msg/mc/y.tab.h
@@ -91,7 +91,7 @@ typedef union YYSTYPE
 {
 
 /* Line 1676 of yacc.c  */
-#line 9 "parserPromela.yacc"
+#line 11 "parserPromela.yacc"
 
   double real;
   int integer;

diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h
index a91f8ab..500309d 100644 (file)
--- a/include/xbt/automaton.h
+++ b/include/xbt/automaton.h
@@ -5,6 +5,7 @@
 #include <string.h>
 #include "xbt/dynar.h"
 #include "xbt/sysdep.h"
+#include "xbt/graph.h"
 
 SG_BEGIN_DECL()
 
@@ -58,7 +59,7 @@ typedef struct xbt_propositional_symbol{
 typedef struct xbt_propositional_symbol* xbt_propositional_symbol_t;
 
 
-XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new_automaton();
+XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new_automaton(void);
 
 XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id);
 
@@ -96,7 +97,9 @@ XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a);
 
 XBT_PUBLIC(void) xbt_automaton_display_exp(xbt_exp_label_t l);
 
-XBT_PUBLIC(xbt_propositional_symbol_t) xbt_new_propositional_symbol(xbt_automaton_t a, char* id, void* fct);
+XBT_PUBLIC(xbt_propositional_symbol_t) xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct);
+
+XBT_PUBLIC(xbt_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
 
 SG_END_DECL()
 

diff --git a/include/xbt/automatonparse_promela.h b/include/xbt/automatonparse_promela.h
index edcad66..cb4fc9c 100644 (file)
--- a/include/xbt/automatonparse_promela.h
+++ b/include/xbt/automatonparse_promela.h
@@ -9,7 +9,7 @@ xbt_automaton_t automaton;
 
 SG_BEGIN_DECL()
 
-XBT_PUBLIC(void) init();
+XBT_PUBLIC(void) init(void);
 
 XBT_PUBLIC(void) new_state(char* id, int src);
 
@@ -17,7 +17,9 @@ XBT_PUBLIC(void) new_transition(char* id, xbt_exp_label_t label);
 
 XBT_PUBLIC(xbt_exp_label_t) new_label(int type, ...);
 
-XBT_PUBLIC(xbt_automaton_t) get_automaton();
+XBT_PUBLIC(xbt_automaton_t) get_automaton(void);
+                           
+XBT_PUBLIC(void) display_automaton(void);
 
 SG_END_DECL()
 

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 401ce5b..c715276 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -29,6 +29,7 @@ SG_BEGIN_DECL()
 
 /********************************* Global *************************************/
 XBT_PUBLIC(void) MC_init(void);
+XBT_PUBLIC(void) MC_init_with_automaton(xbt_automaton_t a);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(void) MC_modelcheck(void);

diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c
index 1c443d1..6f7102d 100644 (file)
--- a/src/mc/mc_dfs.c
+++ b/src/mc/mc_dfs.c
@@ -156,6 +156,8 @@ int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
     return 2;
     break;
   }
+  default : 
+    return -1;
   }
 }
 
@@ -241,7 +243,6 @@ void MC_dfs(xbt_automaton_t a, int search_cycle){
 
   smx_process_t process = NULL;
   int value;
-  mc_state_t state = NULL;
   mc_state_t next_graph_state = NULL;
   smx_req_t req = NULL;
   char *req_str;
@@ -271,7 +272,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle){
 
   //FIXME : vérifier condition permettant d'avoir tous les successeurs possibles dans le graph
 
-  while(req = MC_state_get_request(current_pair->graph_state, &value)){
+  while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
     
     /* Debug information */
     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){

diff --git a/src/xbt/automaton.c b/src/xbt/automaton.c
index 436e293..7eb3904 100644 (file)
--- a/src/xbt/automaton.c
+++ b/src/xbt/automaton.c
@@ -1,4 +1,5 @@
 #include "xbt/automaton.h"
+#include "xbt/dynar.h"
 
 xbt_automaton_t xbt_automaton_new_automaton(){
   xbt_automaton_t automaton = NULL;
@@ -268,7 +269,7 @@ xbt_state_t xbt_automaton_get_current_state(xbt_automaton_t a){
   return a->current_state;
 }
 
-xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, char* id, void* fct){
+xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct){
   xbt_propositional_symbol_t prop_symb = NULL;
   prop_symb = xbt_new0(struct xbt_propositional_symbol, 1);
   prop_symb->pred = strdup(id);