CBMC
Public Member Functions | Public Attributes | List of all members
reference_allocationt Class Reference

Allocation code which contains a reference. More...

#include <code_with_references.h>

+ Inheritance diagram for reference_allocationt:
+ Collaboration diagram for reference_allocationt:

Public Member Functions

 reference_allocationt (std::string reference_id, source_locationt loc)
 
code_blockt to_code (reference_substitutiont &references) const override
 
- Public Member Functions inherited from code_with_referencest
virtual ~code_with_referencest ()=default
 

Public Attributes

std::string reference_id
 
source_locationt loc
 

Additional Inherited Members

- Public Types inherited from code_with_referencest
using reference_substitutiont = std::function< const object_creation_referencet &(const std::string &)>
 

Detailed Description

Allocation code which contains a reference.

The generated code will be of the form: 

    array_length = nondet(int)
    assume(array_length >= 0)
    array_expr = new array_type[array_length];

Where array_length and array_expr are given by the reference substitution function.

Definition at line 76 of file code_with_references.h.

Constructor & Destructor Documentation

◆ reference_allocationt()

reference_allocationt::reference_allocationt ( std::string  reference_id,
source_locationt  loc 
)
inline

Definition at line 82 of file code_with_references.h.

Member Function Documentation

◆ to_code()

code_blockt reference_allocationt::to_code ( reference_substitutiont &  references) const
overridevirtual

Implements code_with_referencest.

Definition at line 31 of file code_with_references.cpp.

Member Data Documentation

◆ loc

source_locationt reference_allocationt::loc

Definition at line 80 of file code_with_references.h.

◆ reference_id

std::string reference_allocationt::reference_id

Definition at line 79 of file code_with_references.h.

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