cprover
|
Correspondance between arrays and pointers string representations. More...
#include <string_constraint_generator.h>
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 |
Correspondance between arrays and pointers string representations.
Definition at line 49 of file string_constraint_generator.h.
|
inlineexplicit |
Definition at line 52 of file string_constraint_generator.h.
const std::set< array_string_exprt > & array_poolt::created_strings | ( | ) | const |
Definition at line 160 of file string_constraint_generator_main.cpp.
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.
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
Definition at line 87 of file string_constraint_generator_main.cpp.
|
inline |
Definition at line 58 of file string_constraint_generator.h.
exprt array_poolt::get_length | ( | const array_string_exprt & | s | ) | const |
Associate an actual finite length to infinite arrays.
s | array expression representing a string |
s
Definition at line 72 of file string_constraint_generator_main.cpp.
void array_poolt::insert | ( | const exprt & | pointer_expr, |
array_string_exprt & | array | ||
) |
Definition at line 141 of file string_constraint_generator_main.cpp.
|
private |
Definition at line 99 of file string_constraint_generator_main.cpp.
|
private |
Definition at line 76 of file string_constraint_generator.h.
|
private |
Definition at line 86 of file string_constraint_generator.h.
|
private |
Definition at line 83 of file string_constraint_generator.h.
|
private |
Definition at line 80 of file string_constraint_generator.h.