goto-checker Directory Reference

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.