goto_symex_property_decidert::goalt Struct Reference
#include <goto_symex_property_decider.h>
Collaboration diagram for goto_symex_property_decidert::goalt:Public Member Functions | |
| exprt | as_expr () const |
Public Attributes | |
| std::vector< symex_target_equationt::SSA_stepst::iterator > | instances |
| A property holds if all instances of it are true. More... | |
| exprt | condition |
| The goal variable. More... | |
Detailed Description
Definition at line 74 of file goto_symex_property_decider.h.
Member Function Documentation
◆ as_expr()
| exprt goto_symex_property_decidert::goalt::as_expr | ( | ) | const |
Definition at line 33 of file goto_symex_property_decider.cpp.
Member Data Documentation
◆ condition
| exprt goto_symex_property_decidert::goalt::condition |
The goal variable.
Definition at line 80 of file goto_symex_property_decider.h.
◆ instances
| std::vector<symex_target_equationt::SSA_stepst::iterator> goto_symex_property_decidert::goalt::instances |
A property holds if all instances of it are true.
Definition at line 77 of file goto_symex_property_decider.h.
The documentation for this struct was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-checker/goto_symex_property_decider.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-checker/goto_symex_property_decider.cpp
