goto-instrument Directory Reference

Directory dependency graph for goto-instrument:

Directories
directory	accelerate
directory	wmm

Files
file	alignment_checks.cpp [code]
	Alignment Checks.
file	alignment_checks.h [code]
	Alignment Checks.
file	branch.cpp [code]
	Branch Instrumentation.
file	branch.h [code]
	Branch Instrumentation.
file	call_sequences.cpp [code]
	Printing function call sequences for Ofer.
file	call_sequences.h [code]
	Memory-mapped I/O Instrumentation for Goto Programs.
file	code_contracts.cpp [code]
	Verify and use annotated invariants and pre/post-conditions.
file	code_contracts.h [code]
	Verify and use annotated invariants and pre/post-conditions.
file	concurrency.cpp [code]
	Encoding for Threaded Goto Programs.
file	concurrency.h [code]
	Encoding for Threaded Goto Programs.
file	count_eloc.cpp [code]
	Count effective lines of code.
file	count_eloc.h [code]
	Count effective lines of code.
file	cover.cpp [code]
	Coverage Instrumentation.
file	cover.h [code]
	Coverage Instrumentation.
file	document_properties.cpp [code]
	Subgoal Documentation.
file	document_properties.h [code]
	Documentation of Properties.
file	dot.cpp [code]
	Dump Goto-Program as DOT Graph.
file	dot.h [code]
	Dump Goto-Program as DOT Graph.
file	dump_c.cpp [code]
	Dump Goto-Program as C/C++ Source.
file	dump_c.h [code]
	Dump C from Goto Program.
file	dump_c_class.h [code]
	Dump Goto-Program as C/C++ Source.
file	full_slicer.cpp [code]
	Slicing.
file	full_slicer.h [code]
	Slicing.
file	full_slicer_class.h [code]
	Goto Program Slicing.
file	function.cpp [code]
	Function Entering and Exiting.
file	function.h [code]
	Function Entering and Exiting.
file	function_modifies.cpp [code]
	Modifies.
file	function_modifies.h [code]
	Modifies.
file	goto_instrument_languages.cpp [code]
	Language Registration.
file	goto_instrument_main.cpp [code]
	Main Module.
file	goto_instrument_parse_options.cpp [code]
	Main Module.
file	goto_instrument_parse_options.h [code]
	Command Line Parsing.
file	goto_program2code.cpp [code]
	Dump Goto-Program as C/C++ Source.
file	goto_program2code.h [code]
	Dump Goto-Program as C/C++ Source.
file	havoc_loops.cpp [code]
	Havoc Loops.
file	havoc_loops.h [code]
	Havoc Loops.
file	horn_encoding.cpp [code]
	Horn-clause Encoding.
file	horn_encoding.h [code]
	Horn-clause Encoding.
file	interrupt.cpp [code]
	Interrupt Instrumentation.
file	interrupt.h [code]
	Interrupt Instrumentation for Goto Programs.
file	k_induction.cpp [code]
	k-induction
file	k_induction.h [code]
	k-induction
file	loop_utils.cpp [code]
	Helper functions for k-induction and loop invariants.
file	loop_utils.h [code]
	Helper functions for k-induction and loop invariants.
file	mmio.cpp [code]
	Memory-mapped I/O Instrumentation for Goto Programs.
file	mmio.h [code]
	Memory-mapped I/O Instrumentation for Goto Programs.
file	model_argc_argv.cpp [code]
	Initialize command line arguments.
file	model_argc_argv.h [code]
	Initialize command line arguments.
file	nondet_static.cpp [code]
	Nondeterministic initialization of certain global scope variables.
file	nondet_static.h [code]
	Nondeterministic initialization of certain global scope variables.
file	nondet_volatile.cpp [code]
	Volatile Variables.
file	nondet_volatile.h [code]
	Volatile Variables.
file	object_id.cpp [code]
	Object Identifiers.
file	object_id.h [code]
	Object Identifiers.
file	points_to.cpp [code]
	Field-sensitive, location-insensitive points-to analysis.
file	points_to.h [code]
	Field-sensitive, location-insensitive points-to analysis.
file	race_check.cpp [code]
	Race Detection for Threaded Goto Programs.
file	race_check.h [code]
	Race Detection for Threaded Goto Programs.
file	reachability_slicer.cpp [code]
	Slicer.
file	reachability_slicer.h [code]
	Slicing.
file	reachability_slicer_class.h [code]
	Goto Program Slicing.
file	remove_function.cpp [code]
	Remove function definition.
file	remove_function.h [code]
	Remove function definition.
file	rw_set.cpp [code]
	Race Detection for Threaded Goto Programs.
file	rw_set.h [code]
	Race Detection for Threaded Goto Programs.
file	show_locations.cpp [code]
	Show program locations.
file	show_locations.h [code]
	Show program locations.
file	skip_loops.cpp [code]
	Skip over selected loops by adding gotos.
file	skip_loops.h [code]
	Skip over selected loops by adding gotos.
file	stack_depth.cpp [code]
	Stack depth checks.
file	stack_depth.h [code]
	Stack depth checks.
file	thread_instrumentation.cpp [code]
file	thread_instrumentation.h [code]
file	undefined_functions.cpp [code]
	Handling of functions without body.
file	undefined_functions.h [code]
	Handling of functions without body.
file	uninitialized.cpp [code]
	Detection for Uninitialized Local Variables.
file	uninitialized.h [code]
	Detection for Uninitialized Local Variables.
file	unwind.cpp [code]
	Loop unwinding.
file	unwind.h [code]
	Loop unwinding.