cprover
character_refine_preprocesst Class Reference

#include <character_refine_preprocess.h>

+ Collaboration diagram for character_refine_preprocesst:

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_calltconversion_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)
 
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)
 
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)
 
static codet convert_to_chars (conversion_inputt &target)
 
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_functiontconversion_table
 

Detailed Description

Definition at line 28 of file character_refine_preprocess.h.

Member Typedef Documentation

◆ conversion_functiont

typedef codet(* character_refine_preprocesst::conversion_functiont) (conversion_inputt &target)
private

Definition at line 36 of file character_refine_preprocess.h.

◆ conversion_inputt

Member Function Documentation

◆ convert_char_count()

codet character_refine_preprocesst::convert_char_count ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.charCount:(I)I.

Parameters
targeta position in a goto program

Definition at line 82 of file character_refine_preprocess.cpp.

◆ convert_char_function()

codet character_refine_preprocesst::convert_char_function ( exprt(*)(const exprt &chr, const typet &type)  expr_function,
conversion_inputt target 
)
staticprivate

converts based on a function on expressions

Parameters
expr_functionA reference to a function on expressions
targetA position in a goto program

Definition at line 24 of file character_refine_preprocess.cpp.

◆ convert_char_value()

codet character_refine_preprocesst::convert_char_value ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.charValue:()C.

Parameters
targeta position in a goto program

Definition at line 100 of file character_refine_preprocess.cpp.

◆ convert_compare()

codet character_refine_preprocesst::convert_compare ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.compare:(CC)I.

Parameters
targeta position in a goto program

Definition at line 110 of file character_refine_preprocess.cpp.

◆ convert_digit_char()

codet character_refine_preprocesst::convert_digit_char ( conversion_inputt target)
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.

Parameters
targeta position in a goto program
Returns
code assigning the result of the Character.digit function to the left-hand-side of the given target

Definition at line 135 of file character_refine_preprocess.cpp.

◆ convert_digit_int()

codet character_refine_preprocesst::convert_digit_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.digit:(II)I.

Parameters
targeta position in a goto program

Definition at line 212 of file character_refine_preprocess.cpp.

◆ convert_for_digit()

codet character_refine_preprocesst::convert_for_digit ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 222 of file character_refine_preprocess.cpp.

◆ convert_get_directionality_char()

codet character_refine_preprocesst::convert_get_directionality_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(C)I.

Parameters
targeta position in a goto program

Definition at line 241 of file character_refine_preprocess.cpp.

◆ convert_get_directionality_int()

codet character_refine_preprocesst::convert_get_directionality_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(I)I.

Parameters
targeta position in a goto program

Definition at line 252 of file character_refine_preprocess.cpp.

◆ convert_get_numeric_value_char()

codet character_refine_preprocesst::convert_get_numeric_value_char ( conversion_inputt target)
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 262 of file character_refine_preprocess.cpp.

◆ convert_get_numeric_value_int()

codet character_refine_preprocesst::convert_get_numeric_value_int ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 273 of file character_refine_preprocess.cpp.

◆ convert_get_type_char()

codet character_refine_preprocesst::convert_get_type_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.getType:(C)I.

Parameters
targeta position in a goto program

Definition at line 282 of file character_refine_preprocess.cpp.

◆ convert_get_type_int()

codet character_refine_preprocesst::convert_get_type_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.getType:(I)I.

Parameters
targeta position in a goto program

Definition at line 293 of file character_refine_preprocess.cpp.

◆ convert_hash_code()

codet character_refine_preprocesst::convert_hash_code ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.hashCode:()I.

Parameters
targeta position in a goto program

Definition at line 302 of file character_refine_preprocess.cpp.

◆ convert_high_surrogate()

static codet character_refine_preprocesst::convert_high_surrogate ( conversion_inputt target)
staticprivate

◆ convert_is_alphabetic()

codet character_refine_preprocesst::convert_is_alphabetic ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isAlphabetic:(I)Z.

Parameters
targeta position in a goto program

Definition at line 381 of file character_refine_preprocess.cpp.

◆ convert_is_bmp_code_point()

codet character_refine_preprocesst::convert_is_bmp_code_point ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isBmpCodePoint:(I)Z.

Parameters
targeta position in a goto program

Definition at line 406 of file character_refine_preprocess.cpp.

◆ convert_is_defined_char()

codet character_refine_preprocesst::convert_is_defined_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isDefined:(C)Z.

Parameters
targeta position in a goto program

Definition at line 452 of file character_refine_preprocess.cpp.

◆ convert_is_defined_int()

codet character_refine_preprocesst::convert_is_defined_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isDefined:(I)Z.

Parameters
targeta position in a goto program

Definition at line 462 of file character_refine_preprocess.cpp.

◆ convert_is_digit_char()

codet character_refine_preprocesst::convert_is_digit_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isDigit:(C)Z.

Parameters
targeta position in a goto program

Definition at line 500 of file character_refine_preprocess.cpp.

◆ convert_is_digit_int()

codet character_refine_preprocesst::convert_is_digit_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.digit:(I)Z.

Parameters
targeta position in a goto program

Definition at line 510 of file character_refine_preprocess.cpp.

◆ convert_is_high_surrogate()

codet character_refine_preprocesst::convert_is_high_surrogate ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isHighSurrogate:(C)Z.

Parameters
targeta position in a goto program

Definition at line 531 of file character_refine_preprocess.cpp.

◆ convert_is_identifier_ignorable_char()

codet character_refine_preprocesst::convert_is_identifier_ignorable_char ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 563 of file character_refine_preprocess.cpp.

◆ convert_is_identifier_ignorable_int()

codet character_refine_preprocesst::convert_is_identifier_ignorable_int ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 575 of file character_refine_preprocess.cpp.

◆ convert_is_ideographic()

codet character_refine_preprocesst::convert_is_ideographic ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isIdeographic:(I)Z.

Parameters
targeta position in a goto program

Definition at line 584 of file character_refine_preprocess.cpp.

◆ convert_is_ISO_control_char()

codet character_refine_preprocesst::convert_is_ISO_control_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(C)Z.

Parameters
targeta position in a goto program

Definition at line 598 of file character_refine_preprocess.cpp.

◆ convert_is_ISO_control_int()

codet character_refine_preprocesst::convert_is_ISO_control_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(I)Z.

Parameters
targeta position in a goto program

Definition at line 613 of file character_refine_preprocess.cpp.

◆ convert_is_java_identifier_part_char()

codet character_refine_preprocesst::convert_is_java_identifier_part_char ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 625 of file character_refine_preprocess.cpp.

◆ convert_is_java_identifier_part_int()

codet character_refine_preprocesst::convert_is_java_identifier_part_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierPart:(I)Z.

Parameters
targeta position in a goto program

Definition at line 635 of file character_refine_preprocess.cpp.

◆ convert_is_java_identifier_start_char()

codet character_refine_preprocesst::convert_is_java_identifier_start_char ( conversion_inputt target)
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.

Parameters
targeta position in a goto program

Definition at line 648 of file character_refine_preprocess.cpp.

◆ convert_is_java_identifier_start_int()

codet character_refine_preprocesst::convert_is_java_identifier_start_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierStart:(I)Z.

Parameters
targeta position in a goto program

Definition at line 658 of file character_refine_preprocess.cpp.

◆ convert_is_java_letter()

codet character_refine_preprocesst::convert_is_java_letter ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isJavaLetter:(C)Z.

Parameters
targeta position in a goto program

Definition at line 667 of file character_refine_preprocess.cpp.

◆ convert_is_java_letter_or_digit()

codet character_refine_preprocesst::convert_is_java_letter_or_digit ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method isJavaLetterOrDigit:(C)Z.

Parameters
targeta position in a goto program

Definition at line 676 of file character_refine_preprocess.cpp.

◆ convert_is_letter_char()

codet character_refine_preprocesst::convert_is_letter_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(C)Z.

Parameters
targeta position in a goto program

Definition at line 685 of file character_refine_preprocess.cpp.

◆ convert_is_letter_int()

codet character_refine_preprocesst::convert_is_letter_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(I)Z.

Parameters
targeta position in a goto program

Definition at line 695 of file character_refine_preprocess.cpp.

◆ convert_is_letter_or_digit_char()

codet character_refine_preprocesst::convert_is_letter_or_digit_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(C)Z.

Parameters
targeta position in a goto program

Definition at line 714 of file character_refine_preprocess.cpp.

◆ convert_is_letter_or_digit_int()

codet character_refine_preprocesst::convert_is_letter_or_digit_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(I)Z.

Parameters
targeta position in a goto program

Definition at line 724 of file character_refine_preprocess.cpp.

◆ convert_is_low_surrogate()

codet character_refine_preprocesst::convert_is_low_surrogate ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isLowSurrogate:(C)Z.

Parameters
targeta position in a goto program

Definition at line 756 of file character_refine_preprocess.cpp.

◆ convert_is_lower_case_char()

codet character_refine_preprocesst::convert_is_lower_case_char ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 735 of file character_refine_preprocess.cpp.

◆ convert_is_lower_case_int()

codet character_refine_preprocesst::convert_is_lower_case_int ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 747 of file character_refine_preprocess.cpp.

◆ convert_is_mirrored_char()

codet character_refine_preprocesst::convert_is_mirrored_char ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 786 of file character_refine_preprocess.cpp.

◆ convert_is_mirrored_int()

codet character_refine_preprocesst::convert_is_mirrored_int ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 798 of file character_refine_preprocess.cpp.

◆ convert_is_space()

codet character_refine_preprocesst::convert_is_space ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isSpace:(C)Z.

Parameters
targeta position in a goto program

Definition at line 807 of file character_refine_preprocess.cpp.

◆ convert_is_space_char()

codet character_refine_preprocesst::convert_is_space_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(C)Z.

Parameters
targeta position in a goto program

Definition at line 831 of file character_refine_preprocess.cpp.

◆ convert_is_space_char_int()

codet character_refine_preprocesst::convert_is_space_char_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(I)Z.

Parameters
targeta position in a goto program

Definition at line 841 of file character_refine_preprocess.cpp.

◆ convert_is_supplementary_code_point()

codet character_refine_preprocesst::convert_is_supplementary_code_point ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isSupplementaryCodePoint:(I)Z.

Parameters
targeta position in a goto program

Definition at line 862 of file character_refine_preprocess.cpp.

◆ convert_is_surrogate()

codet character_refine_preprocesst::convert_is_surrogate ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogate:(C)Z.

Parameters
targeta position in a goto program

Definition at line 883 of file character_refine_preprocess.cpp.

◆ convert_is_surrogate_pair()

codet character_refine_preprocesst::convert_is_surrogate_pair ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogatePair:(CC)Z.

Parameters
targeta position in a goto program

Definition at line 893 of file character_refine_preprocess.cpp.

◆ convert_is_title_case_char()

codet character_refine_preprocesst::convert_is_title_case_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(C)Z.

Parameters
targeta position in a goto program

Definition at line 927 of file character_refine_preprocess.cpp.

◆ convert_is_title_case_int()

codet character_refine_preprocesst::convert_is_title_case_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(I)Z.

Parameters
targeta position in a goto program

Definition at line 937 of file character_refine_preprocess.cpp.

◆ convert_is_unicode_identifier_part_char()

codet character_refine_preprocesst::convert_is_unicode_identifier_part_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(C)Z.

Parameters
targeta position in a goto program

Definition at line 989 of file character_refine_preprocess.cpp.

◆ convert_is_unicode_identifier_part_int()

codet character_refine_preprocesst::convert_is_unicode_identifier_part_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(I)Z.

Parameters
targeta position in a goto program

Definition at line 999 of file character_refine_preprocess.cpp.

◆ convert_is_unicode_identifier_start_char()

codet character_refine_preprocesst::convert_is_unicode_identifier_start_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(C)Z.

Parameters
targeta position in a goto program

Definition at line 1020 of file character_refine_preprocess.cpp.

◆ convert_is_unicode_identifier_start_int()

codet character_refine_preprocesst::convert_is_unicode_identifier_start_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(I)Z.

Parameters
targeta position in a goto program

Definition at line 1030 of file character_refine_preprocess.cpp.

◆ convert_is_upper_case_char()

codet character_refine_preprocesst::convert_is_upper_case_char ( conversion_inputt target)
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

Parameters
targeta position in a goto program

Definition at line 1041 of file character_refine_preprocess.cpp.

◆ convert_is_upper_case_int()

codet character_refine_preprocesst::convert_is_upper_case_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isUpperCase:(I)Z.

Parameters
targeta position in a goto program

Definition at line 1051 of file character_refine_preprocess.cpp.

◆ convert_is_valid_code_point()

codet character_refine_preprocesst::convert_is_valid_code_point ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isValidCodePoint:(I)Z.

Parameters
targeta position in a goto program

Definition at line 1072 of file character_refine_preprocess.cpp.

◆ convert_is_whitespace_char()

codet character_refine_preprocesst::convert_is_whitespace_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(C)Z.

Parameters
targeta position in a goto program

Definition at line 1105 of file character_refine_preprocess.cpp.

◆ convert_is_whitespace_int()

codet character_refine_preprocesst::convert_is_whitespace_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(I)Z.

Parameters
targeta position in a goto program

Definition at line 1115 of file character_refine_preprocess.cpp.

◆ convert_low_surrogate()

static codet character_refine_preprocesst::convert_low_surrogate ( conversion_inputt target)
staticprivate

◆ convert_reverse_bytes()

codet character_refine_preprocesst::convert_reverse_bytes ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.reverseBytes:(C)C.

Parameters
targeta position in a goto program

Definition at line 1151 of file character_refine_preprocess.cpp.

◆ convert_to_chars()

static codet character_refine_preprocesst::convert_to_chars ( conversion_inputt target)
staticprivate

◆ convert_to_lower_case_char()

codet character_refine_preprocesst::convert_to_lower_case_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(C)C.

Parameters
targeta position in a goto program

Definition at line 1178 of file character_refine_preprocess.cpp.

◆ convert_to_lower_case_int()

codet character_refine_preprocesst::convert_to_lower_case_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(I)I.

Parameters
targeta position in a goto program

Definition at line 1188 of file character_refine_preprocess.cpp.

◆ convert_to_title_case_char()

codet character_refine_preprocesst::convert_to_title_case_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(C)C.

Parameters
targeta position in a goto program

Definition at line 1229 of file character_refine_preprocess.cpp.

◆ convert_to_title_case_int()

codet character_refine_preprocesst::convert_to_title_case_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(I)I.

Parameters
targeta position in a goto program

Definition at line 1239 of file character_refine_preprocess.cpp.

◆ convert_to_upper_case_char()

codet character_refine_preprocesst::convert_to_upper_case_char ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(C)C.

Parameters
targeta position in a goto program

Definition at line 1265 of file character_refine_preprocess.cpp.

◆ convert_to_upper_case_int()

codet character_refine_preprocesst::convert_to_upper_case_int ( conversion_inputt target)
staticprivate

Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(I)I.

Parameters
targeta position in a goto program

Definition at line 1275 of file character_refine_preprocess.cpp.

◆ expr_of_char_count()

exprt character_refine_preprocesst::expr_of_char_count ( const exprt chr,
const typet type 
)
staticprivate

Determines the number of char values needed to represent the specified character (Unicode code point).

Parameters
chrAn expression of type character
typeA type for the output
Returns
A integer expression of the given type

Definition at line 71 of file character_refine_preprocess.cpp.

◆ expr_of_char_value()

exprt character_refine_preprocesst::expr_of_char_value ( const exprt chr,
const typet type 
)
staticprivate

Casts the given expression to the given type.

Returns
An expression of the given type

Definition at line 91 of file character_refine_preprocess.cpp.

◆ expr_of_high_surrogate()

exprt character_refine_preprocesst::expr_of_high_surrogate ( const exprt chr,
const typet type 
)
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.

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 313 of file character_refine_preprocess.cpp.

◆ expr_of_is_alphabetic()

exprt character_refine_preprocesst::expr_of_is_alphabetic ( const exprt chr,
const typet type 
)
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.

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 372 of file character_refine_preprocess.cpp.

◆ expr_of_is_ascii_lower_case()

exprt character_refine_preprocesst::expr_of_is_ascii_lower_case ( const exprt chr,
const typet type 
)
staticprivate

Determines if the specified character is an ASCII lowercase character.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 328 of file character_refine_preprocess.cpp.

◆ expr_of_is_ascii_upper_case()

exprt character_refine_preprocesst::expr_of_is_ascii_upper_case ( const exprt chr,
const typet type 
)
staticprivate

Determines if the specified character is an ASCII uppercase character.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 339 of file character_refine_preprocess.cpp.

◆ expr_of_is_bmp_code_point()

exprt character_refine_preprocesst::expr_of_is_bmp_code_point ( const exprt chr,
const typet type 
)
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.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 394 of file character_refine_preprocess.cpp.

◆ expr_of_is_defined()

exprt character_refine_preprocesst::expr_of_is_defined ( const exprt chr,
const typet type 
)
staticprivate

Determines if a character is defined in Unicode.

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 417 of file character_refine_preprocess.cpp.

◆ expr_of_is_digit()

exprt character_refine_preprocesst::expr_of_is_digit ( const exprt chr,
const typet type 
)
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.

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 482 of file character_refine_preprocess.cpp.

◆ expr_of_is_high_surrogate()

exprt character_refine_preprocesst::expr_of_is_high_surrogate ( const exprt chr,
const typet type 
)
staticprivate

Determines if the given char value is a Unicode high-surrogate code unit (also known as leading-surrogate code unit).

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 521 of file character_refine_preprocess.cpp.

◆ expr_of_is_identifier_ignorable()

exprt character_refine_preprocesst::expr_of_is_identifier_ignorable ( const exprt chr,
const typet type 
)
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

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 546 of file character_refine_preprocess.cpp.

◆ expr_of_is_letter()

exprt character_refine_preprocesst::expr_of_is_letter ( const exprt chr,
const typet type 
)
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

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 354 of file character_refine_preprocess.cpp.

◆ expr_of_is_letter_number()

exprt character_refine_preprocesst::expr_of_is_letter_number ( const exprt chr,
const typet type 
)
staticprivate

Determines if the specified character is in the LETTER_NUMBER category of Unicode.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 948 of file character_refine_preprocess.cpp.

◆ expr_of_is_letter_or_digit()

exprt character_refine_preprocesst::expr_of_is_letter_or_digit ( const exprt chr,
const typet type 
)
staticprivate

Determines if the specified character is a letter or digit.

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 705 of file character_refine_preprocess.cpp.

◆ expr_of_is_mirrored()

exprt character_refine_preprocesst::expr_of_is_mirrored ( const exprt chr,
const typet type 
)
staticprivate

Determines whether the character is mirrored according to the Unicode specification.

TODO: For now only ASCII characters are considered

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 774 of file character_refine_preprocess.cpp.

◆ expr_of_is_space_char()

exprt character_refine_preprocesst::expr_of_is_space_char ( const exprt chr,
const typet type 
)
staticprivate

Determines if the specified character is white space according to Unicode (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR)

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 817 of file character_refine_preprocess.cpp.

◆ expr_of_is_supplementary_code_point()

exprt character_refine_preprocesst::expr_of_is_supplementary_code_point ( const exprt chr,
const typet type 
)
staticprivate

Determines whether the specified character (Unicode code point) is in the supplementary character range.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 852 of file character_refine_preprocess.cpp.

◆ expr_of_is_surrogate()

exprt character_refine_preprocesst::expr_of_is_surrogate ( const exprt chr,
const typet type 
)
staticprivate

Determines if the given char value is a Unicode surrogate code unit.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 873 of file character_refine_preprocess.cpp.

◆ expr_of_is_title_case()

exprt character_refine_preprocesst::expr_of_is_title_case ( const exprt chr,
const typet type 
)
staticprivate

Determines if the specified character is a titlecase character.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 910 of file character_refine_preprocess.cpp.

◆ expr_of_is_unicode_identifier_part()

exprt character_refine_preprocesst::expr_of_is_unicode_identifier_part ( const exprt chr,
const typet type 
)
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

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 976 of file character_refine_preprocess.cpp.

◆ expr_of_is_unicode_identifier_start()

exprt character_refine_preprocesst::expr_of_is_unicode_identifier_start ( const exprt chr,
const typet type 
)
staticprivate

Determines if the specified character is permissible as the first character in a Unicode identifier.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 1010 of file character_refine_preprocess.cpp.

◆ expr_of_is_valid_code_point()

exprt character_refine_preprocesst::expr_of_is_valid_code_point ( const exprt chr,
const typet type 
)
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

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 1062 of file character_refine_preprocess.cpp.

◆ expr_of_is_whitespace()

exprt character_refine_preprocesst::expr_of_is_whitespace ( const exprt chr,
const typet type 
)
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

Parameters
chrAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 1087 of file character_refine_preprocess.cpp.

◆ expr_of_low_surrogate()

exprt character_refine_preprocesst::expr_of_low_surrogate ( const exprt chr,
const typet type 
)
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.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A integer expression of the given type

Definition at line 1127 of file character_refine_preprocess.cpp.

◆ expr_of_reverse_bytes()

exprt character_refine_preprocesst::expr_of_reverse_bytes ( const exprt chr,
const typet type 
)
staticprivate

Returns the value obtained by reversing the order of the bytes in the specified char value.

Parameters
chrAn expression of type character
typeA type for the output
Returns
A character expression of the given type

Definition at line 1140 of file character_refine_preprocess.cpp.

◆ expr_of_to_chars()

static exprt character_refine_preprocesst::expr_of_to_chars ( const exprt chr,
const typet type 
)
staticprivate

◆ expr_of_to_lower_case()

exprt character_refine_preprocesst::expr_of_to_lower_case ( const exprt chr,
const typet type 
)
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

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 1166 of file character_refine_preprocess.cpp.

◆ expr_of_to_title_case()

exprt character_refine_preprocesst::expr_of_to_title_case ( const exprt chr,
const typet type 
)
staticprivate

Converts the character argument to titlecase.

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 1198 of file character_refine_preprocess.cpp.

◆ expr_of_to_upper_case()

exprt character_refine_preprocesst::expr_of_to_upper_case ( const exprt chr,
const typet type 
)
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

Parameters
chrAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 1253 of file character_refine_preprocess.cpp.

◆ in_interval_expr()

exprt character_refine_preprocesst::in_interval_expr ( const exprt chr,
const mp_integer lower_bound,
const mp_integer upper_bound 
)
staticprivate

The returned expression is true when the first argument is in the interval defined by the lower and upper bounds (included)

Parameters
chrExpression we want to bound
lower_boundInteger lower bound
upper_boundInteger upper bound
Returns
A Boolean expression

Definition at line 42 of file character_refine_preprocess.cpp.

◆ in_list_expr()

exprt character_refine_preprocesst::in_list_expr ( const exprt chr,
const std::list< mp_integer > &  list 
)
staticprivate

The returned expression is true when the given character is equal to one of the element in the list.

Parameters
chrAn expression of type character
listA list of integer representing unicode characters
Returns
A Boolean expression

Definition at line 57 of file character_refine_preprocess.cpp.

◆ initialize_conversion_table()

void character_refine_preprocesst::initialize_conversion_table ( )

fill maps with correspondance from java method names to conversion functions

Definition at line 1303 of file character_refine_preprocess.cpp.

◆ replace_character_call()

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.

Parameters
codethe code of a function call
Returns
code where character function call get replaced by an simple instruction

Definition at line 1287 of file character_refine_preprocess.cpp.

Member Data Documentation

◆ conversion_table

std::unordered_map<irep_idt, conversion_functiont> character_refine_preprocesst::conversion_table
private

Definition at line 38 of file character_refine_preprocess.h.


The documentation for this class was generated from the following files: