goto-programs Directory Reference

Directory dependency graph for goto-programs:

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