cprover
Loading...
Searching...
No Matches
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

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 29 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: