2 * @brief Entry point for the model checker.
14 /* global "model" object */
17 #include "snapshot-interface.h"
20 void param_defaults(struct model_params *params)
22 params->verbose = !!DBG_ENABLED();
23 params->uninitvalue = 0;
24 params->maxexecutions = 10;
25 params->nofork = false;
28 static void print_usage(struct model_params *params)
30 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
31 /* Reset defaults before printing */
32 param_defaults(params);
35 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
36 "Distributed under the GPLv2\n"
37 "Written by Brian Norris and Brian Demsky\n"
39 "Usage: C11TESTER=[MODEL-CHECKER OPTIONS]\n"
41 "MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
42 "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
44 "Model-checker options:\n"
45 "-h, --help Display this help message and exit\n"
46 "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
47 " 0 is quiet; 1 shows valid executions; 2 is noisy;\n"
50 "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n"
51 " uninitialized atomic.\n"
53 "-t, --analysis=NAME Use Analysis Plugin.\n"
54 "-o, --options=NAME Option for previous analysis plugin. \n"
55 "-x, --maxexec=NUM Maximum number of executions.\n"
57 " -o help for a list of options\n"
61 params->maxexecutions);
62 model_print("Analysis plugins:\n");
63 for(unsigned int i=0;i<registeredanalysis->size();i++) {
64 TraceAnalysis * analysis=(*registeredanalysis)[i];
65 model_print("%s\n", analysis->name());
70 bool install_plugin(char * name) {
71 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
72 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
74 for(unsigned int i=0;i<registeredanalysis->size();i++) {
75 TraceAnalysis * analysis=(*registeredanalysis)[i];
76 if (strcmp(name, analysis->name())==0) {
77 installedanalysis->push_back(analysis);
81 model_print("Analysis %s Not Found\n", name);
85 void parse_options(struct model_params *params) {
86 const char *shortopts = "hnt:o:u:x:v::";
87 const struct option longopts[] = {
88 {"help", no_argument, NULL, 'h'},
89 {"verbose", optional_argument, NULL, 'v'},
90 {"uninitialized", required_argument, NULL, 'u'},
91 {"analysis", required_argument, NULL, 't'},
92 {"options", required_argument, NULL, 'o'},
93 {"maxexecutions", required_argument, NULL, 'x'},
94 {0, 0, 0, 0} /* Terminator */
97 int tmpoptind = optind;
99 char * options = getenv("C11TESTER");
104 for(int index = 0;options[index]!=0;index++) {
105 if (options[index] == ' ')
108 argc++; //first parameter is executable name
109 char * argv[argc + 1];
112 for(int index = 0, count = 2;options[index]!=0;index++) {
113 if (options[index]==' ')
114 argv[count++] = &options[index];
117 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
123 params->nofork = true;
126 params->maxexecutions = atoi(optarg);
129 params->verbose = optarg ? atoi(optarg) : 1;
132 params->uninitvalue = atoi(optarg);
135 if (install_plugin(optarg))
140 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
141 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
151 /* Restore (global) optind for potential use by user program */
158 void install_trace_analyses(ModelExecution *execution) {
159 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
160 for(unsigned int i=0;i<installedanalysis->size();i++) {
161 TraceAnalysis * ta=(*installedanalysis)[i];
162 ta->setExecution(execution);
163 model->add_trace_analysis(ta);
164 /** Call the installation event for each installed plugin */
165 ta->actionAtInstallation();