Include dependency graph for array_pool.cpp:Go to the source code of this file.
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. More... | |
| array_string_exprt | of_argument (array_poolt &array_pool, const exprt &arg) |
| Converts a struct containing a length and pointer to an array. More... | |
| array_string_exprt | get_string_expr (array_poolt &array_pool, const exprt &expr) |
| Fetch the string_exprt corresponding to the given refined_string_exprt. More... | |
Function Documentation
◆ attempt_assign_length_from_type()
|
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_exprts, 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.
