#include <simgrid/modelchecker.h> /* our public interface (and definition of SIMGRID_HAVE_MC) */
#include <simgrid/simix.h>
-#include <src/internal_config.h>
-#if HAVE_UCONTEXT_H
-#include <ucontext.h> /* context relative declarations */
-#endif
/* Maximum size of the application heap.
*
XBT_PUBLIC(double) MC_process_clock_get(smx_actor_t);
XBT_PRIVATE void MC_automaton_load(const char *file);
-/****************************** MC ignore **********************************/
-XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size);
-XBT_PUBLIC(void) MC_remove_ignore_heap(void *address, size_t size);
-XBT_PUBLIC(void) MC_ignore_local_variable(const char *var_name, const char *frame);
-XBT_PUBLIC(void) MC_ignore_global_variable(const char *var_name);
-#if HAVE_UCONTEXT_H
-XBT_PUBLIC(void) MC_register_stack_area(void *stack, smx_actor_t process, ucontext_t* context, size_t size);
-#endif
-
/********************************* Memory *************************************/
XBT_PUBLIC(void) MC_memory_init(); /* Initialize the memory subsystem */
XBT_PUBLIC(void) MC_memory_exit();
-/* Copyright (c) 2007-2010, 2012-2015. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2007-2017. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include <cstdint>
-
-#include <memory>
-#include <functional>
-#include <utility>
-
-#include <simgrid/simix.hpp>
-
#include "mc/mc.h"
#include "src/kernel/context/Context.hpp"
#include "src/simix/smx_private.h"
+#include "src/mc/mc_ignore.h"
+
/**
* @brief creates a new context for a user level process
-/* Copyright (c) 2009-2015. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2009-2017. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include <math.h>
-
-#include <utility>
-#include <functional>
-
#include "src/internal_config.h"
-#include "xbt/log.h"
#include "xbt/parmap.h"
-#include "xbt/dynar.h"
#include "src/simix/smx_private.h"
#include "mc/mc.h"
+#include "src/mc/mc_ignore.h"
XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_context);
-/* Copyright (c) 2009-2015. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2009-2017. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
#include <ucontext.h> /* context relative declarations */
-#include "mc/mc.h"
#include "src/simix/ActorImpl.hpp"
#include "src/simix/smx_private.h"
#include "xbt/parmap.h"
+#include "mc/mc.h"
+#include "src/mc/mc_ignore.h"
+
/** Many integers are needed to store a pointer
*
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include <cassert>
-
#include <simgrid_config.h>
-#include <xbt/log.h>
-#include <xbt/asserts.h>
-#include <xbt/dynar.h>
-
-#include <simgrid/simix.h>
-
#include "mc/mc.h"
-#include "src/mc/mc_base.h"
#include "src/mc/mc_replay.h"
-#include "src/mc/remote/mc_protocol.h"
-#include "src/simix/smx_private.h"
-
-#include "src/kernel/activity/ActivityImpl.hpp"
-#include "src/kernel/activity/SynchroIo.hpp"
-#include "src/kernel/activity/SynchroComm.hpp"
-#include "src/kernel/activity/SynchroRaw.hpp"
-#include "src/kernel/activity/SynchroSleep.hpp"
-#include "src/kernel/activity/SynchroExec.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/mc_request.h"
-#include "src/mc/Process.hpp"
#include "src/mc/ModelChecker.hpp"
-#include "src/mc/mc_smx.h"
using simgrid::mc::remote;
#endif
{
#if SIMGRID_HAVE_MC
xbt_assert(mc_model_checker == nullptr);
- /* TODO, if the MC is disabled we do not really need to make a simcall for
- * this :) */
#endif
+ /* TODO, if the MC is disabled we do not really need to make a simcall for this :) */
return simcall_mc_random(min, max);
}
#if SIMGRID_HAVE_MC
#include <libunwind.h>
#include "src/mc/mc_comm_pattern.h"
+#include "src/mc/mc_ignore.h"
#include "src/mc/mc_request.h"
#include "src/mc/mc_safety.h"
#include "src/mc/mc_snapshot.h"
#ifndef SIMGRID_MC_IGNORE_H
#define SIMGRID_MC_IGNORE_H
-#include <xbt/base.h> /* SG_BEGIN_DECL */
-#include <xbt/dynar.h>
+#include "src/internal_config.h"
+#include "xbt/dynar.h"
+
+#if HAVE_UCONTEXT_H
+#include <ucontext.h> /* context relative declarations */
+#endif
+
SG_BEGIN_DECL();
-XBT_PRIVATE xbt_dynar_t MC_checkpoint_ignore_new(void);
+XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size);
+XBT_PUBLIC(void) MC_remove_ignore_heap(void *address, size_t size);
+XBT_PUBLIC(void) MC_ignore_local_variable(const char *var_name, const char *frame);
+XBT_PUBLIC(void) MC_ignore_global_variable(const char *var_name);
+
+#if HAVE_UCONTEXT_H
+XBT_PUBLIC(void) MC_register_stack_area(void *stack, smx_actor_t process, ucontext_t* context, size_t size);
+#endif
+
SG_END_DECL();
message.type = MC_MESSAGE_STACK_REGION;
message.stack_region = region;
if (channel_.send(message))
- xbt_die("Coule not send STACK_REGION to model-checker");
+ xbt_die("Could not send STACK_REGION to model-checker");
}
}
}
#include "mc/mc.h"
#include "src/instr/instr_private.h"
#include "src/msg/msg_private.h"
+#include "src/mc/mc_ignore.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(instr_msg, instr, "MSG instrumentation");
#include "instr/instr_interface.h"
#include "mc/mc.h"
#include "src/msg/msg_private.h"
+#include "src/mc/mc_ignore.h"
XBT_LOG_NEW_CATEGORY(msg, "All MSG categories");
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(msg_kernel, msg, "Logging specific to MSG (kernel)");
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "mc/mc.h"
+#include "src/mc/mc_ignore.h"
#include "src/mc/mc_replay.h"
#include "src/msg/msg_private.h"
#include "src/simix/smx_private.h"
#include "src/smpi/smpi_group.hpp"
#include "src/smpi/smpi_comm.hpp"
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_process, smpi, "Logging specific to SMPI (kernel)");
//TODO : replace
/* Free a block of memory allocated by `mmalloc'. */
-/* Copyright (c) 2010-2015. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2010-2017. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "mmprivate.h"
#include "xbt/ex.h"
#include "mc/mc.h"
+#include "src/mc/mc_ignore.h"
/* Return memory to the heap.
Like `mfree' but don't call a mfree_hook if there is one. */