CBMC
Public Member Functions | Protected Attributes | List of all members
all_properties_verifiert< incremental_goto_checkerT > Class Template Reference

#include <all_properties_verifier.h>

+ Inheritance diagram for all_properties_verifiert< incremental_goto_checkerT >:
+ Collaboration diagram for all_properties_verifiert< incremental_goto_checkerT >:

Public Member Functions

 all_properties_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
 
std::size_t iterations = 1
 
- 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 all_properties_verifiert< incremental_goto_checkerT >

Definition at line 22 of file all_properties_verifier.h.

Constructor & Destructor Documentation

◆ all_properties_verifiert()

template<class incremental_goto_checkerT >
all_properties_verifiert< incremental_goto_checkerT >::all_properties_verifiert ( const optionst &  options,
ui_message_handlert &  ui_message_handler,
abstract_goto_modelt &  goto_model 
)
inline

Definition at line 25 of file all_properties_verifier.h.

Member Function Documentation

◆ operator()()

template<class incremental_goto_checkerT >
resultt all_properties_verifiert< incremental_goto_checkerT >::operator() ( )
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 all_properties_verifier.h.

◆ report()

template<class incremental_goto_checkerT >
void all_properties_verifiert< incremental_goto_checkerT >::report ( )
inlineoverridevirtual

Report results.

Implements goto_verifiert.

Definition at line 47 of file all_properties_verifier.h.

Member Data Documentation

◆ goto_model

template<class incremental_goto_checkerT >
abstract_goto_modelt& all_properties_verifiert< incremental_goto_checkerT >::goto_model
protected

Definition at line 54 of file all_properties_verifier.h.

◆ incremental_goto_checker

template<class incremental_goto_checkerT >
incremental_goto_checkerT all_properties_verifiert< incremental_goto_checkerT >::incremental_goto_checker
protected

Definition at line 55 of file all_properties_verifier.h.

◆ iterations

template<class incremental_goto_checkerT >
std::size_t all_properties_verifiert< incremental_goto_checkerT >::iterations = 1
protected

Definition at line 56 of file all_properties_verifier.h.

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