stop_on_fail_verifiert< incremental_goto_checkerT > Class Template Reference
Stops when the first failing property is found. More...
#include <stop_on_fail_verifier.h>
Inheritance diagram for stop_on_fail_verifiert< incremental_goto_checkerT >: Collaboration diagram for stop_on_fail_verifiert< incremental_goto_checkerT >:Public Member Functions | |
| stop_on_fail_verifiert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) | |
| resultt | operator() () override |
| Check whether all properties hold. More... | |
| void | report () override |
| Report results. More... | |
| Public Member Functions inherited from goto_verifiert | |
| goto_verifiert ()=delete | |
| goto_verifiert (const goto_verifiert &)=delete | |
| virtual | ~goto_verifiert ()=default |
| const propertiest & | get_properties () |
| Returns the properties. More... | |
Protected Attributes | |
| abstract_goto_modelt & | goto_model |
| incremental_goto_checkerT | incremental_goto_checker |
| Protected Attributes inherited from goto_verifiert | |
| const optionst & | options |
| ui_message_handlert & | ui_message_handler |
| messaget | log |
| propertiest | properties |
Additional Inherited Members | |
| Protected Member Functions inherited from goto_verifiert | |
| goto_verifiert (const optionst &, ui_message_handlert &) | |
Detailed Description
template<class incremental_goto_checkerT>
class stop_on_fail_verifiert< incremental_goto_checkerT >
Stops when the first failing property is found.
Requires an incremental goto checker that is a goto_trace_providert and witness_providert.
Definition at line 22 of file stop_on_fail_verifier.h.
Constructor & Destructor Documentation
◆ stop_on_fail_verifiert()
template<class incremental_goto_checkerT >
|
inline |
Definition at line 25 of file stop_on_fail_verifier.h.
Member Function Documentation
◆ operator()()
template<class incremental_goto_checkerT >
|
inlineoverridevirtual |
Check whether all properties hold.
- Returns
- PASS if all properties are PASS, FAIL if at least one property is FAIL and no property is ERROR, UNKNOWN if no property is FAIL or ERROR and at least one property is UNKNOWN, ERROR if at least one property is error.
Implements goto_verifiert.
Definition at line 36 of file stop_on_fail_verifier.h.
◆ report()
template<class incremental_goto_checkerT >
|
inlineoverridevirtual |
Member Data Documentation
◆ goto_model
template<class incremental_goto_checkerT >
|
protected |
Definition at line 78 of file stop_on_fail_verifier.h.
◆ incremental_goto_checker
template<class incremental_goto_checkerT >
|
protected |
Definition at line 79 of file stop_on_fail_verifier.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-checker/stop_on_fail_verifier.h
