cprover
character_refine_preprocesst Class Reference

#include <character_refine_preprocess.h>

+ Inheritance diagram for character_refine_preprocesst:
+ Collaboration diagram for character_refine_preprocesst:

Public Member Functions

void initialize_conversion_table ()
 fill maps with correspondance from java method names to conversion functions More...
 
codet replace_character_call (const code_function_callt &call) const
 replace function calls to functions of the Character by an affectation if possible, returns the same code otherwise. More...
 
- 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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. 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: '\u0000' through '\u0008' '\u000E' through '\u001B' '\u007F' through '\u009F'. More...
 
static codet convert_is_identifier_ignorable_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isIdentifierIgnorable:(C)Z. More...
 
static codet convert_is_identifier_ignorable_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isIdentifierIgnorable:(I)Z. More...
 
static codet convert_is_ideographic (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isIdeographic:(I)Z. More...
 
static codet convert_is_ISO_control_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(C)Z. More...
 
static codet convert_is_ISO_control_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isISOControl:(I)Z. More...
 
static codet convert_is_java_identifier_part_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isJavaIdentifierPart:(C)Z. More...
 
static codet convert_is_java_identifier_part_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierPart:(I)Z. More...
 
static codet convert_is_java_identifier_start_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierStart:(C)Z. More...
 
static codet convert_is_java_identifier_start_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method isJavaIdentifierStart:(I)Z. More...
 
static codet convert_is_java_letter (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isJavaLetter:(C)Z. More...
 
static codet convert_is_java_letter_or_digit (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method isJavaLetterOrDigit:(C)Z. More...
 
static exprt expr_of_is_letter (const exprt &chr, const typet &type)
 Determines if the specified character is a letter. More...
 
static codet convert_is_letter_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(C)Z. More...
 
static codet convert_is_letter_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLetter:(I)Z. More...
 
static exprt expr_of_is_letter_or_digit (const exprt &chr, const typet &type)
 Determines if the specified character is a letter or digit. More...
 
static codet convert_is_letter_or_digit_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(C)Z. More...
 
static codet convert_is_letter_or_digit_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLetterOrDigit:(I)Z. More...
 
static exprt expr_of_is_ascii_lower_case (const exprt &chr, const typet &type)
 Determines if the specified character is an ASCII lowercase character. More...
 
static codet convert_is_lower_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLowerCase:(C)Z. More...
 
static codet convert_is_lower_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLowerCase:(I)Z. More...
 
static codet convert_is_low_surrogate (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isLowSurrogate:(C)Z. More...
 
static exprt expr_of_is_mirrored (const exprt &chr, const typet &type)
 Determines whether the character is mirrored according to the Unicode specification. More...
 
static codet convert_is_mirrored_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isMirrored:(C)Z. More...
 
static codet convert_is_mirrored_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isMirrored:(I)Z. More...
 
static codet convert_is_space (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSpace:(C)Z. More...
 
static exprt expr_of_is_space_char (const exprt &chr, const typet &type)
 Determines if the specified character is white space according to Unicode (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR) More...
 
static codet convert_is_space_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(C)Z. More...
 
static codet convert_is_space_char_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSpaceChar:(I)Z. More...
 
static exprt expr_of_is_supplementary_code_point (const exprt &chr, const typet &type)
 Determines whether the specified character (Unicode code point) is in the supplementary character range. More...
 
static codet convert_is_supplementary_code_point (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSupplementaryCodePoint:(I)Z. More...
 
static exprt expr_of_is_surrogate (const exprt &chr, const typet &type)
 Determines if the given char value is a Unicode surrogate code unit. More...
 
static codet convert_is_surrogate (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogate:(C)Z. More...
 
static codet convert_is_surrogate_pair (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isSurrogatePair:(CC)Z. More...
 
static exprt expr_of_is_title_case (const exprt &chr, const typet &type)
 Determines if the specified character is a titlecase character. More...
 
static codet convert_is_title_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(C)Z. More...
 
static codet convert_is_title_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isTitleCase:(I)Z. More...
 
static exprt expr_of_is_letter_number (const exprt &chr, const typet &type)
 Determines if the specified character is in the LETTER_NUMBER category of Unicode. More...
 
static exprt expr_of_is_unicode_identifier_part (const exprt &chr, const typet &type)
 Determines if the character may be part of a Unicode identifier. More...
 
static codet convert_is_unicode_identifier_part_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(C)Z. More...
 
static codet convert_is_unicode_identifier_part_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierPart:(I)Z. More...
 
static exprt expr_of_is_unicode_identifier_start (const exprt &chr, const typet &type)
 Determines if the specified character is permissible as the first character in a Unicode identifier. More...
 
static codet convert_is_unicode_identifier_start_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(C)Z. More...
 
static codet convert_is_unicode_identifier_start_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUnicodeIdentifierStart:(I)Z. More...
 
static exprt expr_of_is_ascii_upper_case (const exprt &chr, const typet &type)
 Determines if the specified character is an ASCII uppercase character. More...
 
static codet convert_is_upper_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUpperCase:(C)Z. More...
 
static codet convert_is_upper_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isUpperCase:(I)Z. More...
 
static exprt expr_of_is_valid_code_point (const exprt &chr, const typet &type)
 Determines whether the specified code point is a valid Unicode code point value. More...
 
static codet convert_is_valid_code_point (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isValidCodePoint:(I)Z. More...
 
static exprt expr_of_is_whitespace (const exprt &chr, const typet &type)
 Determines if the specified character is white space according to Java. More...
 
static codet convert_is_whitespace_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(C)Z. More...
 
static codet convert_is_whitespace_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.isWhitespace:(I)Z. More...
 
static exprt expr_of_low_surrogate (const exprt &chr, const typet &type)
 Returns the trailing surrogate (a low surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding. More...
 
static codet convert_low_surrogate (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.lowSurrogate:(I)C. More...
 
static exprt expr_of_reverse_bytes (const exprt &chr, const typet &type)
 Returns the value obtained by reversing the order of the bytes in the specified char value. More...
 
static codet convert_reverse_bytes (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.reverseBytes:(C)C. More...
 
static exprt expr_of_to_chars (const exprt &chr, const typet &type)
 Converts the specified character (Unicode code point) to its UTF-16 representation stored in a char array. More...
 
static codet convert_to_chars (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toChars:(I)[C. More...
 
static codet convert_to_code_point (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toCodePoint:(CC)I. More...
 
static exprt expr_of_to_lower_case (const exprt &chr, const typet &type)
 Converts the character argument to lowercase. More...
 
static codet convert_to_lower_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(C)C. More...
 
static codet convert_to_lower_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toLowerCase:(I)I. More...
 
static exprt expr_of_to_title_case (const exprt &chr, const typet &type)
 Converts the character argument to titlecase. More...
 
static codet convert_to_title_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(C)C. More...
 
static codet convert_to_title_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toTitleCase:(I)I. More...
 
static exprt expr_of_to_upper_case (const exprt &chr, const typet &type)
 Converts the character argument to uppercase. More...
 
static codet convert_to_upper_case_char (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(C)C. More...
 
static codet convert_to_upper_case_int (conversion_inputt &target)
 Converts function call to an assignment of an expression corresponding to the java method Character.toUpperCase:(I)I. More...
 
static codet convert_char_function (exprt(*expr_function)(const exprt &chr, const typet &type), conversion_inputt &target)
 converts based on a function on expressions More...
 
static exprt in_interval_expr (const exprt &chr, const mp_integer &lower_bound, const mp_integer &upper_bound)
 The returned expression is true when the first argument is in the interval defined by the lower and upper bounds (included) More...
 
static exprt in_list_expr (const exprt &chr, const std::list< mp_integer > &list)
 The returned expression is true when the given character is equal to one of the element in the list. More...
 

Private Attributes

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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 
- 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.

◆ convert_char_function()

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

converts based on a function on expressions

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

Definition at line 24 of file character_refine_preprocess.cpp.

◆ convert_char_value()

codet character_refine_preprocesst::convert_char_value ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 100 of file character_refine_preprocess.cpp.

◆ convert_compare()

codet character_refine_preprocesst::convert_compare ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 110 of file character_refine_preprocess.cpp.

◆ convert_digit_char()

codet character_refine_preprocesst::convert_digit_char ( conversion_inputt target)
staticprivate

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

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

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

Definition at line 136 of file character_refine_preprocess.cpp.

◆ convert_digit_int()

codet character_refine_preprocesst::convert_digit_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 213 of file character_refine_preprocess.cpp.

◆ convert_for_digit()

codet character_refine_preprocesst::convert_for_digit ( conversion_inputt target)
staticprivate

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

TODO: For now the radix argument is ignored

Parameters
targeta position in a goto program

Definition at line 223 of file character_refine_preprocess.cpp.

◆ convert_get_directionality_char()

codet character_refine_preprocesst::convert_get_directionality_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 242 of file character_refine_preprocess.cpp.

◆ convert_get_directionality_int()

codet character_refine_preprocesst::convert_get_directionality_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 253 of file character_refine_preprocess.cpp.

◆ convert_get_numeric_value_char()

codet character_refine_preprocesst::convert_get_numeric_value_char ( conversion_inputt target)
staticprivate

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

TODO: For now this is only for ASCII characters

Definition at line 263 of file character_refine_preprocess.cpp.

◆ convert_get_numeric_value_int()

codet character_refine_preprocesst::convert_get_numeric_value_int ( conversion_inputt target)
staticprivate

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

TODO: For now this is only for ASCII characters

Parameters
targeta position in a goto program

Definition at line 274 of file character_refine_preprocess.cpp.

◆ convert_get_type_char()

codet character_refine_preprocesst::convert_get_type_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 283 of file character_refine_preprocess.cpp.

◆ convert_get_type_int()

codet character_refine_preprocesst::convert_get_type_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 294 of file character_refine_preprocess.cpp.

◆ convert_hash_code()

codet character_refine_preprocesst::convert_hash_code ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 303 of file character_refine_preprocess.cpp.

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

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

◆ convert_is_bmp_code_point()

codet character_refine_preprocesst::convert_is_bmp_code_point ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 416 of file character_refine_preprocess.cpp.

◆ convert_is_defined_char()

codet character_refine_preprocesst::convert_is_defined_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 462 of file character_refine_preprocess.cpp.

◆ convert_is_defined_int()

codet character_refine_preprocesst::convert_is_defined_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 472 of file character_refine_preprocess.cpp.

◆ convert_is_digit_char()

codet character_refine_preprocesst::convert_is_digit_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 510 of file character_refine_preprocess.cpp.

◆ convert_is_digit_int()

codet character_refine_preprocesst::convert_is_digit_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 520 of file character_refine_preprocess.cpp.

◆ convert_is_high_surrogate()

codet character_refine_preprocesst::convert_is_high_surrogate ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 541 of file character_refine_preprocess.cpp.

◆ convert_is_identifier_ignorable_char()

codet character_refine_preprocesst::convert_is_identifier_ignorable_char ( conversion_inputt target)
staticprivate

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

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

Parameters
targeta position in a goto program

Definition at line 573 of file character_refine_preprocess.cpp.

◆ convert_is_identifier_ignorable_int()

codet character_refine_preprocesst::convert_is_identifier_ignorable_int ( conversion_inputt target)
staticprivate

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

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

Parameters
targeta position in a goto program

Definition at line 585 of file character_refine_preprocess.cpp.

◆ convert_is_ideographic()

codet character_refine_preprocesst::convert_is_ideographic ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 594 of file character_refine_preprocess.cpp.

◆ convert_is_ISO_control_char()

codet character_refine_preprocesst::convert_is_ISO_control_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 608 of file character_refine_preprocess.cpp.

◆ convert_is_ISO_control_int()

codet character_refine_preprocesst::convert_is_ISO_control_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 623 of file character_refine_preprocess.cpp.

◆ convert_is_java_identifier_part_char()

codet character_refine_preprocesst::convert_is_java_identifier_part_char ( conversion_inputt target)
staticprivate

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

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

Parameters
targeta position in a goto program

Definition at line 635 of file character_refine_preprocess.cpp.

◆ convert_is_java_identifier_part_int()

codet character_refine_preprocesst::convert_is_java_identifier_part_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 645 of file character_refine_preprocess.cpp.

◆ convert_is_java_identifier_start_char()

codet character_refine_preprocesst::convert_is_java_identifier_start_char ( conversion_inputt target)
staticprivate

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

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

Parameters
targeta position in a goto program

Definition at line 658 of file character_refine_preprocess.cpp.

◆ convert_is_java_identifier_start_int()

codet character_refine_preprocesst::convert_is_java_identifier_start_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 668 of file character_refine_preprocess.cpp.

◆ convert_is_java_letter()

codet character_refine_preprocesst::convert_is_java_letter ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 677 of file character_refine_preprocess.cpp.

◆ convert_is_java_letter_or_digit()

codet character_refine_preprocesst::convert_is_java_letter_or_digit ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 686 of file character_refine_preprocess.cpp.

◆ convert_is_letter_char()

codet character_refine_preprocesst::convert_is_letter_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 695 of file character_refine_preprocess.cpp.

◆ convert_is_letter_int()

codet character_refine_preprocesst::convert_is_letter_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 705 of file character_refine_preprocess.cpp.

◆ convert_is_letter_or_digit_char()

codet character_refine_preprocesst::convert_is_letter_or_digit_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 724 of file character_refine_preprocess.cpp.

◆ convert_is_letter_or_digit_int()

codet character_refine_preprocesst::convert_is_letter_or_digit_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 734 of file character_refine_preprocess.cpp.

◆ convert_is_low_surrogate()

codet character_refine_preprocesst::convert_is_low_surrogate ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 766 of file character_refine_preprocess.cpp.

◆ convert_is_lower_case_char()

codet character_refine_preprocesst::convert_is_lower_case_char ( conversion_inputt target)
staticprivate

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

TODO: For now we only consider ASCII characters

Parameters
targeta position in a goto program

Definition at line 745 of file character_refine_preprocess.cpp.

◆ convert_is_lower_case_int()

codet character_refine_preprocesst::convert_is_lower_case_int ( conversion_inputt target)
staticprivate

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

TODO: For now we only consider ASCII characters

Parameters
targeta position in a goto program

Definition at line 757 of file character_refine_preprocess.cpp.

◆ convert_is_mirrored_char()

codet character_refine_preprocesst::convert_is_mirrored_char ( conversion_inputt target)
staticprivate

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

TODO: For now only ASCII characters are considered

Parameters
targeta position in a goto program

Definition at line 796 of file character_refine_preprocess.cpp.

◆ convert_is_mirrored_int()

codet character_refine_preprocesst::convert_is_mirrored_int ( conversion_inputt target)
staticprivate

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

TODO: For now only ASCII characters are considered

Parameters
targeta position in a goto program

Definition at line 808 of file character_refine_preprocess.cpp.

◆ convert_is_space()

codet character_refine_preprocesst::convert_is_space ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 817 of file character_refine_preprocess.cpp.

◆ convert_is_space_char()

codet character_refine_preprocesst::convert_is_space_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 841 of file character_refine_preprocess.cpp.

◆ convert_is_space_char_int()

codet character_refine_preprocesst::convert_is_space_char_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 851 of file character_refine_preprocess.cpp.

◆ convert_is_supplementary_code_point()

codet character_refine_preprocesst::convert_is_supplementary_code_point ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 872 of file character_refine_preprocess.cpp.

◆ convert_is_surrogate()

codet character_refine_preprocesst::convert_is_surrogate ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 893 of file character_refine_preprocess.cpp.

◆ convert_is_surrogate_pair()

codet character_refine_preprocesst::convert_is_surrogate_pair ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 903 of file character_refine_preprocess.cpp.

◆ convert_is_title_case_char()

codet character_refine_preprocesst::convert_is_title_case_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 937 of file character_refine_preprocess.cpp.

◆ convert_is_title_case_int()

codet character_refine_preprocesst::convert_is_title_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 947 of file character_refine_preprocess.cpp.

◆ convert_is_unicode_identifier_part_char()

codet character_refine_preprocesst::convert_is_unicode_identifier_part_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 999 of file character_refine_preprocess.cpp.

◆ convert_is_unicode_identifier_part_int()

codet character_refine_preprocesst::convert_is_unicode_identifier_part_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1009 of file character_refine_preprocess.cpp.

◆ convert_is_unicode_identifier_start_char()

codet character_refine_preprocesst::convert_is_unicode_identifier_start_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1030 of file character_refine_preprocess.cpp.

◆ convert_is_unicode_identifier_start_int()

codet character_refine_preprocesst::convert_is_unicode_identifier_start_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1040 of file character_refine_preprocess.cpp.

◆ convert_is_upper_case_char()

codet character_refine_preprocesst::convert_is_upper_case_char ( conversion_inputt target)
staticprivate

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

TODO: For now we only consider ASCII characters

Parameters
targeta position in a goto program

Definition at line 1051 of file character_refine_preprocess.cpp.

◆ convert_is_upper_case_int()

codet character_refine_preprocesst::convert_is_upper_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1061 of file character_refine_preprocess.cpp.

◆ convert_is_valid_code_point()

codet character_refine_preprocesst::convert_is_valid_code_point ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1082 of file character_refine_preprocess.cpp.

◆ convert_is_whitespace_char()

codet character_refine_preprocesst::convert_is_whitespace_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1115 of file character_refine_preprocess.cpp.

◆ convert_is_whitespace_int()

codet character_refine_preprocesst::convert_is_whitespace_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1125 of file character_refine_preprocess.cpp.

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

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

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

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

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

◆ convert_to_lower_case_int()

codet character_refine_preprocesst::convert_to_lower_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1269 of file character_refine_preprocess.cpp.

◆ convert_to_title_case_char()

codet character_refine_preprocesst::convert_to_title_case_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1315 of file character_refine_preprocess.cpp.

◆ convert_to_title_case_int()

codet character_refine_preprocesst::convert_to_title_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1325 of file character_refine_preprocess.cpp.

◆ convert_to_upper_case_char()

codet character_refine_preprocesst::convert_to_upper_case_char ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1352 of file character_refine_preprocess.cpp.

◆ convert_to_upper_case_int()

codet character_refine_preprocesst::convert_to_upper_case_int ( conversion_inputt target)
staticprivate

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

Parameters
targeta position in a goto program

Definition at line 1362 of file character_refine_preprocess.cpp.

◆ expr_of_char_count()

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

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

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

Definition at line 71 of file character_refine_preprocess.cpp.

◆ expr_of_char_value()

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

Casts the given expression to the given type.

Returns
An expression of the given type

Definition at line 91 of file character_refine_preprocess.cpp.

◆ expr_of_high_surrogate()

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

Returns the leading surrogate (a high surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding.

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

Definition at line 314 of file character_refine_preprocess.cpp.

◆ expr_of_is_alphabetic()

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

Determines if the specified character (Unicode code point) is alphabetic.

TODO: for now this is only for ASCII characters, the following unicode categorise are not yet considered: TITLECASE_LETTER MODIFIER_LETTER OTHER_LETTER LETTER_NUMBER and contributory property Other_Alphabetic as defined by the Unicode Standard.

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

Definition at line 382 of file character_refine_preprocess.cpp.

◆ expr_of_is_ascii_lower_case()

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

Determines if the specified character is an ASCII lowercase character.

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

Definition at line 338 of file character_refine_preprocess.cpp.

◆ expr_of_is_ascii_upper_case()

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

Determines if the specified character is an ASCII uppercase character.

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

Definition at line 349 of file character_refine_preprocess.cpp.

◆ expr_of_is_bmp_code_point()

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

Determines whether the specified character (Unicode code point) is in the Basic Multilingual Plane (BMP).

Such code points can be represented using a single char.

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

Definition at line 404 of file character_refine_preprocess.cpp.

◆ expr_of_is_defined()

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

Determines if a character is defined in Unicode.

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

Definition at line 427 of file character_refine_preprocess.cpp.

◆ expr_of_is_digit()

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

Determines if the specified character is a digit.

A character is a digit if its general category type, provided by Character.getType(ch), is DECIMAL_DIGIT_NUMBER.

TODO: for now we only support these ranges of digits: '\u0030' through '\u0039', ISO-LATIN-1 digits ('0' through '9') '\u0660' through '\u0669', Arabic-Indic digits '\u06F0' through '\u06F9', Extended Arabic-Indic digits '\u0966' through '\u096F', Devanagari digits '\uFF10' through '\uFF19', Fullwidth digits Many other character ranges contain digits as well.

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

Definition at line 492 of file character_refine_preprocess.cpp.

◆ expr_of_is_high_surrogate()

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

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

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

Definition at line 531 of file character_refine_preprocess.cpp.

◆ expr_of_is_identifier_ignorable()

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

Determines if the character is one of ignorable in a Java identifier, that is, it is in one of these ranges: '\u0000' through '\u0008' '\u000E' through '\u001B' '\u007F' through '\u009F'.

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

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

Definition at line 556 of file character_refine_preprocess.cpp.

◆ expr_of_is_letter()

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

Determines if the specified character is a letter.

TODO: for now this is only for ASCII characters, the following unicode categories are not yet considered: TITLECASE_LETTER MODIFIER_LETTER OTHER_LETTER LETTER_NUMBER

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

Definition at line 364 of file character_refine_preprocess.cpp.

◆ expr_of_is_letter_number()

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

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

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

Definition at line 958 of file character_refine_preprocess.cpp.

◆ expr_of_is_letter_or_digit()

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

Determines if the specified character is a letter or digit.

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

Definition at line 715 of file character_refine_preprocess.cpp.

◆ expr_of_is_mirrored()

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

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

TODO: For now only ASCII characters are considered

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

Definition at line 784 of file character_refine_preprocess.cpp.

◆ expr_of_is_space_char()

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

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

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

Definition at line 827 of file character_refine_preprocess.cpp.

◆ expr_of_is_supplementary_code_point()

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

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

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

Definition at line 862 of file character_refine_preprocess.cpp.

◆ expr_of_is_surrogate()

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

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

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

Definition at line 883 of file character_refine_preprocess.cpp.

◆ expr_of_is_title_case()

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

Determines if the specified character is a titlecase character.

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

Definition at line 920 of file character_refine_preprocess.cpp.

◆ expr_of_is_unicode_identifier_part()

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

Determines if the character may be part of a Unicode identifier.

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

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

Definition at line 986 of file character_refine_preprocess.cpp.

◆ expr_of_is_unicode_identifier_start()

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

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

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

Definition at line 1020 of file character_refine_preprocess.cpp.

◆ expr_of_is_valid_code_point()

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

Determines whether the specified code point is a valid Unicode code point value.

That is, in the range of integers from 0 to 0x10FFFF

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

Definition at line 1072 of file character_refine_preprocess.cpp.

◆ expr_of_is_whitespace()

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

Determines if the specified character is white space according to Java.

It is the case when it one of the following: * a Unicode space character (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR) but is not also a non-breaking space ('\u00A0', '\u2007', '\u202F'). * it is one of these: U+0009 U+000A U+000B U+000C U+000D U+001C U+001D U+001E U+001F

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

Definition at line 1097 of file character_refine_preprocess.cpp.

◆ expr_of_low_surrogate()

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

Returns the trailing surrogate (a low surrogate code unit) of the surrogate pair representing the specified supplementary character (Unicode code point) in the UTF-16 encoding.

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

Definition at line 1137 of file character_refine_preprocess.cpp.

◆ expr_of_reverse_bytes()

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

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

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

Definition at line 1160 of file character_refine_preprocess.cpp.

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

Definition at line 1186 of file character_refine_preprocess.cpp.

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

◆ expr_of_to_title_case()

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

Converts the character argument to titlecase.

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

Definition at line 1279 of file character_refine_preprocess.cpp.

◆ expr_of_to_upper_case()

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

Converts the character argument to uppercase.

TODO: For now we only consider ASCII characters but ultimately we should use case mapping information from the UnicodeData file

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

Definition at line 1339 of file character_refine_preprocess.cpp.

◆ in_interval_expr()

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

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

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

Definition at line 42 of file character_refine_preprocess.cpp.

◆ in_list_expr()

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

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

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

Definition at line 57 of file character_refine_preprocess.cpp.

◆ initialize_conversion_table()

void character_refine_preprocesst::initialize_conversion_table ( )

fill maps with correspondance from java method names to conversion functions

Definition at line 1390 of file character_refine_preprocess.cpp.

◆ replace_character_call()

codet character_refine_preprocesst::replace_character_call ( const code_function_callt code) const

replace function calls to functions of the Character by an affectation if possible, returns the same code otherwise.

For this method to have an effect initialize_conversion_table must have been called before.

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

Definition at line 1374 of file character_refine_preprocess.cpp.

Member Data Documentation

◆ conversion_table

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

Definition at line 39 of file character_refine_preprocess.h.


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