Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
MC further cleanups (let it compile, this time)
[simgrid.git] / include / simgrid / modelchecker.h
index ea97b21..c61a45d 100644 (file)
@@ -5,12 +5,6 @@
 /* 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. */
 
-/** \file modelchecker.h
- *
- *  This is the API used by the user simulated program to communicate
- *  with the MC.
- */
-
 #ifndef SIMGRID_MODELCHECKER_H
 #define SIMGRID_MODELCHECKER_H
 
@@ -26,9 +20,7 @@ XBT_PUBLIC int MC_random(int min, int max);
 
 #if SIMGRID_HAVE_MC
 
-/* Internal variable used to check if we're running under the MC
- *
- * Please don't use directly: you should use MC_is_active. */
+/* Internal variable used to check if we're running under the MC. Please use MC_is_active instead. */
 extern XBT_PUBLIC int _sg_do_model_check;
 extern XBT_PUBLIC int _sg_mc_max_visited_states;
 
@@ -44,11 +36,8 @@ XBT_PUBLIC void MC_assert(int);
 XBT_PUBLIC void MC_automaton_new_propositional_symbol(const char* id, int (*fct)(void));
 XBT_PUBLIC void MC_automaton_new_propositional_symbol_pointer(const char* id, int* value);
 
-XBT_PUBLIC void MC_ignore(void* addr, size_t size);
-
 XBT_PUBLIC void MC_ignore_heap(void* address, size_t size);
 XBT_PUBLIC void MC_unignore_heap(void* address, size_t size);
-XBT_PUBLIC void MC_ignore_global_variable(const char* var_name);
 
 #else
 
@@ -56,13 +45,12 @@ XBT_PUBLIC void MC_ignore_global_variable(const char* var_name);
 #define MC_visited_reduction()          0
 
 #define MC_assert(a)                    xbt_assert(a)
+
 #define MC_automaton_new_propositional_symbol(a, b) ((void)0)
 #define MC_automaton_new_propositional_symbol_pointer(a, b) ((void)0)
-#define MC_ignore(a, b)                 ((void)0)
 
-#define MC_ignore_heap(a,s)             ((void)0)
-#define MC_remove_ignore_heap(a,s)      ((void)0)
-#define MC_ignore_global_variable(v)    ((void)0)
+#define MC_ignore_heap(a, s) ((void)0)
+#define MC_unignore_heap(a, s) ((void)0)
 
 #endif