X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=action.h;h=36c72079b165a6a7462d5a32698e61dbdef12dbd;hp=30c8a35b80ed7681ce74bc5388c0667b9b4e4fec;hb=123c66e0c1b0f58aae2916cc22b2100143a2ceb4;hpb=8548c711d71b6474802af83f5a4800eb4ac30718 diff --git a/action.h b/action.h index 30c8a35..36c7207 100644 --- a/action.h +++ b/action.h @@ -13,7 +13,10 @@ #include "mymemory.h" #include "clockvector.h" -#define VALUE_NONE -1 +/** Note that this value can be legitimately used by a program, and + hence by iteself does not indicate no value. */ + +#define VALUE_NONE 1234567890 /** @brief Represents an action type, identifying one of several types of * ModelAction */ @@ -38,7 +41,7 @@ class ClockVector; */ class ModelAction { public: - ModelAction(action_type_t type, memory_order order, void *loc, int value = VALUE_NONE); + ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE); ~ModelAction(); void print(void) const; @@ -47,7 +50,7 @@ public: memory_order get_mo() const { return order; } void * get_location() const { return location; } modelclock_t get_seq_number() const { return seq_number; } - int get_value() const { return value; } + uint64_t get_value() const { return value; } const ModelAction * get_reads_from() const { return reads_from; } Node * get_node() const { return node; } @@ -94,7 +97,7 @@ private: /** The value read or written (if RMW, then the value written). This * should probably be something longer. */ - int value; + uint64_t value; /** The action that this action reads from. Only valid for reads */ const ModelAction *reads_from;