-"Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
-"Distributed under the GPLv2\n"
-"Written by Brian Norris and Brian Demsky\n"
-"\n"
-"Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
-"\n"
-"Options:\n"
-"-h Display this help message and exit\n"
-"-m Maximum times a thread can read from the same write\n"
-" while other writes exist. Default: %d\n"
-"-M Maximum number of future values that can be sent to\n"
-" the same read. Default: %d\n"
-"-s Maximum actions that the model checker will wait for\n"
-" a write from the future past the expected number of\n"
-" actions. Default: %d\n"
-"-S Future value expiration sloppiness. Default: %u\n"
-"-f Specify a fairness window in which actions that are\n"
-" enabled sufficiently many times should receive\n"
-" priority for execution. Default: %d\n"
-"-y Turn on CHESS yield-based fairness support.\n"
-" Default: %d\n"
-"-e Enabled count. Default: %d\n"
-"-b Upper length bound. Default: %d\n"
-"-v Print verbose execution information.\n"
-"-u Value for uninitialized reads. Default: %u\n"
-"-c Use SC Trace Analysis.\n"
-"-- Program arguments follow.\n\n",
-params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->enabledcount, params->bound, params->uninitvalue);
+ "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
+ "Distributed under the GPLv2\n"
+ "Written by Brian Norris and Brian Demsky\n"
+ "\n"
+ "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
+ "\n"
+ "MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
+ "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
+ "\n"
+ "Model-checker options:\n"
+ "-h, --help Display this help message and exit\n"
+ "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
+ " 0 is quiet; 1 shows valid executions; 2 is noisy;\n"
+ " 3 is noisier.\n"
+ " Default: %d\n"
+ "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n"
+ " uninitialized atomic.\n"
+ " Default: %u\n"
+ "-t, --analysis=NAME Use Analysis Plugin.\n"
+ "-o, --options=NAME Option for previous analysis plugin. \n"
+ "-x, --maxexec=NUM Maximum number of executions.\n"
+ " Default: %u\n"
+ " -o help for a list of options\n"
+ "-n No fork\n"
+ " -- Program arguments follow.\n\n",
+ program_name,
+ params->verbose,
+ params->uninitvalue,
+ params->maxexecutions);
+ model_print("Analysis plugins:\n");
+ for(unsigned int i=0;i<registeredanalysis->size();i++) {
+ TraceAnalysis * analysis=(*registeredanalysis)[i];
+ model_print("%s\n", analysis->name());
+ }