The result of verifying a single assertion As well as the status of the assertion (see above), it also contains the location (source_location and function_id) and the set of histories in which the assertion is unknown or false, so that more detailed post-processing or error output can be done. More...
#include <static_verifier.h>
Collaboration diagram for static_verifier_resultt:Public Member Functions | |
| static_verifier_resultt (const ai_baset &ai, goto_programt::const_targett assert_location, irep_idt func_id, const namespacet &ns) | |
| jsont | output_json (void) const |
| xmlt | output_xml (void) const |
Public Attributes | |
| ai_verifier_statust | status |
| source_locationt | source_location |
| irep_idt | function_id |
| ai_history_baset::trace_sett | unknown_histories |
| ai_history_baset::trace_sett | false_histories |
Detailed Description
The result of verifying a single assertion As well as the status of the assertion (see above), it also contains the location (source_location and function_id) and the set of histories in which the assertion is unknown or false, so that more detailed post-processing or error output can be done.
Definition at line 66 of file static_verifier.h.
Constructor & Destructor Documentation
◆ static_verifier_resultt()
| static_verifier_resultt::static_verifier_resultt | ( | const ai_baset & | ai, |
| goto_programt::const_targett | assert_location, | ||
| irep_idt | func_id, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 111 of file static_verifier.cpp.
Member Function Documentation
◆ output_json()
| jsont static_verifier_resultt::output_json | ( | void | ) | const |
Definition at line 39 of file static_verifier.cpp.
◆ output_xml()
| xmlt static_verifier_resultt::output_xml | ( | void | ) | const |
Definition at line 57 of file static_verifier.cpp.
Member Data Documentation
◆ false_histories
| ai_history_baset::trace_sett static_verifier_resultt::false_histories |
Definition at line 73 of file static_verifier.h.
◆ function_id
| irep_idt static_verifier_resultt::function_id |
Definition at line 71 of file static_verifier.h.
◆ source_location
| source_locationt static_verifier_resultt::source_location |
Definition at line 70 of file static_verifier.h.
◆ status
| ai_verifier_statust static_verifier_resultt::status |
Definition at line 69 of file static_verifier.h.
◆ unknown_histories
| ai_history_baset::trace_sett static_verifier_resultt::unknown_histories |
Definition at line 72 of file static_verifier.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-analyzer/static_verifier.h
- /home/runner/work/cbmc/cbmc/src/goto-analyzer/static_verifier.cpp
