cprover
|
Generates string constraints for Java functions dealing with code points. More...
Go to the source code of this file.
Functions | |
std::pair< exprt, string_constraintst > | add_axioms_for_code_point (const array_string_exprt &res, const exprt &code_point) |
add axioms for the conversion of an integer representing a java code point to a utf-16 string More... | |
static exprt | is_high_surrogate (const exprt &chr) |
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF More... | |
static exprt | is_low_surrogate (const exprt &chr) |
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF More... | |
exprt | pair_value (exprt char1, exprt char2, typet return_type) |
the output corresponds to the unicode character given by the pair of characters of inputs assuming it has been encoded in UTF-16, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; the operation we perform is: pair_value=0x10000+(((char1%0x0800)*0x0400)+char2%0x0400) More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_code_point_at (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
add axioms corresponding to the String.codePointAt java function More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_code_point_before (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
add axioms corresponding to the String.codePointBefore java function More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_code_point_count (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
add axioms giving approximate bounds on the result of the String.codePointCount java function More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_offset_by_code_point (symbol_generatort &fresh_symbol, const function_application_exprt &f) |
add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function. More... | |
Generates string constraints for Java functions dealing with code points.
Definition in file string_constraint_generator_code_points.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_code_point | ( | const array_string_exprt & | res, |
const exprt & | code_point | ||
) |
add axioms for the conversion of an integer representing a java code point to a utf-16 string
res | array of characters corresponding to the result fo the function |
code_point | an expression representing a java code point |
Definition at line 20 of file string_constraint_generator_code_points.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_code_point_at | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
add axioms corresponding to the String.codePointAt java function
fresh_symbol | generator of fresh symbols |
f | function application with arguments a string and an index |
array_pool | pool of arrays representing strings |
Definition at line 122 of file string_constraint_generator_code_points.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_code_point_before | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
add axioms corresponding to the String.codePointBefore java function
Definition at line 155 of file string_constraint_generator_code_points.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_code_point_count | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
add axioms giving approximate bounds on the result of the String.codePointCount java function
Add axioms corresponding the String.codePointCount java function.
fresh_symbol | generator of fresh symbols |
f | function application with three arguments string str , integer begin and integer end . |
array_pool | pool of arrays representing strings |
Definition at line 193 of file string_constraint_generator_code_points.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_offset_by_code_point | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f | ||
) |
add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function.
Add axioms corresponding the String.offsetByCodePointCount java function.
We approximate the result by saying the result is between index + offset and index + 2 * offset
fresh_symbol | generator of fresh symbols |
f | function application with arguments string str , integer index and integer offset . |
Definition at line 222 of file string_constraint_generator_code_points.cpp.
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF
chr | a character expression |
Definition at line 76 of file string_constraint_generator_code_points.cpp.
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF
chr | a character expression |
Definition at line 89 of file string_constraint_generator_code_points.cpp.
the output corresponds to the unicode character given by the pair of characters of inputs assuming it has been encoded in UTF-16, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; the operation we perform is: pair_value=0x10000+(((char1%0x0800)*0x0400)+char2%0x0400)
char1 | a character expression |
char2 | a character expression |
return_type | type of the expression to return |
Definition at line 105 of file string_constraint_generator_code_points.cpp.