X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f4ed74ca6d4a744d2956a4f2906c897e1886cefd..c1111cb247ab39f89dcae0d63a255c669b2ed48e:/src/mc/mc_client_api.cpp diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index c80d9dd3ec..9bbceb0248 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -9,13 +9,13 @@ #include #include -#include "mc_record.h" -#include "mc_private.h" -#include "mc_mmalloc.h" -#include "mc_ignore.h" -#include "mc_protocol.h" -#include "mc_client.h" -#include "ModelChecker.hpp" +#include "src/mc/mc_record.h" +#include "src/mc/mc_private.h" +#include "src/mc/mc_mmalloc.h" +#include "src/mc/mc_ignore.h" +#include "src/mc/mc_protocol.h" +#include "src/mc/mc_client.h" +#include "src/mc/ModelChecker.hpp" /** \file mc_client_api.cpp * @@ -28,6 +28,10 @@ extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc, "Public API for the model-checked application"); +} + +// MC_random() is in mc_base.cpp + void MC_assert(int prop) { if (MC_is_active() && !prop) { @@ -36,8 +40,6 @@ void MC_assert(int prop) } } -// TODO, MC_automaton_new_propositional_symbol - void *MC_snapshot(void) { return simcall_mc_snapshot(); @@ -98,5 +100,3 @@ void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value) message.data = value; MC_client_send_message(&message, sizeof(message)); } - -}