A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
[simix] Use std::string for s_smx_process_arg
[simgrid.git]
/
src
/
mc
/
mc_client_api.cpp
diff --git
a/src/mc/mc_client_api.cpp
b/src/mc/mc_client_api.cpp
index
9f6c575
..
d12eeff
100644
(file)
--- a/
src/mc/mc_client_api.cpp
+++ b/
src/mc/mc_client_api.cpp
@@
-5,7
+5,6
@@
* under the terms of the license (GNU LGPL) which comes with this package. */
#include <xbt/log.h>
* under the terms of the license (GNU LGPL) which comes with this package. */
#include <xbt/log.h>
-#include <xbt/fifo.h>
#include <xbt/sysdep.h>
#include <simgrid/modelchecker.h>
#include <xbt/sysdep.h>
#include <simgrid/modelchecker.h>
@@
-29,40
+28,41
@@
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
void MC_assert(int prop)
{
void MC_assert(int prop)
{
+ xbt_assert(mc_model_checker == nullptr);
if (MC_is_active() && !prop)
simgrid::mc::Client::get()->reportAssertionFailure();
}
void MC_cut(void)
{
if (MC_is_active() && !prop)
simgrid::mc::Client::get()->reportAssertionFailure();
}
void MC_cut(void)
{
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
+ return;
// FIXME, We want to do this in the model-checker:
// FIXME, We want to do this in the model-checker:
- // user_max_depth_reached = 1;
xbt_die("MC_cut() not implemented");
}
void MC_ignore(void* addr, size_t size)
{
xbt_die("MC_cut() not implemented");
}
void MC_ignore(void* addr, size_t size)
{
- xbt_assert(mc_mode
!= MC_MODE_SERVER
);
- if (
mc_mode != MC_MODE_CLIENT
)
+ xbt_assert(mc_mode
l_checker == nullptr
);
+ if (
!MC_is_active()
)
return;
simgrid::mc::Client::get()->ignoreMemory(addr, size);
}
void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
{
return;
simgrid::mc::Client::get()->ignoreMemory(addr, size);
}
void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
{
- xbt_assert(mc_mode
!= MC_MODE_SERVER
);
- if (
mc_mode != MC_MODE_CLIENT
)
+ xbt_assert(mc_mode
l_checker == nullptr
);
+ if (
!MC_is_active()
)
return;
return;
-
xbt_die("Support for client-side function proposition is not implemented: "
xbt_die("Support for client-side function proposition is not implemented: "
- "use MC_automaton_new_propositional_symbol_pointer instead."
- );
+ "use MC_automaton_new_propositional_symbol_pointer instead.");
}
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
{
}
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
{
- xbt_assert(mc_mode
!= MC_MODE_SERVER
);
- if (
mc_mode != MC_MODE_CLIENT
)
+ xbt_assert(mc_mode
l_checker == nullptr
);
+ if (
!MC_is_active()
)
return;
simgrid::mc::Client::get()->declareSymbol(name, value);
}
return;
simgrid::mc::Client::get()->declareSymbol(name, value);
}
@@
-80,27
+80,33
@@
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
*/
void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* context, size_t size)
{
*/
void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* context, size_t size)
{
- if (mc_mode != MC_MODE_CLIENT)
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
return;
simgrid::mc::Client::get()->declareStack(stack, size, process, context);
}
void MC_ignore_global_variable(const char *name)
{
return;
simgrid::mc::Client::get()->declareStack(stack, size, process, context);
}
void MC_ignore_global_variable(const char *name)
{
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
+ return;
// TODO, send a message to the model_checker
xbt_die("Unimplemented");
}
void MC_ignore_heap(void *address, size_t size)
{
// TODO, send a message to the model_checker
xbt_die("Unimplemented");
}
void MC_ignore_heap(void *address, size_t size)
{
- if (mc_mode != MC_MODE_CLIENT)
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
return;
simgrid::mc::Client::get()->ignoreHeap(address, size);
}
void MC_remove_ignore_heap(void *address, size_t size)
{
return;
simgrid::mc::Client::get()->ignoreHeap(address, size);
}
void MC_remove_ignore_heap(void *address, size_t size)
{
- if (mc_mode != MC_MODE_CLIENT)
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
return;
simgrid::mc::Client::get()->unignoreHeap(address, size);
}
return;
simgrid::mc::Client::get()->unignoreHeap(address, size);
}