#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_callt &	conversion_inputt

typedef codet(*	conversion_functiont) (conversion_inputt &target)

Static Private Member Functions
static exprt	expr_of_char_count (const exprt &chr, const typet &type)
	Determines the number of char values needed to represent the specified character (Unicode code point). More...

static codet	convert_char_count (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.charCount:(I)I. More...

static exprt	expr_of_char_value (const exprt &chr, const typet &type)
	Casts the given expression to the given type. More...

static codet	convert_char_value (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.charValue:()C. More...

static codet	convert_compare (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.compare:(CC)I. More...

static codet	convert_digit_char (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.digit:(CI)I. More...

static codet	convert_digit_int (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.digit:(II)I. More...

static codet	convert_for_digit (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.forDigit:(II)C. More...

static codet	convert_get_directionality_char (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(C)I. More...

static codet	convert_get_directionality_int (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(I)I. More...

static codet	convert_get_numeric_value_char (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.getNumericValue:(C)I. More...

static codet	convert_get_numeric_value_int (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.getNumericValue:(C)I. More...

static codet	convert_get_type_char (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.getType:(C)I. More...

static codet	convert_get_type_int (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.getType:(I)I. More...

static codet	convert_hash_code (conversion_inputt &target)
	Converts function call to an assignment of an expression corresponding to the java method Character.hashCode:()I. More...

static exprt	expr_of_high_surrogate (const exprt &chr, const typet &type)
	Returns the leading surrogate (a high surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding. More...

static codet	convert_high_surrogate (conversion_inputt &target)

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_functiont >	conversion_table

Detailed Description

Definition at line 31 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 39 of file character_refine_preprocess.h.

◆ conversion_inputt

typedef const code_function_callt& character_refine_preprocesst::conversion_inputt

private

Definition at line 38 of file character_refine_preprocess.h.

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

target a position in a goto program

Definition at line 85 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_function	A reference to a function on expressions
target	A position in a goto program

Definition at line 27 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

target a position in a goto program

Definition at line 103 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

target a position in a goto program

Definition at line 113 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

target a 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 138 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

target a position in a goto program

Definition at line 215 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

target a position in a goto program

Definition at line 225 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

target a position in a goto program

Definition at line 244 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

target a position in a goto program

Definition at line 255 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 265 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

target a position in a goto program

Definition at line 276 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

target a position in a goto program

Definition at line 285 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

target a position in a goto program

Definition at line 296 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

target a position in a goto program

Definition at line 305 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

target a position in a goto program

Definition at line 384 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

target a position in a goto program

Definition at line 409 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

target a position in a goto program

Definition at line 455 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

target a position in a goto program

Definition at line 465 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

target a position in a goto program

Definition at line 503 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

target a position in a goto program

Definition at line 513 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

target a position in a goto program

Definition at line 534 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

target a position in a goto program

Definition at line 566 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

target a position in a goto program

Definition at line 578 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

target a position in a goto program

Definition at line 587 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

target a position in a goto program

Definition at line 601 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

target a position in a goto program

Definition at line 616 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

target a position in a goto program

Definition at line 628 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

target a position in a goto program

Definition at line 638 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

target a position in a goto program

Definition at line 651 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

target a position in a goto program

Definition at line 661 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

target a position in a goto program

Definition at line 670 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

target a position in a goto program

Definition at line 679 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

target a position in a goto program

Definition at line 688 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

target a position in a goto program

Definition at line 698 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

target a position in a goto program

Definition at line 717 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

target a position in a goto program

Definition at line 727 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

target a position in a goto program

Definition at line 759 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

target a position in a goto program

Definition at line 738 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

target a position in a goto program

Definition at line 750 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

target a position in a goto program

Definition at line 789 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

target a position in a goto program

Definition at line 801 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

target a position in a goto program

Definition at line 810 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

target a position in a goto program

Definition at line 834 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

target a position in a goto program

Definition at line 844 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

target a position in a goto program

Definition at line 865 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

target a position in a goto program

Definition at line 886 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

target a position in a goto program

Definition at line 896 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

target a position in a goto program

Definition at line 930 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

target a position in a goto program

Definition at line 940 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

target a position in a goto program

Definition at line 992 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

target a position in a goto program

Definition at line 1002 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

target a position in a goto program

Definition at line 1023 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

target a position in a goto program

Definition at line 1033 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

target a position in a goto program

Definition at line 1044 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

target a position in a goto program

Definition at line 1054 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

target a position in a goto program

Definition at line 1075 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

target a position in a goto program

Definition at line 1108 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

target a position in a goto program

Definition at line 1118 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

target a position in a goto program

Definition at line 1154 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

target a position in a goto program

Definition at line 1181 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

target a position in a goto program

Definition at line 1191 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

target a position in a goto program

Definition at line 1232 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

target a position in a goto program

Definition at line 1242 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

target a position in a goto program

Definition at line 1268 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

target a position in a goto program

Definition at line 1278 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

chr	An expression of type character
type	A type for the output

Returns: A integer expression of the given type

Definition at line 74 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 94 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 316 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 375 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 331 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 342 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 397 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 420 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 485 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 524 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 549 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 357 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 951 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 708 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 777 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 820 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 855 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 876 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 913 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 979 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 1013 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 1065 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

chr	An expression of type character
type	A type for the output

Returns: A Boolean expression

Definition at line 1090 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

chr	An expression of type character
type	A type for the output

Returns: A integer expression of the given type

Definition at line 1130 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

chr	An expression of type character
type	A type for the output

Returns: A character expression of the given type

Definition at line 1143 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 1169 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 1201 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

chr	An expression of type character
type	A type for the output

Returns: An expression of the given type

Definition at line 1256 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

chr	Expression we want to bound
lower_bound	Integer lower bound
upper_bound	Integer upper bound

Returns: A Boolean expression

Definition at line 45 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

chr	An expression of type character
list	A list of integer representing unicode characters

Returns: A Boolean expression

Definition at line 60 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 1306 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

code	the code of a function call

Returns: code where character function call get replaced by an simple instruction

Definition at line 1290 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 41 of file character_refine_preprocess.h.

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

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/character_refine_preprocess.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/character_refine_preprocess.cpp

Public Member Functions

Private Types

Static Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ conversion_functiont

◆ conversion_inputt

Member Function Documentation

◆ convert_char_count()

◆ convert_char_function()

◆ convert_char_value()

◆ convert_compare()

◆ convert_digit_char()

◆ convert_digit_int()

◆ convert_for_digit()

◆ convert_get_directionality_char()

◆ convert_get_directionality_int()

◆ convert_get_numeric_value_char()

◆ convert_get_numeric_value_int()

◆ convert_get_type_char()

◆ convert_get_type_int()

◆ convert_hash_code()

◆ convert_high_surrogate()

◆ convert_is_alphabetic()

◆ convert_is_bmp_code_point()

◆ convert_is_defined_char()

◆ convert_is_defined_int()

◆ convert_is_digit_char()

◆ convert_is_digit_int()

◆ convert_is_high_surrogate()

◆ convert_is_identifier_ignorable_char()

◆ convert_is_identifier_ignorable_int()

◆ convert_is_ideographic()

◆ convert_is_ISO_control_char()

◆ convert_is_ISO_control_int()

◆ convert_is_java_identifier_part_char()

◆ convert_is_java_identifier_part_int()

◆ convert_is_java_identifier_start_char()

◆ convert_is_java_identifier_start_int()

◆ convert_is_java_letter()

◆ convert_is_java_letter_or_digit()

◆ convert_is_letter_char()

◆ convert_is_letter_int()

◆ convert_is_letter_or_digit_char()

◆ convert_is_letter_or_digit_int()

◆ convert_is_low_surrogate()

◆ convert_is_lower_case_char()

◆ convert_is_lower_case_int()

◆ convert_is_mirrored_char()

◆ convert_is_mirrored_int()

◆ convert_is_space()

◆ convert_is_space_char()

◆ convert_is_space_char_int()

◆ convert_is_supplementary_code_point()

◆ convert_is_surrogate()

◆ convert_is_surrogate_pair()

◆ convert_is_title_case_char()

◆ convert_is_title_case_int()

◆ convert_is_unicode_identifier_part_char()

◆ convert_is_unicode_identifier_part_int()

◆ convert_is_unicode_identifier_start_char()

◆ convert_is_unicode_identifier_start_int()

◆ convert_is_upper_case_char()

◆ convert_is_upper_case_int()

◆ convert_is_valid_code_point()

◆ convert_is_whitespace_char()

◆ convert_is_whitespace_int()

◆ convert_low_surrogate()

◆ convert_reverse_bytes()

◆ convert_to_chars()

◆ convert_to_lower_case_char()

◆ convert_to_lower_case_int()

◆ convert_to_title_case_char()

◆ convert_to_title_case_int()

◆ convert_to_upper_case_char()

◆ convert_to_upper_case_int()

◆ expr_of_char_count()

◆ expr_of_char_value()

◆ expr_of_high_surrogate()