From 56596a27332a3622b935d5b75f81f4773dcbf757 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 15 Apr 2013 00:02:58 -0700 Subject: [PATCH] params: move model_params to header file --- main.cc | 1 + model.h | 34 +--------------------------------- params.h | 37 +++++++++++++++++++++++++++++++++++++ 3 files changed, 39 insertions(+), 33 deletions(-) create mode 100644 params.h diff --git a/main.cc b/main.cc index 815a3823..689fe9dd 100644 --- a/main.cc +++ b/main.cc @@ -11,6 +11,7 @@ /* global "model" object */ #include "model.h" +#include "params.h" #include "snapshot-interface.h" #include "scanalysis.h" diff --git a/model.h b/model.h index fba6eccd..ff4b2c18 100644 --- a/model.h +++ b/model.h @@ -15,6 +15,7 @@ #include "modeltypes.h" #include "stl-model.h" #include "context.h" +#include "params.h" /* Forward declaration */ class Node; @@ -31,39 +32,6 @@ struct model_snapshot_members; typedef ModelVector rel_heads_list_t; typedef SnapList action_list_t; -/** - * Model checker parameter structure. Holds run-time configuration options for - * the model checker. - */ -struct model_params { - int maxreads; - int maxfuturedelay; - bool yieldon; - bool sc_trace_analysis; - unsigned int fairwindow; - unsigned int enabledcount; - unsigned int bound; - unsigned int uninitvalue; - - /** @brief Maximum number of future values that can be sent to the same - * read */ - int maxfuturevalues; - - /** @brief Only generate a new future value/expiration pair if the - * expiration time exceeds the existing one by more than the slop - * value */ - unsigned int expireslop; - - /** @brief Verbosity (0 = quiet; 1 = noisy) */ - int verbose; - - /** @brief Command-line argument count to pass to user program */ - int argc; - - /** @brief Command-line arguments to pass to user program */ - char **argv; -}; - /** @brief Model checker execution stats */ struct execution_stats { int num_total; /**< @brief Total number of executions */ diff --git a/params.h b/params.h new file mode 100644 index 00000000..946c801e --- /dev/null +++ b/params.h @@ -0,0 +1,37 @@ +#ifndef __PARAMS_H__ +#define __PARAMS_H__ + +/** + * Model checker parameter structure. Holds run-time configuration options for + * the model checker. + */ +struct model_params { + int maxreads; + int maxfuturedelay; + bool yieldon; + bool sc_trace_analysis; + unsigned int fairwindow; + unsigned int enabledcount; + unsigned int bound; + unsigned int uninitvalue; + + /** @brief Maximum number of future values that can be sent to the same + * read */ + int maxfuturevalues; + + /** @brief Only generate a new future value/expiration pair if the + * expiration time exceeds the existing one by more than the slop + * value */ + unsigned int expireslop; + + /** @brief Verbosity (0 = quiet; 1 = noisy) */ + int verbose; + + /** @brief Command-line argument count to pass to user program */ + int argc; + + /** @brief Command-line arguments to pass to user program */ + char **argv; +}; + +#endif /* __PARAMS_H__ */ -- 2.34.1