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