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) |
array_string_exprt | find (const exprt &pointer, const exprt &length) |
Creates a new array if the pointer is not pointing to an array. More... | |
array_string_exprt | find (const refined_string_exprt &str) |
array_string_exprt | of_argument (const exprt &arg) |
Converts a struct containing a length and pointer to an array. 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 |
Correspondance between arrays and pointers string representations.
Definition at line 43 of file string_constraint_generator.h.
|
inlineexplicit |
Definition at line 46 of file string_constraint_generator.h.
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 359 of file string_constraint_generator_main.cpp.
References make_char_array_for_char_pointer(), typet::subtype(), and exprt::type().
Referenced by add_dependency_to_string_subexprs(), string_constraint_generatort::char_array_of_pointer(), find(), of_argument(), string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(), string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(), string_insertion_builtin_functiont::string_insertion_builtin_functiont(), and string_transformation_builtin_functiont::string_transformation_builtin_functiont().
array_string_exprt array_poolt::find | ( | const refined_string_exprt & | str | ) |
Definition at line 375 of file string_constraint_generator_main.cpp.
References refined_string_exprt::content(), find(), and refined_string_exprt::length().
|
inline |
Definition at line 52 of file string_constraint_generator.h.
References arrays_of_pointers.
Referenced by debug_model(), and string_refinementt::dec_solve().
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 150 of file string_constraint_generator_main.cpp.
References array_string_exprt::length(), length_of_array, and exprt::type().
Referenced by string_constraint_generatort::associate_length_to_array(), and string_refinementt::get().
void array_poolt::insert | ( | const exprt & | pointer_expr, |
array_string_exprt & | array | ||
) |
Definition at line 220 of file string_constraint_generator_main.cpp.
References arrays_of_pointers, fresh_symbol, INVARIANT, array_string_exprt::length(), length_of_array, and exprt::type().
Referenced by string_constraint_generatort::associate_array_to_pointer().
|
private |
Definition at line 178 of file string_constraint_generator_main.cpp.
References arrays_of_pointers, if_exprt::cond(), if_exprt::false_case(), fresh_symbol, irept::id(), id2string(), address_of_exprt::object(), exprt::op0(), PRECONDITION, typet::subtype(), to_address_of_expr(), to_array_string_expr(), to_array_type(), to_if_expr(), to_index_expr(), if_exprt::true_case(), and exprt::type().
Referenced by find().
array_string_exprt array_poolt::of_argument | ( | 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 380 of file string_constraint_generator_main.cpp.
References expr_checked_cast(), and find().
Referenced by add_dependency_to_string_subexprs().
|
private |
Definition at line 73 of file string_constraint_generator.h.
Referenced by get_arrays_of_pointers(), insert(), and make_char_array_for_char_pointer().
|
private |
Definition at line 80 of file string_constraint_generator.h.
Referenced by insert(), and make_char_array_for_char_pointer().
|
private |
Definition at line 77 of file string_constraint_generator.h.
Referenced by get_length(), and insert().