fence_shared.cpp File Reference

#include "fence_shared.h"
#include <iostream>
#include <sstream>
#include <fstream>
#include <list>
#include <vector>
#include <set>
#include <util/cprover_prefix.h>
#include <util/prefix.h>
#include <util/message.h>
#include <goto-programs/remove_skip.h>
#include <goto-programs/goto_functions.h>
#include <goto-instrument/wmm/goto2graph.h>
#include <goto-instrument/rw_set.h>

Include dependency graph for fence_shared.cpp:

Go to the source code of this file.

Classes
class	simple_insertiont
class	fence_all_sharedt
class	fence_all_shared_aegt
class	fence_volatilet

Macros
#define	OUTPUT(s, fence, file, line, id, type)   s<<fence<<"|"<<file<<"|"<<line<<"|"<<id<<"|"<<type<<'\n'

Functions
void	fence_all_shared (message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
void	fence_all_shared_aeg (message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
void	fence_volatile (message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)

Macro Definition Documentation

OUTPUT

#define OUTPUT	(		s,
			fence,
			file,
			line,
			id,
			type
	)		s<<fence<<"|"<<file<<"|"<<line<<"|"<<id<<"|"<<type<<'\n'

Definition at line 32 of file fence_shared.cpp.

Referenced by simple_insertiont::print_to_file().

Function Documentation

fence_all_shared()

void fence_all_shared	(	message_handlert &	message_handler,
		value_setst &	value_sets,
		symbol_tablet &	symbol_table,
		goto_functionst &	goto_functions
	)

Definition at line 565 of file fence_shared.cpp.

References simple_insertiont::do_it().

Referenced by goto_fence_inserter_parse_optionst::instrument_goto_program().

fence_all_shared_aeg()

void fence_all_shared_aeg	(	message_handlert &	message_handler,
		value_setst &	value_sets,
		symbol_tablet &	symbol_table,
		goto_functionst &	goto_functions
	)

Definition at line 577 of file fence_shared.cpp.

References simple_insertiont::do_it().

Referenced by goto_fence_inserter_parse_optionst::instrument_goto_program().

fence_volatile()

void fence_volatile	(	message_handlert &	message_handler,
		value_setst &	value_sets,
		symbol_tablet &	symbol_table,
		goto_functionst &	goto_functions
	)

Definition at line 589 of file fence_shared.cpp.

References simple_insertiont::do_it().

Referenced by goto_fence_inserter_parse_optionst::instrument_goto_program().