Functions

static void attempt_assign_length_from_type (const array_string_exprt &array_expr, std::unordered_map< array_string_exprt, exprt, irep_hash > &length_of_array, symbol_generatort &symbol_generator)

Given an array_string_exprt, get the size of the underlying array.

array_string_exprt of_argument (array_poolt &array_pool, const exprt &arg)

Converts a struct containing a length and pointer to an array.

array_string_exprt get_string_expr (array_poolt &array_pool, const exprt &expr)

Fetch the string_exprt corresponding to the given refined_string_exprt.

Function Documentation

◆ attempt_assign_length_from_type()

static void attempt_assign_length_from_type ( const array_string_exprt & array_expr,

std::unordered_map< array_string_exprt, exprt, irep_hash > & length_of_array,

symbol_generatort & symbol_generator

)

static

Given an array_string_exprt, get the size of the underlying array.

If that size is undefined, create a new symbol for the size. Then add an entry from array_expr to that size in the length_of_array map.

This function should only be used at the creation of the array_string_exprt s, as it is the only place where we can reliably refer to the size in the type of the array.

Definition at line 135 of file array_pool.cpp.

◆ get_string_expr()

array_string_exprt get_string_expr ( array_poolt & array_pool,

const exprt & expr

)

Fetch the string_exprt corresponding to the given refined_string_exprt.

Parameters: array_pool pool of arrays representing strings

expr an expression of refined string type

Returns: a string expression

Definition at line 199 of file array_pool.cpp.

◆ of_argument()

array_string_exprt of_argument ( array_poolt & array_pool,

const exprt & arg

)

Converts a struct containing a length and pointer to an array.

This allows to get a string expression from arguments of a string builtion function, because string arguments in these function calls are given as a struct containing a length and pointer to an array.

Definition at line 193 of file array_pool.cpp.