goto-programs Directory Reference

Directory dependency graph for goto-programs:

Files
	abstract_goto_model.h
	Abstract interface to eager or lazy GOTO models.
	adjust_float_expressions.cpp
	Symbolic Execution.
	adjust_float_expressions.h
	Symbolic Execution.
	cfg.h
	Control Flow Graph.
	class_hierarchy.cpp
	Class Hierarchy.
	class_hierarchy.h
	Class Hierarchy.
	class_identifier.cpp
	Extract class identifier.
	class_identifier.h
	Extract class identifier.
	compute_called_functions.cpp
	Query Called Functions.
	compute_called_functions.h
	Query Called Functions.
	elf_reader.cpp
	Read ELF.
	elf_reader.h
	Read ELF.
	ensure_one_backedge_per_target.cpp
	Ensure one backedge per target.
	ensure_one_backedge_per_target.h
	Ensure one backedge per target.
	goto_check.cpp
	GOTO Programs.
	goto_check.h
	Checks for Errors in C and Java Programs.
	goto_function.cpp
	Goto Function.
	goto_function.h
	Goto Function.
	goto_functions.cpp
	Goto Programs with Functions.
	goto_functions.h
	Goto Programs with Functions.
	goto_inline.cpp
	Function Inlining.
	goto_inline.h
	Function Inlining This gives a number of different interfaces to the function inlining functionality of goto_inlinet.
	goto_inline_class.cpp
	Function Inlining.
	goto_inline_class.h
	Function Inlining This is a class that encapsulates the state and functionality needed to do inline multiple function calls.
	goto_instruction_code.cpp
	Data structures representing instructions in a GOTO program.
	goto_instruction_code.h
	goto_model.h
	Symbol Table + CFG.
	goto_program.cpp
	Program Transformation.
	goto_program.h
	Concrete Goto Program.
	goto_trace.cpp
	Traces of GOTO Programs.
	goto_trace.h
	Traces of GOTO Programs.
	graphml_witness.cpp
	Witnesses for Traces and Proofs.
	graphml_witness.h
	Witnesses for Traces and Proofs.
	initialize_goto_model.cpp
	Get a Goto Program.
	initialize_goto_model.h
	Initialize a Goto Program.
	instrument_preconditions.cpp
	instrument_preconditions.h
	interpreter.cpp
	Interpreter for GOTO Programs.
	interpreter.h
	Interpreter for GOTO Programs.
	interpreter_class.h
	Interpreter for GOTO Programs.
	interpreter_evaluate.cpp
	Interpreter for GOTO Programs.
	json_expr.cpp
	Expressions in JSON.
	json_expr.h
	Expressions in JSON.
	json_goto_trace.cpp
	Traces of GOTO Programs.
	json_goto_trace.h
	Traces of GOTO Programs.
	label_function_pointer_call_sites.cpp
	Label function pointer call sites across a goto model.
	label_function_pointer_call_sites.h
	Label function pointer call sites across a goto model.
	link_goto_model.cpp
	Link Goto Programs.
	link_goto_model.h
	Read Goto Programs.
	loop_ids.cpp
	Loop IDs.
	loop_ids.h
	Loop IDs.
	mm_io.cpp
	Perform Memory-mapped I/O instrumentation.
	mm_io.h
	Perform Memory-mapped I/O instrumentation.
	name_mangler.cpp
	name_mangler.h
	Mangle names of file-local functions to make them unique.
	osx_fat_reader.cpp
	Read Mach-O.
	osx_fat_reader.h
	Read OS X Fat Binaries.
	parameter_assignments.cpp
	Add parameter assignments.
	parameter_assignments.h
	Add parameter assignments.
	pointer_arithmetic.cpp
	pointer_arithmetic.h
	process_goto_program.cpp
	Get a Goto Program.
	process_goto_program.h
	read_bin_goto_object.cpp
	Read goto object files.
	read_bin_goto_object.h
	Read goto object files.
	read_goto_binary.cpp
	Read Goto Programs.
	read_goto_binary.h
	Read Goto Programs.
	rebuild_goto_start_function.cpp
	Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m.
	rebuild_goto_start_function.h
	Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m.
	remove_calls_no_body.cpp
	Remove calls to functions without a body.
	remove_calls_no_body.h
	Remove calls to functions without a body.
	remove_complex.cpp
	Remove 'complex' data type.
	remove_complex.h
	Remove the 'complex' data type by compilation into structs.
	remove_const_function_pointers.cpp
	Goto Programs.
	remove_const_function_pointers.h
	Goto Programs.
	remove_function_pointers.cpp
	Program Transformation.
	remove_function_pointers.h
	Remove Indirect Function Calls.
	remove_returns.cpp
	Replace function returns by assignments to global variables.
	remove_returns.h
	Replace function returns by assignments to global variables.
	remove_skip.cpp
	Program Transformation.
	remove_skip.h
	Program Transformation.
	remove_unreachable.cpp
	Program Transformation.
	remove_unreachable.h
	Program Transformation.
	remove_unused_functions.cpp
	Unused function removal.
	remove_unused_functions.h
	Unused function removal.
	remove_vector.cpp
	Remove 'vector' data type.
	remove_vector.h
	Remove the 'vector' data type by compilation into arrays.
	remove_virtual_functions.cpp
	Remove Virtual Function (Method) Calls.
	remove_virtual_functions.h
	Functions for replacing virtual function call with a static function calls in functions, groups of functions and goto programs.
	resolve_inherited_component.cpp
	resolve_inherited_component.h
	Given a class and a component (either field or method), find the closest parent that defines that component.
	restrict_function_pointers.cpp
	restrict_function_pointers.h
	Given goto functions and a list of function parameters or globals that are function pointers with lists of possible candidates, replace use of these function pointers with calls to the candidate.
	rewrite_rw_ok.cpp
	rewrite_rw_ok.h
	Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.
	rewrite_union.cpp
	Symbolic Execution of ANSI-C.
	rewrite_union.h
	Symbolic Execution.
	safety_checker.cpp
	Safety Checker Interface.
	safety_checker.h
	Safety Checker Interface.
	set_properties.cpp
	Set Properties.
	set_properties.h
	Set the properties to check.
	show_goto_functions.cpp
	Show goto functions.
	show_goto_functions.h
	Show the goto functions.
	show_goto_functions_json.cpp
	Goto Program.
	show_goto_functions_json.h
	Goto Program.
	show_goto_functions_xml.cpp
	Goto Program.
	show_goto_functions_xml.h
	Goto Program.
	show_properties.cpp
	Show Claims.
	show_properties.h
	Show the properties.
	show_symbol_table.cpp
	Show the symbol table.
	show_symbol_table.h
	Show the symbol table.
	slice_global_inits.cpp
	Remove initializations of unused global variables.
	slice_global_inits.h
	Remove initializations of unused global variables.
	string_abstraction.cpp
	String Abstraction.
	string_abstraction.h
	String Abstraction.
	structured_trace_util.cpp
	Utilities for printing location info steps in the trace in a format agnostic way.
	structured_trace_util.h
	Utilities for printing location info steps in the trace in a format agnostic way.
	system_library_symbols.cpp
	Goto Programs.
	system_library_symbols.h
	Goto Programs.
	unwindset.cpp
	unwindset.h
	Loop unwinding.
	validate_code.cpp
	validate_code.h
	validate_goto_model.cpp
	validate_goto_model.h
	vcd_goto_trace.cpp
	Traces of GOTO Programs in VCD (Value Change Dump) Format.
	vcd_goto_trace.h
	Traces of GOTO Programs in VCD (Value Change Dump) Format.
	wp.cpp
	Weakest Preconditions.
	wp.h
	Weakest Preconditions.
	write_goto_binary.cpp
	Write GOTO binaries.
	write_goto_binary.h
	Write GOTO binaries.
	xml_expr.cpp
	Expressions in XML.
	xml_expr.h
	xml_goto_trace.cpp
	Traces of GOTO Programs.
	xml_goto_trace.h
	Traces of GOTO Programs.