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 static void install_trace_analyses(ModelExecution *execution)
160 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
161 for(unsigned int i=0;i<installedanalysis->size();i++) {
162 TraceAnalysis * ta=(*installedanalysis)[i];
163 ta->setExecution(execution);
164 model->add_trace_analysis(ta);
165 /** Call the installation event for each installed plugin */
166 ta->actionAtInstallation();
171 * Main function. Just initializes snapshotting library and the
172 * snapshotting library calls the model_main function.
174 int main(int argc, char **argv)
177 * If this printf statement is removed, C11Tester will fail on an
178 * assert on some versions of glibc. The first time printf is
179 * called, it allocated internal buffers. We can't easily snapshot
180 * libc since we also use it.
184 "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
185 "Distributed under the GPLv2\n"
186 "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
189 //Initialize snapshotting library and model checker object
191 snapshot_system_init(10000, 1024, 1024, 40000);
192 model = new ModelChecker();
193 model->startChecker();
196 /* Configure output redirection for the model-checker */
200 //Stash command line options
201 model_params *params = model->getParams();
205 install_trace_analyses(model->get_execution());
207 model->startMainThread();