CBMC
|
#include <shared_buffers.h>
Public Member Functions | |
cfg_visitort (shared_bufferst &_shared, symbol_table_baset &_symbol_table, goto_functionst &_goto_functions) | |
void | weak_memory (value_setst &value_sets, const irep_idt &function_id, memory_modelt model) |
instruments the program for the pairs detected through the CFG More... | |
Protected Attributes | |
shared_bufferst & | shared_buffers |
symbol_table_baset & | symbol_table |
goto_functionst & | goto_functions |
unsigned | current_thread |
unsigned | coming_from |
unsigned | max_thread |
std::set< irep_idt > | past_writes |
Definition at line 189 of file shared_buffers.h.
|
inline |
Definition at line 205 of file shared_buffers.h.
void shared_bufferst::cfg_visitort::weak_memory | ( | value_setst & | value_sets, |
const irep_idt & | function_id, | ||
memory_modelt | model | ||
) |
instruments the program for the pairs detected through the CFG
Definition at line 1048 of file shared_buffers.cpp.
|
protected |
Definition at line 198 of file shared_buffers.h.
|
protected |
Definition at line 197 of file shared_buffers.h.
|
protected |
Definition at line 194 of file shared_buffers.h.
|
protected |
Definition at line 199 of file shared_buffers.h.
|
protected |
Definition at line 202 of file shared_buffers.h.
|
protected |
Definition at line 192 of file shared_buffers.h.
|
protected |
Definition at line 193 of file shared_buffers.h.