1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
5 * This program is free software; you can redistribute it and/or
6 * modify it under the terms of the GNU General Public License
7 * version 2 as published by the Free Software Foundation.
11 * @brief Entry point for the model checker.
23 /* global "model" object */
25 #include "snapshot-interface.h"
27 static void param_defaults(struct model_params *params)
29 params->branches = false;
30 params->noyields = false;
31 params->verbose = !!DBG_ENABLED();
34 static void print_usage(const char *program_name, struct model_params *params)
36 /* Reset defaults before printing */
37 param_defaults(params);
40 "Model-checker options:\n"
41 "-h, --help Display this help message and exit\n"
42 "-Y, --avoidyields Fairness support by not executing yields\n"
43 "-b, --branches Only explore all branches\n"
44 "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
45 " -- Program arguments follow.\n\n");
49 static void parse_options(struct model_params *params, int argc, char **argv)
51 const char *shortopts = "hbYv::";
52 const struct option longopts[] = {
53 {"help", no_argument, NULL, 'h'},
54 {"avoidyields", no_argument, NULL, 'Y'},
55 {"branches", no_argument, NULL, 'b'},
56 {"verbose", optional_argument, NULL, 'v'},
57 {0, 0, 0, 0} /* Terminator */
61 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
64 print_usage(argv[0], params);
67 params->branches = true;
70 params->noyields = true;
73 params->verbose = optarg ? atoi(optarg) : 1;
81 /* Pass remaining arguments to user program */
82 params->argc = argc - (optind - 1);
83 params->argv = argv + (optind - 1);
85 /* Reset program name */
86 params->argv[0] = argv[0];
88 /* Reset (global) optind for potential use by user program */
92 print_usage(argv[0], params);
98 /** The model_main function contains the main model checking loop. */
99 static void model_main()
101 struct model_params params;
103 param_defaults(¶ms);
105 parse_options(¶ms, main_argc, main_argv);
108 model_print("TSO\n");
110 snapshot_stack_init();
112 model = new MC(params);
120 * Main function. Just initializes snapshotting library and the
121 * snapshotting library calls the model_main function.
123 int main(int argc, char **argv)
129 * If this printf statement is removed, CDSChecker will fail on an
130 * assert on some versions of glibc. The first time printf is
131 * called, it allocated internal buffers. We can't easily snapshot
132 * libc since we also use it.
136 "Copyright (c) 2016 Regents of the University of California. All rights reserved.\n"
137 "Distributed under the GPLv2\n"
138 "Written by Brian Demsky and Patrick Lam\n\n");
140 /* Configure output redirection for the model-checker */
143 /* Let's jump in quickly and start running stuff */
144 snapshot_system_init(200000, 1024, 1024, 90000, &model_main);