CBMC
shared_bufferst Member List

This is the complete list of members for shared_bufferst, including all inherited members.

add(const symbolt &object, const std::string &suffix, const typet &type, bool added_as_instrumentation)shared_bufferstprotected
add(const symbolt &object, const std::string &suffix, const typet &type)shared_bufferstinlineprotected
add_fresh_var(const symbolt &object, const std::string &suffix, const typet &type)shared_bufferstinlineprotected
add_initialization(goto_programt &goto_program)shared_bufferstprotected
add_initialization_code(goto_functionst &goto_functions)shared_bufferst
affected_by_delay(value_setst &value_sets, goto_functionst &goto_functions)shared_bufferst
affected_by_delay_setshared_bufferst
assignment(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const exprt &rhs)shared_bufferst
assignment(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const irep_idt &id_rhs)shared_bufferstinline
cav11shared_bufferstprotected
choice(const irep_idt &function_id, const std::string &suffix)shared_bufferstinline
cyclesshared_bufferst
cycles_locshared_bufferst
cycles_r_locshared_bufferst
delay_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &read_object, const irep_idt &write_object)shared_bufferst
det_flush(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread)shared_bufferst
flush_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)shared_bufferst
instrumentationsshared_bufferstprotected
is_buffered(const namespacet &, const symbol_exprt &, bool is_write)shared_bufferst
is_buffered_in_general(const symbol_exprt &, bool is_write)shared_bufferst
messageshared_bufferstprotected
nb_threadsshared_bufferstprotected
nondet_flush(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread, const bool tso_pso_rmo)shared_bufferst
operator()(const irep_idt &object)shared_bufferst
set_cav11(memory_modelt model)shared_bufferstinline
shared_bufferst(symbol_table_baset &_symbol_table, unsigned _nb_threads, messaget &_message)shared_bufferstinline
symbol_tableshared_bufferstprotected
track(const irep_idt &id) constshared_bufferstinline
uniqshared_bufferstprotected
unique()shared_bufferstprotected
var_mapshared_bufferst
var_mapt typedefshared_bufferst
weak_memory(value_setst &value_sets, symbol_table_baset &symbol_table, goto_programt &goto_program, memory_modelt model, goto_functionst &goto_functions)shared_bufferst
write(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, goto_programt::instructiont &original_instruction, const unsigned current_thread)shared_bufferst