incremental_goto_checkert::resultt Struct Reference

#include <incremental_goto_checker.h>

Collaboration diagram for incremental_goto_checkert::resultt:

Public Types
enum class	progresst { FOUND_FAIL , DONE }

Public Member Functions
	resultt ()=delete
	resultt (progresst)

Public Attributes
progresst	progress
std::unordered_set< irep_idt >	updated_properties
	Changed properties since the last call to incremental_goto_checkert::operator() More...

Detailed Description

Definition at line 42 of file incremental_goto_checker.h.

Member Enumeration Documentation

progresst

enum incremental_goto_checkert::resultt::progresst

strong

Enumerator
FOUND_FAIL	The goto checker may be able to find another FAILed property if operator() is called again.
DONE	The goto checker has returned all results for the given set of properties.

Definition at line 44 of file incremental_goto_checker.h.

Constructor & Destructor Documentation

resultt() [1/2]

incremental_goto_checkert::resultt::resultt ( )

delete

resultt() [2/2]

incremental_goto_checkert::resultt::resultt ( resultt::progresst  progress )

explicit

Definition at line 25 of file incremental_goto_checker.cpp.

Member Data Documentation

progress

progresst incremental_goto_checkert::resultt::progress

Definition at line 54 of file incremental_goto_checker.h.

updated_properties

std::unordered_set<irep_idt> incremental_goto_checkert::resultt::updated_properties

Changed properties since the last call to incremental_goto_checkert::operator()

Definition at line 61 of file incremental_goto_checker.h.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-checker/incremental_goto_checker.h
• /home/runner/work/cbmc/cbmc/src/goto-checker/incremental_goto_checker.cpp