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)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

Private Types

typedef const code_function_calltconversion_inputt
 
typedef codet(* conversion_functiont) (conversion_inputt &target)
 

Static Private Member Functions

static exprt expr_of_char_count (const exprt &chr, const typet &type)
 Determines the number of char values needed to represent the specified character (Unicode code point). More...
 
static codet convert_char_count (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.charCount:(I)I. More...
 
static exprt expr_of_char_value (const exprt &chr, const typet &type)
 Casts the given expression to the given type. More...
 
static codet convert_char_value (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.charValue:()C. More...
 
static codet convert_compare (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.compare:(CC)I. More...
 
static codet convert_digit_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.digit:(CI)I. More...
 
static codet convert_digit_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.digit:(II)I. More...
 
static codet convert_for_digit (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.forDigit:(II)C. More...
 
static codet convert_get_directionality_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(C)I. More...
 
static codet convert_get_directionality_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.getDirectionality:(I)I. More...
 
static codet convert_get_numeric_value_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.getNumericValue:(C)I. More...
 
static codet convert_get_numeric_value_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.getNumericValue:(C)I. More...
 
static codet convert_get_type_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.getType:(C)I. More...
 
static codet convert_get_type_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.getType:(I)I. More...
 
static codet convert_hash_code (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.hashCode:()I. More...
 
static exprt expr_of_high_surrogate (const exprt &chr, const typet &type)
 Returns the leading surrogate (a high surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding. More...
 
static codet convert_high_surrogate (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.highSurrogate:(C)Z. More...
 
static exprt expr_of_is_alphabetic (const exprt &chr, const typet &type)
 Determines if the specified character (Unicode code point) is alphabetic. More...
 
static codet convert_is_alphabetic (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isAlphabetic:(I)Z. More...
 
static exprt expr_of_is_bmp_code_point (const exprt &chr, const typet &type)
 Determines whether the specified character (Unicode code point) is in the Basic Multilingual Plane (BMP). More...
 
static codet convert_is_bmp_code_point (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isBmpCodePoint:(I)Z. More...
 
static exprt expr_of_is_defined (const exprt &chr, const typet &type)
 Determines if a character is defined in Unicode. More...
 
static codet convert_is_defined_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isDefined:(C)Z. More...
 
static codet convert_is_defined_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isDefined:(I)Z. More...
 
static exprt expr_of_is_digit (const exprt &chr, const typet &type)
 Determines if the specified character is a digit. More...
 
static codet convert_is_digit_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isDigit:(C)Z. More...
 
static codet convert_is_digit_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.digit:(I)Z. More...
 
static exprt expr_of_is_high_surrogate (const exprt &chr, const typet &type)
 Determines if the given char value is a Unicode high-surrogate code unit (also known as leading-surrogate code unit). More...
 
static codet convert_is_high_surrogate (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isHighSurrogate:(C)Z. More...
 
static exprt expr_of_is_identifier_ignorable (const exprt &chr, const typet &type)
 Determines if the character is one of ignorable in a Java identifier, that is, it is in one of these ranges: '' through '' '' through '' '' through ''. More...
 
static codet convert_is_identifier_ignorable_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isIdentifierIgnorable:(C)Z. More...
 
static codet convert_is_identifier_ignorable_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isIdentifierIgnorable:(I)Z. More...
 
static codet convert_is_ideographic (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isIdeographic:(I)Z. More...
 
static codet convert_is_ISO_control_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(C)Z. More...
 
static codet convert_is_ISO_control_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(I)Z. More...
 
static codet convert_is_java_identifier_part_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isJavaIdentifierPart:(C)Z. More...
 
static codet convert_is_java_identifier_part_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierPart:(I)Z. More...
 
static codet convert_is_java_identifier_start_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierStart:(C)Z. More...
 
static codet convert_is_java_identifier_start_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierStart:(I)Z. More...
 
static codet convert_is_java_letter (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isJavaLetter:(C)Z. More...
 
static codet convert_is_java_letter_or_digit (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method isJavaLetterOrDigit:(C)Z. More...
 
static exprt expr_of_is_letter (const exprt &chr, const typet &type)
 Determines if the specified character is a letter. More...
 
static codet convert_is_letter_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(C)Z. More...
 
static codet convert_is_letter_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(I)Z. More...
 
static exprt expr_of_is_letter_or_digit (const exprt &chr, const typet &type)
 Determines if the specified character is a letter or digit. More...
 
static codet convert_is_letter_or_digit_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(C)Z. More...
 
static codet convert_is_letter_or_digit_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(I)Z. More...
 
static exprt expr_of_is_ascii_lower_case (const exprt &chr, const typet &type)
 Determines if the specified character is an ASCII lowercase character. More...
 
static codet convert_is_lower_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLowerCase:(C)Z. More...
 
static codet convert_is_lower_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLowerCase:(I)Z. More...
 
static codet convert_is_low_surrogate (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLowSurrogate:(C)Z. More...
 
static exprt expr_of_is_mirrored (const exprt &chr, const typet &type)
 Determines whether the character is mirrored according to the Unicode specification. More...
 
static codet convert_is_mirrored_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isMirrored:(C)Z. More...
 
static codet convert_is_mirrored_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isMirrored:(I)Z. More...
 
static codet convert_is_space (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSpace:(C)Z. More...
 
static exprt expr_of_is_space_char (const exprt &chr, const typet &type)
 Determines if the specified character is white space according to Unicode (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR) More...
 
static codet convert_is_space_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(C)Z. More...
 
static codet convert_is_space_char_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(I)Z. More...
 
static exprt expr_of_is_supplementary_code_point (const exprt &chr, const typet &type)
 Determines whether the specified character (Unicode code point) is in the supplementary character range. More...
 
static codet convert_is_supplementary_code_point (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSupplementaryCodePoint:(I)Z. More...
 
static exprt expr_of_is_surrogate (const exprt &chr, const typet &type)
 Determines if the given char value is a Unicode surrogate code unit. More...
 
static codet convert_is_surrogate (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogate:(C)Z. More...
 
static codet convert_is_surrogate_pair (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogatePair:(CC)Z. More...
 
static exprt expr_of_is_title_case (const exprt &chr, const typet &type)
 Determines if the specified character is a titlecase character. More...
 
static codet convert_is_title_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(C)Z. More...
 
static codet convert_is_title_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(I)Z. More...
 
static exprt expr_of_is_letter_number (const exprt &chr, const typet &type)
 Determines if the specified character is in the LETTER_NUMBER category of Unicode. More...
 
static exprt expr_of_is_unicode_identifier_part (const exprt &chr, const typet &type)
 Determines if the character may be part of a Unicode identifier. More...
 
static codet convert_is_unicode_identifier_part_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(C)Z. More...
 
static codet convert_is_unicode_identifier_part_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(I)Z. More...
 
static exprt expr_of_is_unicode_identifier_start (const exprt &chr, const typet &type)
 Determines if the specified character is permissible as the first character in a Unicode identifier. More...
 
static codet convert_is_unicode_identifier_start_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(C)Z. More...
 
static codet convert_is_unicode_identifier_start_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(I)Z. More...
 
static exprt expr_of_is_ascii_upper_case (const exprt &chr, const typet &type)
 Determines if the specified character is an ASCII uppercase character. More...
 
static codet convert_is_upper_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUpperCase:(C)Z. More...
 
static codet convert_is_upper_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUpperCase:(I)Z. More...
 
static exprt expr_of_is_valid_code_point (const exprt &chr, const typet &type)
 Determines whether the specified code point is a valid Unicode code point value. More...
 
static codet convert_is_valid_code_point (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isValidCodePoint:(I)Z. More...
 
static exprt expr_of_is_whitespace (const exprt &chr, const typet &type)
 Determines if the specified character is white space according to Java. More...
 
static codet convert_is_whitespace_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(C)Z. More...
 
static codet convert_is_whitespace_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(I)Z. More...
 
static exprt expr_of_low_surrogate (const exprt &chr, const typet &type)
 Returns the trailing surrogate (a low surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding. More...
 
static codet convert_low_surrogate (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.lowSurrogate:(I)C. More...
 
static exprt expr_of_reverse_bytes (const exprt &chr, const typet &type)
 Returns the value obtained by reversing the order of the bytes in the specified char value. More...
 
static codet convert_reverse_bytes (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.reverseBytes:(C)C. More...
 
static exprt expr_of_to_chars (const exprt &chr, const typet &type)
 Converts the specified character (Unicode code point) to its UTF-16 representation stored in a char array. More...
 
static codet convert_to_chars (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toChars:(I)[C. More...
 
static codet convert_to_code_point (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toCodePoint:(CC)I. More...
 
static exprt expr_of_to_lower_case (const exprt &chr, const typet &type)
 Converts the character argument to lowercase. More...
 
static codet convert_to_lower_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(C)C. More...
 
static codet convert_to_lower_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(I)I. More...
 
static exprt expr_of_to_title_case (const exprt &chr, const typet &type)
 Converts the character argument to titlecase. More...
 
static codet convert_to_title_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(C)C. More...
 
static codet convert_to_title_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(I)I. More...
 
static exprt expr_of_to_upper_case (const exprt &chr, const typet &type)
 Converts the character argument to uppercase. More...
 
static codet convert_to_upper_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(C)C. More...
 
static codet convert_to_upper_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(I)I. More...
 
static codet convert_char_function (exprt(*expr_function)(const exprt &chr, const typet &type), conversion_inputt &target)
 converts based on a function on expressions More...
 
static exprt in_interval_expr (const exprt &chr, const mp_integer &lower_bound, const mp_integer &upper_bound)
 The returned expression is true when the first argument is in the interval defined by the lower and upper bounds (included) More...
 
static exprt in_list_expr (const exprt &chr, const std::list< mp_integer > &list)
 The returned expression is true when the given character is equal to one of the element in the list. More...
 

Private Attributes

std::unordered_map< irep_idt, conversion_functiontconversion_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 unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

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

◆ conversion_inputt

Member Function Documentation

◆ convert_char_count()

codet character_refine_preprocesst::convert_char_count ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 82 of file character_refine_preprocess.cpp.

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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 100 of file character_refine_preprocess.cpp.

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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 110 of file character_refine_preprocess.cpp.

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_inputt target)
staticprivate

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

The function call has one character argument and an optional integer radix argument. If the radix is not given it is set to 36 by default.

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

Definition at line 136 of file character_refine_preprocess.cpp.

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

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

◆ convert_digit_int()

codet character_refine_preprocesst::convert_digit_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 213 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_inputt target)
staticprivate

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

TODO: For now the radix argument is ignored

Parameters
targeta position in a goto program

Definition at line 223 of file character_refine_preprocess.cpp.

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

Referenced by initialize_conversion_table().

◆ convert_get_directionality_char()

codet character_refine_preprocesst::convert_get_directionality_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 242 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 253 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_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 263 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_inputt target)
staticprivate

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

TODO: For now this is only for ASCII characters

Parameters
targeta position in a goto program

Definition at line 274 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 283 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 294 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 303 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_inputt target)
staticprivate

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

Definition at line 327 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_high_surrogate().

Referenced by initialize_conversion_table().

◆ convert_is_alphabetic()

codet character_refine_preprocesst::convert_is_alphabetic ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 389 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 412 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 457 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_defined().

Referenced by convert_is_defined_int(), and initialize_conversion_table().

◆ convert_is_defined_int()

codet character_refine_preprocesst::convert_is_defined_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 467 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 504 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_digit().

Referenced by convert_is_digit_int(), and initialize_conversion_table().

◆ convert_is_digit_int()

codet character_refine_preprocesst::convert_is_digit_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 514 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 534 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_inputt target)
staticprivate

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

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

Parameters
targeta position in a goto program

Definition at line 565 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_identifier_ignorable().

Referenced by convert_is_identifier_ignorable_int(), and initialize_conversion_table().

◆ convert_is_identifier_ignorable_int()

codet character_refine_preprocesst::convert_is_identifier_ignorable_int ( conversion_inputt target)
staticprivate

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

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

Parameters
targeta position in a goto program

Definition at line 577 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 586 of file character_refine_preprocess.cpp.

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

Referenced by initialize_conversion_table().

◆ convert_is_ISO_control_char()

codet character_refine_preprocesst::convert_is_ISO_control_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 600 of file character_refine_preprocess.cpp.

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

Referenced by convert_is_ISO_control_int(), and initialize_conversion_table().

◆ convert_is_ISO_control_int()

codet character_refine_preprocesst::convert_is_ISO_control_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 615 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_inputt target)
staticprivate

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

TODO: For now we do not allow currency symbol, connecting punctuation, combining mark, non-spacing mark

Parameters
targeta position in a goto program

Definition at line 627 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_unicode_identifier_part().

Referenced by convert_is_java_letter_or_digit(), and initialize_conversion_table().

◆ convert_is_java_identifier_part_int()

codet character_refine_preprocesst::convert_is_java_identifier_part_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 637 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_inputt target)
staticprivate

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

TODO: For now we only allow letters and letter numbers. The java specification for this function is not precise on the other characters.

Parameters
targeta position in a goto program

Definition at line 650 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_unicode_identifier_start().

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

◆ convert_is_java_identifier_start_int()

codet character_refine_preprocesst::convert_is_java_identifier_start_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 660 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 669 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 678 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 687 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_letter().

Referenced by convert_is_letter_int(), and initialize_conversion_table().

◆ convert_is_letter_int()

codet character_refine_preprocesst::convert_is_letter_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 697 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 716 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_digit().

Referenced by convert_is_letter_or_digit_int(), and initialize_conversion_table().

◆ convert_is_letter_or_digit_int()

codet character_refine_preprocesst::convert_is_letter_or_digit_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 726 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 758 of file character_refine_preprocess.cpp.

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

Referenced by initialize_conversion_table().

◆ convert_is_lower_case_char()

codet character_refine_preprocesst::convert_is_lower_case_char ( conversion_inputt target)
staticprivate

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

TODO: For now we only consider ASCII characters

Parameters
targeta position in a goto program

Definition at line 737 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_ascii_lower_case().

Referenced by convert_is_lower_case_int(), and initialize_conversion_table().

◆ convert_is_lower_case_int()

codet character_refine_preprocesst::convert_is_lower_case_int ( conversion_inputt target)
staticprivate

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

TODO: For now we only consider ASCII characters

Parameters
targeta position in a goto program

Definition at line 749 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_inputt target)
staticprivate

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

TODO: For now only ASCII characters are considered

Parameters
targeta position in a goto program

Definition at line 787 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_mirrored().

Referenced by convert_is_mirrored_int(), and initialize_conversion_table().

◆ convert_is_mirrored_int()

codet character_refine_preprocesst::convert_is_mirrored_int ( conversion_inputt target)
staticprivate

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

TODO: For now only ASCII characters are considered

Parameters
targeta position in a goto program

Definition at line 799 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 808 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 831 of file character_refine_preprocess.cpp.

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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 841 of file character_refine_preprocess.cpp.

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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 861 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 881 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 891 of file character_refine_preprocess.cpp.

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

Referenced by initialize_conversion_table().

◆ convert_is_title_case_char()

codet character_refine_preprocesst::convert_is_title_case_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 924 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_title_case().

Referenced by convert_is_title_case_int(), and initialize_conversion_table().

◆ convert_is_title_case_int()

codet character_refine_preprocesst::convert_is_title_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 934 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 985 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_unicode_identifier_part().

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

◆ convert_is_unicode_identifier_part_int()

codet character_refine_preprocesst::convert_is_unicode_identifier_part_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 995 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1016 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_unicode_identifier_start().

Referenced by convert_is_unicode_identifier_start_int(), and initialize_conversion_table().

◆ convert_is_unicode_identifier_start_int()

codet character_refine_preprocesst::convert_is_unicode_identifier_start_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1026 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_inputt target)
staticprivate

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

TODO: For now we only consider ASCII characters

Parameters
targeta position in a goto program

Definition at line 1037 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_ascii_upper_case().

Referenced by convert_is_upper_case_int(), and initialize_conversion_table().

◆ convert_is_upper_case_int()

codet character_refine_preprocesst::convert_is_upper_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1047 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1067 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1099 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_is_whitespace().

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

◆ convert_is_whitespace_int()

codet character_refine_preprocesst::convert_is_whitespace_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1109 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1132 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1155 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_inputt 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 1188 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_inputt 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 1197 of file character_refine_preprocess.cpp.

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

Referenced by initialize_conversion_table().

◆ convert_to_lower_case_char()

codet character_refine_preprocesst::convert_to_lower_case_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1243 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_to_lower_case().

Referenced by convert_to_lower_case_int(), and initialize_conversion_table().

◆ convert_to_lower_case_int()

codet character_refine_preprocesst::convert_to_lower_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1253 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1299 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_to_title_case().

Referenced by convert_to_title_case_int(), and initialize_conversion_table().

◆ convert_to_title_case_int()

codet character_refine_preprocesst::convert_to_title_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1309 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_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1336 of file character_refine_preprocess.cpp.

References convert_char_function(), and expr_of_to_upper_case().

Referenced by convert_to_upper_case_int(), and initialize_conversion_table().

◆ convert_to_upper_case_int()

codet character_refine_preprocesst::convert_to_upper_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1346 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 91 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 314 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 380 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 338 of file character_refine_preprocess.cpp.

References in_interval_expr().

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

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

References in_interval_expr().

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

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

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

Referenced by convert_is_bmp_code_point(), and expr_of_to_chars().

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

References in_interval_expr().

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

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

References in_interval_expr().

Referenced by convert_is_identifier_ignorable_char(), and expr_of_is_unicode_identifier_part().

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

References expr_of_is_ascii_lower_case(), and expr_of_is_ascii_upper_case().

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

◆ 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 945 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 707 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 776 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 818 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 852 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 872 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 908 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 972 of file character_refine_preprocess.cpp.

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

Referenced by convert_is_java_identifier_part_char(), and convert_is_unicode_identifier_part_char().

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

References expr_of_is_letter(), and expr_of_is_letter_number().

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

◆ 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 1058 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 1082 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 1121 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 1144 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 1170 of file character_refine_preprocess.cpp.

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

Referenced by convert_to_chars().

◆ 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 1230 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 1263 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 1323 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 1374 of file character_refine_preprocess.cpp.

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

Referenced by java_string_library_preprocesst::initialize_conversion_table().

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

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

Referenced by java_string_library_preprocesst::replace_character_call().

Member Data Documentation

◆ conversion_table

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

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