Specifics of how the object size lookup is implemented in SMT terms. More...
#include <smt_object_size.h>
Collaboration diagram for smt_object_sizet:Public Types | |
| using | make_applicationt = smt_function_application_termt::factoryt< smt_command_functiont > |
| Function which makes applications of the smt function. More... | |
Public Member Functions | |
| smt_object_sizet () | |
| smt_commandt | make_definition (std::size_t unique_id, smt_termt size) const |
Makes the command to define the resulting size of calling the object size function with unique_id. More... | |
Public Attributes | |
| smt_declare_function_commandt | declaration |
| The command for declaring the object size function. More... | |
| make_applicationt | make_application |
Detailed Description
Specifics of how the object size 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 / size output pairs.
Definition at line 14 of file smt_object_size.h.
Member Typedef Documentation
◆ make_applicationt
| using smt_object_sizet::make_applicationt = smt_function_application_termt::factoryt<smt_command_functiont> |
Function which makes applications of the smt function.
Definition at line 21 of file smt_object_size.h.
Constructor & Destructor Documentation
◆ smt_object_sizet()
| smt_object_sizet::smt_object_sizet | ( | ) |
Definition at line 20 of file smt_object_size.cpp.
Member Function Documentation
◆ make_definition()
| smt_commandt smt_object_sizet::make_definition | ( | std::size_t | unique_id, |
| smt_termt | size | ||
| ) | const |
Makes the command to define the resulting size of calling the object size function with unique_id.
Definition at line 26 of file smt_object_size.cpp.
Member Data Documentation
◆ declaration
| smt_declare_function_commandt smt_object_sizet::declaration |
The command for declaring the object size function.
The defined function takes a bit vector encoded unique object identifier and returns
Definition at line 19 of file smt_object_size.h.
◆ make_application
| make_applicationt smt_object_sizet::make_application |
Definition at line 23 of file smt_object_size.h.
The documentation for this struct was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/smt_object_size.h
- /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/smt_object_size.cpp
