projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
c29b803
)
model: add 'const'
author
Brian Norris
<banorris@uci.edu>
Thu, 21 Mar 2013 23:17:16 +0000
(16:17 -0700)
committer
Brian Norris
<banorris@uci.edu>
Thu, 21 Mar 2013 23:17:16 +0000
(16:17 -0700)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index f0763cbfca28971b9dfd36a0fe5e76dcae41f8aa..7ce959e90b9c5aeaf649df1f422868a63aa34421 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-2049,7
+2049,7
@@
bool ModelChecker::w_modification_order(ModelAction *curr, ModelVector<ModelActi
/** Arbitrary reads from the future are not allowed. Section 29.3
* part 9 places some constraints. This method checks one result of constraint
* constraint. Others require compiler support. */
/** Arbitrary reads from the future are not allowed. Section 29.3
* part 9 places some constraints. This method checks one result of constraint
* constraint. Others require compiler support. */
-bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
+bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
const
{
if (!writer->is_rmw())
return true;
{
if (!writer->is_rmw())
return true;
diff --git
a/model.h
b/model.h
index faa0dfe353a6c908100cafafdac9415a7c278f28..3e9d0643d5e4f7496cb5b51bd8fd8a42ac31c505 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-146,7
+146,7
@@
private:
void add_thread(Thread *t);
bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
void add_thread(Thread *t);
bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
- bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader);
+ bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
const
;
bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
bool has_asserted() const;
void set_assert();
bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
bool has_asserted() const;
void set_assert();