CBMC
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  fatal_assertions.cpp [code]
 Fatal Assertions.
 
file  fatal_assertions.h [code]
 Fatal Assertions.
 
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.