CBMC
smt_is_dynamic_objectt Struct Referencefinal

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. More...
 

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. More...
 

Public Attributes

smt_declare_function_commandt declaration
 The command for declaring the is_dynamic_object function. More...
 
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

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: