cprover
string_refinement_util.h File Reference
Include dependency graph for string_refinement_util.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  index_set_pairt
 
struct  string_axiomst
 
class  sparse_arrayt
 Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list of entries (i,a), (j,b) etc. More...
 
class  interval_sparse_arrayt
 Represents arrays by the indexes up to which the value remains the same. More...
 
class  equation_symbol_mappingt
 Maps equation to expressions contained in them and conversely expressions to equations that contain them. More...
 
class  string_dependenciest
 Keep track of dependencies between strings. More...
 
class  string_dependenciest::builtin_function_nodet
 A builtin function node contains a builtin function call. More...
 
class  string_dependenciest::string_nodet
 A string node points to builtin_function on which it depends. More...
 
class  string_dependenciest::nodet
 
struct  string_dependenciest::node_hash
 Hash function for nodes. More...
 

Functions

bool is_char_type (const typet &type)
 For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character. More...
 
bool is_char_array_type (const typet &type, const namespacet &ns)
 Distinguish char array from other types. More...
 
bool is_char_pointer_type (const typet &type)
 For now, any unsigned bitvector type is considered a character. More...
 
bool has_char_pointer_subtype (const typet &type, const namespacet &ns)
 
bool has_char_array_subexpr (const exprt &expr, const namespacet &ns)
 
bool add_node (string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool)
 When right hand side of equation is a builtin_function add a "string_builtin_function" node to the graph and connect it to the strings on which it depends and which depends on it. More...
 

Function Documentation

◆ add_node()

bool add_node ( string_dependenciest dependencies,
const equal_exprt equation,
array_poolt array_pool 
)

When right hand side of equation is a builtin_function add a "string_builtin_function" node to the graph and connect it to the strings on which it depends and which depends on it.

If the string builtin_function is not a supported one, mark all the string arguments as depending on an unknown builtin_function.

Parameters
dependenciesgraph to which we add the node
equationan equation whose right hand side is possibly a call to a string builtin_function.
array_poolarray pool containing arrays corresponding to the string exprt arguments of the builtin_function call
Returns
true if a node was added, if false is returned it either means that the right hand side is not a function application

Definition at line 373 of file string_refinement_util.cpp.

References string_dependenciest::add_dependency(), add_dependency_to_string_subexprs(), CHECK_RETURN, expr_try_dynamic_cast(), for_each_atomic_string(), string_dependenciest::get_builtin_function(), string_dependenciest::get_node(), binary_relation_exprt::lhs(), string_dependenciest::make_node(), string_dependenciest::string_nodet::result_from, binary_relation_exprt::rhs(), string_builtin_functiont::string_result(), and to_string_builtin_function().

Referenced by string_refinementt::dec_solve().

◆ has_char_array_subexpr()

bool has_char_array_subexpr ( const exprt expr,
const namespacet ns 
)
Parameters
expran expression
nsnamespace
Returns
true if a subexpression of expr is an array of characters

Definition at line 54 of file string_refinement_util.cpp.

References has_subexpr(), is_char_array_type(), and exprt::type().

Referenced by string_refinementt::set_to().

◆ has_char_pointer_subtype()

bool has_char_pointer_subtype ( const typet type,
const namespacet ns 
)
Parameters
typea type
nsnamespace
Returns
true if a subtype of type is an pointer of characters. The meaning of "subtype" is in the algebraic datatype sense: for example, the subtypes of a struct are the types of its components, the subtype of a pointer is the type it points to, etc...

Definition at line 49 of file string_refinement_util.cpp.

References has_subtype(), and is_char_pointer_type().

Referenced by generate_symbol_resolution_from_equations().

◆ is_char_array_type()

bool is_char_array_type ( const typet type,
const namespacet ns 
)

Distinguish char array from other types.

For now, any unsigned bitvector type is considered a character.

Parameters
typea type
nsnamespace
Returns
true if the given type is an array of characters

Definition at line 37 of file string_refinement_util.cpp.

References namespace_baset::follow(), irept::id(), is_char_array_type(), is_char_type(), and typet::subtype().

Referenced by string_refinementt::get(), has_char_array_subexpr(), and is_char_array_type().

◆ is_char_pointer_type()

bool is_char_pointer_type ( const typet type)

For now, any unsigned bitvector type is considered a character.

Parameters
typea type
Returns
true if the given type represents a pointer to characters

Definition at line 44 of file string_refinement_util.cpp.

References irept::id(), is_char_type(), and typet::subtype().

Referenced by generate_symbol_resolution_from_equations(), and has_char_pointer_subtype().

◆ is_char_type()

bool is_char_type ( const typet type)

For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.

Note
type that are not characters maybe detected as characters (for instance unsigned char in C), this will make dec_solve do unnecessary steps for these, but should not affect correctness.
Parameters
typea type
Returns
true if the given type represents characters

Definition at line 30 of file string_refinement_util.cpp.

References bitvector_typet::get_width(), irept::id(), STRING_REFINEMENT_MAX_CHAR_WIDTH, and to_unsignedbv_type().

Referenced by string_refinementt::get(), initial_index_set(), is_char_array_type(), is_char_pointer_type(), and update_index_set().