projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model: remove old "uninitialized" bug check
[model-checker.git]
/
action.cc
diff --git
a/action.cc
b/action.cc
index a90878f73d9edc34148359f127df6886d4574cd8..121f5ee7499d7161257dd136e5edd646bc8c8c94 100644
(file)
--- a/
action.cc
+++ b/
action.cc
@@
-66,6
+66,8
@@
void ModelAction::copy_from_new(ModelAction *newaction)
void ModelAction::set_seq_number(modelclock_t num)
{
void ModelAction::set_seq_number(modelclock_t num)
{
+ /* ATOMIC_UNINIT actions should never have non-zero clock */
+ ASSERT(!is_uninitialized());
ASSERT(seq_number == ACTION_INITIAL_CLOCK);
seq_number = num;
}
ASSERT(seq_number == ACTION_INITIAL_CLOCK);
seq_number = num;
}
@@
-122,6
+124,11
@@
bool ModelAction::is_failed_trylock() const
return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
}
return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
}
+bool ModelAction::is_uninitialized() const
+{
+ return type == ATOMIC_UNINIT;
+}
+
bool ModelAction::is_read() const
{
return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMW;
bool ModelAction::is_read() const
{
return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMW;
@@
-129,7
+136,7
@@
bool ModelAction::is_read() const
bool ModelAction::is_write() const
{
bool ModelAction::is_write() const
{
- return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT;
+ return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT
|| type == ATOMIC_UNINIT
;
}
bool ModelAction::could_be_write() const
}
bool ModelAction::could_be_write() const
@@
-339,6
+346,12
@@
void ModelAction::set_try_lock(bool obtainedlock) {
value=VALUE_TRYFAILED;
}
value=VALUE_TRYFAILED;
}
+/** @return The Node associated with this ModelAction */
+Node * ModelAction::get_node() const
+{
+ return node;
+}
+
/**
* Update the model action's read_from action
* @param act The action to read from; should be a write
/**
* Update the model action's read_from action
* @param act The action to read from; should be a write
@@
-346,6
+359,8
@@
void ModelAction::set_try_lock(bool obtainedlock) {
void ModelAction::set_read_from(const ModelAction *act)
{
reads_from = act;
void ModelAction::set_read_from(const ModelAction *act)
{
reads_from = act;
+ if (act && act->is_uninitialized())
+ model->assert_bug("May read from uninitialized atomic\n");
}
/**
}
/**
@@
-401,6
+416,9
@@
void ModelAction::print() const
case THREAD_FINISH:
type_str = "thread finish";
break;
case THREAD_FINISH:
type_str = "thread finish";
break;
+ case ATOMIC_UNINIT:
+ type_str = "uninitialized";
+ break;
case ATOMIC_READ:
type_str = "atomic read";
break;
case ATOMIC_READ:
type_str = "atomic read";
break;