CBMC: Member List

add_constraint(symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const partial_order_concurrencyt protected

add_init_writes(symex_target_equationt &) partial_order_concurrencyt protected

address(event_it event) const partial_order_concurrencyt inlineprotected

address_map partial_order_concurrencyt protected

address_mapt typedef partial_order_concurrencyt protected

AX_NO_THINAIR enum value partial_order_concurrencyt

AX_OBSERVATION enum value partial_order_concurrencyt

AX_PROPAGATION enum value partial_order_concurrencyt

AX_SC_PER_LOCATION enum value partial_order_concurrencyt

axiomt enum name partial_order_concurrencyt

before(event_it e1, event_it e2) memory_model_sct protectedvirtual

memory_model_baset::before(event_it e1, event_it e2, unsigned axioms) partial_order_concurrencyt protected

build_clock_type() partial_order_concurrencyt protected

build_event_lists(symex_target_equationt &equation, message_handlert &message_handler) partial_order_concurrencyt protected

build_per_thread_map(const symex_target_equationt &equation, per_thread_mapt &dest) const memory_model_sct protected

choice_symbols memory_model_baset protected

choice_symbolst typedef memory_model_baset protected

clock(event_it e, axiomt axiom) partial_order_concurrencyt protected

clock_type partial_order_concurrencyt protected

event_it typedef partial_order_concurrencyt

event_listt typedef partial_order_concurrencyt protected

eventst typedef partial_order_concurrencyt

eventt typedef partial_order_concurrencyt

from_read(symex_target_equationt &equation) memory_model_sct protected

id(event_it event) partial_order_concurrencyt inlineprotectedstatic

memory_model_baset(const namespacet &_ns) memory_model_baset explicit

memory_model_sct(const namespacet &_ns) memory_model_sct inlineexplicit

nondet_bool_symbol(const std::string &prefix) memory_model_baset protected

ns partial_order_concurrencyt protected

numbering partial_order_concurrencyt protected

numberingt typedef partial_order_concurrencyt protected

operator()(symex_target_equationt &equation, message_handlert &) memory_model_sct virtual

partial_order_concurrencyt(const namespacet &_ns) partial_order_concurrencyt explicit

per_thread_mapt typedef memory_model_baset protected

po(event_it e1, event_it e2) memory_model_baset protected

program_order(symex_target_equationt &equation) memory_model_sct protected

program_order_is_relaxed(partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const memory_model_sct protectedvirtual

read_from(symex_target_equationt &equation) memory_model_baset protected

register_read_from_choice_symbol(const event_it &r, const event_it &w, symex_target_equationt &equation) memory_model_baset protected

rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION) partial_order_concurrencyt static

thread_spawn(symex_target_equationt &equation, const per_thread_mapt &per_thread_map) memory_model_sct protected

var_cnt memory_model_baset protected

write_serialization_external(symex_target_equationt &equation) memory_model_sct protected

~memory_model_baset() memory_model_baset virtual

~partial_order_concurrencyt() partial_order_concurrencyt virtual