Correspondance between arrays and pointers string representations. More...
#include <array_pool.h>
Collaboration diagram for array_poolt:Public Member Functions | |
| array_poolt (symbol_generatort &symbol_generator) | |
| const std::unordered_map< exprt, array_string_exprt, irep_hash > & | get_arrays_of_pointers () const |
| exprt | get_or_create_length (const array_string_exprt &s) |
| Get the length of an array_string_exprt from the array_pool. More... | |
| std::optional< exprt > | get_length_if_exists (const array_string_exprt &s) const |
| As opposed to get_length(), do not create a new symbol if the length of the array_string_exprt does not have one in the array_pool, but instead return an empty optional. More... | |
| void | insert (const exprt &pointer_expr, const array_string_exprt &array) |
| array_string_exprt | find (const exprt &pointer, const exprt &length) |
| Creates a new array if the pointer is not pointing to an array. More... | |
| const std::unordered_map< array_string_exprt, exprt, irep_hash > & | created_strings () const |
| Return a map mapping all array_string_exprt of the array_pool to their length. More... | |
| array_string_exprt | fresh_string (const typet &index_type, const typet &char_type) |
| Construct a string expression whose length and content are new variables. More... | |
Private Member Functions | |
| array_string_exprt | make_char_array_for_char_pointer (const exprt &char_pointer, const typet &char_array_type) |
| Helper function for find. More... | |
Private Attributes | |
| std::unordered_map< exprt, array_string_exprt, irep_hash > | arrays_of_pointers |
| Associate arrays to char pointers Invariant: Each array_string_exprt in this map has a corresponding entry in length_of_array. More... | |
| std::unordered_map< array_string_exprt, exprt, irep_hash > | length_of_array |
| Associate length to arrays of infinite size. More... | |
| symbol_generatort & | fresh_symbol |
| Generate fresh symbols. More... | |
Detailed Description
Correspondance between arrays and pointers string representations.
Definition at line 41 of file array_pool.h.
Constructor & Destructor Documentation
◆ array_poolt()
|
inlineexplicit |
Definition at line 44 of file array_pool.h.
Member Function Documentation
◆ created_strings()
| const std::unordered_map< array_string_exprt, exprt, irep_hash > & array_poolt::created_strings | ( | ) | const |
Return a map mapping all array_string_exprt of the array_pool to their length.
Definition at line 179 of file array_pool.cpp.
◆ find()
| array_string_exprt array_poolt::find | ( | const exprt & | pointer, |
| const exprt & | length | ||
| ) |
Creates a new array if the pointer is not pointing to an array.
Definition at line 184 of file array_pool.cpp.
◆ fresh_string()
| array_string_exprt array_poolt::fresh_string | ( | const typet & | index_type, |
| const typet & | char_type | ||
| ) |
Construct a string expression whose length and content are new variables.
- Parameters
-
index_type type used to index characters of the strings char_type type of characters
- Returns
- a string expression
Definition at line 57 of file array_pool.cpp.
◆ get_arrays_of_pointers()
|
inline |
Definition at line 50 of file array_pool.h.
◆ get_length_if_exists()
| std::optional< exprt > array_poolt::get_length_if_exists | ( | const array_string_exprt & | s | ) | const |
As opposed to get_length(), do not create a new symbol if the length of the array_string_exprt does not have one in the array_pool, but instead return an empty optional.
- Parameters
-
s array expression representing a string
- Returns
- expression for the length of
s, or empty optional
Definition at line 48 of file array_pool.cpp.
◆ get_or_create_length()
| exprt array_poolt::get_or_create_length | ( | const array_string_exprt & | s | ) |
Get the length of an array_string_exprt from the array_pool.
If the length does not yet exist, create a new symbol and add it to the pool.
If the array_string_exprt is an if expression, the true and false parts are handled independently (and recursively). That is, no new length symbol is added to the pool for if expressions, but symbols may be added for each of the parts.
- Parameters
-
s array expression representing a string
- Returns
- expression for the length of
s
Definition at line 26 of file array_pool.cpp.
◆ insert()
| void array_poolt::insert | ( | const exprt & | pointer_expr, |
| const array_string_exprt & | array | ||
| ) |
Definition at line 160 of file array_pool.cpp.
◆ make_char_array_for_char_pointer()
|
private |
Helper function for find.
Make a new char array for a char pointer. The size of the char array is a variable with no constraint.
Definition at line 74 of file array_pool.cpp.
Member Data Documentation
◆ arrays_of_pointers
|
private |
Associate arrays to char pointers Invariant: Each array_string_exprt in this map has a corresponding entry in length_of_array.
This is enforced whenever we add an element to arrays_of_pointers, i.e. fresh_string() and make_char_array_for_char_pointer().
Definition at line 95 of file array_pool.h.
◆ fresh_symbol
|
private |
Generate fresh symbols.
Definition at line 101 of file array_pool.h.
◆ length_of_array
|
private |
Associate length to arrays of infinite size.
Definition at line 98 of file array_pool.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/strings/array_pool.h
- /home/runner/work/cbmc/cbmc/src/solvers/strings/array_pool.cpp
