Fix SMPI builds by reintroducing a killed MC function that it actually use

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index c61a45d..69217b7 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -36,6 +36,7 @@ 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);
 
@@ -49,6 +50,7 @@ XBT_PUBLIC void MC_unignore_heap(void* address, size_t size);
 #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_unignore_heap(a, s) ((void)0)
 

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index 3897cf2..e64019f 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -47,6 +47,14 @@ void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
   simgrid::mc::AppSide::get()->declare_symbol(name, value);
 }
 
+void MC_ignore(void* addr, size_t size)
+{
+  xbt_assert(mc_model_checker == nullptr);
+  if (not MC_is_active())
+    return;
+  simgrid::mc::AppSide::get()->ignore_memory(addr, size);
+}
+
 void MC_ignore_heap(void *address, size_t size)
 {
   xbt_assert(mc_model_checker == nullptr);