projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
threads/model: allocate Thread from w/in ModelChecker
[model-checker.git]
/
main.cc
diff --git
a/main.cc
b/main.cc
index 53bf7c5dfa6130f14a3ad539c90f78866f1d4d43..dc3f6f4dca002d6e763e5bbf25068260d3edc828 100644
(file)
--- a/
main.cc
+++ b/
main.cc
@@
-4,9
+4,7
@@
#include <unistd.h>
#include <unistd.h>
-#include <threads.h>
#include "common.h"
#include "common.h"
-#include "threads-model.h"
#include "output.h"
#include "datarace.h"
#include "output.h"
#include "datarace.h"
@@
-15,7
+13,8
@@
#include "model.h"
#include "snapshot-interface.h"
#include "model.h"
#include "snapshot-interface.h"
-static void param_defaults(struct model_params * params) {
+static void param_defaults(struct model_params *params)
+{
params->maxreads = 0;
params->maxfuturedelay = 100;
params->fairwindow = 0;
params->maxreads = 0;
params->maxfuturedelay = 100;
params->fairwindow = 0;
@@
-26,7
+25,8
@@
static void param_defaults(struct model_params * params) {
params->verbose = 0;
}
params->verbose = 0;
}
-static void print_usage(struct model_params *params) {
+static void print_usage(struct model_params *params)
+{
/* Reset defaults before printing */
param_defaults(params);
/* Reset defaults before printing */
param_defaults(params);
@@
-54,7
+54,8
@@
params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expir
exit(EXIT_SUCCESS);
}
exit(EXIT_SUCCESS);
}
-static void parse_options(struct model_params *params, int argc, char **argv) {
+static void parse_options(struct model_params *params, int argc, char **argv)
+{
const char *shortopts = "hm:M:s:S:f:e:b:v";
int opt;
bool error = false;
const char *shortopts = "hm:M:s:S:f:e:b:v";
int opt;
bool error = false;
@@
-111,7
+112,8
@@
int main_argc;
char **main_argv;
/** The model_main function contains the main model checking loop. */
char **main_argv;
/** The model_main function contains the main model checking loop. */
-static void model_main() {
+static void model_main()
+{
struct model_params params;
param_defaults(¶ms);
struct model_params params;
param_defaults(¶ms);
@@
-121,11
+123,10
@@
static void model_main() {
//Initialize race detector
initRaceDetector();
//Initialize race detector
initRaceDetector();
- //Create the singleton SnapshotStack object
- snapshotObject = new SnapshotStack();
+ snapshot_stack_init();
model = new ModelChecker(params);
model = new ModelChecker(params);
- snapshot
Object->snapshotStep
(0);
+ snapshot
_record
(0);
model->run();
delete model;
model->run();
delete model;
@@
-136,7
+137,8
@@
static void model_main() {
* Main function. Just initializes snapshotting library and the
* snapshotting library calls the model_main function.
*/
* Main function. Just initializes snapshotting library and the
* snapshotting library calls the model_main function.
*/
-int main(int argc, char ** argv) {
+int main(int argc, char **argv)
+{
main_argc = argc;
main_argv = argv;
main_argc = argc;
main_argv = argv;
@@
-144,5
+146,5
@@
int main(int argc, char ** argv) {
redirect_output();
/* Let's jump in quickly and start running stuff */
redirect_output();
/* Let's jump in quickly and start running stuff */
-
initSnapshotLibrary
(10000, 1024, 1024, 4000, &model_main);
+
snapshot_system_init
(10000, 1024, 1024, 4000, &model_main);
}
}