Loading...

Searching...

No Matches

Public Member Functions | Public Attributes | List of all members

static_verifier_resultt Class Reference

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:

[フレーム]

[legend]

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