Bug: ModelExecution had bogus model_params reference.

Fix.

diff --git a/execution.cc b/execution.cc
index c8c4b89ac2910abd7024b531ea1bed5e97187faa..47a6ebbff7b76dfbbd7f0ec9898606e4f469d29e 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -58,7 +58,7 @@ struct model_snapshot_members {
 
 /** @brief Constructor */
 ModelExecution::ModelExecution(ModelChecker *m,
-               struct model_params *params,
+               const struct model_params *params,
                Scheduler *scheduler,
                NodeStack *node_stack) :
        model(m),

diff --git a/execution.h b/execution.h
index 8a2bcfa9402a8b2d9c0153aa743c5fc5554613cf..1ba030b6d93a2d61fc97009dcf869db4c634e6ce 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -61,7 +61,7 @@ struct release_seq {
 class ModelExecution {
 public:
        ModelExecution(ModelChecker *m,
-                       struct model_params *params,
+                       const struct model_params *params,
                        Scheduler *scheduler,
                        NodeStack *node_stack);
        ~ModelExecution();

diff --git a/model.cc b/model.cc
index 0d79a39c623158858a8cc5efa29b16322191150e..e0c3089e4ec1558e072cd3577b22caa3d3a546e1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -24,7 +24,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        params(params),
        scheduler(new Scheduler()),
        node_stack(new NodeStack()),
-       execution(new ModelExecution(this, &params, scheduler, node_stack)),
+       execution(new ModelExecution(this, &this->params, scheduler, node_stack)),
        execution_number(1),
        diverge(NULL),
        earliest_diverge(NULL),