scanalysis: install ModelExecution object in the analysis

diff --git a/main.cc b/main.cc
index 689fe9dd4dbd3698e66d5bfe5adfbd66330efbe6..56eb311dd86f755d45989972d1fe165be74c60a2 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -133,9 +133,10 @@ static void parse_options(struct model_params *params, int argc, char **argv)
 int main_argc;
 char **main_argv;
 
 int main_argc;
 char **main_argv;
 

-void install_trace_analyses() {
+static void install_trace_analyses(const ModelExecution *execution)
+{

        if (model->params.sc_trace_analysis)
        if (model->params.sc_trace_analysis)

-               model->add_trace_analysis(new SCAnalysis());
+               model->add_trace_analysis(new SCAnalysis(execution));

 }
 
 /** The model_main function contains the main model checking loop. */
 }
 
 /** The model_main function contains the main model checking loop. */


@@ -153,7 +154,7 @@ static void model_main()
        snapshot_stack_init();
 
        model = new ModelChecker(params);
        snapshot_stack_init();
 
        model = new ModelChecker(params);

-       install_trace_analyses();
+       install_trace_analyses(model->get_execution());

 
        snapshot_record(0);
        model->run();
 
        snapshot_record(0);
        model->run();

diff --git a/scanalysis.cc b/scanalysis.cc
index ff7854a87e8a31aec8e3ae105d403ad0b3559c66..7e0e8453f2d060a45b5a1c723d9ab2612a837550 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -2,8 +2,11 @@
 #include "action.h"
 #include "threads-model.h"
 #include "clockvector.h"
 #include "action.h"
 #include "threads-model.h"
 #include "clockvector.h"

+#include "execution.h"

 
 

-SCAnalysis::SCAnalysis() {
+SCAnalysis::SCAnalysis(const ModelExecution *execution) :
+       execution(execution)
+{

        cvmap=new HashTable<const ModelAction *, ClockVector *, uintptr_t, 4>();
        cycleset=new HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4>();
        threadlists=new SnapVector<action_list_t>(1);
        cvmap=new HashTable<const ModelAction *, ClockVector *, uintptr_t, 4>();
        cycleset=new HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4>();
        threadlists=new SnapVector<action_list_t>(1);

diff --git a/scanalysis.h b/scanalysis.h
index 06fc2ed54d7cc0b04bd04071a2649895e4a4ef05..7e300e0c1e71451905a2dee56f99a3e1e3605681 100644 (file)
--- a/scanalysis.h
+++ b/scanalysis.h
@@ -5,7 +5,7 @@
 
 class SCAnalysis : public TraceAnalysis {
  public:
 
 class SCAnalysis : public TraceAnalysis {
  public:

-       SCAnalysis();
+       SCAnalysis(const ModelExecution *execution);

        ~SCAnalysis();
        virtual void analyze(action_list_t *);
 
        ~SCAnalysis();
        virtual void analyze(action_list_t *);
 


@@ -23,5 +23,6 @@ class SCAnalysis : public TraceAnalysis {
        HashTable<const ModelAction *,ClockVector *, uintptr_t, 4 > * cvmap;
        HashTable<const ModelAction *,const ModelAction *, uintptr_t, 4 > * cycleset;
        SnapVector<action_list_t> * threadlists;
        HashTable<const ModelAction *,ClockVector *, uintptr_t, 4 > * cvmap;
        HashTable<const ModelAction *,const ModelAction *, uintptr_t, 4 > * cycleset;
        SnapVector<action_list_t> * threadlists;

+       const ModelExecution *execution;

 };
 #endif
 };
 #endif