cprover
|
Generates string constraints for functions adding content add the end of strings. More...
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) |
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... | |
Generates string constraints for functions adding content add the end of strings.
Definition in 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 95 of file string_constraint_generator_concat.cpp.
References array_string_exprt::length().
Referenced by string_concatenation_builtin_functiont::length_constraint().
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 135 of file string_constraint_generator_concat.cpp.
References from_integer(), and array_string_exprt::length().
Referenced by string_constraint_generatort::add_axioms_for_concat_char(), and string_concat_char_builtin_functiont::length_constraint().
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 77 of file string_constraint_generator_concat.cpp.
References from_integer(), irept::id(), array_string_exprt::length(), maximum(), minimum(), PRECONDITION, sum_overflows(), to_signedbv_type(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_concat_substr(), and string_concatenation_builtin_functiont::length_constraint().