X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=action.cc;h=876de1262c82475f3f9e6610ba339f305963a0a5;hp=3d38e81c93d1111bf8828448fd5a52718c17eea6;hb=a65e234b607444355eb6e34097ee55ba93d4c01b;hpb=f2325500e8d1264ea811d5e68419b28d154b54ca diff --git a/action.cc b/action.cc index 3d38e81..876de12 100644 --- a/action.cc +++ b/action.cc @@ -9,6 +9,7 @@ #include "common.h" #include "threads-model.h" #include "nodestack.h" +#include "wildcard.h" #define ACTION_INITIAL_CLOCK 0 @@ -34,6 +35,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, Thread *thread) : type(type), order(order), + original_order(order), location(loc), value(value), reads_from(NULL), @@ -192,6 +194,11 @@ bool ModelAction::is_initialization() const return type == ATOMIC_INIT; } +bool ModelAction::is_annotation() const +{ + return type == ATOMIC_ANNOTATION; +} + bool ModelAction::is_relaxed() const { return order == std::memory_order_relaxed; @@ -547,7 +554,8 @@ const char * ModelAction::get_type_str() const case ATOMIC_TRYLOCK: return "trylock"; case ATOMIC_WAIT: return "wait"; case ATOMIC_NOTIFY_ONE: return "notify one"; - case ATOMIC_NOTIFY_ALL: return "notify all"; + case ATOMIC_NOTIFY_ALL: return "notify all"; + case ATOMIC_ANNOTATION: return "annotation"; default: return "unknown type"; }; }