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");
105 for(index = 0;options[index]!=0;index++) {
106 if (options[index] == ' ')
109 argc++; //first parameter is executable name
110 char optcpy[index + 1];
111 memcpy(optcpy, options, index+1);
112 char * argv[argc + 1];
116 for(index = 0;optcpy[index]!=0;index++) {
117 if (optcpy[index] == ' ') {
118 argv[count++] = &optcpy[index+1];
123 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
129 params->nofork = true;
132 params->maxexecutions = atoi(optarg);
135 params->verbose = optarg ? atoi(optarg) : 1;
138 params->uninitvalue = atoi(optarg);
141 if (install_plugin(optarg))
146 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
147 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
157 /* Restore (global) optind for potential use by user program */
164 void install_trace_analyses(ModelExecution *execution) {
165 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
166 for(unsigned int i=0;i<installedanalysis->size();i++) {
167 TraceAnalysis * ta=(*installedanalysis)[i];
168 ta->setExecution(execution);
169 model->add_trace_analysis(ta);
170 /** Call the installation event for each installed plugin */
171 ta->actionAtInstallation();