move license to LICENSE file

[model-checker.git] / scanalysis.cc

diff --git a/scanalysis.cc b/scanalysis.cc
index 2bc275d7cada1f25fe4d3af3d1076f1c79325a4a..ff7854a87e8a31aec8e3ae105d403ad0b3559c66 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -159,7 +159,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 +228,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);
                        }