CBMC
Public Types | Public Member Functions | List of all members
code_with_referencest Class Referenceabstract

Base class for code which can contain references which can get replaced before generating actual codet. More...

#include <code_with_references.h>

+ Inheritance diagram for code_with_referencest:

Public Types

using reference_substitutiont = std::function< const object_creation_referencet &(const std::string &)>
 

Public Member Functions

virtual code_blockt to_code (reference_substitutiont &) const =0
 
virtual ~code_with_referencest ()=default
 

Detailed Description

Base class for code which can contain references which can get replaced before generating actual codet.

Currently only references in array allocations are supported, because this is currently the only use required by assign_from_json.

Definition at line 40 of file code_with_references.h.

Member Typedef Documentation

◆ reference_substitutiont

using code_with_referencest::reference_substitutiont = std::function<const object_creation_referencet &(const std::string &)>

Definition at line 43 of file code_with_references.h.

Constructor & Destructor Documentation

◆ ~code_with_referencest()

virtual code_with_referencest::~code_with_referencest ( )
virtualdefault

Member Function Documentation

◆ to_code()

virtual code_blockt code_with_referencest::to_code ( reference_substitutiont &  ) const
pure virtual

Implemented in reference_allocationt, and code_without_referencest.

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