Builtin functions for string concatenations. More...
Include dependency graph for string_concatenation_builtin_function.cpp:Go to the source code of this file.
Functions | |
| exprt | length_constraint_for_concat_substr (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start, const exprt &end, array_poolt &array_pool) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at indexend'‘. More... | |
| exprt | length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, array_poolt &array_pool) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 More... | |
| exprt | length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1, array_poolt &array_pool) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with. More... | |
Detailed Description
Builtin functions for string concatenations.
Definition in file string_concatenation_builtin_function.cpp.
Function Documentation
◆ length_constraint_for_concat()
| exprt length_constraint_for_concat | ( | const array_string_exprt & | res, |
| const array_string_exprt & | s1, | ||
| const array_string_exprt & | s2, | ||
| array_poolt & | array_pool | ||
| ) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2
Definition at line 125 of file string_concatenation_builtin_function.cpp.
◆ length_constraint_for_concat_char()
| exprt length_constraint_for_concat_char | ( | const array_string_exprt & | res, |
| const array_string_exprt & | s1, | ||
| array_poolt & | array_pool | ||
| ) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
Definition at line 140 of file string_concatenation_builtin_function.cpp.
◆ length_constraint_for_concat_substr()
| exprt length_constraint_for_concat_substr | ( | const array_string_exprt & | res, |
| const array_string_exprt & | s1, | ||
| const array_string_exprt & | s2, | ||
| const exprt & | start, | ||
| const exprt & | end, | ||
| array_poolt & | array_pool | ||
| ) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at indexend'‘.
Where start_index’ is max(0, start) and end' is max(min(end, s2.length), start')
Definition at line 102 of file string_concatenation_builtin_function.cpp.
