Correspondance between arrays and pointers string representations. More...
#include <string_constraint_generator.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_length (const array_string_exprt &s) const |
| Associate an actual finite length to infinite arrays. More... | |
| void | insert (const exprt &pointer_expr, array_string_exprt &array) |
| const 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::set< array_string_exprt > & | created_strings () const |
| 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) |
Private Attributes | |
| std::unordered_map< exprt, array_string_exprt, irep_hash > | arrays_of_pointers |
| std::unordered_map< array_string_exprt, symbol_exprt, irep_hash > | length_of_array |
| symbol_generatort & | fresh_symbol |
| std::set< array_string_exprt > | created_strings_value |
Detailed Description
Correspondance between arrays and pointers string representations.
Definition at line 49 of file string_constraint_generator.h.
Constructor & Destructor Documentation
◆ array_poolt()
|
inlineexplicit |
Definition at line 52 of file string_constraint_generator.h.
Member Function Documentation
◆ created_strings()
| const std::set< array_string_exprt > & array_poolt::created_strings | ( | ) | const |
Definition at line 160 of file string_constraint_generator_main.cpp.
◆ find()
| const 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 314 of file string_constraint_generator_main.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: a type for string
- Returns
- a string expression
Definition at line 87 of file string_constraint_generator_main.cpp.
◆ get_arrays_of_pointers()
|
inline |
Definition at line 58 of file string_constraint_generator.h.
◆ get_length()
| exprt array_poolt::get_length | ( | const array_string_exprt & | s | ) | const |
Associate an actual finite length to infinite arrays.
- Parameters
-
s array expression representing a string
- Returns
- expression for the length of
s
Definition at line 72 of file string_constraint_generator_main.cpp.
◆ insert()
| void array_poolt::insert | ( | const exprt & | pointer_expr, |
| array_string_exprt & | array | ||
| ) |
Definition at line 141 of file string_constraint_generator_main.cpp.
◆ make_char_array_for_char_pointer()
|
private |
Definition at line 99 of file string_constraint_generator_main.cpp.
Member Data Documentation
◆ arrays_of_pointers
|
private |
Definition at line 76 of file string_constraint_generator.h.
◆ created_strings_value
|
private |
Definition at line 86 of file string_constraint_generator.h.
◆ fresh_symbol
|
private |
Definition at line 83 of file string_constraint_generator.h.
◆ length_of_array
|
private |
Definition at line 80 of file string_constraint_generator.h.
The documentation for this class was generated from the following files:
- solvers/refinement/string_constraint_generator.h
- solvers/refinement/string_constraint_generator_main.cpp
