cprover
|
#include <shared_buffers.h>
Classes | |
class | cfg_visitort |
class | varst |
Public Types | |
typedef std::map< irep_idt, varst > | var_mapt |
Public Attributes | |
var_mapt | var_map |
std::set< irep_idt > | cycles |
std::multimap< irep_idt, source_locationt > | cycles_loc |
std::multimap< irep_idt, source_locationt > | cycles_r_loc |
std::set< irep_idt > | affected_by_delay_set |
Protected Member Functions | |
std::string | unique () |
returns a unique id (for fresh variables) | |
irep_idt | add (const symbolt &object, const std::string &suffix, const typet &type, bool added_as_instrumentation) |
add a new var for instrumenting the input var | |
irep_idt | add (const symbolt &object, const std::string &suffix, const typet &type) |
irep_idt | add_fresh_var (const symbolt &object, const std::string &suffix, const typet &type) |
void | add_initialization (goto_programt &goto_program) |
Protected Attributes | |
class symbol_table_baset & | symbol_table |
unsigned | nb_threads |
std::set< irep_idt > | instrumentations |
unsigned | uniq |
bool | cav11 |
messaget & | message |
Definition at line 29 of file shared_buffers.h.
typedef std::map<irep_idt, varst> shared_bufferst::var_mapt |
Definition at line 79 of file shared_buffers.h.
|
inline |
Definition at line 32 of file shared_buffers.h.
|
inlineprotected |
Definition at line 256 of file shared_buffers.h.
|
protected |
add a new var for instrumenting the input var
Definition at line 72 of file shared_buffers.cpp.
|
inlineprotected |
Definition at line 262 of file shared_buffers.h.
|
protected |
Definition at line 96 of file shared_buffers.cpp.
void shared_bufferst::add_initialization_code | ( | goto_functionst & | goto_functions | ) |
Definition at line 125 of file shared_buffers.cpp.
void shared_bufferst::affected_by_delay | ( | value_setst & | value_sets, |
goto_functionst & | goto_functions ) |
analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily shared themselves) whose value could be changed as effect of a read delay
Definition at line 1008 of file shared_buffers.cpp.
void shared_bufferst::assignment | ( | goto_programt & | goto_program, |
goto_programt::targett & | t, | ||
const source_locationt & | source_location, | ||
const irep_idt & | id_lhs, | ||
const exprt & | rhs ) |
add an assignment in the goto-program
Definition at line 140 of file shared_buffers.cpp.
|
inline |
Definition at line 138 of file shared_buffers.h.
|
inline |
Definition at line 163 of file shared_buffers.h.
void 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 ) |
delays a read (POWER)
Definition at line 176 of file shared_buffers.cpp.
void 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 ) |
flush buffers (instruments fence)
Definition at line 327 of file shared_buffers.cpp.
void shared_bufferst::flush_read | ( | goto_programt & | goto_program, |
goto_programt::targett & | t, | ||
const source_locationt & | source_location, | ||
const irep_idt & | write_object ) |
flushes read (POWER)
Definition at line 225 of file shared_buffers.cpp.
bool shared_bufferst::is_buffered | ( | const namespacet & | ns, |
const symbol_exprt & | symbol_expr, | ||
bool | is_write ) |
Definition at line 932 of file shared_buffers.cpp.
bool shared_bufferst::is_buffered_in_general | ( | const symbol_exprt & | symbol_expr, |
bool | is_write ) |
Definition at line 966 of file shared_buffers.cpp.
void shared_bufferst::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 ) |
instruments read
Definition at line 433 of file shared_buffers.cpp.
const shared_bufferst::varst & shared_bufferst::operator() | ( | const irep_idt & | object | ) |
instruments the variable
Definition at line 31 of file shared_buffers.cpp.
|
inline |
Definition at line 44 of file shared_buffers.h.
Definition at line 150 of file shared_buffers.h.
|
protected |
returns a unique id (for fresh variables)
Definition at line 24 of file shared_buffers.cpp.
void shared_bufferst::weak_memory | ( | value_setst & | value_sets, |
symbol_table_baset & | symbol_table, | ||
goto_programt & | goto_program, | ||
memory_modelt | model, | ||
goto_functionst & | goto_functions ) |
void 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 ) |
instruments write
Definition at line 265 of file shared_buffers.cpp.
std::set<irep_idt> shared_bufferst::affected_by_delay_set |
Definition at line 236 of file shared_buffers.h.
|
protected |
Definition at line 244 of file shared_buffers.h.
std::set<irep_idt> shared_bufferst::cycles |
Definition at line 84 of file shared_buffers.h.
std::multimap<irep_idt, source_locationt> shared_bufferst::cycles_loc |
Definition at line 86 of file shared_buffers.h.
std::multimap<irep_idt, source_locationt> shared_bufferst::cycles_r_loc |
Definition at line 88 of file shared_buffers.h.
|
protected |
Definition at line 232 of file shared_buffers.h.
|
protected |
Definition at line 247 of file shared_buffers.h.
|
protected |
Definition at line 229 of file shared_buffers.h.
|
protected |
Definition at line 226 of file shared_buffers.h.
|
protected |
Definition at line 240 of file shared_buffers.h.
var_mapt shared_bufferst::var_map |
Definition at line 80 of file shared_buffers.h.