CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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

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

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