#include <allocate_objects.h>

Collaboration diagram for allocate_objectst:

Public Member Functions
	allocate_objectst (const irep_idt &symbol_mode, const source_locationt &source_location, const irep_idt &name_prefix, symbol_table_baset &symbol_table)

exprt	allocate_object (code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const lifetimet lifetime, const irep_idt &basename_prefix="tmp")
	Allocates a new object, either by creating a local variable with automatic lifetime, a global variable with static lifetime, or by dynamically allocating memory via ALLOCATE().

exprt	allocate_automatic_local_object (code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
	Creates a local variable with automatic lifetime.

exprt	allocate_static_global_object (code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
	Creates a global variable with static lifetime.

exprt	allocate_dynamic_object_symbol (code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
	Generates code for allocating a dynamic object.

exprt	allocate_dynamic_object (code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
	Generate the same code as allocate_dynamic_object_symbol, but return a dereference_exprt that dereferences the newly created pointer to the allocated memory.

symbol_exprt	allocate_automatic_local_object (const typet &allocate_type, const irep_idt &basename_prefix="tmp")
	Creates a local variable with automatic lifetime and returns it as a symbol expression.

void	add_created_symbol (const symbolt &symbol)
	Add a pointer to a symbol to the list of pointers to symbols created so far.

void	declare_created_symbols (code_blockt &init_code)
	Adds declarations for all non-static symbols created.

void	mark_created_symbols_as_input (code_blockt &init_code)
	Adds code to mark the created symbols as input.

Private Member Functions
exprt	allocate_non_dynamic_object (code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const bool static_lifetime, const irep_idt &basename_prefix)

Private Attributes
const irep_idt	symbol_mode

const source_locationt	source_location

const irep_idt	name_prefix

symbol_table_baset &	symbol_table

const namespacet	ns

std::vector< irep_idt >	symbols_created

Detailed Description

Definition at line 26 of file allocate_objects.h.

Constructor & Destructor Documentation

◆ allocate_objectst()

allocate_objectst::allocate_objectst	(	const irep_idt &	symbol_mode,
		const source_locationt &	source_location,
		const irep_idt &	name_prefix,
		symbol_table_baset &	symbol_table
	)

inline

Definition at line 29 of file allocate_objects.h.

Member Function Documentation

◆ add_created_symbol()

void allocate_objectst::add_created_symbol ( const symbolt & symbol )

Add a pointer to a symbol to the list of pointers to symbols created so far.

Parameters

symbol symbol in the symbol table

Definition at line 221 of file allocate_objects.cpp.

◆ allocate_automatic_local_object() [1/2]

exprt allocate_objectst::allocate_automatic_local_object	(	code_blockt &	assignments,
		const exprt &	target_expr,
		const typet &	allocate_type,
		const irep_idt &	basename_prefix = `"tmp"`
	)

Creates a local variable with automatic lifetime.

Code is added to assignments which assigns a pointer to the variable to target_expr. The allocate_type may differ from target_expr.type(), e.g. for target_expr having type int* and allocate_type being an int[10]..

Parameters

assignments	The code block to add code to.
target_expr	A pointer to the variable will be assigned to this lvalue expression
allocate_type	Type of the new variable
basename_prefix	prefix of the basename of the new variable

Returns: An expression denoting the variable

Definition at line 72 of file allocate_objects.cpp.

◆ allocate_automatic_local_object() [2/2]

symbol_exprt allocate_objectst::allocate_automatic_local_object	(	const typet &	allocate_type,
		const irep_idt &	basename_prefix = `"tmp"`
	)

Creates a local variable with automatic lifetime and returns it as a symbol expression.

Parameters

allocate_type	Type of the new variable
basename_prefix	prefix of the basename of the new variable

Returns: A symbol expression denoting the variable

Definition at line 109 of file allocate_objects.cpp.

◆ allocate_dynamic_object()

exprt allocate_objectst::allocate_dynamic_object	(	code_blockt &	output_code,
		const exprt &	target_expr,
		const typet &	allocate_type
	)

Generate the same code as allocate_dynamic_object_symbol, but return a dereference_exprt that dereferences the newly created pointer to the allocated memory.

Definition at line 174 of file allocate_objects.cpp.

◆ allocate_dynamic_object_symbol()

exprt allocate_objectst::allocate_dynamic_object_symbol	(	code_blockt &	output_code,
		const exprt &	target_expr,
		const typet &	allocate_type
	)

Generates code for allocating a dynamic object.

A new variable with basename prefix alloc_site is introduced to which the allocated memory is assigned. Then, the variable is assigned to target_expr. For example, with target_expr being *p the following code is generated:

alloc_site$1 = ALLOCATE(object_size, FALSE); *p = alloc_site$1;

Parameters

output_code	Code block to which the necessary code is added
target_expr	A pointer to the allocated memory will be assigned to this (lvalue) expression
allocate_type	Type of the object allocated

Returns: The pointer to the allocated memory, or an empty expression when allocate_type is void

Definition at line 126 of file allocate_objects.cpp.

◆ allocate_non_dynamic_object()

exprt allocate_objectst::allocate_non_dynamic_object	(	code_blockt &	assignments,
		const exprt &	target_expr,
		const typet &	allocate_type,
		const bool	static_lifetime,
		const irep_idt &	basename_prefix
	)

private

Definition at line 183 of file allocate_objects.cpp.

◆ allocate_object()

exprt allocate_objectst::allocate_object	(	code_blockt &	assignments,
		const exprt &	target_expr,
		const typet &	allocate_type,
		const lifetimet	lifetime,
		const irep_idt &	basename_prefix = `"tmp"`
	)

Allocates a new object, either by creating a local variable with automatic lifetime, a global variable with static lifetime, or by dynamically allocating memory via ALLOCATE().

Code is added to assignments which assigns a pointer to the allocated memory to target_expr. The allocate_type may differ from target_expr.type(), e.g. for target_expr having type int* and allocate_type being an int[10].

Parameters

assignments	The code block to add code to.
target_expr	A pointer to the allocated memory will be assigned to this lvalue expression
allocate_type	Type of the object allocated
lifetime	Lifetime of the allocated object (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
basename_prefix	prefix of the basename of the new variable

Returns: An lvalue expression denoting the newly allocated object

Definition at line 34 of file allocate_objects.cpp.

◆ allocate_static_global_object()

exprt allocate_objectst::allocate_static_global_object	(	code_blockt &	assignments,
		const exprt &	target_expr,
		const typet &	allocate_type,
		const irep_idt &	basename_prefix = `"tmp"`
	)

Creates a global variable with static lifetime.

Code is added to assignments which assigns a pointer to the variable to target_expr. The allocate_type may differ from target_expr.type(), e.g. for target_expr having type int* and allocate_type being an int[10].

Parameters

assignments	The code block to add code to.
target_expr	A pointer to the variable will be assigned to this lvalue expression
allocate_type	Type of the new variable
basename_prefix	prefix of the basename of the new variable

Returns: An expression denoting the variable

Definition at line 93 of file allocate_objects.cpp.

◆ declare_created_symbols()

void allocate_objectst::declare_created_symbols ( code_blockt & init_code )

Adds declarations for all non-static symbols created.

Parameters

init_code code block to which to add the declarations

Definition at line 229 of file allocate_objects.cpp.

◆ mark_created_symbols_as_input()

void allocate_objectst::mark_created_symbols_as_input ( code_blockt & init_code )

Adds code to mark the created symbols as input.

Parameters

init_code code block to which to add the generated code

Definition at line 248 of file allocate_objects.cpp.

Member Data Documentation

◆ name_prefix

const irep_idt allocate_objectst::name_prefix

private

Definition at line 102 of file allocate_objects.h.

◆ ns

const namespacet allocate_objectst::ns

private

Definition at line 105 of file allocate_objects.h.

◆ source_location

const source_locationt allocate_objectst::source_location

private

Definition at line 101 of file allocate_objects.h.

◆ symbol_mode

const irep_idt allocate_objectst::symbol_mode

private

Definition at line 100 of file allocate_objects.h.

◆ symbol_table

symbol_table_baset& allocate_objectst::symbol_table

private

Definition at line 104 of file allocate_objects.h.

◆ symbols_created

std::vector<irep_idt> allocate_objectst::symbols_created

private

Definition at line 107 of file allocate_objects.h.

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

/home/runner/work/cbmc/cbmc/src/ansi-c/allocate_objects.h
/home/runner/work/cbmc/cbmc/src/ansi-c/allocate_objects.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ allocate_objectst()

Member Function Documentation

◆ add_created_symbol()

◆ allocate_automatic_local_object() [1/2]

◆ allocate_automatic_local_object() [2/2]

◆ allocate_dynamic_object()

◆ allocate_dynamic_object_symbol()

◆ allocate_non_dynamic_object()

◆ allocate_object()

◆ allocate_static_global_object()

◆ declare_created_symbols()

◆ mark_created_symbols_as_input()

Member Data Documentation

◆ name_prefix

◆ ns

◆ source_location

◆ symbol_mode

◆ symbol_table

◆ symbols_created