cprover
|
#include <character_refine_preprocess.h>
Public Member Functions | |
void | initialize_conversion_table () |
fill maps with correspondance from java method names to conversion functions More... | |
codet | replace_character_call (const code_function_callt &call) const |
replace function calls to functions of the Character by an affectation if possible, returns the same code otherwise. More... | |
Private Types | |
typedef const code_function_callt & | conversion_inputt |
typedef codet(* | conversion_functiont) (conversion_inputt &target) |
Static Private Member Functions | |
static exprt | expr_of_char_count (const exprt &chr, const typet &type) |
Determines the number of char values needed to represent the specified character (Unicode code point). More... | |
static codet | convert_char_count (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.charCount:(I)I. More... | |
static exprt | expr_of_char_value (const exprt &chr, const typet &type) |
Casts the given expression to the given type. More... | |
static codet | convert_char_value (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.charValue:()C. More... | |
static codet | convert_compare (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.compare:(CC)I. More... | |
static codet | convert_digit_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.digit:(CI)I. More... | |
static codet | convert_digit_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.digit:(II)I. More... | |
static codet | convert_for_digit (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.forDigit:(II)C. More... | |
static codet | convert_get_directionality_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(C)I. More... | |
static codet | convert_get_directionality_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(I)I. More... | |
static codet | convert_get_numeric_value_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.getNumericValue:(C)I. More... | |
static codet | convert_get_numeric_value_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.getNumericValue:(C)I. More... | |
static codet | convert_get_type_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.getType:(C)I. More... | |
static codet | convert_get_type_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.getType:(I)I. More... | |
static codet | convert_hash_code (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.hashCode:()I. More... | |
static exprt | expr_of_high_surrogate (const exprt &chr, const typet &type) |
Returns the leading surrogate (a high surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding. More... | |
static codet | convert_high_surrogate (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.highSurrogate:(C)Z. More... | |
static exprt | expr_of_is_alphabetic (const exprt &chr, const typet &type) |
Determines if the specified character (Unicode code point) is alphabetic. More... | |
static codet | convert_is_alphabetic (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isAlphabetic:(I)Z. More... | |
static exprt | expr_of_is_bmp_code_point (const exprt &chr, const typet &type) |
Determines whether the specified character (Unicode code point) is in the Basic Multilingual Plane (BMP). More... | |
static codet | convert_is_bmp_code_point (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isBmpCodePoint:(I)Z. More... | |
static exprt | expr_of_is_defined (const exprt &chr, const typet &type) |
Determines if a character is defined in Unicode. More... | |
static codet | convert_is_defined_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isDefined:(C)Z. More... | |
static codet | convert_is_defined_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isDefined:(I)Z. More... | |
static exprt | expr_of_is_digit (const exprt &chr, const typet &type) |
Determines if the specified character is a digit. More... | |
static codet | convert_is_digit_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isDigit:(C)Z. More... | |
static codet | convert_is_digit_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.digit:(I)Z. More... | |
static exprt | expr_of_is_high_surrogate (const exprt &chr, const typet &type) |
Determines if the given char value is a Unicode high-surrogate code unit (also known as leading-surrogate code unit). More... | |
static codet | convert_is_high_surrogate (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isHighSurrogate:(C)Z. More... | |
static exprt | expr_of_is_identifier_ignorable (const exprt &chr, const typet &type) |
Determines if the character is one of ignorable in a Java identifier, that is, it is in one of these ranges: '' through '' '' through '' '' through ''. More... | |
static codet | convert_is_identifier_ignorable_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isIdentifierIgnorable:(C)Z. More... | |
static codet | convert_is_identifier_ignorable_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isIdentifierIgnorable:(I)Z. More... | |
static codet | convert_is_ideographic (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isIdeographic:(I)Z. More... | |
static codet | convert_is_ISO_control_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(C)Z. More... | |
static codet | convert_is_ISO_control_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(I)Z. More... | |
static codet | convert_is_java_identifier_part_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isJavaIdentifierPart:(C)Z. More... | |
static codet | convert_is_java_identifier_part_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierPart:(I)Z. More... | |
static codet | convert_is_java_identifier_start_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierStart:(C)Z. More... | |
static codet | convert_is_java_identifier_start_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierStart:(I)Z. More... | |
static codet | convert_is_java_letter (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isJavaLetter:(C)Z. More... | |
static codet | convert_is_java_letter_or_digit (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method isJavaLetterOrDigit:(C)Z. More... | |
static exprt | expr_of_is_letter (const exprt &chr, const typet &type) |
Determines if the specified character is a letter. More... | |
static codet | convert_is_letter_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(C)Z. More... | |
static codet | convert_is_letter_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(I)Z. More... | |
static exprt | expr_of_is_letter_or_digit (const exprt &chr, const typet &type) |
Determines if the specified character is a letter or digit. More... | |
static codet | convert_is_letter_or_digit_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(C)Z. More... | |
static codet | convert_is_letter_or_digit_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(I)Z. More... | |
static exprt | expr_of_is_ascii_lower_case (const exprt &chr, const typet &type) |
Determines if the specified character is an ASCII lowercase character. More... | |
static codet | convert_is_lower_case_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isLowerCase:(C)Z. More... | |
static codet | convert_is_lower_case_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isLowerCase:(I)Z. More... | |
static codet | convert_is_low_surrogate (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isLowSurrogate:(C)Z. More... | |
static exprt | expr_of_is_mirrored (const exprt &chr, const typet &type) |
Determines whether the character is mirrored according to the Unicode specification. More... | |
static codet | convert_is_mirrored_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isMirrored:(C)Z. More... | |
static codet | convert_is_mirrored_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isMirrored:(I)Z. More... | |
static codet | convert_is_space (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isSpace:(C)Z. More... | |
static exprt | expr_of_is_space_char (const exprt &chr, const typet &type) |
Determines if the specified character is white space according to Unicode (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR) More... | |
static codet | convert_is_space_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(C)Z. More... | |
static codet | convert_is_space_char_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(I)Z. More... | |
static exprt | expr_of_is_supplementary_code_point (const exprt &chr, const typet &type) |
Determines whether the specified character (Unicode code point) is in the supplementary character range. More... | |
static codet | convert_is_supplementary_code_point (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isSupplementaryCodePoint:(I)Z. More... | |
static exprt | expr_of_is_surrogate (const exprt &chr, const typet &type) |
Determines if the given char value is a Unicode surrogate code unit. More... | |
static codet | convert_is_surrogate (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogate:(C)Z. More... | |
static codet | convert_is_surrogate_pair (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogatePair:(CC)Z. More... | |
static exprt | expr_of_is_title_case (const exprt &chr, const typet &type) |
Determines if the specified character is a titlecase character. More... | |
static codet | convert_is_title_case_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(C)Z. More... | |
static codet | convert_is_title_case_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(I)Z. More... | |
static exprt | expr_of_is_letter_number (const exprt &chr, const typet &type) |
Determines if the specified character is in the LETTER_NUMBER category of Unicode. More... | |
static exprt | expr_of_is_unicode_identifier_part (const exprt &chr, const typet &type) |
Determines if the character may be part of a Unicode identifier. More... | |
static codet | convert_is_unicode_identifier_part_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(C)Z. More... | |
static codet | convert_is_unicode_identifier_part_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(I)Z. More... | |
static exprt | expr_of_is_unicode_identifier_start (const exprt &chr, const typet &type) |
Determines if the specified character is permissible as the first character in a Unicode identifier. More... | |
static codet | convert_is_unicode_identifier_start_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(C)Z. More... | |
static codet | convert_is_unicode_identifier_start_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(I)Z. More... | |
static exprt | expr_of_is_ascii_upper_case (const exprt &chr, const typet &type) |
Determines if the specified character is an ASCII uppercase character. More... | |
static codet | convert_is_upper_case_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isUpperCase:(C)Z. More... | |
static codet | convert_is_upper_case_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isUpperCase:(I)Z. More... | |
static exprt | expr_of_is_valid_code_point (const exprt &chr, const typet &type) |
Determines whether the specified code point is a valid Unicode code point value. More... | |
static codet | convert_is_valid_code_point (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isValidCodePoint:(I)Z. More... | |
static exprt | expr_of_is_whitespace (const exprt &chr, const typet &type) |
Determines if the specified character is white space according to Java. More... | |
static codet | convert_is_whitespace_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(C)Z. More... | |
static codet | convert_is_whitespace_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(I)Z. More... | |
static exprt | expr_of_low_surrogate (const exprt &chr, const typet &type) |
Returns the trailing surrogate (a low surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding. More... | |
static codet | convert_low_surrogate (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.lowSurrogate:(I)C. More... | |
static exprt | expr_of_reverse_bytes (const exprt &chr, const typet &type) |
Returns the value obtained by reversing the order of the bytes in the specified char value. More... | |
static codet | convert_reverse_bytes (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.reverseBytes:(C)C. More... | |
static exprt | expr_of_to_chars (const exprt &chr, const typet &type) |
Converts the specified character (Unicode code point) to its UTF-16 representation stored in a char array. More... | |
static codet | convert_to_chars (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.toChars:(I)[C. More... | |
static codet | convert_to_code_point (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.toCodePoint:(CC)I. More... | |
static exprt | expr_of_to_lower_case (const exprt &chr, const typet &type) |
Converts the character argument to lowercase. More... | |
static codet | convert_to_lower_case_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(C)C. More... | |
static codet | convert_to_lower_case_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(I)I. More... | |
static exprt | expr_of_to_title_case (const exprt &chr, const typet &type) |
Converts the character argument to titlecase. More... | |
static codet | convert_to_title_case_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(C)C. More... | |
static codet | convert_to_title_case_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(I)I. More... | |
static exprt | expr_of_to_upper_case (const exprt &chr, const typet &type) |
Converts the character argument to uppercase. More... | |
static codet | convert_to_upper_case_char (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(C)C. More... | |
static codet | convert_to_upper_case_int (conversion_inputt &target) |
Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(I)I. More... | |
static codet | convert_char_function (exprt(*expr_function)(const exprt &chr, const typet &type), conversion_inputt &target) |
converts based on a function on expressions More... | |
static exprt | in_interval_expr (const exprt &chr, const mp_integer &lower_bound, const mp_integer &upper_bound) |
The returned expression is true when the first argument is in the interval defined by the lower and upper bounds (included) More... | |
static exprt | in_list_expr (const exprt &chr, const std::list< mp_integer > &list) |
The returned expression is true when the given character is equal to one of the element in the list. More... | |
Private Attributes | |
std::unordered_map< irep_idt, conversion_functiont > | conversion_table |
Additional Inherited Members |
Definition at line 29 of file character_refine_preprocess.h.
|
private |
Definition at line 37 of file character_refine_preprocess.h.
|
private |
Definition at line 36 of file character_refine_preprocess.h.
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.charCount:(I)I.
target | a position in a goto program |
Definition at line 82 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_char_count().
Referenced by initialize_conversion_table().
|
staticprivate |
converts based on a function on expressions
expr_function | A reference to a function on expressions |
target | A position in a goto program |
Definition at line 24 of file character_refine_preprocess.cpp.
References code_function_callt::arguments(), code_function_callt::lhs(), and messaget::result().
Referenced by convert_char_count(), convert_char_value(), convert_high_surrogate(), convert_is_alphabetic(), convert_is_bmp_code_point(), convert_is_defined_char(), convert_is_digit_char(), convert_is_high_surrogate(), convert_is_identifier_ignorable_char(), convert_is_java_identifier_part_char(), convert_is_java_identifier_start_char(), convert_is_letter_char(), convert_is_letter_or_digit_char(), convert_is_lower_case_char(), convert_is_mirrored_char(), convert_is_space_char(), convert_is_supplementary_code_point(), convert_is_surrogate(), convert_is_title_case_char(), convert_is_unicode_identifier_part_char(), convert_is_unicode_identifier_start_char(), convert_is_upper_case_char(), convert_is_valid_code_point(), convert_is_whitespace_char(), convert_low_surrogate(), convert_reverse_bytes(), convert_to_chars(), convert_to_lower_case_char(), convert_to_title_case_char(), and convert_to_upper_case_char().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.charValue:()C.
target | a position in a goto program |
Definition at line 100 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_char_value().
Referenced by convert_hash_code(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.compare:(CC)I.
target | a position in a goto program |
Definition at line 110 of file character_refine_preprocess.cpp.
References code_function_callt::arguments(), from_integer(), code_function_callt::lhs(), and messaget::result().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.digit:(CI)I.
The function call has one character argument and an optional integer radix argument. If the radix is not given it is set to 36 by default.
target | a position in a goto program |
Definition at line 136 of file character_refine_preprocess.cpp.
References code_function_callt::arguments(), from_integer(), in_interval_expr(), code_function_callt::lhs(), PRECONDITION, messaget::result(), and exprt::type().
Referenced by convert_digit_int(), convert_get_numeric_value_char(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.digit:(II)I.
target | a position in a goto program |
Definition at line 213 of file character_refine_preprocess.cpp.
References convert_digit_char().
Referenced by convert_get_numeric_value_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.forDigit:(II)C.
TODO: For now the radix argument is ignored
target | a position in a goto program |
Definition at line 223 of file character_refine_preprocess.cpp.
References code_function_callt::arguments(), from_integer(), code_function_callt::lhs(), and messaget::result().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(C)I.
target | a position in a goto program |
Definition at line 242 of file character_refine_preprocess.cpp.
Referenced by convert_get_directionality_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(I)I.
target | a position in a goto program |
Definition at line 253 of file character_refine_preprocess.cpp.
References convert_get_directionality_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.getNumericValue:(C)I.
TODO: For now this is only for ASCII characters
Definition at line 263 of file character_refine_preprocess.cpp.
References convert_digit_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.getNumericValue:(C)I.
TODO: For now this is only for ASCII characters
target | a position in a goto program |
Definition at line 274 of file character_refine_preprocess.cpp.
References convert_digit_int().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.getType:(C)I.
target | a position in a goto program |
Definition at line 283 of file character_refine_preprocess.cpp.
Referenced by convert_get_type_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.getType:(I)I.
target | a position in a goto program |
Definition at line 294 of file character_refine_preprocess.cpp.
References convert_get_type_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.hashCode:()I.
target | a position in a goto program |
Definition at line 303 of file character_refine_preprocess.cpp.
References convert_char_value().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.highSurrogate:(C)Z.
Definition at line 327 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_high_surrogate().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isAlphabetic:(I)Z.
target | a position in a goto program |
Definition at line 389 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_alphabetic().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isBmpCodePoint:(I)Z.
target | a position in a goto program |
Definition at line 412 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_bmp_code_point().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isDefined:(C)Z.
target | a position in a goto program |
Definition at line 457 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_defined().
Referenced by convert_is_defined_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isDefined:(I)Z.
target | a position in a goto program |
Definition at line 467 of file character_refine_preprocess.cpp.
References convert_is_defined_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isDigit:(C)Z.
target | a position in a goto program |
Definition at line 504 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_digit().
Referenced by convert_is_digit_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.digit:(I)Z.
target | a position in a goto program |
Definition at line 514 of file character_refine_preprocess.cpp.
References convert_is_digit_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isHighSurrogate:(C)Z.
target | a position in a goto program |
Definition at line 534 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_high_surrogate().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isIdentifierIgnorable:(C)Z.
TODO: For now, we ignore the FORMAT general category value
target | a position in a goto program |
Definition at line 565 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_identifier_ignorable().
Referenced by convert_is_identifier_ignorable_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isIdentifierIgnorable:(I)Z.
TODO: For now, we ignore the FORMAT general category value
target | a position in a goto program |
Definition at line 577 of file character_refine_preprocess.cpp.
References convert_is_identifier_ignorable_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isIdeographic:(I)Z.
target | a position in a goto program |
Definition at line 586 of file character_refine_preprocess.cpp.
References code_function_callt::arguments(), in_interval_expr(), code_function_callt::lhs(), and messaget::result().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(C)Z.
target | a position in a goto program |
Definition at line 600 of file character_refine_preprocess.cpp.
References code_function_callt::arguments(), in_interval_expr(), code_function_callt::lhs(), and messaget::result().
Referenced by convert_is_ISO_control_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(I)Z.
target | a position in a goto program |
Definition at line 615 of file character_refine_preprocess.cpp.
References convert_is_ISO_control_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isJavaIdentifierPart:(C)Z.
TODO: For now we do not allow currency symbol, connecting punctuation, combining mark, non-spacing mark
target | a position in a goto program |
Definition at line 627 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_unicode_identifier_part().
Referenced by convert_is_java_letter_or_digit(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierPart:(I)Z.
target | a position in a goto program |
Definition at line 637 of file character_refine_preprocess.cpp.
References convert_is_unicode_identifier_part_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierStart:(C)Z.
TODO: For now we only allow letters and letter numbers. The java specification for this function is not precise on the other characters.
target | a position in a goto program |
Definition at line 650 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_unicode_identifier_start().
Referenced by convert_is_java_identifier_start_int(), convert_is_java_letter(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierStart:(I)Z.
target | a position in a goto program |
Definition at line 660 of file character_refine_preprocess.cpp.
References convert_is_java_identifier_start_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isJavaLetter:(C)Z.
target | a position in a goto program |
Definition at line 669 of file character_refine_preprocess.cpp.
References convert_is_java_identifier_start_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method isJavaLetterOrDigit:(C)Z.
target | a position in a goto program |
Definition at line 678 of file character_refine_preprocess.cpp.
References convert_is_java_identifier_part_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(C)Z.
target | a position in a goto program |
Definition at line 687 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_letter().
Referenced by convert_is_letter_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(I)Z.
target | a position in a goto program |
Definition at line 697 of file character_refine_preprocess.cpp.
References convert_is_letter_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(C)Z.
target | a position in a goto program |
Definition at line 716 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_digit().
Referenced by convert_is_letter_or_digit_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(I)Z.
target | a position in a goto program |
Definition at line 726 of file character_refine_preprocess.cpp.
References convert_is_letter_or_digit_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isLowSurrogate:(C)Z.
target | a position in a goto program |
Definition at line 758 of file character_refine_preprocess.cpp.
References code_function_callt::arguments(), in_interval_expr(), code_function_callt::lhs(), and messaget::result().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isLowerCase:(C)Z.
TODO: For now we only consider ASCII characters
target | a position in a goto program |
Definition at line 737 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_ascii_lower_case().
Referenced by convert_is_lower_case_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isLowerCase:(I)Z.
TODO: For now we only consider ASCII characters
target | a position in a goto program |
Definition at line 749 of file character_refine_preprocess.cpp.
References convert_is_lower_case_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isMirrored:(C)Z.
TODO: For now only ASCII characters are considered
target | a position in a goto program |
Definition at line 787 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_mirrored().
Referenced by convert_is_mirrored_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isMirrored:(I)Z.
TODO: For now only ASCII characters are considered
target | a position in a goto program |
Definition at line 799 of file character_refine_preprocess.cpp.
References convert_is_mirrored_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isSpace:(C)Z.
target | a position in a goto program |
Definition at line 808 of file character_refine_preprocess.cpp.
References convert_is_whitespace_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(C)Z.
target | a position in a goto program |
Definition at line 831 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_space_char().
Referenced by convert_is_space_char_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(I)Z.
target | a position in a goto program |
Definition at line 841 of file character_refine_preprocess.cpp.
References convert_is_space_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isSupplementaryCodePoint:(I)Z.
target | a position in a goto program |
Definition at line 861 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_supplementary_code_point().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogate:(C)Z.
target | a position in a goto program |
Definition at line 881 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_surrogate().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogatePair:(CC)Z.
target | a position in a goto program |
Definition at line 891 of file character_refine_preprocess.cpp.
References code_function_callt::arguments(), in_interval_expr(), code_function_callt::lhs(), and messaget::result().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(C)Z.
target | a position in a goto program |
Definition at line 924 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_title_case().
Referenced by convert_is_title_case_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(I)Z.
target | a position in a goto program |
Definition at line 934 of file character_refine_preprocess.cpp.
References convert_is_title_case_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(C)Z.
target | a position in a goto program |
Definition at line 985 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_unicode_identifier_part().
Referenced by convert_is_java_identifier_part_int(), convert_is_unicode_identifier_part_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(I)Z.
target | a position in a goto program |
Definition at line 995 of file character_refine_preprocess.cpp.
References convert_is_unicode_identifier_part_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(C)Z.
target | a position in a goto program |
Definition at line 1016 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_unicode_identifier_start().
Referenced by convert_is_unicode_identifier_start_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(I)Z.
target | a position in a goto program |
Definition at line 1026 of file character_refine_preprocess.cpp.
References convert_is_unicode_identifier_start_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isUpperCase:(C)Z.
TODO: For now we only consider ASCII characters
target | a position in a goto program |
Definition at line 1037 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_ascii_upper_case().
Referenced by convert_is_upper_case_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isUpperCase:(I)Z.
target | a position in a goto program |
Definition at line 1047 of file character_refine_preprocess.cpp.
References convert_is_upper_case_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isValidCodePoint:(I)Z.
target | a position in a goto program |
Definition at line 1067 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_valid_code_point().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(C)Z.
target | a position in a goto program |
Definition at line 1099 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_is_whitespace().
Referenced by convert_is_space(), convert_is_whitespace_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(I)Z.
target | a position in a goto program |
Definition at line 1109 of file character_refine_preprocess.cpp.
References convert_is_whitespace_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.lowSurrogate:(I)C.
target | a position in a goto program |
Definition at line 1132 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_low_surrogate().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.reverseBytes:(C)C.
target | a position in a goto program |
Definition at line 1155 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_reverse_bytes().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.toChars:(I)[C.
target | a position in a goto program |
Definition at line 1188 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_to_chars().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.toCodePoint:(CC)I.
target | a position in a goto program |
Definition at line 1197 of file character_refine_preprocess.cpp.
References code_function_callt::arguments(), from_integer(), code_function_callt::lhs(), pair_value(), and messaget::result().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(C)C.
target | a position in a goto program |
Definition at line 1243 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_to_lower_case().
Referenced by convert_to_lower_case_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(I)I.
target | a position in a goto program |
Definition at line 1253 of file character_refine_preprocess.cpp.
References convert_to_lower_case_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(C)C.
target | a position in a goto program |
Definition at line 1299 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_to_title_case().
Referenced by convert_to_title_case_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(I)I.
target | a position in a goto program |
Definition at line 1309 of file character_refine_preprocess.cpp.
References convert_to_title_case_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(C)C.
target | a position in a goto program |
Definition at line 1336 of file character_refine_preprocess.cpp.
References convert_char_function(), and expr_of_to_upper_case().
Referenced by convert_to_upper_case_int(), and initialize_conversion_table().
|
staticprivate |
Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(I)I.
target | a position in a goto program |
Definition at line 1346 of file character_refine_preprocess.cpp.
References convert_to_upper_case_char().
Referenced by initialize_conversion_table().
|
staticprivate |
Determines the number of char values needed to represent the specified character (Unicode code point).
expr | An expression of type character |
type | A type for the output |
Definition at line 71 of file character_refine_preprocess.cpp.
References from_integer().
Referenced by convert_char_count().
|
staticprivate |
Casts the given expression to the given type.
Definition at line 91 of file character_refine_preprocess.cpp.
Referenced by convert_char_value().
|
staticprivate |
Returns the leading surrogate (a high surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding.
expr | An expression of type character |
type | A type for the output |
Definition at line 314 of file character_refine_preprocess.cpp.
References from_integer().
Referenced by convert_high_surrogate(), and expr_of_to_chars().
|
staticprivate |
Determines if the specified character (Unicode code point) is alphabetic.
TODO: for now this is only for ASCII characters, the following unicode categorise are not yet considered: TITLECASE_LETTER MODIFIER_LETTER OTHER_LETTER LETTER_NUMBER and contributory property Other_Alphabetic as defined by the Unicode Standard.
expr | An expression of type character |
type | A type for the output |
Definition at line 380 of file character_refine_preprocess.cpp.
References expr_of_is_letter().
Referenced by convert_is_alphabetic().
|
staticprivate |
Determines if the specified character is an ASCII lowercase character.
chr | An expression of type character |
type | A type for the output |
Definition at line 338 of file character_refine_preprocess.cpp.
References in_interval_expr().
Referenced by convert_is_lower_case_char(), expr_of_is_letter(), and expr_of_to_upper_case().
|
staticprivate |
Determines if the specified character is an ASCII uppercase character.
expr | An expression of type character |
type | A type for the output |
Definition at line 348 of file character_refine_preprocess.cpp.
References in_interval_expr().
Referenced by convert_is_upper_case_char(), expr_of_is_letter(), and expr_of_to_lower_case().
|
staticprivate |
Determines whether the specified character (Unicode code point) is in the Basic Multilingual Plane (BMP).
Such code points can be represented using a single char.
expr | An expression of type character |
type | A type for the output |
Definition at line 402 of file character_refine_preprocess.cpp.
References from_integer(), and exprt::type().
Referenced by convert_is_bmp_code_point(), and expr_of_to_chars().
|
staticprivate |
Determines if a character is defined in Unicode.
expr | An expression of type character |
type | A type for the output |
Definition at line 423 of file character_refine_preprocess.cpp.
References disjunction(), from_integer(), in_interval_expr(), and exprt::type().
Referenced by convert_is_defined_char().
|
staticprivate |
Determines if the specified character is a digit.
A character is a digit if its general category type, provided by Character.getType(ch), is DECIMAL_DIGIT_NUMBER.
TODO: for now we only support these ranges of digits: '' through '', ISO-LATIN-1 digits ('0' through '9') '' through '', Arabic-Indic digits '' through '', Extended Arabic-Indic digits '' through '', Devanagari digits '' through '', Fullwidth digits Many other character ranges contain digits as well.
chr | An expression of type character |
type | A type for the output |
Definition at line 487 of file character_refine_preprocess.cpp.
References in_interval_expr().
Referenced by convert_is_digit_char(), convert_is_letter_or_digit_char(), expr_of_is_letter_or_digit(), and expr_of_is_unicode_identifier_part().
|
staticprivate |
Determines if the given char value is a Unicode high-surrogate code unit (also known as leading-surrogate code unit).
expr | An expression of type character |
type | A type for the output |
Definition at line 525 of file character_refine_preprocess.cpp.
References in_interval_expr().
Referenced by convert_is_high_surrogate().
|
staticprivate |
Determines if the character is one of ignorable in a Java identifier, that is, it is in one of these ranges: '' through '' '' through '' '' through ''.
TODO: For now, we ignore the FORMAT general category value
expr | An expression of type character |
type | A type for the output |
Definition at line 549 of file character_refine_preprocess.cpp.
References in_interval_expr().
Referenced by convert_is_identifier_ignorable_char(), and expr_of_is_unicode_identifier_part().
|
staticprivate |
Determines if the specified character is a letter.
TODO: for now this is only for ASCII characters, the following unicode categories are not yet considered: TITLECASE_LETTER MODIFIER_LETTER OTHER_LETTER LETTER_NUMBER
expr | An expression of type character |
type | A type for the output |
Definition at line 362 of file character_refine_preprocess.cpp.
References expr_of_is_ascii_lower_case(), and expr_of_is_ascii_upper_case().
Referenced by convert_is_letter_char(), expr_of_is_alphabetic(), expr_of_is_letter_or_digit(), and expr_of_is_unicode_identifier_start().
|
staticprivate |
Determines if the specified character is in the LETTER_NUMBER category of Unicode.
expr | An expression of type character |
type | A type for the output |
Definition at line 945 of file character_refine_preprocess.cpp.
References in_interval_expr(), and in_list_expr().
Referenced by expr_of_is_unicode_identifier_start().
|
staticprivate |
Determines if the specified character is a letter or digit.
chr | An expression of type character |
type | A type for the output |
Definition at line 707 of file character_refine_preprocess.cpp.
References expr_of_is_digit(), and expr_of_is_letter().
|
staticprivate |
Determines whether the character is mirrored according to the Unicode specification.
TODO: For now only ASCII characters are considered
expr | An expression of type character |
type | A type for the output |
Definition at line 776 of file character_refine_preprocess.cpp.
References in_list_expr().
Referenced by convert_is_mirrored_char().
|
staticprivate |
Determines if the specified character is white space according to Unicode (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR)
expr | An expression of type character |
type | A type for the output |
Definition at line 818 of file character_refine_preprocess.cpp.
References in_interval_expr(), and in_list_expr().
Referenced by convert_is_space_char().
|
staticprivate |
Determines whether the specified character (Unicode code point) is in the supplementary character range.
expr | An expression of type character |
type | A type for the output |
Definition at line 852 of file character_refine_preprocess.cpp.
References from_integer(), and exprt::type().
Referenced by convert_is_supplementary_code_point().
|
staticprivate |
Determines if the given char value is a Unicode surrogate code unit.
expr | An expression of type character |
type | A type for the output |
Definition at line 872 of file character_refine_preprocess.cpp.
References in_interval_expr().
Referenced by convert_is_surrogate().
|
staticprivate |
Determines if the specified character is a titlecase character.
expr | An expression of type character |
type | A type for the output |
Definition at line 908 of file character_refine_preprocess.cpp.
References disjunction(), in_interval_expr(), and in_list_expr().
Referenced by convert_is_title_case_char().
|
staticprivate |
Determines if the character may be part of a Unicode identifier.
TODO: For now we do not allow connecting punctuation, combining mark, non-spacing mark
expr | An expression of type character |
type | A type for the output |
Definition at line 972 of file character_refine_preprocess.cpp.
References disjunction(), expr_of_is_digit(), expr_of_is_identifier_ignorable(), and expr_of_is_unicode_identifier_start().
Referenced by convert_is_java_identifier_part_char(), and convert_is_unicode_identifier_part_char().
|
staticprivate |
Determines if the specified character is permissible as the first character in a Unicode identifier.
chr | An expression of type character |
type | A type for the output |
Definition at line 1006 of file character_refine_preprocess.cpp.
References expr_of_is_letter(), and expr_of_is_letter_number().
Referenced by convert_is_java_identifier_start_char(), convert_is_unicode_identifier_start_char(), and expr_of_is_unicode_identifier_part().
|
staticprivate |
Determines whether the specified code point is a valid Unicode code point value.
That is, in the range of integers from 0 to 0x10FFFF
chr | An expression of type character |
type | A type for the output |
Definition at line 1058 of file character_refine_preprocess.cpp.
References from_integer(), and exprt::type().
Referenced by convert_is_valid_code_point().
|
staticprivate |
Determines if the specified character is white space according to Java.
It is the case when it one of the following: * a Unicode space character (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR) but is not also a non-breaking space ('', '', ''). * it is one of these: U+0009 U+000A U+000B U+000C U+000D U+001C U+001D U+001E U+001F
expr | An expression of type character |
type | A type for the output |
Definition at line 1082 of file character_refine_preprocess.cpp.
References disjunction(), in_interval_expr(), and in_list_expr().
Referenced by convert_is_whitespace_char().
|
staticprivate |
Returns the trailing surrogate (a low surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding.
expr | An expression of type character |
type | A type for the output |
Definition at line 1121 of file character_refine_preprocess.cpp.
References from_integer().
Referenced by convert_low_surrogate(), and expr_of_to_chars().
|
staticprivate |
Returns the value obtained by reversing the order of the bytes in the specified char value.
expr | An expression of type character |
type | A type for the output |
Definition at line 1144 of file character_refine_preprocess.cpp.
References from_integer().
Referenced by convert_reverse_bytes().
|
staticprivate |
Converts the specified character (Unicode code point) to its UTF-16 representation stored in a char array.
If the specified code point is a BMP (Basic Multilingual Plane or Plane 0) value, the resulting char array has the same value as codePoint. If the specified code point is a supplementary code point, the resulting char array has the corresponding surrogate pair.
expr | An expression of type character |
type | A type for the output |
Definition at line 1170 of file character_refine_preprocess.cpp.
References char_type(), exprt::copy_to_operands(), expr_of_high_surrogate(), expr_of_is_bmp_code_point(), expr_of_low_surrogate(), exprt::move_to_operands(), typet::subtype(), and to_array_type().
Referenced by convert_to_chars().
|
staticprivate |
Converts the character argument to lowercase.
TODO: For now we only consider ASCII characters but ultimately we should use case mapping information from the UnicodeData file
chr | An expression of type character |
type | A type for the output |
Definition at line 1230 of file character_refine_preprocess.cpp.
References expr_of_is_ascii_upper_case(), and from_integer().
Referenced by convert_to_lower_case_char().
|
staticprivate |
Converts the character argument to titlecase.
chr | An expression of type character |
type | A type for the output |
Definition at line 1263 of file character_refine_preprocess.cpp.
References from_integer(), in_interval_expr(), and in_list_expr().
Referenced by convert_to_title_case_char().
|
staticprivate |
Converts the character argument to uppercase.
TODO: For now we only consider ASCII characters but ultimately we should use case mapping information from the UnicodeData file
chr | An expression of type character |
type | A type for the output |
Definition at line 1323 of file character_refine_preprocess.cpp.
References expr_of_is_ascii_lower_case(), and from_integer().
Referenced by convert_to_upper_case_char().
|
staticprivate |
The returned expression is true when the first argument is in the interval defined by the lower and upper bounds (included)
arg | Expression we want to bound |
lower_bound | Integer lower bound |
upper_bound | Integer upper bound |
Definition at line 42 of file character_refine_preprocess.cpp.
References from_integer(), and exprt::type().
Referenced by convert_digit_char(), convert_is_ideographic(), convert_is_ISO_control_char(), convert_is_low_surrogate(), convert_is_surrogate_pair(), expr_of_is_ascii_lower_case(), expr_of_is_ascii_upper_case(), expr_of_is_defined(), expr_of_is_digit(), expr_of_is_high_surrogate(), expr_of_is_identifier_ignorable(), expr_of_is_letter_number(), expr_of_is_space_char(), expr_of_is_surrogate(), expr_of_is_title_case(), expr_of_is_whitespace(), and expr_of_to_title_case().
|
staticprivate |
The returned expression is true when the given character is equal to one of the element in the list.
chr | An expression of type character |
list | A list of integer representing unicode characters |
Definition at line 57 of file character_refine_preprocess.cpp.
References disjunction(), from_integer(), and exprt::type().
Referenced by expr_of_is_letter_number(), expr_of_is_mirrored(), expr_of_is_space_char(), expr_of_is_title_case(), expr_of_is_whitespace(), and expr_of_to_title_case().
void character_refine_preprocesst::initialize_conversion_table | ( | ) |
fill maps with correspondance from java method names to conversion functions
Definition at line 1374 of file character_refine_preprocess.cpp.
References conversion_table, convert_char_count(), convert_char_value(), convert_compare(), convert_digit_char(), convert_digit_int(), convert_for_digit(), convert_get_directionality_char(), convert_get_directionality_int(), convert_get_numeric_value_char(), convert_get_numeric_value_int(), convert_get_type_char(), convert_get_type_int(), convert_hash_code(), convert_high_surrogate(), convert_is_alphabetic(), convert_is_bmp_code_point(), convert_is_defined_char(), convert_is_defined_int(), convert_is_digit_char(), convert_is_digit_int(), convert_is_high_surrogate(), convert_is_identifier_ignorable_char(), convert_is_identifier_ignorable_int(), convert_is_ideographic(), convert_is_ISO_control_char(), convert_is_ISO_control_int(), convert_is_java_identifier_part_char(), convert_is_java_identifier_part_int(), convert_is_java_identifier_start_char(), convert_is_java_identifier_start_int(), convert_is_java_letter(), convert_is_java_letter_or_digit(), convert_is_letter_char(), convert_is_letter_int(), convert_is_letter_or_digit_char(), convert_is_letter_or_digit_int(), convert_is_low_surrogate(), convert_is_lower_case_char(), convert_is_lower_case_int(), convert_is_mirrored_char(), convert_is_mirrored_int(), convert_is_space(), convert_is_space_char(), convert_is_space_char_int(), convert_is_supplementary_code_point(), convert_is_surrogate(), convert_is_surrogate_pair(), convert_is_title_case_char(), convert_is_title_case_int(), convert_is_unicode_identifier_part_char(), convert_is_unicode_identifier_part_int(), convert_is_unicode_identifier_start_char(), convert_is_unicode_identifier_start_int(), convert_is_upper_case_char(), convert_is_upper_case_int(), convert_is_valid_code_point(), convert_is_whitespace_char(), convert_is_whitespace_int(), convert_reverse_bytes(), convert_to_chars(), convert_to_code_point(), convert_to_lower_case_char(), convert_to_lower_case_int(), convert_to_title_case_char(), convert_to_title_case_int(), convert_to_upper_case_char(), and convert_to_upper_case_int().
Referenced by java_string_library_preprocesst::initialize_conversion_table().
codet character_refine_preprocesst::replace_character_call | ( | const code_function_callt & | code | ) | const |
replace function calls to functions of the Character by an affectation if possible, returns the same code otherwise.
For this method to have an effect initialize_conversion_table must have been called before.
code | the code of a function call |
Definition at line 1358 of file character_refine_preprocess.cpp.
References conversion_table, code_function_callt::function(), irept::id(), and to_symbol_expr().
Referenced by java_string_library_preprocesst::replace_character_call().
|
private |
Definition at line 39 of file character_refine_preprocess.h.
Referenced by initialize_conversion_table(), and replace_character_call().