|
virtual exprt | before (event_it e1, event_it e2) |
|
virtual bool | program_order_is_relaxed (partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const |
|
void | build_per_thread_map (const symex_target_equationt &equation, per_thread_mapt &dest) const |
|
void | thread_spawn (symex_target_equationt &equation, const per_thread_mapt &per_thread_map) |
|
void | program_order (symex_target_equationt &equation) |
|
void | from_read (symex_target_equationt &equation) |
|
void | write_serialization_external (symex_target_equationt &equation) |
|
bool | po (event_it e1, event_it e2) |
| In-thread program order. More...
|
|
symbol_exprt | nondet_bool_symbol (const std::string &prefix) |
|
void | read_from (symex_target_equationt &equation) |
| For each read r from every address we collect the choice symbols S via register_read_from_choice_symbol (for potential read-write pairs) and add a constraint r.guard => \/S. More...
|
|
symbol_exprt | register_read_from_choice_symbol (const event_it &r, const event_it &w, symex_target_equationt &equation) |
| Introduce a new choice symbol s for the pair (r , w ) add constraint s => (w.guard /\ r.lhs=w.lhs) add constraint s => before(w,r) [if w is from another thread]. More...
|
|
void | build_event_lists (symex_target_equationt &) |
| First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (with a list of reads/writes for the address of each event) 2) the numbering map (with per-thread unique number of every event) More...
|
|
void | add_init_writes (symex_target_equationt &) |
| For each shared read event and for each shared write event that appears after spawn or has false guard prepend a shared write SSA step with non-deterministic value. More...
|
|
irep_idt | address (event_it event) const |
| Produce an address ID for an event. More...
|
|
symbol_exprt | clock (event_it e, axiomt axiom) |
| Produce a clock symbol for some event. More...
|
|
void | build_clock_type () |
| Initialize the clock_type so that it can be used to number events. More...
|
|
void | add_constraint (symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const |
| Simplify and add a constraint to equation. More...
|
|
exprt | before (event_it e1, event_it e2, unsigned axioms) |
| Build the partial order constraint for two events: if e1 and e2 are in the same atomic section then constrain with equality between their clocks otherwise constrain with e1 clock being less than e2 clock. More...
|
|
|
enum | axiomt { AX_SC_PER_LOCATION =1,
AX_NO_THINAIR =2,
AX_OBSERVATION =4,
AX_PROPAGATION =8
} |
|
typedef SSA_stept | eventt |
|
typedef symex_target_equationt::SSA_stepst | eventst |
|
typedef eventst::const_iterator | event_it |
|
enum | message_levelt {
M_ERROR =1,
M_WARNING =2,
M_RESULT =4,
M_STATUS =6,
M_STATISTICS =8,
M_PROGRESS =9,
M_DEBUG =10
} |
|
static irep_idt | rw_clock_id (event_it e, axiomt axiom=AX_PROPAGATION) |
| Build identifier for the read/write clock variable. More...
|
|
static unsigned | eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) |
| Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
|
|
static commandt | command (unsigned c) |
| Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
|
|
static eomt | eom |
|
static const commandt | reset |
| return to default formatting, as defined by the terminal More...
|
|
static const commandt | red |
| render text with red foreground color More...
|
|
static const commandt | green |
| render text with green foreground color More...
|
|
static const commandt | yellow |
| render text with yellow foreground color More...
|
|
static const commandt | blue |
| render text with blue foreground color More...
|
|
static const commandt | magenta |
| render text with magenta foreground color More...
|
|
static const commandt | cyan |
| render text with cyan foreground color More...
|
|
static const commandt | bright_red |
| render text with bright red foreground color More...
|
|
static const commandt | bright_green |
| render text with bright green foreground color More...
|
|
static const commandt | bright_yellow |
| render text with bright yellow foreground color More...
|
|
static const commandt | bright_blue |
| render text with bright blue foreground color More...
|
|
static const commandt | bright_magenta |
| render text with bright magenta foreground color More...
|
|
static const commandt | bright_cyan |
| render text with bright cyan foreground color More...
|
|
static const commandt | bold |
| render text with bold font More...
|
|
static const commandt | faint |
| render text with faint font More...
|
|
static const commandt | italic |
| render italic text More...
|
|
static const commandt | underline |
| render underlined text More...
|
|
typedef std::map< std::pair< event_it, event_it >, symbol_exprt > | choice_symbolst |
|
typedef std::map< unsigned, event_listt > | per_thread_mapt |
|
typedef std::vector< event_it > | event_listt |
|
typedef std::map< irep_idt, a_rect > | address_mapt |
|
typedef std::map< event_it, unsigned > | numberingt |
|
static irep_idt | id (event_it event) |
| Produce the symbol ID for an event. More...
|
|
unsigned | var_cnt |
|
choice_symbolst | choice_symbols |
|
const namespacet & | ns |
|
address_mapt | address_map |
|
numberingt | numbering |
|
typet | clock_type |
|
message_handlert * | message_handler |
|
mstreamt | mstream |
|
Definition at line 17 of file memory_model_sc.h.