cprover
character_refine_preprocesst Class Reference

#include <character_refine_preprocess.h>

Inheritance diagram for character_refine_preprocesst:
[legend]
Collaboration diagram for character_refine_preprocesst:
[legend]

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...
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Private Types

typedef const code_function_calltconversion_input
 
typedef codet(* conversion_functiont) (conversion_input &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_input &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_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.charValue:()C. More...
 
static codet convert_compare (conversion_input &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_input &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_input &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_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.forDigit:(II)I. More...
 
static codet convert_get_directionality_char (conversion_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.highSurrogate:(C)Z. More...
 
static exprt expr_of_is_alphabetic (const exprt &chr, const typet &type)
 Determines if the specified character (Unicode code point) is alphabetic. More...
 
static codet convert_is_alphabetic (conversion_input &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_input &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_input &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_input &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_input &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_input &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_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isHighSurrogate:(C)Z. More...
 
static exprt expr_of_is_identifier_ignorable (const exprt &chr, const typet &type)
 Determines if the character is one of ignorable in a Java identifier, that is, it is in one of these ranges: '' through '' '' through '' '' through ''. More...
 
static codet convert_is_identifier_ignorable_char (conversion_input &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_input &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_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isIdeographic:(C)Z. More...
 
static codet convert_is_ISO_control_char (conversion_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLowSurrogate:(I)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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &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_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.lowSurrogate:(I)Z. More...
 
static exprt expr_of_reverse_bytes (const exprt &chr, const typet &type)
 Returns the value obtained by reversing the order of the bytes in the specified char value. More...
 
static codet convert_reverse_bytes (conversion_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.reverseBytes:(C)C. More...
 
static exprt expr_of_to_chars (const exprt &chr, const typet &type)
 Converts the specified character (Unicode code point) to its UTF-16 representation stored in a char array. More...
 
static codet convert_to_chars (conversion_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toChars:(I)[C. More...
 
static codet convert_to_code_point (conversion_input &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toCodePoint:(CC)I. More...
 
static exprt expr_of_to_lower_case (const exprt &chr, const typet &type)
 Converts the character argument to lowercase. More...
 
static codet convert_to_lower_case_char (conversion_input &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_input &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_input &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_input &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_input &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_input &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_input &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, irep_id_hashconversion_table
 

Additional Inherited Members

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 27 of file character_refine_preprocess.h.

Member Typedef Documentation

◆ conversion_functiont

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

Definition at line 35 of file character_refine_preprocess.h.

◆ conversion_input

Member Function Documentation

◆ convert_char_count()

codet character_refine_preprocesst::convert_char_count ( conversion_input 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.

References convert_char_function(), and expr_of_char_count().

Referenced by initialize_conversion_table().

◆ convert_char_function()

◆ convert_char_value()

codet character_refine_preprocesst::convert_char_value ( conversion_input 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 99 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_char_value().

Referenced by convert_hash_code(), and initialize_conversion_table().

◆ convert_compare()

codet character_refine_preprocesst::convert_compare ( conversion_input 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 108 of file character_refine_preprocess.cpp.

References code_function_callt::arguments(), from_integer(), code_function_callt::lhs(), and messaget::result().

Referenced by initialize_conversion_table().

◆ convert_digit_char()

codet character_refine_preprocesst::convert_digit_char ( conversion_input target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 130 of file character_refine_preprocess.cpp.

References code_function_callt::arguments(), from_integer(), in_interval_expr(), code_function_callt::lhs(), and messaget::result().

Referenced by convert_digit_int(), convert_get_numeric_value_char(), and initialize_conversion_table().

◆ convert_digit_int()

codet character_refine_preprocesst::convert_digit_int ( conversion_input 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 203 of file character_refine_preprocess.cpp.

References convert_digit_char().

Referenced by convert_get_numeric_value_int(), and initialize_conversion_table().

◆ convert_for_digit()

codet character_refine_preprocesst::convert_for_digit ( conversion_input target)
staticprivate

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

TODO: For now the radix argument is ignored

Parameters
targeta position in a goto program

Definition at line 213 of file character_refine_preprocess.cpp.

References code_function_callt::arguments(), from_integer(), code_function_callt::lhs(), and messaget::result().

Referenced by initialize_conversion_table().

◆ convert_get_directionality_char()

codet character_refine_preprocesst::convert_get_directionality_char ( conversion_input 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 231 of file character_refine_preprocess.cpp.

Referenced by convert_get_directionality_int(), and initialize_conversion_table().

◆ convert_get_directionality_int()

codet character_refine_preprocesst::convert_get_directionality_int ( conversion_input 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 242 of file character_refine_preprocess.cpp.

References convert_get_directionality_char().

Referenced by initialize_conversion_table().

◆ convert_get_numeric_value_char()

codet character_refine_preprocesst::convert_get_numeric_value_char ( conversion_input 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 252 of file character_refine_preprocess.cpp.

References convert_digit_char().

Referenced by initialize_conversion_table().

◆ convert_get_numeric_value_int()

codet character_refine_preprocesst::convert_get_numeric_value_int ( conversion_input 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 263 of file character_refine_preprocess.cpp.

References convert_digit_int().

Referenced by initialize_conversion_table().

◆ convert_get_type_char()

codet character_refine_preprocesst::convert_get_type_char ( conversion_input 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 272 of file character_refine_preprocess.cpp.

Referenced by convert_get_type_int(), and initialize_conversion_table().

◆ convert_get_type_int()

codet character_refine_preprocesst::convert_get_type_int ( conversion_input 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 283 of file character_refine_preprocess.cpp.

References convert_get_type_char().

Referenced by initialize_conversion_table().

◆ convert_hash_code()

codet character_refine_preprocesst::convert_hash_code ( conversion_input 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 292 of file character_refine_preprocess.cpp.

References convert_char_value().

Referenced by initialize_conversion_table().

◆ convert_high_surrogate()

codet character_refine_preprocesst::convert_high_surrogate ( conversion_input target)
staticprivate

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

Definition at line 316 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_high_surrogate().

Referenced by initialize_conversion_table().

◆ convert_is_alphabetic()

codet character_refine_preprocesst::convert_is_alphabetic ( conversion_input 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 378 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_alphabetic().

Referenced by initialize_conversion_table().

◆ convert_is_bmp_code_point()

codet character_refine_preprocesst::convert_is_bmp_code_point ( conversion_input 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 401 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_bmp_code_point().

Referenced by initialize_conversion_table().

◆ convert_is_defined_char()

codet character_refine_preprocesst::convert_is_defined_char ( conversion_input 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 446 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_defined().

Referenced by convert_is_defined_int(), and initialize_conversion_table().

◆ convert_is_defined_int()

codet character_refine_preprocesst::convert_is_defined_int ( conversion_input 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 456 of file character_refine_preprocess.cpp.

References convert_is_defined_char().

Referenced by initialize_conversion_table().

◆ convert_is_digit_char()

codet character_refine_preprocesst::convert_is_digit_char ( conversion_input 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 493 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_digit().

Referenced by convert_is_digit_int(), and initialize_conversion_table().

◆ convert_is_digit_int()

codet character_refine_preprocesst::convert_is_digit_int ( conversion_input 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 503 of file character_refine_preprocess.cpp.

References convert_is_digit_char().

Referenced by initialize_conversion_table().

◆ convert_is_high_surrogate()

codet character_refine_preprocesst::convert_is_high_surrogate ( conversion_input 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 523 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_high_surrogate().

Referenced by initialize_conversion_table().

◆ convert_is_identifier_ignorable_char()

codet character_refine_preprocesst::convert_is_identifier_ignorable_char ( conversion_input 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 554 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_identifier_ignorable().

Referenced by convert_is_identifier_ignorable_int(), and initialize_conversion_table().

◆ convert_is_identifier_ignorable_int()

codet character_refine_preprocesst::convert_is_identifier_ignorable_int ( conversion_input 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 566 of file character_refine_preprocess.cpp.

References convert_is_identifier_ignorable_char().

Referenced by initialize_conversion_table().

◆ convert_is_ideographic()

codet character_refine_preprocesst::convert_is_ideographic ( conversion_input target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 575 of file character_refine_preprocess.cpp.

References code_function_callt::arguments(), in_interval_expr(), code_function_callt::lhs(), and messaget::result().

Referenced by initialize_conversion_table().

◆ convert_is_ISO_control_char()

codet character_refine_preprocesst::convert_is_ISO_control_char ( conversion_input 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 589 of file character_refine_preprocess.cpp.

References code_function_callt::arguments(), in_interval_expr(), code_function_callt::lhs(), and messaget::result().

Referenced by convert_is_ISO_control_int(), and initialize_conversion_table().

◆ convert_is_ISO_control_int()

codet character_refine_preprocesst::convert_is_ISO_control_int ( conversion_input 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 604 of file character_refine_preprocess.cpp.

References convert_is_ISO_control_char().

Referenced by initialize_conversion_table().

◆ convert_is_java_identifier_part_char()

codet character_refine_preprocesst::convert_is_java_identifier_part_char ( conversion_input 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 616 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_unicode_identifier_part().

Referenced by convert_is_java_letter_or_digit(), and initialize_conversion_table().

◆ convert_is_java_identifier_part_int()

codet character_refine_preprocesst::convert_is_java_identifier_part_int ( conversion_input 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 626 of file character_refine_preprocess.cpp.

References convert_is_unicode_identifier_part_char().

Referenced by initialize_conversion_table().

◆ convert_is_java_identifier_start_char()

codet character_refine_preprocesst::convert_is_java_identifier_start_char ( conversion_input 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 639 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_unicode_identifier_start().

Referenced by convert_is_java_identifier_start_int(), convert_is_java_letter(), and initialize_conversion_table().

◆ convert_is_java_identifier_start_int()

codet character_refine_preprocesst::convert_is_java_identifier_start_int ( conversion_input 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 649 of file character_refine_preprocess.cpp.

References convert_is_java_identifier_start_char().

Referenced by initialize_conversion_table().

◆ convert_is_java_letter()

codet character_refine_preprocesst::convert_is_java_letter ( conversion_input 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 658 of file character_refine_preprocess.cpp.

References convert_is_java_identifier_start_char().

Referenced by initialize_conversion_table().

◆ convert_is_java_letter_or_digit()

codet character_refine_preprocesst::convert_is_java_letter_or_digit ( conversion_input 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 667 of file character_refine_preprocess.cpp.

References convert_is_java_identifier_part_char().

Referenced by initialize_conversion_table().

◆ convert_is_letter_char()

codet character_refine_preprocesst::convert_is_letter_char ( conversion_input 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 676 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_letter().

Referenced by convert_is_letter_int(), and initialize_conversion_table().

◆ convert_is_letter_int()

codet character_refine_preprocesst::convert_is_letter_int ( conversion_input 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 686 of file character_refine_preprocess.cpp.

References convert_is_letter_char().

Referenced by initialize_conversion_table().

◆ convert_is_letter_or_digit_char()

codet character_refine_preprocesst::convert_is_letter_or_digit_char ( conversion_input 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 705 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_digit().

Referenced by convert_is_letter_or_digit_int(), and initialize_conversion_table().

◆ convert_is_letter_or_digit_int()

codet character_refine_preprocesst::convert_is_letter_or_digit_int ( conversion_input 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 715 of file character_refine_preprocess.cpp.

References convert_is_letter_or_digit_char().

Referenced by initialize_conversion_table().

◆ convert_is_low_surrogate()

codet character_refine_preprocesst::convert_is_low_surrogate ( conversion_input target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 747 of file character_refine_preprocess.cpp.

References code_function_callt::arguments(), in_interval_expr(), code_function_callt::lhs(), and messaget::result().

Referenced by initialize_conversion_table().

◆ convert_is_lower_case_char()

codet character_refine_preprocesst::convert_is_lower_case_char ( conversion_input 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 726 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_ascii_lower_case().

Referenced by convert_is_lower_case_int(), and initialize_conversion_table().

◆ convert_is_lower_case_int()

codet character_refine_preprocesst::convert_is_lower_case_int ( conversion_input 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 738 of file character_refine_preprocess.cpp.

References convert_is_lower_case_char().

Referenced by initialize_conversion_table().

◆ convert_is_mirrored_char()

codet character_refine_preprocesst::convert_is_mirrored_char ( conversion_input 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 776 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_mirrored().

Referenced by convert_is_mirrored_int(), and initialize_conversion_table().

◆ convert_is_mirrored_int()

codet character_refine_preprocesst::convert_is_mirrored_int ( conversion_input 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 788 of file character_refine_preprocess.cpp.

References convert_is_mirrored_char().

Referenced by initialize_conversion_table().

◆ convert_is_space()

codet character_refine_preprocesst::convert_is_space ( conversion_input 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 797 of file character_refine_preprocess.cpp.

References convert_is_whitespace_char().

Referenced by initialize_conversion_table().

◆ convert_is_space_char()

codet character_refine_preprocesst::convert_is_space_char ( conversion_input 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 820 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_space_char().

Referenced by convert_is_space_char_int(), and initialize_conversion_table().

◆ convert_is_space_char_int()

codet character_refine_preprocesst::convert_is_space_char_int ( conversion_input 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 830 of file character_refine_preprocess.cpp.

References convert_is_space_char().

Referenced by initialize_conversion_table().

◆ convert_is_supplementary_code_point()

codet character_refine_preprocesst::convert_is_supplementary_code_point ( conversion_input 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 850 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_supplementary_code_point().

Referenced by initialize_conversion_table().

◆ convert_is_surrogate()

codet character_refine_preprocesst::convert_is_surrogate ( conversion_input 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 870 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_surrogate().

Referenced by initialize_conversion_table().

◆ convert_is_surrogate_pair()

codet character_refine_preprocesst::convert_is_surrogate_pair ( conversion_input 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 880 of file character_refine_preprocess.cpp.

References code_function_callt::arguments(), in_interval_expr(), code_function_callt::lhs(), and messaget::result().

Referenced by initialize_conversion_table().

◆ convert_is_title_case_char()

codet character_refine_preprocesst::convert_is_title_case_char ( conversion_input 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 913 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_title_case().

Referenced by convert_is_title_case_int(), and initialize_conversion_table().

◆ convert_is_title_case_int()

codet character_refine_preprocesst::convert_is_title_case_int ( conversion_input 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 923 of file character_refine_preprocess.cpp.

References convert_is_title_case_char().

Referenced by initialize_conversion_table().

◆ convert_is_unicode_identifier_part_char()

codet character_refine_preprocesst::convert_is_unicode_identifier_part_char ( conversion_input 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 974 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_unicode_identifier_part().

Referenced by convert_is_java_identifier_part_int(), convert_is_unicode_identifier_part_int(), and initialize_conversion_table().

◆ convert_is_unicode_identifier_part_int()

codet character_refine_preprocesst::convert_is_unicode_identifier_part_int ( conversion_input 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 984 of file character_refine_preprocess.cpp.

References convert_is_unicode_identifier_part_char().

Referenced by initialize_conversion_table().

◆ convert_is_unicode_identifier_start_char()

codet character_refine_preprocesst::convert_is_unicode_identifier_start_char ( conversion_input 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 1005 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_unicode_identifier_start().

Referenced by convert_is_unicode_identifier_start_int(), and initialize_conversion_table().

◆ convert_is_unicode_identifier_start_int()

codet character_refine_preprocesst::convert_is_unicode_identifier_start_int ( conversion_input 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 1015 of file character_refine_preprocess.cpp.

References convert_is_unicode_identifier_start_char().

Referenced by initialize_conversion_table().

◆ convert_is_upper_case_char()

codet character_refine_preprocesst::convert_is_upper_case_char ( conversion_input 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 1026 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_ascii_upper_case().

Referenced by convert_is_upper_case_int(), and initialize_conversion_table().

◆ convert_is_upper_case_int()

codet character_refine_preprocesst::convert_is_upper_case_int ( conversion_input 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 1036 of file character_refine_preprocess.cpp.

References convert_is_upper_case_char().

Referenced by initialize_conversion_table().

◆ convert_is_valid_code_point()

codet character_refine_preprocesst::convert_is_valid_code_point ( conversion_input 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 1056 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_valid_code_point().

Referenced by initialize_conversion_table().

◆ convert_is_whitespace_char()

codet character_refine_preprocesst::convert_is_whitespace_char ( conversion_input 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 1088 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_whitespace().

Referenced by convert_is_space(), convert_is_whitespace_int(), and initialize_conversion_table().

◆ convert_is_whitespace_int()

codet character_refine_preprocesst::convert_is_whitespace_int ( conversion_input 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 1098 of file character_refine_preprocess.cpp.

References convert_is_whitespace_char().

Referenced by initialize_conversion_table().

◆ convert_low_surrogate()

codet character_refine_preprocesst::convert_low_surrogate ( conversion_input target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1121 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_low_surrogate().

◆ convert_reverse_bytes()

codet character_refine_preprocesst::convert_reverse_bytes ( conversion_input 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 1144 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_reverse_bytes().

Referenced by initialize_conversion_table().

◆ convert_to_chars()

codet character_refine_preprocesst::convert_to_chars ( conversion_input target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1177 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_to_chars().

Referenced by initialize_conversion_table().

◆ convert_to_code_point()

codet character_refine_preprocesst::convert_to_code_point ( conversion_input target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1186 of file character_refine_preprocess.cpp.

References code_function_callt::arguments(), from_integer(), code_function_callt::lhs(), pair_value(), and messaget::result().

Referenced by initialize_conversion_table().

◆ convert_to_lower_case_char()

codet character_refine_preprocesst::convert_to_lower_case_char ( conversion_input 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 1232 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_to_lower_case().

Referenced by convert_to_lower_case_int(), and initialize_conversion_table().

◆ convert_to_lower_case_int()

codet character_refine_preprocesst::convert_to_lower_case_int ( conversion_input 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 1242 of file character_refine_preprocess.cpp.

References convert_to_lower_case_char().

Referenced by initialize_conversion_table().

◆ convert_to_title_case_char()

codet character_refine_preprocesst::convert_to_title_case_char ( conversion_input 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 1288 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_to_title_case().

Referenced by convert_to_title_case_int(), and initialize_conversion_table().

◆ convert_to_title_case_int()

codet character_refine_preprocesst::convert_to_title_case_int ( conversion_input 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 1298 of file character_refine_preprocess.cpp.

References convert_to_title_case_char().

Referenced by initialize_conversion_table().

◆ convert_to_upper_case_char()

codet character_refine_preprocesst::convert_to_upper_case_char ( conversion_input 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 1325 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_to_upper_case().

Referenced by convert_to_upper_case_int(), and initialize_conversion_table().

◆ convert_to_upper_case_int()

codet character_refine_preprocesst::convert_to_upper_case_int ( conversion_input 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 1335 of file character_refine_preprocess.cpp.

References convert_to_upper_case_char().

Referenced by initialize_conversion_table().

◆ 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
exprAn 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.

References from_integer().

Referenced by convert_char_count().

◆ 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 90 of file character_refine_preprocess.cpp.

Referenced by convert_char_value().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 303 of file character_refine_preprocess.cpp.

References from_integer().

Referenced by convert_high_surrogate(), and expr_of_to_chars().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 369 of file character_refine_preprocess.cpp.

References expr_of_is_letter().

Referenced by convert_is_alphabetic().

◆ 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 327 of file character_refine_preprocess.cpp.

References in_interval_expr().

Referenced by convert_is_lower_case_char(), expr_of_is_letter(), and expr_of_to_upper_case().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 337 of file character_refine_preprocess.cpp.

References in_interval_expr().

Referenced by convert_is_upper_case_char(), expr_of_is_letter(), and expr_of_to_lower_case().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 391 of file character_refine_preprocess.cpp.

References from_integer(), and exprt::type().

Referenced by convert_is_bmp_code_point(), and expr_of_to_chars().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 412 of file character_refine_preprocess.cpp.

References disjunction(), from_integer(), in_interval_expr(), and exprt::type().

Referenced by convert_is_defined_char().

◆ 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: '' through '', ISO-LATIN-1 digits ('0' through '9') '' through '', Arabic-Indic digits '' through '', Extended Arabic-Indic digits '' through '', Devanagari digits '' through '', Fullwidth digits Many other character ranges contain digits as well.

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

Definition at line 476 of file character_refine_preprocess.cpp.

References in_interval_expr().

Referenced by convert_is_digit_char(), convert_is_letter_or_digit_char(), expr_of_is_letter_or_digit(), and expr_of_is_unicode_identifier_part().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 514 of file character_refine_preprocess.cpp.

References in_interval_expr().

Referenced by convert_is_high_surrogate().

◆ 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: '' through '' '' through '' '' through ''.

TODO: For now, we ignore the FORMAT general category value

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

Definition at line 538 of file character_refine_preprocess.cpp.

References in_interval_expr().

Referenced by convert_is_identifier_ignorable_char(), and expr_of_is_unicode_identifier_part().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 351 of file character_refine_preprocess.cpp.

References expr_of_is_ascii_lower_case(), and expr_of_is_ascii_upper_case().

Referenced by convert_is_letter_char(), expr_of_is_alphabetic(), expr_of_is_letter_or_digit(), and expr_of_is_unicode_identifier_start().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 934 of file character_refine_preprocess.cpp.

References in_interval_expr(), and in_list_expr().

Referenced by expr_of_is_unicode_identifier_start().

◆ 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 696 of file character_refine_preprocess.cpp.

References expr_of_is_digit(), and expr_of_is_letter().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
An expression of the given type

Definition at line 765 of file character_refine_preprocess.cpp.

References in_list_expr().

Referenced by convert_is_mirrored_char().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 807 of file character_refine_preprocess.cpp.

References in_interval_expr(), and in_list_expr().

Referenced by convert_is_space_char().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 841 of file character_refine_preprocess.cpp.

References from_integer(), and exprt::type().

Referenced by convert_is_supplementary_code_point().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 861 of file character_refine_preprocess.cpp.

References in_interval_expr().

Referenced by convert_is_surrogate().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 897 of file character_refine_preprocess.cpp.

References disjunction(), in_interval_expr(), and in_list_expr().

Referenced by convert_is_title_case_char().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A Boolean expression

Definition at line 961 of file character_refine_preprocess.cpp.

References disjunction(), expr_of_is_digit(), expr_of_is_identifier_ignorable(), and expr_of_is_unicode_identifier_start().

Referenced by convert_is_java_identifier_part_char(), and convert_is_unicode_identifier_part_char().

◆ 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 995 of file character_refine_preprocess.cpp.

References expr_of_is_letter(), and expr_of_is_letter_number().

Referenced by convert_is_java_identifier_start_char(), convert_is_unicode_identifier_start_char(), and expr_of_is_unicode_identifier_part().

◆ 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 1047 of file character_refine_preprocess.cpp.

References from_integer(), and exprt::type().

Referenced by convert_is_valid_code_point().

◆ 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 ('', '', ''). * it is one of these: U+0009 U+000A U+000B U+000C U+000D U+001C U+001D U+001E U+001F

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

Definition at line 1071 of file character_refine_preprocess.cpp.

References disjunction(), in_interval_expr(), and in_list_expr().

Referenced by convert_is_whitespace_char().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A integer expression of the given type

Definition at line 1110 of file character_refine_preprocess.cpp.

References from_integer().

Referenced by convert_low_surrogate(), and expr_of_to_chars().

◆ 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
exprAn expression of type character
typeA type for the output
Returns
A character expression of the given type

Definition at line 1133 of file character_refine_preprocess.cpp.

References from_integer().

Referenced by convert_reverse_bytes().

◆ expr_of_to_chars()

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

Converts the specified character (Unicode code point) to its UTF-16 representation stored in a char array.

If the specified code point is a BMP (Basic Multilingual Plane or Plane 0) value, the resulting char array has the same value as codePoint. If the specified code point is a supplementary code point, the resulting char array has the corresponding surrogate pair.

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

Definition at line 1159 of file character_refine_preprocess.cpp.

References char_type(), exprt::copy_to_operands(), expr_of_high_surrogate(), expr_of_is_bmp_code_point(), expr_of_low_surrogate(), exprt::move_to_operands(), typet::subtype(), and to_array_type().

Referenced by convert_to_chars().

◆ 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 1219 of file character_refine_preprocess.cpp.

References expr_of_is_ascii_upper_case(), and from_integer().

Referenced by convert_to_lower_case_char().

◆ 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 1252 of file character_refine_preprocess.cpp.

References from_integer(), in_interval_expr(), and in_list_expr().

Referenced by convert_to_title_case_char().

◆ 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 1312 of file character_refine_preprocess.cpp.

References expr_of_is_ascii_lower_case(), and from_integer().

Referenced by convert_to_upper_case_char().

◆ 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
argExpression 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.

References from_integer(), and exprt::type().

Referenced by convert_digit_char(), convert_is_ideographic(), convert_is_ISO_control_char(), convert_is_low_surrogate(), convert_is_surrogate_pair(), expr_of_is_ascii_lower_case(), expr_of_is_ascii_upper_case(), expr_of_is_defined(), expr_of_is_digit(), expr_of_is_high_surrogate(), expr_of_is_identifier_ignorable(), expr_of_is_letter_number(), expr_of_is_space_char(), expr_of_is_surrogate(), expr_of_is_title_case(), expr_of_is_whitespace(), and expr_of_to_title_case().

◆ 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.

References disjunction(), from_integer(), and exprt::type().

Referenced by expr_of_is_letter_number(), expr_of_is_mirrored(), expr_of_is_space_char(), expr_of_is_title_case(), expr_of_is_whitespace(), and expr_of_to_title_case().

◆ initialize_conversion_table()

void character_refine_preprocesst::initialize_conversion_table ( )

fill maps with correspondance from java method names to conversion functions

Definition at line 1363 of file character_refine_preprocess.cpp.

References conversion_table, convert_char_count(), convert_char_value(), convert_compare(), convert_digit_char(), convert_digit_int(), convert_for_digit(), convert_get_directionality_char(), convert_get_directionality_int(), convert_get_numeric_value_char(), convert_get_numeric_value_int(), convert_get_type_char(), convert_get_type_int(), convert_hash_code(), convert_high_surrogate(), convert_is_alphabetic(), convert_is_bmp_code_point(), convert_is_defined_char(), convert_is_defined_int(), convert_is_digit_char(), convert_is_digit_int(), convert_is_high_surrogate(), convert_is_identifier_ignorable_char(), convert_is_identifier_ignorable_int(), convert_is_ideographic(), convert_is_ISO_control_char(), convert_is_ISO_control_int(), convert_is_java_identifier_part_char(), convert_is_java_identifier_part_int(), convert_is_java_identifier_start_char(), convert_is_java_identifier_start_int(), convert_is_java_letter(), convert_is_java_letter_or_digit(), convert_is_letter_char(), convert_is_letter_int(), convert_is_letter_or_digit_char(), convert_is_letter_or_digit_int(), convert_is_low_surrogate(), convert_is_lower_case_char(), convert_is_lower_case_int(), convert_is_mirrored_char(), convert_is_mirrored_int(), convert_is_space(), convert_is_space_char(), convert_is_space_char_int(), convert_is_supplementary_code_point(), convert_is_surrogate(), convert_is_surrogate_pair(), convert_is_title_case_char(), convert_is_title_case_int(), convert_is_unicode_identifier_part_char(), convert_is_unicode_identifier_part_int(), convert_is_unicode_identifier_start_char(), convert_is_unicode_identifier_start_int(), convert_is_upper_case_char(), convert_is_upper_case_int(), convert_is_valid_code_point(), convert_is_whitespace_char(), convert_is_whitespace_int(), convert_reverse_bytes(), convert_to_chars(), convert_to_code_point(), convert_to_lower_case_char(), convert_to_lower_case_int(), convert_to_title_case_char(), convert_to_title_case_int(), convert_to_upper_case_char(), and convert_to_upper_case_int().

Referenced by java_bytecode_languaget::typecheck().

◆ 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 1347 of file character_refine_preprocess.cpp.

References conversion_table, code_function_callt::function(), irept::id(), and to_symbol_expr().

Referenced by java_bytecode_convert_methodt::convert_instructions().

Member Data Documentation

◆ conversion_table

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

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