fencer.h File Reference

Fence inference. More...

#include <goto-instrument/wmm/wmm.h>
#include <goto-instrument/wmm/weak_memory.h>
#include "infer_mode.h"

Include dependency graph for fencer.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	fence_weak_memory (memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned max_var, unsigned max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, bool print_graph, infer_modet mode, message_handlert &message_handler, bool ignore_arrays)

Detailed Description

Fence inference.

Definition in file fencer.h.

Function Documentation

fence_weak_memory()

void fence_weak_memory	(	memory_modelt	model,
		value_setst &	value_sets,
		symbol_tablet &	symbol_table,
		goto_functionst &	goto_functions,
		bool	SCC,
		instrumentation_strategyt	event_strategy,
		unsigned	unwinding_bound,
		bool	no_cfg_kill,
		bool	no_dependencies,
		loop_strategyt	duplicate_body,
		unsigned	max_var,
		unsigned	max_po_trans,
		bool	render_po,
		bool	render_file,
		bool	render_function,
		bool	cav11_option,
		bool	hide_internals,
		bool	print_graph,
		infer_modet	mode,
		message_handlert &	message_handler,
		bool	ignore_arrays
	)

Definition at line 25 of file fencer.cpp.

References instrumentert::cfg_cycles_filter(), instrumentert::collect_cycles(), instrumentert::collect_cycles_by_SCCs(), fence_insertert::compute(), CPROVER_PREFIX, instrumentert::egraph, instrumentert::egraph_SCCs, goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), Forall_goto_functions, instrumentert::goto2graph_cfg(), INFER, introduce_temporaries(), instrumentert::num_sccs, event_grapht::print_graph(), instrumentert::print_map_function_graph(), instrumentert::print_outputs(), fence_insertert::print_to_file_3(), remove_skip(), instrumentert::set_of_cycles, instrumentert::set_of_cycles_per_SCC, instrumentert::set_parameters_collection(), instrumentert::set_rendering_options(), messaget::status(), goto_functions_templatet< bodyT >::update(), USER_ASSERT, and USER_DEF.

Referenced by goto_fence_inserter_parse_optionst::instrument_goto_program().