CBMC
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
goto_verifiert Class Referenceabstract

An implementation of goto_verifiert checks all properties in a goto model. More...

#include <goto_verifier.h>

+ Inheritance diagram for goto_verifiert:
+ Collaboration diagram for goto_verifiert:

Public Member Functions

 goto_verifiert ()=delete
 
 goto_verifiert (const goto_verifiert &)=delete
 
virtual ~goto_verifiert ()=default
 
virtual resultt operator() ()=0
 Check whether all properties hold. More...
 
virtual void report ()=0
 Report results. More...
 
const propertiest & get_properties ()
 Returns the properties. More...
 

Protected Member Functions

 goto_verifiert (const optionst &, ui_message_handlert &)
 

Protected Attributes

const optionst & options
 
ui_message_handlert & ui_message_handler
 
messaget log
 
propertiest properties
 

Detailed Description

An implementation of goto_verifiert checks all properties in a goto model.

It typically uses, but doesn't have to use, an incremental_goto_checkert to iteratively determine the verification status of each property.

Definition at line 26 of file goto_verifier.h.

Constructor & Destructor Documentation

◆ goto_verifiert() [1/3]

goto_verifiert::goto_verifiert ( )
delete

◆ goto_verifiert() [2/3]

goto_verifiert::goto_verifiert ( const goto_verifiert &  )
delete

◆ ~goto_verifiert()

virtual goto_verifiert::~goto_verifiert ( )
virtualdefault

◆ goto_verifiert() [3/3]

goto_verifiert::goto_verifiert ( const optionst &  _options,
ui_message_handlert &  ui_message_handler 
)
protected

Definition at line 16 of file goto_verifier.cpp.

Member Function Documentation

◆ get_properties()

const propertiest& goto_verifiert::get_properties ( )
inline

Returns the properties.

Definition at line 45 of file goto_verifier.h.

◆ operator()()

virtual resultt goto_verifiert::operator() ( )
pure virtual

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.

Implemented in all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >, all_properties_verifier_with_trace_storaget< incremental_goto_checkerT >, cover_goals_verifier_with_trace_storaget< incremental_goto_checkerT >, stop_on_fail_verifier_with_fault_localizationt< incremental_goto_checkerT >, all_properties_verifiert< incremental_goto_checkerT >, and stop_on_fail_verifiert< incremental_goto_checkerT >.

◆ report()

virtual void goto_verifiert::report ( )
pure virtual

Report results.

Implemented in all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >, all_properties_verifier_with_trace_storaget< incremental_goto_checkerT >, cover_goals_verifier_with_trace_storaget< incremental_goto_checkerT >, all_properties_verifiert< incremental_goto_checkerT >, stop_on_fail_verifier_with_fault_localizationt< incremental_goto_checkerT >, and stop_on_fail_verifiert< incremental_goto_checkerT >.

Member Data Documentation

◆ log

messaget goto_verifiert::log
protected

Definition at line 55 of file goto_verifier.h.

◆ options

const optionst& goto_verifiert::options
protected

Definition at line 53 of file goto_verifier.h.

◆ properties

propertiest goto_verifiert::properties
protected

Definition at line 56 of file goto_verifier.h.

◆ ui_message_handler

ui_message_handlert& goto_verifiert::ui_message_handler
protected

Definition at line 54 of file goto_verifier.h.

The documentation for this class was generated from the following files: