#include <shared_buffers.h>
Definition at line 190 of file shared_buffers.h.
§ cfg_visitort()
§ weak_memory()
instruments the program for the pairs detected through the CFG
Definition at line 1050 of file shared_buffers.cpp.
References CPROVER_PREFIX, rw_set_baset::empty(), messaget::eom(), shared_bufferst::varst::flush_delayed, Forall_goto_program_instructions, forall_rw_set_r_entries, forall_rw_set_w_entries, code_function_callt::function(), goto_program_templatet< codeT, guardT >::insert_before(), is_fence(), is_lwfence(), shared_bufferst::varst::mem_tmp, pointer_type(), Power, PSO, shared_bufferst::varst::read_delayed, shared_bufferst::varst::read_delayed_var, RMO, shared_bufferst::symbol_table, to_code_function_call(), to_symbol_expr(), TSO, shared_bufferst::varst::type, and shared_bufferst::weak_memory().
Referenced by weak_memory().
§ coming_from
unsigned shared_bufferst::cfg_visitort::coming_from |
|
protected |
§ current_thread
unsigned shared_bufferst::cfg_visitort::current_thread |
|
protected |
§ goto_functions
§ max_thread
unsigned shared_bufferst::cfg_visitort::max_thread |
|
protected |
§ past_writes
std::set<irep_idt> shared_bufferst::cfg_visitort::past_writes |
|
protected |
§ shared_buffers
§ symbol_table
The documentation for this class was generated from the following files: