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 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: '\u0000' through '\u0008' '\u000E' through '\u001B' '\u007F' through '\u009F'. 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 | |
const typedef code_function_callt & | conversion_inputt |
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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 391 of file character_refine_preprocess.cpp.
|
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 416 of file character_refine_preprocess.cpp.
|
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 462 of file character_refine_preprocess.cpp.
|
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 472 of file character_refine_preprocess.cpp.
|
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 510 of file character_refine_preprocess.cpp.
|
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 520 of file character_refine_preprocess.cpp.
|
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 541 of file character_refine_preprocess.cpp.
|
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 573 of file character_refine_preprocess.cpp.
|
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 585 of file character_refine_preprocess.cpp.
|
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 594 of file character_refine_preprocess.cpp.
|
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 608 of file character_refine_preprocess.cpp.
|
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 623 of file character_refine_preprocess.cpp.
|
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 635 of file character_refine_preprocess.cpp.
|
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 645 of file character_refine_preprocess.cpp.
|
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 658 of file character_refine_preprocess.cpp.
|
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 668 of file character_refine_preprocess.cpp.
|
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 677 of file character_refine_preprocess.cpp.
|
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 686 of file character_refine_preprocess.cpp.
|
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 695 of file character_refine_preprocess.cpp.
|
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 705 of file character_refine_preprocess.cpp.
|
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 724 of file character_refine_preprocess.cpp.
|
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 734 of file character_refine_preprocess.cpp.
|
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 766 of file character_refine_preprocess.cpp.
|
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 745 of file character_refine_preprocess.cpp.
|
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 757 of file character_refine_preprocess.cpp.
|
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 796 of file character_refine_preprocess.cpp.
|
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 808 of file character_refine_preprocess.cpp.
|
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 817 of file character_refine_preprocess.cpp.
|
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 841 of file character_refine_preprocess.cpp.
|
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 851 of file character_refine_preprocess.cpp.
|
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 872 of file character_refine_preprocess.cpp.
|
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 893 of file character_refine_preprocess.cpp.
|
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 903 of file character_refine_preprocess.cpp.
|
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 937 of file character_refine_preprocess.cpp.
|
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 947 of file character_refine_preprocess.cpp.
|
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 999 of file character_refine_preprocess.cpp.
|
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 1009 of file character_refine_preprocess.cpp.
|
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 1030 of file character_refine_preprocess.cpp.
|
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 1040 of file character_refine_preprocess.cpp.
|
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 1051 of file character_refine_preprocess.cpp.
|
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 1061 of file character_refine_preprocess.cpp.
|
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 1082 of file character_refine_preprocess.cpp.
|
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 1115 of file character_refine_preprocess.cpp.
|
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 1125 of file character_refine_preprocess.cpp.
|
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 1148 of file character_refine_preprocess.cpp.
|
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 1171 of file character_refine_preprocess.cpp.
|
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 1204 of file character_refine_preprocess.cpp.
|
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 1213 of file character_refine_preprocess.cpp.
|
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 1259 of file character_refine_preprocess.cpp.
|
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 1269 of file character_refine_preprocess.cpp.
|
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 1315 of file character_refine_preprocess.cpp.
|
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 1325 of file character_refine_preprocess.cpp.
|
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 1352 of file character_refine_preprocess.cpp.
|
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 1362 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines the number of char values needed to represent the specified character (Unicode code point).
chr | An expression of type character |
type | A type for the output |
Definition at line 71 of file character_refine_preprocess.cpp.
|
staticprivate |
Casts the given expression to the given type.
Definition at line 91 of file character_refine_preprocess.cpp.
|
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.
chr | An expression of type character |
type | A type for the output |
Definition at line 314 of file character_refine_preprocess.cpp.
|
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.
chr | An expression of type character |
type | A type for the output |
Definition at line 382 of file character_refine_preprocess.cpp.
|
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.
|
staticprivate |
Determines if the specified character is an ASCII uppercase character.
chr | An expression of type character |
type | A type for the output |
Definition at line 349 of file character_refine_preprocess.cpp.
|
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.
chr | An expression of type character |
type | A type for the output |
Definition at line 404 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines if a character is defined in Unicode.
chr | An expression of type character |
type | A type for the output |
Definition at line 427 of file character_refine_preprocess.cpp.
|
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: '\u0030' through '\u0039', ISO-LATIN-1 digits ('0' through '9') '\u0660' through '\u0669', Arabic-Indic digits '\u06F0' through '\u06F9', Extended Arabic-Indic digits '\u0966' through '\u096F', Devanagari digits '\uFF10' through '\uFF19', 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 492 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines if the given char value is a Unicode high-surrogate code unit (also known as leading-surrogate code unit).
chr | An expression of type character |
type | A type for the output |
Definition at line 531 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines if the character is one of ignorable in a Java identifier, that is, it is in one of these ranges: '\u0000' through '\u0008' '\u000E' through '\u001B' '\u007F' through '\u009F'.
TODO: For now, we ignore the FORMAT general category value
chr | An expression of type character |
type | A type for the output |
Definition at line 556 of file character_refine_preprocess.cpp.
|
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
chr | An expression of type character |
type | A type for the output |
Definition at line 364 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines if the specified character is in the LETTER_NUMBER category of Unicode.
chr | An expression of type character |
type | A type for the output |
Definition at line 958 of file character_refine_preprocess.cpp.
|
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 715 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines whether the character is mirrored according to the Unicode specification.
TODO: For now only ASCII characters are considered
chr | An expression of type character |
type | A type for the output |
Definition at line 784 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines if the specified character is white space according to Unicode (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR)
chr | An expression of type character |
type | A type for the output |
Definition at line 827 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines whether the specified character (Unicode code point) is in the supplementary character range.
chr | An expression of type character |
type | A type for the output |
Definition at line 862 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines if the given char value is a Unicode surrogate code unit.
chr | An expression of type character |
type | A type for the output |
Definition at line 883 of file character_refine_preprocess.cpp.
|
staticprivate |
Determines if the specified character is a titlecase character.
chr | An expression of type character |
type | A type for the output |
Definition at line 920 of file character_refine_preprocess.cpp.
|
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
chr | An expression of type character |
type | A type for the output |
Definition at line 986 of file character_refine_preprocess.cpp.
|
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 1020 of file character_refine_preprocess.cpp.
|
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 1072 of file character_refine_preprocess.cpp.
|
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 ('\u00A0', '\u2007', '\u202F'). * it is one of these: U+0009 U+000A U+000B U+000C U+000D U+001C U+001D U+001E U+001F
chr | An expression of type character |
type | A type for the output |
Definition at line 1097 of file character_refine_preprocess.cpp.
|
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.
chr | An expression of type character |
type | A type for the output |
Definition at line 1137 of file character_refine_preprocess.cpp.
|
staticprivate |
Returns the value obtained by reversing the order of the bytes in the specified char value.
chr | An expression of type character |
type | A type for the output |
Definition at line 1160 of file character_refine_preprocess.cpp.
|
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.
chr | An expression of type character |
type | A type for the output |
Definition at line 1186 of file character_refine_preprocess.cpp.
|
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 1246 of file character_refine_preprocess.cpp.
|
staticprivate |
Converts the character argument to titlecase.
chr | An expression of type character |
type | A type for the output |
Definition at line 1279 of file character_refine_preprocess.cpp.
|
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 1339 of file character_refine_preprocess.cpp.
|
staticprivate |
The returned expression is true when the first argument is in the interval defined by the lower and upper bounds (included)
chr | 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.
|
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.
void character_refine_preprocesst::initialize_conversion_table | ( | ) |
fill maps with correspondance from java method names to conversion functions
Definition at line 1390 of file character_refine_preprocess.cpp.
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 1374 of file character_refine_preprocess.cpp.
|
private |
Definition at line 36 of file character_refine_preprocess.h.
|
private |
Definition at line 39 of file character_refine_preprocess.h.