scanalysis: install ModelExecution object in the analysis

[model-checker.git] / scanalysis.cc

diff --git a/scanalysis.cc b/scanalysis.cc
index 2bc275d7cada1f25fe4d3af3d1076f1c79325a4a..7e0e8453f2d060a45b5a1c723d9ab2612a837550 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -2,8 +2,11 @@
 #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);
@@ -159,7 +162,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
        /* Merge in the clock vector from the write */
        const ModelAction *write=read->get_reads_from();
        ClockVector *writecv=cvmap->get(write);
-       changed|= ( writecv == NULL || merge(cv, read, writecv) && (*read < *write));
+       changed |= writecv == NULL || (merge(cv, read, writecv) && (*read < *write));
 
        for(int i=0;i<=maxthreads;i++) {
                thread_id_t tid=int_to_id(i);
@@ -228,12 +231,6 @@ void SCAnalysis::computeCV(action_list_t *list) {
                                ClockVector *finishcv = cvmap->get(finish);
                                changed |= (finishcv == NULL) || merge(cv, act, finishcv);
                        }
-                       if (act->is_thread_join()) {
-                               Thread *joinedthr = act->get_thread_operand();
-                               ModelAction *finish = model->get_last_action(joinedthr->get_id());
-                               ClockVector *finishcv = cvmap->get(finish);
-                               changed |= (finishcv == NULL) || cv->merge(finishcv);
-                       }
                        if (act->is_read()) {
                                changed|=processRead(act, cv);
                        }