cprover
|
Go to the source code of this file.
Functions | |
std::pair< exprt, string_constraintst > | add_axioms_for_equals (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool) |
Equality of the content of two strings. More... | |
static exprt | character_equals_ignore_case (const exprt &char1, const exprt &char2, const exprt &char_a, const exprt &char_A, const exprt &char_Z) |
Returns an expression which is true when the two given characters are equal when ignoring case for ASCII. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_equals_ignore_case (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool) |
Equality of the content ignoring case of characters. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_compare_to (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool) |
Lexicographic comparison of two strings. More... | |
Generates string constraints for function comparing strings, such as: equals, equalsIgnoreCase, compareTo, hashCode, intern
Definition in file string_constraint_generator_comparison.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_compare_to | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | pool | ||
) |
Lexicographic comparison of two strings.
Add axioms ensuring the result corresponds to that of the String.compareTo
Java function. In the lexicographic comparison, x
representing the first point where the two strings differ, we add axioms:
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string s1 and refined_string s2 |
pool | pool of arrays representing strings |
res
Definition at line 241 of file string_constraint_generator_comparison.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_equals | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | pool | ||
) |
Equality of the content of two strings.
Add axioms stating that the result is true exactly when the strings represented by the arguments are equal. These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string s1 and refined_string s2 |
pool | pool of arrays representing strings |
eq
Definition at line 31 of file string_constraint_generator_comparison.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | pool | ||
) |
Equality of the content ignoring case of characters.
Add axioms ensuring the result is true when the two strings are equal if case is ignored. These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string s1 and refined_string s2 |
pool | pool of arrays representing strings |
eq
Definition at line 132 of file string_constraint_generator_comparison.cpp.
|
static |
Returns an expression which is true when the two given characters are equal when ignoring case for ASCII.
char1 | character expression |
char2 | character expression |
char_a | constant character 'a' |
char_A | constant character 'A' |
char_Z | constant character 'Z' |
Definition at line 87 of file string_constraint_generator_comparison.cpp.