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)
128 /* Configure output redirection for the model-checker */
131 /* Let's jump in quickly and start running stuff */
132 snapshot_system_init(200000, 1024, 1024, 90000, &model_main);