cprover
array_poolt Class Referencefinal

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_exprtfind (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_hasharrays_of_pointers
 
std::unordered_map< array_string_exprt, symbol_exprt, irep_hashlength_of_array
 
symbol_generatortfresh_symbol
 
std::set< array_string_exprtcreated_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()

array_poolt::array_poolt ( symbol_generatort symbol_generator)
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()

const std::unordered_map<exprt, array_string_exprt, irep_hash>& array_poolt::get_arrays_of_pointers ( ) const
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
sarray 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()

array_string_exprt array_poolt::make_char_array_for_char_pointer ( const exprt char_pointer,
const typet char_array_type 
)
private

Definition at line 99 of file string_constraint_generator_main.cpp.

Member Data Documentation

◆ arrays_of_pointers

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

Definition at line 76 of file string_constraint_generator.h.

◆ created_strings_value

std::set<array_string_exprt> array_poolt::created_strings_value
private

Definition at line 86 of file string_constraint_generator.h.

◆ fresh_symbol

symbol_generatort& array_poolt::fresh_symbol
private

Definition at line 83 of file string_constraint_generator.h.

◆ length_of_array

std::unordered_map<array_string_exprt, symbol_exprt, irep_hash> array_poolt::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: