cprover
|
Generates string constraints for functions adding content add the end of strings. More...
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.