Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_SYMEX_MEMORY_MODEL_H
13 #define CPROVER_GOTO_SYMEX_MEMORY_MODEL_H
45 #endif // CPROVER_GOTO_SYMEX_MEMORY_MODEL_H
eventst::const_iterator event_it
void read_from(symex_target_equationt &equation)
std::map< unsigned, event_listt > per_thread_mapt
virtual void operator()(symex_target_equationt &)=0
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
memory_model_baset(const namespacet &_ns)
std::map< std::pair< event_it, event_it >, symbol_exprt > choice_symbolst
bool po(event_it e1, event_it e2)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
choice_symbolst choice_symbols
symbol_exprt nondet_bool_symbol(const std::string &prefix)
virtual ~memory_model_baset()