/** 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;
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();