CBMC
memory_model_pso.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Memory models for partial order concurrency
4 
5 Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_MEMORY_MODEL_PSO_H
13 #define CPROVER_GOTO_SYMEX_MEMORY_MODEL_PSO_H
14 
15 #include "memory_model_tso.h"
16 
18 {
19 public:
20  explicit memory_model_psot(const namespacet &_ns):
22  {
23  }
24 
25  virtual void operator()(symex_target_equationt &equation, message_handlert &);
26 
27 protected:
28  virtual bool program_order_is_relaxed(
31 };
32 
33 #endif // 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...
Definition: namespace.h:94
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.