Directory dependency graph for goto-checker:

Files
file	all_properties_verifier.h [code]
	Goto Verifier for Verifying all Properties.

file	all_properties_verifier_with_fault_localization.h [code]
	Goto verifier for verifying all properties that stores traces and localizes faults.

file	all_properties_verifier_with_trace_storage.h [code]
	Goto verifier for verifying all properties that stores traces.

file	bmc_util.cpp [code]
	Bounded Model Checking Utilities.

file	bmc_util.h [code]
	Bounded Model Checking Utilities.

file	counterexample_beautification.cpp [code]
	Counterexample Beautification using Incremental SAT.

file	counterexample_beautification.h [code]
	Counterexample Beautification.

file	cover_goals_report_util.cpp [code]
	Cover Goals Reporting Utilities.

file	cover_goals_report_util.h [code]
	Cover Goals Reporting Utilities.

file	cover_goals_verifier_with_trace_storage.h [code]
	Goto verifier for covering goals that stores traces.

file	fault_localization_provider.h [code]
	Interface for Goto Checkers to provide Fault Localization.

file	goto_symex_fault_localizer.cpp [code]
	Fault Localization for Goto Symex.

file	goto_symex_fault_localizer.h [code]
	Fault Localization for Goto Symex.

file	goto_symex_property_decider.cpp [code]
	Property Decider for Goto-Symex.

file	goto_symex_property_decider.h [code]
	Property Decider for Goto-Symex.

file	goto_trace_provider.h [code]
	Interface for returning Goto Traces from Goto Checkers.

file	goto_trace_storage.cpp [code]
	Goto Trace Storage.

file	goto_trace_storage.h [code]
	Goto Trace Storage.

file	goto_verifier.cpp [code]
	Goto Verifier Interface.

file	goto_verifier.h [code]
	Goto Verifier Interface.

file	incremental_goto_checker.cpp [code]
	Incremental Goto Checker Interface.

file	incremental_goto_checker.h [code]
	Incremental Goto Checker Interface.

file	multi_path_symex_checker.cpp [code]
	Goto Checker using Bounded Model Checking.

file	multi_path_symex_checker.h [code]
	Goto Checker using Multi-Path Symbolic Execution.

file	multi_path_symex_only_checker.cpp [code]
	Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)

file	multi_path_symex_only_checker.h [code]
	Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)

file	properties.cpp [code]
	Properties.

file	properties.h [code]
	Properties.

file	report_util.cpp [code]
	Bounded Model Checking Utilities.

file	report_util.h [code]
	Bounded Model Checking Utilities.

file	single_loop_incremental_symex_checker.cpp [code]
	Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.

file	single_loop_incremental_symex_checker.h [code]
	Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.

file	single_path_symex_checker.cpp [code]
	Goto Checker using Single Path Symbolic Execution.

file	single_path_symex_checker.h [code]
	Goto Checker using Single Path Symbolic Execution.

file	single_path_symex_only_checker.cpp [code]
	Goto Checker using Single Path Symbolic Execution only.

file	single_path_symex_only_checker.h [code]
	Goto Checker using Single Path Symbolic Execution only.

file	solver_factory.cpp [code]
	Solver Factory.

file	solver_factory.h [code]
	Solver Factory.

file	stop_on_fail_verifier.h [code]
	Goto Verifier for stopping at the first failing property.

file	stop_on_fail_verifier_with_fault_localization.h [code]
	Goto Verifier for stopping at the first failing property and localizing the fault.

file	symex_bmc.cpp [code]
	Bounded Model Checking for ANSI-C.

file	symex_bmc.h [code]
	Bounded Model Checking for ANSI-C.

file	symex_bmc_incremental_one_loop.cpp [code]

file	symex_bmc_incremental_one_loop.h [code]

file	symex_coverage.cpp [code]
	Record and print code coverage of symbolic execution.

file	symex_coverage.h [code]
	Record and print code coverage of symbolic execution.

file	witness_provider.h [code]
	Interface for outputting GraphML Witnesses for Goto Checkers.

Files