12 #ifndef CPROVER_GOTO_SYMEX_MEMORY_MODEL_TSO_H 13 #define CPROVER_GOTO_SYMEX_MEMORY_MODEL_TSO_H 35 #endif // CPROVER_GOTO_SYMEX_MEMORY_MODEL_TSO_H
virtual bool program_order_is_relaxed(partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const
void program_order(symex_target_equationt &equation)
virtual exprt before(event_it e1, event_it e2)
virtual void operator()(symex_target_equationt &equation)
eventst::const_iterator event_it
Base class for all expressions.
Memory models for partial order concurrency.
memory_model_tsot(const namespacet &_ns)