weak_memory.cpp File Reference

#include "weak_memory.h"
#include <set>
#include <util/fresh_symbol.h>
#include <goto-programs/remove_skip.h>
#include <linking/static_lifetime_init.h>
#include <goto-instrument/rw_set.h>
#include "shared_buffers.h"
#include "goto2graph.h"

Include dependency graph for weak_memory.cpp:

Go to the source code of this file.

Functions
void	introduce_temporaries (value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, messaget &message)
	all access to shared variables is pushed into assignments More...
void	weak_memory (memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays)

Detailed Description

Weak Memory Instrumentation for Threaded Goto Programs

Definition in file weak_memory.cpp.

Function Documentation

introduce_temporaries()

void introduce_temporaries	(	value_setst &	value_sets,
		symbol_tablet &	symbol_table,
		const irep_idt &	function_id,
		goto_programt &	goto_program,
		messaget &	message
	)

all access to shared variables is pushed into assignments

Definition at line 38 of file weak_memory.cpp.

weak_memory()

void weak_memory	(	memory_modelt	model,
		value_setst &	value_sets,
		goto_modelt &	goto_model,
		bool	SCC,
		instrumentation_strategyt	event_strategy,
		bool	no_cfg_kill,
		bool	no_dependencies,
		loop_strategyt	duplicate_body,
		unsigned	input_max_var,
		unsigned	input_max_po_trans,
		bool	render_po,
		bool	render_file,
		bool	render_function,
		bool	cav11_option,
		bool	hide_internals,
		message_handlert &	message_handler,
		bool	ignore_arrays
	)

Definition at line 107 of file weak_memory.cpp.