An implementation of incremental_goto_checkert provides functionality for checking a set of properties and returning counterexamples one by one to the caller.
More...
#include <incremental_goto_checker.h>
Inheritance diagram for incremental_goto_checkert: Collaboration diagram for incremental_goto_checkert:Classes | |
| struct | resultt |
Public Member Functions | |
| incremental_goto_checkert ()=delete | |
| incremental_goto_checkert (const incremental_goto_checkert &)=delete | |
| virtual | ~incremental_goto_checkert ()=default |
| virtual resultt | operator() (propertiest &properties)=0 |
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert hold. More... | |
| virtual void | report () |
| Additional reporting that may result from the underlying solver, no-op by default. More... | |
Protected Member Functions | |
| incremental_goto_checkert (const optionst &, ui_message_handlert &) | |
Protected Attributes | |
| const optionst & | options |
| ui_message_handlert & | ui_message_handler |
| messaget | log |
Detailed Description
An implementation of incremental_goto_checkert provides functionality for checking a set of properties and returning counterexamples one by one to the caller.
An implementation of incremental_goto_checkert is responsible for maintaining the state of the analysis that it performs (e.g. goto-symex, solver, etc). An implementation of incremental_goto_checkert is not responsible for maintaining outcomes (e.g. property status, counterexamples, etc). However, an implementation may restrict the sets of properties it is asked to check on repeated invocations of its operator (e.g. only sequences of subsets of properties) to optimize the incremental algorithm it uses.
Definition at line 35 of file incremental_goto_checker.h.
Constructor & Destructor Documentation
◆ incremental_goto_checkert() [1/3]
|
delete |
◆ incremental_goto_checkert() [2/3]
|
delete |
◆ ~incremental_goto_checkert()
|
virtualdefault |
◆ incremental_goto_checkert() [3/3]
|
protected |
Definition at line 16 of file incremental_goto_checker.cpp.
Member Function Documentation
◆ operator()()
|
pure virtual |
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert hold.
- Parameters
-
[out] properties Properties updated to whether their status have been determined. Newly discovered properties are added.
- Returns
- whether the goto checker found a violated property (FOUND_FAIL) or whether it is DONE with the given properties, together with the properties whose status changed since the last call to operator(). After returning DONE, another call to operator() with the same properties will return DONE and leave the properties' status unchanged. If there is a property with status FAIL then its counterexample can be retrieved by calling
build_error_tracebefore any subsequent call to operator().incremental_goto_checkertderivatives shall be implemented in a way such that repeated calls to operator() shall return when the next FAILed property has been found until eventually it does not find any failing properties any more.
Implemented in single_path_symex_only_checkert, single_path_symex_checkert, single_loop_incremental_symex_checkert, multi_path_symex_only_checkert, and multi_path_symex_checkert.
◆ report()
|
inlinevirtual |
Additional reporting that may result from the underlying solver, no-op by default.
Reimplemented in multi_path_symex_checkert.
Definition at line 84 of file incremental_goto_checker.h.
Member Data Documentation
◆ log
|
protected |
Definition at line 93 of file incremental_goto_checker.h.
◆ options
|
protected |
Definition at line 91 of file incremental_goto_checker.h.
◆ ui_message_handler
|
protected |
Definition at line 92 of file incremental_goto_checker.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-checker/incremental_goto_checker.h
- /home/runner/work/cbmc/cbmc/src/goto-checker/incremental_goto_checker.cpp
