goto-programs Directory Reference

Directory dependency graph for goto-programs:

Directories
	abstract-interpretation
	contracts

Files
	add_race_assertions.cpp
	add_race_assertions.h
	add_restrict_assertions.cpp
	add_restrict_assertions.h
	assign_params_as_non_det.cpp
	assign_params_as_non_det.h
	builtin_functions.cpp
	cbmc_adapter.cpp
	cbmc_adapter.h
	dead_store_advisory.h
	dead_store_analysis.cpp
	dead_store_analysis.h
	destructor.cpp
	destructor.h
	exception_globals.cpp
	exception_globals.h
	exception_typeid.cpp
	exception_typeid.h
	format_strings.cpp
	format_strings.h
	frame_enforcer.cpp
	Implementation of the observational frame rule.
	frame_enforcer.h
	Observational frame-rule enforcement for verification.
	goto_atomicity_check.cpp
	goto_atomicity_check.h
	goto_binary_reader.cpp
	goto_binary_reader.h
	goto_cfg.cpp
	goto_cfg.h
	goto_check.cpp
	goto_check.h
	goto_check_excessive_alloc.cpp
	goto_check_excessive_alloc.h
	goto_check_unchecked_return.cpp
	goto_check_unchecked_return.h
	goto_check_uninit_vars.cpp
	goto_check_uninit_vars.h
	goto_contractor.cpp
	goto_contractor.h
	goto_convert.cpp
	goto_convert_class.h
	goto_convert_functions.cpp
	goto_convert_functions.h
	goto_coverage.cpp
	goto_coverage.h
	goto_coverage_rm.cpp
	goto_function.cpp
	goto_function_serialization.cpp
	goto_function_serialization.h
	goto_functions.h
	goto_functions_algorithm.cpp
	goto_functions_algorithm.h
	goto_inline.cpp
	goto_inline.h
	goto_invariant_synthesis.cpp
	goto_invariant_synthesis.h
	goto_k_induction.cpp
	goto_k_induction.h
	goto_loop_invariant.cpp
	goto_loop_invariant.h
	goto_loop_simplify.cpp
	goto_loop_simplify.h
	goto_loops.cpp
	goto_loops.h
	goto_main.cpp
	goto_program.cpp
	goto_program.h
	goto_program_irep.cpp
	goto_program_irep.h
	goto_program_serialization.cpp
	goto_program_serialization.h
	goto_sideeffects.cpp
	goto_termination.cpp
	goto_termination.h
	k_path_spanning.cpp
	k_path_spanning.h
	lift_call_expressions.cpp
	lift_call_expressions.h
	loop_numbers.cpp
	loop_numbers.h
	loop_unroll.cpp
	loop_unroll.h
	loopst.cpp
	loopst.h
	lower_longjmp.cpp
	lower_longjmp.h
	mark_decl_as_non_det.cpp
	mark_decl_as_non_det.h
	property_verdict.cpp
	property_verdict.h
	read_bin_goto_object.cpp
	read_bin_goto_object.h
	read_cbmc_goto_object.cpp
	read_cbmc_goto_object.h
	remove_exceptions.cpp
	remove_exceptions.h
	remove_library_assertions.cpp
	remove_library_assertions.h
	remove_no_op.cpp
	remove_no_op.h
	remove_unreachable.cpp
	remove_unreachable.h
	rw_set.cpp
	rw_set.h
	set_claims.cpp
	set_claims.h
	show_claims.cpp
	show_claims.h
	static_analysis.cpp
	static_analysis.h
	write_goto_binary.cpp
	write_goto_binary.h