/* 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
-XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
+XBT_LOG_NEW_DEFAULT_CATEGORY(mc, "All MC categories");
int MC_random(int min, int max)
{
#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);
}
case SIMCALL_NONE:
return false;
- case SIMCALL_SEM_ACQUIRE:
- xbt_die("Don't use semaphores in model-checked code, it's not supported yet");
- case SIMCALL_COND_WAIT:
- xbt_die("Don't use condition variables in model-checked code, it's not supported yet");
-
case SIMCALL_COMM_WAIT:
{
/* FIXME: check also that src and dst processes are not suspended */
return mutex->owner->pid == req->issuer->pid;
}
- default:
- /* The rest of the requests are always enabled */
- return true;
+ case SIMCALL_SEM_ACQUIRE: {
+ static int warned = 0;
+ if (!warned)
+ XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
+ warned = 1;
+ return true;
+ }
+
+ case SIMCALL_COND_WAIT: {
+ static int warned = 0;
+ if (!warned)
+ XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk");
+ warned = 1;
+ return true;
+ }
+
+ default:
+ /* The rest of the requests are always enabled */
+ return true;
}
}