shared_bufferst::cfg_visitort Class Reference

#include <shared_buffers.h>

Collaboration diagram for shared_bufferst::cfg_visitort:

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

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

Detailed Description

Definition at line 189 of file shared_buffers.h.

Constructor & Destructor Documentation

cfg_visitort()

shared_bufferst::cfg_visitort::cfg_visitort ( shared_bufferst &  _shared, symbol_table_baset &  _symbol_table, goto_functionst &  _goto_functions  )

inline

Definition at line 205 of file shared_buffers.h.

Member Function Documentation

weak_memory()

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.

Member Data Documentation

coming_from

unsigned shared_bufferst::cfg_visitort::coming_from

protected

Definition at line 198 of file shared_buffers.h.

current_thread

unsigned shared_bufferst::cfg_visitort::current_thread

protected

Definition at line 197 of file shared_buffers.h.

goto_functions

goto_functionst& shared_bufferst::cfg_visitort::goto_functions

protected

Definition at line 194 of file shared_buffers.h.

max_thread

unsigned shared_bufferst::cfg_visitort::max_thread

protected

Definition at line 199 of file shared_buffers.h.

past_writes

std::set<irep_idt> shared_bufferst::cfg_visitort::past_writes

protected

Definition at line 202 of file shared_buffers.h.

shared_buffers

shared_bufferst& shared_bufferst::cfg_visitort::shared_buffers

protected

Definition at line 192 of file shared_buffers.h.

symbol_table

symbol_table_baset& shared_bufferst::cfg_visitort::symbol_table

protected

Definition at line 193 of file shared_buffers.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/shared_buffers.h
• /home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/shared_buffers.cpp