Loading...

Searching...

No Matches

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:

[フレーム]

[legend]

+ Collaboration diagram for reference_allocationt:

[フレーム]

[legend]

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

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/code_with_references.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/code_with_references.cpp