CBMC
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:

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: