Go to the source code of this file.
◆ add_node()
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
-
dependencies | graph to which we add the node |
equation | an equation whose right hand side is possibly a call to a string builtin_function. |
array_pool | array 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.
◆ has_char_array_subexpr()
- Parameters
-
expr | an expression |
ns | namespace |
- Returns
- true if a subexpression of
expr
is an array of characters
Definition at line 54 of file string_refinement_util.cpp.
◆ has_char_pointer_subtype()
bool has_char_pointer_subtype |
( |
const typet & |
type, |
|
|
const namespacet & |
ns |
|
) |
| |
- Parameters
-
- 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.
◆ is_char_array_type()
Distinguish char array from other types.
For now, any unsigned bitvector type is considered a character.
- Parameters
-
- Returns
- true if the given type is an array of characters
Definition at line 37 of file string_refinement_util.cpp.
◆ is_char_pointer_type()
bool is_char_pointer_type |
( |
const typet & |
type | ) |
|
For now, any unsigned bitvector type is considered a character.
- Parameters
-
- Returns
- true if the given type represents a pointer to characters
Definition at line 44 of file string_refinement_util.cpp.
◆ 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
-
- Returns
- true if the given type represents characters
Definition at line 30 of file string_refinement_util.cpp.