12 #ifndef CPROVER_GOTO_SYMEX_MEMORY_MODEL_PSO_H
13 #define CPROVER_GOTO_SYMEX_MEMORY_MODEL_PSO_H
memory_model_psot(const namespacet &_ns)
virtual bool program_order_is_relaxed(partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const
virtual void operator()(symex_target_equationt &equation, message_handlert &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
eventst::const_iterator event_it
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Memory models for partial order concurrency.