std::unique_ptr<AppSide> AppSide::instance_;
-AppSide* AppSide::initialize(xbt_dynar_t actors_addr)
+AppSide* AppSide::initialize()
{
if (not std::getenv(MC_ENV_SOCKET_FD)) // We are not in MC mode: don't initialize the MC world
return nullptr;
strerror(errno));
s_mc_message_initial_addresses_t message{MessageType::INITIAL_ADDRESSES, mmalloc_get_current_heap(),
- kernel::actor::ActorImpl::get_maxpid_addr(), actors_addr};
+ kernel::actor::ActorImpl::get_maxpid_addr()};
xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
instance_->handle_messages();
#endif
}
coverage_checkpoint();
- xbt_assert(channel_.send(MessageType::DEADLOCK_CHECK_REPLY) ==
- 0, // DEADLOCK_CHECK_REPLY because I'm too lazy to create another message type with no content (FIXME)
- "Could not answer to FINALIZE");
+ xbt_assert(channel_.send(MessageType::FINALIZE_REPLY) == 0, "Could not answer to FINALIZE");
std::fflush(stdout);
if (terminate_asap)
::_Exit(0);
void AppSide::ignore_memory(void* addr, std::size_t size) const
{
+ if (not MC_is_active())
+ return;
+
s_mc_message_ignore_memory_t message;
message.type = MessageType::IGNORE_MEMORY;
message.addr = (std::uintptr_t)addr;
void AppSide::ignore_heap(void* address, std::size_t size) const
{
+ if (not MC_is_active())
+ return;
+
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
s_mc_message_ignore_heap_t message;
void AppSide::unignore_heap(void* address, std::size_t size) const
{
+ if (not MC_is_active())
+ return;
+
s_mc_message_ignore_memory_t message;
message.type = MessageType::UNIGNORE_HEAP;
message.addr = (std::uintptr_t)address;
xbt_assert(channel_.send(message) == 0, "Could send REGISTER_SYMBOL message to model-checker");
}
+/** Register a stack in the model checker
+ *
+ * The stacks are allocated in the heap. The MC handle them specifically
+ * when we analyze/compare the content of the heap so it must be told where
+ * they are with this function.
+ */
void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
{
+ if (not MC_is_active())
+ return;
+
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
s_stack_region_t region;