From 227fe9ac1163fcf5aa85dff730cfa4a8cfffa22f Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 24 Jul 2015 13:01:21 +0200 Subject: [PATCH 1/1] [mc] Move the proposition declaration functions in mc_client_api.cpp --- src/mc/mc_client_api.cpp | 28 ++++++++++++++++++++++++++++ src/mc/mc_global.cpp | 22 ---------------------- 2 files changed, 28 insertions(+), 22 deletions(-) diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index f48a80cbc5..1605801137 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -17,6 +17,12 @@ #include "mc_client.h" #include "ModelChecker.hpp" +/** \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). + */ + extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc, @@ -64,4 +70,26 @@ void MC_ignore(void* addr, size_t size) } } +void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) +{ + xbt_die("Support for client-side function proposition is not implemented: " + "use MC_automaton_new_propositional_symbol_pointer instead." + ); +} + +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) + return; + s_mc_register_symbol_message_t message; + message.type = MC_MESSAGE_REGISTER_SYMBOL; + if (strlen(name) + 1 > sizeof(message.name)) + xbt_die("Symbol is too long"); + strncpy(message.name, name, sizeof(message.name)); + message.callback = nullptr; + message.data = value; + MC_client_send_message(&message, sizeof(message)); +} + } diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 85a8ecd372..610ffac912 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -517,28 +517,6 @@ void MC_automaton_load(const char *file) xbt_automaton_load(_mc_property_automaton, file); } -void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) -{ - xbt_die("Support for client-side function proposition is not implemented: " - "use MC_automaton_new_propositional_symbol_pointer instead." - ); -} - -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) - return; - s_mc_register_symbol_message_t message; - message.type = MC_MESSAGE_REGISTER_SYMBOL; - if (strlen(name) + 1 > sizeof(message.name)) - xbt_die("Symbol is too long"); - strncpy(message.name, name, sizeof(message.name)); - message.callback = nullptr; - message.data = value; - MC_client_send_message(&message, sizeof(message)); -} - // TODO, fix cross-process access (this function is not used) void MC_dump_stacks(FILE* file) { -- 2.20.1