goto-instrument Directory Reference

Directory dependency graph for goto-instrument:

Directories
	accelerate
	contracts
	wmm

Files
	aggressive_slicer.cpp
	Aggressive program slicer.
	aggressive_slicer.h
	Aggressive slicer Consider the control flow graph of the goto program and a criterion description of aggressive slicer here.
	alignment_checks.cpp
	Alignment Checks.
	alignment_checks.h
	Alignment Checks.
	branch.cpp
	Branch Instrumentation.
	branch.h
	Branch Instrumentation.
	call_sequences.cpp
	Printing function call sequences for Ofer.
	call_sequences.h
	Memory-mapped I/O Instrumentation for Goto Programs.
	concurrency.cpp
	Encoding for Threaded Goto Programs.
	concurrency.h
	Encoding for Threaded Goto Programs.
	count_eloc.cpp
	Count effective lines of code.
	count_eloc.h
	Count effective lines of code.
	cover.cpp
	Coverage Instrumentation.
	cover.h
	Coverage Instrumentation.
	cover_basic_blocks.cpp
	Basic blocks detection for Coverage Instrumentation.
	cover_basic_blocks.h
	Basic blocks detection for Coverage Instrumentation.
	cover_filter.cpp
	Filters for the Coverage Instrumentation.
	cover_filter.h
	Filters for the Coverage Instrumentation.
	cover_instrument.h
	Coverage Instrumentation.
	cover_instrument_assume.cpp
	Author: Diffblue Ltd.
	cover_instrument_branch.cpp
	Coverage Instrumentation for Branches.
	cover_instrument_condition.cpp
	Coverage Instrumentation for Conditions.
	cover_instrument_decision.cpp
	Coverage Instrumentation for Decisions.
	cover_instrument_location.cpp
	Coverage Instrumentation for Location, i.e.
	cover_instrument_mcdc.cpp
	Coverage Instrumentation for MC/DC.
	cover_instrument_other.cpp
	Further coverage instrumentations.
	cover_util.cpp
	Coverage Instrumentation Utilities.
	cover_util.h
	Coverage Instrumentation Utilities.
	document_properties.cpp
	Subgoal Documentation.
	document_properties.h
	Documentation of Properties.
	dot.cpp
	Dump Goto-Program as DOT Graph.
	dot.h
	Dump Goto-Program as DOT Graph.
	dump_c.cpp
	Dump Goto-Program as C/C++ Source.
	dump_c.h
	Dump C from Goto Program.
	dump_c_class.h
	Dump Goto-Program as C/C++ Source.
	full_slicer.cpp
	Slicing.
	full_slicer.h
	Slicing.
	full_slicer_class.h
	Goto Program Slicing.
	function.cpp
	Function Entering and Exiting.
	function.h
	Function Entering and Exiting.
	function_assigns.cpp
	Compute objects assigned to in a function.
	function_assigns.h
	Compute objects assigned to in a function.
	generate_function_bodies.cpp
	generate_function_bodies.h
	goto_instrument_languages.cpp
	Language Registration.
	goto_instrument_main.cpp
	Main Module.
	goto_instrument_parse_options.cpp
	Main Module.
	goto_instrument_parse_options.h
	Command Line Parsing.
	goto_program2code.cpp
	Dump Goto-Program as C/C++ Source.
	goto_program2code.h
	Dump Goto-Program as C/C++ Source.
	havoc_loops.cpp
	Havoc Loops.
	havoc_loops.h
	Havoc Loops.
	havoc_utils.cpp
	Utilities for building havoc code for expressions.
	havoc_utils.h
	Utilities for building havoc code for expressions.
	horn_encoding.cpp
	Horn-clause Encoding.
	horn_encoding.h
	Horn-clause Encoding.
	insert_final_assert_false.cpp
	Insert final assert false into a function.
	insert_final_assert_false.h
	Insert final assert false into a function.
	interrupt.cpp
	Interrupt Instrumentation.
	interrupt.h
	Interrupt Instrumentation for Goto Programs.
	k_induction.cpp
	k-induction
	k_induction.h
	k-induction
	loop_utils.cpp
	Helper functions for k-induction and loop invariants.
	loop_utils.h
	Helper functions for k-induction and loop invariants.
	mmio.cpp
	Memory-mapped I/O Instrumentation for Goto Programs.
	mmio.h
	Memory-mapped I/O Instrumentation for Goto Programs.
	model_argc_argv.cpp
	Initialize command line arguments.
	model_argc_argv.h
	Initialize command line arguments.
	nondet_static.cpp
	Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields) and internal variables (such as CPROVER and symex variables, language specific internal variables).
	nondet_static.h
	Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields) and internal variables (such as CPROVER and symex variables, language specific internal variables).
	nondet_volatile.cpp
	Volatile Variables.
	nondet_volatile.h
	Volatile Variables.
	object_id.cpp
	Object Identifiers.
	object_id.h
	Object Identifiers.
	points_to.cpp
	Field-sensitive, location-insensitive points-to analysis.
	points_to.h
	Field-sensitive, location-insensitive points-to analysis.
	race_check.cpp
	Race Detection for Threaded Goto Programs.
	race_check.h
	Race Detection for Threaded Goto Programs.
	reachability_slicer.cpp
	Reachability Slicer Consider the control flow graph of the goto program and a criterion, and remove the parts of the graph from which the criterion is not reachable (and possibly, depending on the parameters, keep those that can be reached from the criterion).
	reachability_slicer.h
	Slicing.
	reachability_slicer_class.h
	Goto Program Slicing.
	remove_function.cpp
	Remove function definition.
	remove_function.h
	Remove function definition.
	replace_calls.cpp
	Replace calls Replaces calls to given functions with calls to other given functions.
	replace_calls.h
	Replace calls to given functions with calls to other given functions.
	rw_set.cpp
	Race Detection for Threaded Goto Programs.
	rw_set.h
	Race Detection for Threaded Goto Programs.
	show_locations.cpp
	Show program locations.
	show_locations.h
	Show program locations.
	skip_loops.cpp
	Skip over selected loops by adding gotos.
	skip_loops.h
	Skip over selected loops by adding gotos.
	source_lines.cpp
	Set of source code lines contributing to a basic block.
	source_lines.h
	Set of source code lines contributing to a basic block.
	splice_call.cpp
	Prepend a nullary call to another function useful for context/ environment setting in arbitrary nodes.
	splice_call.h
	Harnessing for goto functions.
	stack_depth.cpp
	Stack depth checks.
	stack_depth.h
	Stack depth checks.
	thread_instrumentation.cpp
	thread_instrumentation.h
	undefined_functions.cpp
	Handling of functions without body.
	undefined_functions.h
	Handling of functions without body.
	uninitialized.cpp
	Detection for Uninitialized Local Variables.
	uninitialized.h
	Detection for Uninitialized Local Variables.
	unwind.cpp
	Loop unwinding.
	unwind.h
	Loop unwinding.
	value_set_fi_fp_removal.cpp
	value_set_fi_fp_removal.h
	flow insensitive value set function pointer removal