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
rename smx_process_t to smx_actor_t
[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
cb8a785
..
9fbd031
100644
(file)
--- a/
src/mc/mc_client_api.cpp
+++ b/
src/mc/mc_client_api.cpp
@@
-15,7
+15,7
@@
#include "src/mc/Client.hpp"
#include "src/mc/ModelChecker.hpp"
#include "src/mc/Client.hpp"
#include "src/mc/ModelChecker.hpp"
-/**
\
file mc_client_api.cpp
+/**
@
file mc_client_api.cpp
*
* This is the implementation of the API used by the user simulated program to
* communicate with the MC (declared in modelchecker.h).
*
* This is the implementation of the API used by the user simulated program to
* communicate with the MC (declared in modelchecker.h).
@@
-28,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);
}
@@
-69,7
+70,7
@@
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
/** @brief Register a stack in the model checker
*
* The stacks are allocated in the heap. The MC handle them especially
/** @brief Register a stack in the model checker
*
* The stacks are allocated in the heap. The MC handle them especially
- * when we analy
s
e/compare the content of the heap so it must be told where
+ * when we analy
z
e/compare the content of the heap so it must be told where
* they are with this function.
*
* @param stack
* they are with this function.
*
* @param stack
@@
-77,29
+78,35
@@
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
* @param context
* @param size Size of the stack
*/
* @param context
* @param size Size of the stack
*/
-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_
actor
_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);
}