cprover
|
#include <shared_buffers.h>
Public Member Functions | |
cfg_visitort (shared_bufferst &_shared, symbol_tablet &_symbol_table, goto_functionst &_goto_functions) | |
void | weak_memory (value_setst &value_sets, const irep_idt &function, memory_modelt model) |
instruments the program for the pairs detected through the CFG More... | |
Protected Attributes | |
shared_bufferst & | shared_buffers |
symbol_tablet & | symbol_table |
goto_functionst & | goto_functions |
unsigned | current_thread |
unsigned | coming_from |
unsigned | max_thread |
std::set< irep_idt > | past_writes |
Definition at line 191 of file shared_buffers.h.
|
inline |
Definition at line 207 of file shared_buffers.h.
References coming_from, current_thread, and max_thread.
void shared_bufferst::cfg_visitort::weak_memory | ( | value_setst & | value_sets, |
const irep_idt & | function, | ||
memory_modelt | model | ||
) |
instruments the program for the pairs detected through the CFG
Definition at line 1054 of file shared_buffers.cpp.
References shared_bufferst::affected_by_delay_set, shared_bufferst::assignment(), shared_bufferst::choice(), goto_programt::instructiont::code, coming_from, current_thread, messaget::debug(), shared_bufferst::delay_read(), shared_bufferst::det_flush(), rw_set_baset::empty(), messaget::eom(), shared_bufferst::varst::flush_delayed, shared_bufferst::flush_read(), Forall_goto_program_instructions, forall_rw_set_r_entries, forall_rw_set_w_entries, goto_programt::instructiont::function, code_function_callt::function(), goto_functionst::function_map, irept::get_bool(), codet::get_statement(), goto_functions, goto_program, INITIALIZE_FUNCTION, goto_programt::insert_before(), goto_programt::instructiont::is_assign(), shared_bufferst::is_buffered(), goto_programt::instructiont::is_end_thread(), is_fence(), goto_programt::instructiont::is_function_call(), is_lwfence(), goto_programt::instructiont::is_other(), goto_programt::instructiont::is_start_thread(), goto_programt::instructiont::make_atomic_begin(), max_thread, shared_bufferst::varst::mem_tmp, shared_bufferst::message, shared_bufferst::nondet_flush(), exprt::op1(), past_writes, pointer_type(), Power, PSO, shared_bufferst::varst::read_delayed, shared_bufferst::varst::read_delayed_var, RMO, shared_buffers, goto_programt::instructiont::source_location, goto_programt::instructiont::swap(), symbol_table, to_code_function_call(), to_symbol_expr(), TSO, shared_bufferst::varst::type, goto_programt::instructiont::type, messaget::warning(), and shared_bufferst::write().
Referenced by weak_memory().
|
protected |
Definition at line 200 of file shared_buffers.h.
Referenced by cfg_visitort(), and weak_memory().
|
protected |
Definition at line 199 of file shared_buffers.h.
Referenced by cfg_visitort(), and weak_memory().
|
protected |
Definition at line 196 of file shared_buffers.h.
Referenced by weak_memory().
|
protected |
Definition at line 201 of file shared_buffers.h.
Referenced by cfg_visitort(), and weak_memory().
|
protected |
Definition at line 204 of file shared_buffers.h.
Referenced by weak_memory().
|
protected |
Definition at line 194 of file shared_buffers.h.
Referenced by weak_memory().
|
protected |
Definition at line 195 of file shared_buffers.h.
Referenced by weak_memory().