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_id, 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.
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 1061 of file shared_buffers.cpp.
|
protected |
Definition at line 200 of file shared_buffers.h.
|
protected |
Definition at line 199 of file shared_buffers.h.
|
protected |
Definition at line 196 of file shared_buffers.h.
|
protected |
Definition at line 201 of file shared_buffers.h.
|
protected |
Definition at line 204 of file shared_buffers.h.
|
protected |
Definition at line 194 of file shared_buffers.h.
|
protected |
Definition at line 195 of file shared_buffers.h.