cprover
memory_model.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_H
13 #define CPROVER_GOTO_SYMEX_MEMORY_MODEL_H
14 
16 
18 {
19 public:
20  explicit memory_model_baset(const namespacet &_ns);
21  virtual ~memory_model_baset();
22 
23  virtual void operator()(symex_target_equationt &)=0;
24 
25 protected:
26  // program order
27  bool po(event_it e1, event_it e2);
28 
29  // produce fresh symbols
30  unsigned var_cnt;
31  symbol_exprt nondet_bool_symbol(const std::string &prefix);
32 
33  // This gives us the choice symbol for an R-W pair;
34  // built by the method below.
35  typedef std::map<
36  std::pair<event_it, event_it>, symbol_exprt> choice_symbolst;
38 
39  void read_from(symex_target_equationt &equation);
40 
41  // maps thread numbers to an event list
42  typedef std::map<unsigned, event_listt> per_thread_mapt;
43 };
44 
45 #endif // CPROVER_GOTO_SYMEX_MEMORY_MODEL_H
symbol_exprt nondet_bool_symbol(const std::string &prefix)
void read_from(symex_target_equationt &equation)
std::map< unsigned, event_listt > per_thread_mapt
Definition: memory_model.h:42
virtual void operator()(symex_target_equationt &)=0
Add constraints to equation encoding partial orders on events.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool po(event_it e1, event_it e2)
choice_symbolst choice_symbols
Definition: memory_model.h:37
virtual ~memory_model_baset()
memory_model_baset(const namespacet &_ns)
eventst::const_iterator event_it
Expression to hold a symbol (variable)
Definition: std_expr.h:82
std::map< std::pair< event_it, event_it >, symbol_exprt > choice_symbolst
Definition: memory_model.h:36