Specifics of how the dynamic object status lookup is implemented in SMT terms. More...
#include <smt_is_dynamic_object.h>
Collaboration diagram for smt_is_dynamic_objectt:Public Types | |
| using | make_applicationt = smt_function_application_termt::factoryt< smt_command_functiont > |
| Function which makes applications of the smt function. | |
Public Member Functions | |
| smt_is_dynamic_objectt () | |
| smt_commandt | make_definition (std::size_t unique_id, bool is_dynamic_object) const |
Makes the command to define the resulting is_dynamic_object status for calls to the is_dynamic_object function with unique_id. | |
Public Attributes | |
| smt_declare_function_commandt | declaration |
| The command for declaring the is_dynamic_object function. | |
| make_applicationt | make_application |
Detailed Description
Specifics of how the dynamic object status lookup is implemented in SMT terms.
This uses an uninterpreted function as a lookup. Because these functions must return the same result for a specific input, we can just assert the value of the function output for the inputs where we want to define specific ID input / dynamic_object output pairs.
Definition at line 14 of file smt_is_dynamic_object.h.
Member Typedef Documentation
◆ make_applicationt
| using smt_is_dynamic_objectt::make_applicationt = smt_function_application_termt::factoryt<smt_command_functiont> |
Function which makes applications of the smt function.
Definition at line 22 of file smt_is_dynamic_object.h.
Constructor & Destructor Documentation
◆ smt_is_dynamic_objectt()
| smt_is_dynamic_objectt::smt_is_dynamic_objectt | ( | ) |
Definition at line 17 of file smt_is_dynamic_object.cpp.
Member Function Documentation
◆ make_definition()
| smt_commandt smt_is_dynamic_objectt::make_definition | ( | std::size_t | unique_id, |
| bool | is_dynamic_object | ||
| ) | const |
Makes the command to define the resulting is_dynamic_object status for calls to the is_dynamic_object function with unique_id.
Definition at line 23 of file smt_is_dynamic_object.cpp.
Member Data Documentation
◆ declaration
| smt_declare_function_commandt smt_is_dynamic_objectt::declaration |
The command for declaring the is_dynamic_object function.
The defined function takes a bit vector encoded unique object identifier and returns a boolean value.
Definition at line 20 of file smt_is_dynamic_object.h.
◆ make_application
| make_applicationt smt_is_dynamic_objectt::make_application |
Definition at line 24 of file smt_is_dynamic_object.h.
The documentation for this struct was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/smt_is_dynamic_object.h
- /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/smt_is_dynamic_object.cpp
