cprover
|
Go to the source code of this file.
Functions | |
std::pair< exprt, string_constraintst > | add_axioms_for_concat_substr (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index) |
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index ‘start_index’and ending at index end_index'‘. More... | |
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) |
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 index end'‘. More... | |
exprt | length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2) |
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) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_concat (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2) |
Add axioms enforcing that res is equal to the concatenation of s1 and s2 . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_concat_code_point (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function. More... | |
Generates string constraints for functions adding content add the end of strings
Definition in file string_constraint_generator_concat.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_concat | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2 | ||
) |
Add axioms enforcing that res
is equal to the concatenation of s1
and s2
.
fresh_symbol | generator of fresh symbols |
res | string_expression corresponding to the result |
s1 | the string expression to append to |
s2 | the string expression to append to the first one |
Definition at line 126 of file string_constraint_generator_concat.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
fresh_symbol | generator of fresh symbols |
f | function application with two arguments: a string and a code point |
array_pool | pool of arrays representing strings |
Definition at line 143 of file string_constraint_generator_concat.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_concat_substr | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2, | ||
const exprt & | start_index, | ||
const exprt & | end_index | ||
) |
Add axioms enforcing that res
is the concatenation of s1
with the substring of s2
starting at index ‘start_index’and ending at index
end_index'‘.
Where start_index’ is max(0, start_index) and end_index' is max(min(end_index, s2.length), start_index') If s1.length + end_index' - start_index' is greater than the maximal integer of the type of res.length, then the result gets truncated to the size of this maximal integer.
These axioms are:
fresh_symbol | generator of fresh symbols |
res | an array of characters expression |
s1 | an array of characters expression |
s2 | an array of characters expression |
start_index | integer expression |
end_index | integer expression |
0
Definition at line 38 of file string_constraint_generator_concat.cpp.
exprt length_constraint_for_concat | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2 | ||
) |
Add axioms enforcing that the length of res
is that of the concatenation of s1
with s2
Definition at line 99 of file string_constraint_generator_concat.cpp.
exprt length_constraint_for_concat_char | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1 | ||
) |
Add axioms enforcing that the length of res
is that of the concatenation of s1
with.
Definition at line 109 of file string_constraint_generator_concat.cpp.
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 | ||
) |
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 index
end'‘.
Where start_index’ is max(0, start) and end' is max(min(end, s2.length), start')
Definition at line 81 of file string_constraint_generator_concat.cpp.