remove plugins

diff --git a/Makefile b/Makefile
index fe1bf0d17faaa243e88b8ad7158ce6f913f6e324..cf4a493b2a523fed3ed327509d69a396657f8cc9 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -4,7 +4,7 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
           nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
           datarace.o impatomic.o cmodelint.o \
           snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \
-          context.o execution.o plugins.o libannotate.o
+          context.o execution.o libannotate.o
 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS := -ldl -lrt -rdynamic

diff --git a/execution.cc b/execution.cc
index 2a7e0dadd1e0918ac21b5f43dd4e3608935b8f18..861c82a921d0c268cedbaae889f4e3ed08086335 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -83,8 +83,8 @@ ModelExecution::ModelExecution(ModelChecker *m,
        mo_graph(new CycleGraph())
 {
        /* Initialize a model-checker thread, for special ModelActions */
-       model_thread = new Thread(get_next_id());
-       add_thread(model_thread);
+       model_thread = new Thread(get_next_id());       // L: Create model thread
+       add_thread(model_thread);                       // L: Add model thread to scheduler
        scheduler->register_engine(this);
        node_stack->register_engine(this);
 }

diff --git a/main.cc b/main.cc
index 5b764b61be7b2aea8532f41b673bc60c05f23359..61554eaa8e11b0d684d1d13a9df5d9a60aca2e83 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -15,7 +15,6 @@
 #include "model.h"
 #include "params.h"
 #include "snapshot-interface.h"
-#include "plugins.h"
 
 static void param_defaults(struct model_params *params)
 {
@@ -35,7 +34,6 @@ static void param_defaults(struct model_params *params)
 
 static void print_usage(const char *program_name, struct model_params *params)
 {
-       ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
        /* Reset defaults before printing */
        param_defaults(params);
 
@@ -103,26 +101,8 @@ static void print_usage(const char *program_name, struct model_params *params)
     params->uninitvalue,
                params->maxexecutions);
        model_print("Analysis plugins:\n");
-       for(unsigned int i=0;i<registeredanalysis->size();i++) {
-               TraceAnalysis * analysis=(*registeredanalysis)[i];
-               model_print("%s\n", analysis->name());
-       }
-       exit(EXIT_SUCCESS);
-}
 
-bool install_plugin(char * name) {
-       ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
-       ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
-
-       for(unsigned int i=0;i<registeredanalysis->size();i++) {
-               TraceAnalysis * analysis=(*registeredanalysis)[i];
-               if (strcmp(name, analysis->name())==0) {
-                       installedanalysis->push_back(analysis);
-                       return false;
-               }
-       }
-       model_print("Analysis %s Not Found\n", name);
-       return true;
+       exit(EXIT_SUCCESS);
 }
 
 static void parse_options(struct model_params *params, int argc, char **argv)
@@ -186,7 +166,7 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                case 'y':
                        params->yieldon = true;
                        break;
-               case 't':
+/**            case 't':
                        if (install_plugin(optarg))
                                error = true;
                        break;
@@ -197,6 +177,7 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                                        error = true;
                        }
                        break;
+*/
                case 'Y':
                        params->yieldblock = true;
                        break;
@@ -223,25 +204,12 @@ static void parse_options(struct model_params *params, int argc, char **argv)
 int main_argc;
 char **main_argv;
 
-static void install_trace_analyses(ModelExecution *execution)
-{
-       ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
-       for(unsigned int i=0;i<installedanalysis->size();i++) {
-               TraceAnalysis * ta=(*installedanalysis)[i];
-               ta->setExecution(execution);
-               model->add_trace_analysis(ta);
-               /** Call the installation event for each installed plugin */
-               ta->actionAtInstallation();
-       }
-}
-
 /** The model_main function contains the main model checking loop. */
 static void model_main()
 {
        struct model_params params;
 
        param_defaults(&params);
-       register_plugins();
 
        parse_options(&params, main_argc, main_argv);
 
@@ -250,8 +218,8 @@ static void model_main()
 
        snapshot_stack_init();
 
-       model = new ModelChecker(params);
-       install_trace_analyses(model->get_execution());
+       model = new ModelChecker(params);       // L: Model thread is created
+//     install_trace_analyses(model->get_execution());         L: disable plugin
 
        snapshot_record(0);
        model->run();

diff --git a/model.cc b/model.cc
index 3bac9039b4822475bb0226adcf4fd85cc8008ea1..0e65c63c9e18f8bb6c45b6fe389facd6f839ee4a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -27,7 +27,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        exit_flag(false),
        scheduler(new Scheduler()),
        node_stack(new NodeStack()),
-       execution(new ModelExecution(this, &this->params, scheduler, node_stack)),
+       execution(new ModelExecution(this, &this->params, scheduler, node_stack)),      // L: Model thread is created inside
        execution_number(1),
        diverge(NULL),
        earliest_diverge(NULL),