CBMC
Loading...
Searching...
No Matches
all_properties_verifier_with_trace_storaget< incremental_goto_checkerT > Class Template Reference

#include <all_properties_verifier_with_trace_storage.h>

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

Public Member Functions

 all_properties_verifier_with_trace_storaget (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
 
resultt operator() () override
 Check whether all properties hold.
 
void report () override
 Report results.
 
const goto_trace_storagetget_traces () const
 
- Public Member Functions inherited from goto_verifiert
 goto_verifiert ()=delete
 
 goto_verifiert (const goto_verifiert &)=delete
 
virtual ~goto_verifiert ()=default
 
const propertiestget_properties ()
 Returns the properties.
 

Protected Attributes

abstract_goto_modeltgoto_model
 
incremental_goto_checkerT incremental_goto_checker
 
std::size_t iterations = 1
 
goto_trace_storaget traces
 
- Protected Attributes inherited from goto_verifiert
const optionstoptions
 
ui_message_handlertui_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_verifier_with_trace_storaget< incremental_goto_checkerT >

Definition at line 26 of file all_properties_verifier_with_trace_storage.h.

Constructor & Destructor Documentation

◆ all_properties_verifier_with_trace_storaget()

Member Function Documentation

◆ get_traces()

◆ operator()()

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 41 of file all_properties_verifier_with_trace_storage.h.

◆ report()

Report results.

Implements goto_verifiert.

Definition at line 72 of file all_properties_verifier_with_trace_storage.h.

Member Data Documentation

◆ goto_model

◆ incremental_goto_checker

◆ iterations

◆ traces


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