cprover
array_poolt Class Referencefinal

Correspondance between arrays and pointers string representations. More...

#include <string_constraint_generator.h>

Collaboration diagram for array_poolt:
[legend]

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_hasharrays_of_pointers
 
std::unordered_map< array_string_exprt, symbol_exprt, irep_hashlength_of_array
 
symbol_generatortfresh_symbol
 

Detailed Description

Correspondance between arrays and pointers string representations.

Definition at line 43 of file string_constraint_generator.h.

Constructor & Destructor Documentation

◆ array_poolt()

array_poolt::array_poolt ( symbol_generatort symbol_generator)
inlineexplicit

Definition at line 46 of file string_constraint_generator.h.

Member Function Documentation

◆ find() [1/2]

◆ find() [2/2]

◆ get_arrays_of_pointers()

const std::unordered_map<exprt, array_string_exprt, irep_hash>& array_poolt::get_arrays_of_pointers ( ) const
inline

Definition at line 52 of file string_constraint_generator.h.

References arrays_of_pointers.

Referenced by debug_model(), and string_refinementt::dec_solve().

◆ get_length()

exprt array_poolt::get_length ( const array_string_exprt s) const

Associate an actual finite length to infinite arrays.

Parameters
sarray expression representing a string
Returns
expression for the length of 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().

◆ insert()

◆ make_char_array_for_char_pointer()

◆ of_argument()

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().

Member Data Documentation

◆ arrays_of_pointers

std::unordered_map<exprt, array_string_exprt, irep_hash> array_poolt::arrays_of_pointers
private

◆ fresh_symbol

symbol_generatort& array_poolt::fresh_symbol
private

Definition at line 80 of file string_constraint_generator.h.

Referenced by insert(), and make_char_array_for_char_pointer().

◆ length_of_array

std::unordered_map<array_string_exprt, symbol_exprt, irep_hash> array_poolt::length_of_array
private

Definition at line 77 of file string_constraint_generator.h.

Referenced by get_length(), and insert().


The documentation for this class was generated from the following files: