cprover
Loading...
Searching...
No Matches
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.