Associates arrays and length to pointers, so that the string refinement can transform builtin function calls with pointer arguments to formulas over arrays. More...
Include dependency graph for array_pool.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | symbol_generatort |
| Generation of fresh symbols of a given type. More... | |
| class | array_poolt |
| Correspondance between arrays and pointers string representations. More... | |
Functions | |
| 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. | |
Detailed Description
Associates arrays and length to pointers, so that the string refinement can transform builtin function calls with pointer arguments to formulas over arrays.
Definition in file array_pool.h.
Function Documentation
◆ 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.
