X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f4ed74ca6d4a744d2956a4f2906c897e1886cefd..603c44e45e00a577bccb42cf398a924178f17768:/src/mc/mc_client_api.cpp diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index c80d9dd3ec..da2fece992 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -9,13 +9,12 @@ #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_ignore.h" +#include "src/mc/mc_protocol.h" +#include "src/mc/mc_client.h" +#include "src/mc/ModelChecker.hpp" /** \file mc_client_api.cpp * @@ -23,11 +22,11 @@ * communicate with the MC (declared in modelchecker.h). */ -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,24 +35,6 @@ void MC_assert(int prop) } } -// TODO, MC_automaton_new_propositional_symbol - -void *MC_snapshot(void) -{ - return simcall_mc_snapshot(); -} - -int simcall_HANDLER_mc_compare_snapshots(smx_simcall_t simcall, - mc_snapshot_t s1, mc_snapshot_t s2) -{ - return snapshot_compare(s1, s2); -} - -int MC_compare_snapshots(void *s1, void *s2) -{ - return simcall_mc_compare_snapshots(s1, s2); -} - void MC_cut(void) { user_max_depth_reached = 1; @@ -98,5 +79,3 @@ void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value) message.data = value; MC_client_send_message(&message, sizeof(message)); } - -}