goto-checker Directory Reference

Directory dependency graph for goto-checker:

Files
	all_properties_verifier.h
	Goto Verifier for Verifying all Properties.
	all_properties_verifier_with_fault_localization.h
	Goto verifier for verifying all properties that stores traces and localizes faults.
	all_properties_verifier_with_trace_storage.h
	Goto verifier for verifying all properties that stores traces.
	bmc_util.cpp
	Bounded Model Checking Utilities.
	bmc_util.h
	Bounded Model Checking Utilities.
	counterexample_beautification.cpp
	Counterexample Beautification using Incremental SAT.
	counterexample_beautification.h
	Counterexample Beautification.
	cover_goals_report_util.cpp
	Cover Goals Reporting Utilities.
	cover_goals_report_util.h
	Cover Goals Reporting Utilities.
	cover_goals_verifier_with_trace_storage.h
	Goto verifier for covering goals that stores traces.
	fatal_assertions.cpp
	Fatal Assertions.
	fatal_assertions.h
	Fatal Assertions.
	fault_localization_provider.h
	Interface for Goto Checkers to provide Fault Localization.
	goto_symex_fault_localizer.cpp
	Fault Localization for Goto Symex.
	goto_symex_fault_localizer.h
	Fault Localization for Goto Symex.
	goto_symex_property_decider.cpp
	Property Decider for Goto-Symex.
	goto_symex_property_decider.h
	Property Decider for Goto-Symex.
	goto_trace_provider.h
	Interface for returning Goto Traces from Goto Checkers.
	goto_trace_storage.cpp
	Goto Trace Storage.
	goto_trace_storage.h
	Goto Trace Storage.
	goto_verifier.cpp
	Goto Verifier Interface.
	goto_verifier.h
	Goto Verifier Interface.
	incremental_goto_checker.cpp
	Incremental Goto Checker Interface.
	incremental_goto_checker.h
	Incremental Goto Checker Interface.
	multi_path_symex_checker.cpp
	Goto Checker using Bounded Model Checking.
	multi_path_symex_checker.h
	Goto Checker using Multi-Path Symbolic Execution.
	multi_path_symex_only_checker.cpp
	Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
	multi_path_symex_only_checker.h
	Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
	properties.cpp
	Properties.
	properties.h
	Properties.
	report_util.cpp
	Bounded Model Checking Utilities.
	report_util.h
	Bounded Model Checking Utilities.
	single_loop_incremental_symex_checker.cpp
	Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
	single_loop_incremental_symex_checker.h
	Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
	single_path_symex_checker.cpp
	Goto Checker using Single Path Symbolic Execution.
	single_path_symex_checker.h
	Goto Checker using Single Path Symbolic Execution.
	single_path_symex_only_checker.cpp
	Goto Checker using Single Path Symbolic Execution only.
	single_path_symex_only_checker.h
	Goto Checker using Single Path Symbolic Execution only.
	solver_factory.cpp
	Solver Factory.
	solver_factory.h
	Solver Factory.
	stop_on_fail_verifier.h
	Goto Verifier for stopping at the first failing property.
	stop_on_fail_verifier_with_fault_localization.h
	Goto Verifier for stopping at the first failing property and localizing the fault.
	symex_bmc.cpp
	Bounded Model Checking for ANSI-C.
	symex_bmc.h
	Bounded Model Checking for ANSI-C.
	symex_bmc_incremental_one_loop.cpp
	symex_bmc_incremental_one_loop.h
	symex_coverage.cpp
	Record and print code coverage of symbolic execution.
	symex_coverage.h
	Record and print code coverage of symbolic execution.
	witness_provider.h
	Interface for outputting GraphML Witnesses for Goto Checkers.