CBMC
|
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_bufferst | protected |
add(const symbolt &object, const std::string &suffix, const typet &type) | shared_bufferst | inlineprotected |
add_fresh_var(const symbolt &object, const std::string &suffix, const typet &type) | shared_bufferst | inlineprotected |
add_initialization(goto_programt &goto_program) | shared_bufferst | protected |
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_set | shared_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_bufferst | inline |
cav11 | shared_bufferst | protected |
choice(const irep_idt &function_id, const std::string &suffix) | shared_bufferst | inline |
cycles | shared_bufferst | |
cycles_loc | shared_bufferst | |
cycles_r_loc | shared_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 | |
instrumentations | shared_bufferst | protected |
is_buffered(const namespacet &, const symbol_exprt &, bool is_write) | shared_bufferst | |
is_buffered_in_general(const symbol_exprt &, bool is_write) | shared_bufferst | |
message | shared_bufferst | protected |
nb_threads | shared_bufferst | protected |
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_bufferst | inline |
shared_bufferst(symbol_table_baset &_symbol_table, unsigned _nb_threads, messaget &_message) | shared_bufferst | inline |
symbol_table | shared_bufferst | protected |
track(const irep_idt &id) const | shared_bufferst | inline |
uniq | shared_bufferst | protected |
unique() | shared_bufferst | protected |
var_map | shared_bufferst | |
var_mapt typedef | shared_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 |