cprover
character_refine_preprocess.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Preprocess a goto-programs so that calls to the java Character
4  library are replaced by simple expressions.
5  For now support is limited to character in the ASCII range,
6  some methods may have incorrect specifications outside of this range.
7 
8 Author: Romain Brenguier
9 
10 Date: March 2017
11 
12 \*******************************************************************/
13 
19 
20 #ifndef CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
21 #define CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
22 
23 #include <util/std_code.h>
24 #include <util/mp_arith.h>
25 
26 #include <unordered_map>
27 
29 {
30 public:
33 
34 private:
37  // A table tells us what method to call for each java method signature
38  std::unordered_map<irep_idt, conversion_functiont> conversion_table;
39 
40  // Conversion functions
41  static exprt expr_of_char_count(const exprt &chr, const typet &type);
43  static exprt expr_of_char_value(const exprt &chr, const typet &type);
45  static codet convert_compare(conversion_inputt &target);
56  static exprt expr_of_high_surrogate(const exprt &chr, const typet &type);
58  static exprt expr_of_is_alphabetic(const exprt &chr, const typet &type);
60  static exprt expr_of_is_bmp_code_point(const exprt &chr, const typet &type);
62  static exprt expr_of_is_defined(const exprt &chr, const typet &type);
65  static exprt expr_of_is_digit(const exprt &chr, const typet &type);
68  static exprt expr_of_is_high_surrogate(const exprt &chr, const typet &type);
71  const exprt &chr, const typet &type);
83  static exprt expr_of_is_letter(const exprt &chr, const typet &type);
86  static exprt expr_of_is_letter_or_digit(const exprt &chr, const typet &type);
89  static exprt expr_of_is_ascii_lower_case(const exprt &chr, const typet &type);
93  static exprt expr_of_is_mirrored(const exprt &chr, const typet &type);
97  static exprt expr_of_is_space_char(const exprt &chr, const typet &type);
101  const exprt &chr, const typet &type);
103  static exprt expr_of_is_surrogate(const exprt &chr, const typet &type);
106  static exprt expr_of_is_title_case(const exprt &chr, const typet &type);
109  static exprt expr_of_is_letter_number(const exprt &chr, const typet &type);
111  const exprt &chr, const typet &type);
113  conversion_inputt &target);
115  conversion_inputt &target);
117  const exprt &chr, const typet &type);
119  conversion_inputt &target);
121  conversion_inputt &target);
122  static exprt expr_of_is_ascii_upper_case(const exprt &chr, const typet &type);
125  static exprt expr_of_is_valid_code_point(const exprt &chr, const typet &type);
127  static exprt expr_of_is_whitespace(const exprt &chr, const typet &type);
130  static exprt expr_of_low_surrogate(const exprt &chr, const typet &type);
132  static exprt expr_of_reverse_bytes(const exprt &chr, const typet &type);
134  static exprt expr_of_to_chars(const exprt &chr, const typet &type);
136  static exprt expr_of_to_lower_case(const exprt &chr, const typet &type);
139  static exprt expr_of_to_title_case(const exprt &chr, const typet &type);
142  static exprt expr_of_to_upper_case(const exprt &chr, const typet &type);
145 
146  // Helper functions
148  exprt (*expr_function)(const exprt &chr, const typet &type),
149  conversion_inputt &target);
150  static exprt in_interval_expr(
151  const exprt &chr,
152  const mp_integer &lower_bound,
153  const mp_integer &upper_bound);
154  static exprt in_list_expr(
155  const exprt &chr, const std::list<mp_integer> &list);
156 };
157 
158 #endif // CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
character_refine_preprocesst::convert_is_letter_or_digit_int
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....
Definition: character_refine_preprocess.cpp:724
character_refine_preprocesst::expr_of_high_surrogate
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 spe...
Definition: character_refine_preprocess.cpp:313
character_refine_preprocesst::convert_is_unicode_identifier_start_char
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....
Definition: character_refine_preprocess.cpp:1020
character_refine_preprocesst::expr_of_char_value
static exprt expr_of_char_value(const exprt &chr, const typet &type)
Casts the given expression to the given type.
Definition: character_refine_preprocess.cpp:91
character_refine_preprocesst::convert_is_digit_int
static codet convert_is_digit_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:510
character_refine_preprocesst::convert_compare
static codet convert_compare(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:110
character_refine_preprocesst::expr_of_is_supplementary_code_point
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 ran...
Definition: character_refine_preprocess.cpp:852
character_refine_preprocesst::convert_to_lower_case_char
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....
Definition: character_refine_preprocess.cpp:1178
character_refine_preprocesst::convert_char_value
static codet convert_char_value(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:100
character_refine_preprocesst::convert_is_ISO_control_char
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....
Definition: character_refine_preprocess.cpp:598
character_refine_preprocesst::convert_is_lower_case_int
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....
Definition: character_refine_preprocess.cpp:747
mp_arith.h
character_refine_preprocesst::convert_digit_int
static codet convert_digit_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:212
character_refine_preprocesst::convert_reverse_bytes
static codet convert_reverse_bytes(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1151
character_refine_preprocesst::convert_is_surrogate_pair
static codet convert_is_surrogate_pair(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:893
character_refine_preprocesst::convert_is_whitespace_int
static codet convert_is_whitespace_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1115
typet
The type of an expression, extends irept.
Definition: type.h:29
character_refine_preprocesst::convert_is_alphabetic
static codet convert_is_alphabetic(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:381
character_refine_preprocesst::expr_of_low_surrogate
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 spe...
Definition: character_refine_preprocess.cpp:1127
character_refine_preprocesst::expr_of_reverse_bytes
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.
Definition: character_refine_preprocess.cpp:1140
character_refine_preprocesst::convert_hash_code
static codet convert_hash_code(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:302
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
character_refine_preprocesst::convert_is_upper_case_char
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....
Definition: character_refine_preprocess.cpp:1041
character_refine_preprocesst::expr_of_is_mirrored
static exprt expr_of_is_mirrored(const exprt &chr, const typet &type)
Determines whether the character is mirrored according to the Unicode specification.
Definition: character_refine_preprocess.cpp:774
character_refine_preprocesst
Definition: character_refine_preprocess.h:29
character_refine_preprocesst::convert_is_unicode_identifier_part_int
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....
Definition: character_refine_preprocess.cpp:999
character_refine_preprocesst::expr_of_is_identifier_ignorable
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 ...
Definition: character_refine_preprocess.cpp:546
character_refine_preprocesst::convert_is_defined_char
static codet convert_is_defined_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:452
character_refine_preprocesst::expr_of_is_letter_number
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.
Definition: character_refine_preprocess.cpp:948
exprt
Base class for all expressions.
Definition: expr.h:53
character_refine_preprocesst::convert_to_upper_case_int
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....
Definition: character_refine_preprocess.cpp:1275
character_refine_preprocesst::convert_is_lower_case_char
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....
Definition: character_refine_preprocess.cpp:735
character_refine_preprocesst::convert_is_whitespace_char
static codet convert_is_whitespace_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1105
character_refine_preprocesst::expr_of_is_surrogate
static exprt expr_of_is_surrogate(const exprt &chr, const typet &type)
Determines if the given char value is a Unicode surrogate code unit.
Definition: character_refine_preprocess.cpp:873
character_refine_preprocesst::convert_is_letter_or_digit_char
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....
Definition: character_refine_preprocess.cpp:714
character_refine_preprocesst::convert_is_title_case_char
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....
Definition: character_refine_preprocess.cpp:927
character_refine_preprocesst::expr_of_is_valid_code_point
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.
Definition: character_refine_preprocess.cpp:1062
character_refine_preprocesst::convert_is_mirrored_char
static codet convert_is_mirrored_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:786
character_refine_preprocesst::convert_to_chars
static codet convert_to_chars(conversion_inputt &target)
character_refine_preprocesst::expr_of_is_bmp_code_point
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 (B...
Definition: character_refine_preprocess.cpp:394
character_refine_preprocesst::convert_is_unicode_identifier_start_int
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....
Definition: character_refine_preprocess.cpp:1030
character_refine_preprocesst::convert_is_valid_code_point
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....
Definition: character_refine_preprocess.cpp:1072
character_refine_preprocesst::expr_of_is_digit
static exprt expr_of_is_digit(const exprt &chr, const typet &type)
Determines if the specified character is a digit.
Definition: character_refine_preprocess.cpp:482
character_refine_preprocesst::convert_is_surrogate
static codet convert_is_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:883
character_refine_preprocesst::convert_is_java_identifier_start_char
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 isJavaIdent...
Definition: character_refine_preprocess.cpp:648
character_refine_preprocesst::convert_get_directionality_int
static codet convert_get_directionality_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:252
character_refine_preprocesst::conversion_table
std::unordered_map< irep_idt, conversion_functiont > conversion_table
Definition: character_refine_preprocess.h:38
character_refine_preprocesst::convert_is_space
static codet convert_is_space(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:807
character_refine_preprocesst::expr_of_is_title_case
static exprt expr_of_is_title_case(const exprt &chr, const typet &type)
Determines if the specified character is a titlecase character.
Definition: character_refine_preprocess.cpp:910
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
character_refine_preprocesst::convert_for_digit
static codet convert_for_digit(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:222
character_refine_preprocesst::expr_of_is_letter_or_digit
static exprt expr_of_is_letter_or_digit(const exprt &chr, const typet &type)
Determines if the specified character is a letter or digit.
Definition: character_refine_preprocess.cpp:705
character_refine_preprocesst::convert_is_upper_case_int
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....
Definition: character_refine_preprocess.cpp:1051
character_refine_preprocesst::expr_of_to_lower_case
static exprt expr_of_to_lower_case(const exprt &chr, const typet &type)
Converts the character argument to lowercase.
Definition: character_refine_preprocess.cpp:1166
character_refine_preprocesst::expr_of_is_high_surrogate
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-surro...
Definition: character_refine_preprocess.cpp:521
character_refine_preprocesst::convert_get_type_char
static codet convert_get_type_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:282
character_refine_preprocesst::convert_high_surrogate
static codet convert_high_surrogate(conversion_inputt &target)
character_refine_preprocesst::expr_of_is_alphabetic
static exprt expr_of_is_alphabetic(const exprt &chr, const typet &type)
Determines if the specified character (Unicode code point) is alphabetic.
Definition: character_refine_preprocess.cpp:372
character_refine_preprocesst::convert_low_surrogate
static codet convert_low_surrogate(conversion_inputt &target)
character_refine_preprocesst::convert_get_directionality_char
static codet convert_get_directionality_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:241
character_refine_preprocesst::expr_of_to_upper_case
static exprt expr_of_to_upper_case(const exprt &chr, const typet &type)
Converts the character argument to uppercase.
Definition: character_refine_preprocess.cpp:1253
character_refine_preprocesst::convert_is_space_char
static codet convert_is_space_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:831
character_refine_preprocesst::expr_of_to_title_case
static exprt expr_of_to_title_case(const exprt &chr, const typet &type)
Converts the character argument to titlecase.
Definition: character_refine_preprocess.cpp:1198
character_refine_preprocesst::convert_is_defined_int
static codet convert_is_defined_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:462
character_refine_preprocesst::convert_is_high_surrogate
static codet convert_is_high_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:531
character_refine_preprocesst::in_interval_expr
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 u...
Definition: character_refine_preprocess.cpp:42
character_refine_preprocesst::convert_get_numeric_value_char
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....
Definition: character_refine_preprocess.cpp:262
character_refine_preprocesst::convert_to_lower_case_int
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....
Definition: character_refine_preprocess.cpp:1188
character_refine_preprocesst::convert_is_space_char_int
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....
Definition: character_refine_preprocess.cpp:841
character_refine_preprocesst::convert_is_letter_int
static codet convert_is_letter_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:695
character_refine_preprocesst::convert_is_bmp_code_point
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....
Definition: character_refine_preprocess.cpp:406
character_refine_preprocesst::in_list_expr
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.
Definition: character_refine_preprocess.cpp:57
character_refine_preprocesst::convert_is_java_identifier_part_char
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....
Definition: character_refine_preprocess.cpp:625
character_refine_preprocesst::convert_is_low_surrogate
static codet convert_is_low_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:756
character_refine_preprocesst::expr_of_is_unicode_identifier_start
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.
Definition: character_refine_preprocess.cpp:1010
character_refine_preprocesst::expr_of_is_defined
static exprt expr_of_is_defined(const exprt &chr, const typet &type)
Determines if a character is defined in Unicode.
Definition: character_refine_preprocess.cpp:417
character_refine_preprocesst::convert_digit_char
static codet convert_digit_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:135
std_code.h
character_refine_preprocesst::convert_is_letter_char
static codet convert_is_letter_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:685
character_refine_preprocesst::convert_is_mirrored_int
static codet convert_is_mirrored_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:798
character_refine_preprocesst::expr_of_is_space_char
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,...
Definition: character_refine_preprocess.cpp:817
character_refine_preprocesst::convert_to_title_case_char
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....
Definition: character_refine_preprocess.cpp:1229
character_refine_preprocesst::expr_of_is_ascii_lower_case
static exprt expr_of_is_ascii_lower_case(const exprt &chr, const typet &type)
Determines if the specified character is an ASCII lowercase character.
Definition: character_refine_preprocess.cpp:328
character_refine_preprocesst::convert_get_numeric_value_int
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....
Definition: character_refine_preprocess.cpp:273
character_refine_preprocesst::expr_of_is_letter
static exprt expr_of_is_letter(const exprt &chr, const typet &type)
Determines if the specified character is a letter.
Definition: character_refine_preprocess.cpp:354
character_refine_preprocesst::convert_char_count
static codet convert_char_count(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:82
character_refine_preprocesst::convert_get_type_int
static codet convert_get_type_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:293
character_refine_preprocesst::expr_of_to_chars
static exprt expr_of_to_chars(const exprt &chr, const typet &type)
character_refine_preprocesst::convert_is_ISO_control_int
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....
Definition: character_refine_preprocess.cpp:613
character_refine_preprocesst::convert_char_function
static codet convert_char_function(exprt(*expr_function)(const exprt &chr, const typet &type), conversion_inputt &target)
converts based on a function on expressions
Definition: character_refine_preprocess.cpp:24
character_refine_preprocesst::expr_of_is_whitespace
static exprt expr_of_is_whitespace(const exprt &chr, const typet &type)
Determines if the specified character is white space according to Java.
Definition: character_refine_preprocess.cpp:1087
character_refine_preprocesst::convert_is_java_letter
static codet convert_is_java_letter(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:667
character_refine_preprocesst::convert_is_identifier_ignorable_char
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....
Definition: character_refine_preprocess.cpp:563
character_refine_preprocesst::convert_is_java_identifier_start_int
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 isJavaIdent...
Definition: character_refine_preprocess.cpp:658
character_refine_preprocesst::convert_is_title_case_int
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....
Definition: character_refine_preprocess.cpp:937
character_refine_preprocesst::expr_of_is_ascii_upper_case
static exprt expr_of_is_ascii_upper_case(const exprt &chr, const typet &type)
Determines if the specified character is an ASCII uppercase character.
Definition: character_refine_preprocess.cpp:339
character_refine_preprocesst::convert_is_digit_char
static codet convert_is_digit_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:500
character_refine_preprocesst::conversion_inputt
const code_function_callt & conversion_inputt
Definition: character_refine_preprocess.h:35
character_refine_preprocesst::convert_is_java_identifier_part_int
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 isJavaIdent...
Definition: character_refine_preprocess.cpp:635
character_refine_preprocesst::conversion_functiont
codet(* conversion_functiont)(conversion_inputt &target)
Definition: character_refine_preprocess.h:36
character_refine_preprocesst::replace_character_call
codet replace_character_call(const code_function_callt &call) const
replace function calls to functions of the Character by an affectation if possible,...
Definition: character_refine_preprocess.cpp:1287
character_refine_preprocesst::expr_of_is_unicode_identifier_part
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.
Definition: character_refine_preprocess.cpp:976
character_refine_preprocesst::convert_to_title_case_int
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....
Definition: character_refine_preprocess.cpp:1239
character_refine_preprocesst::convert_is_unicode_identifier_part_char
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....
Definition: character_refine_preprocess.cpp:989
character_refine_preprocesst::convert_is_java_letter_or_digit
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 isJavaLette...
Definition: character_refine_preprocess.cpp:676
character_refine_preprocesst::expr_of_char_count
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)...
Definition: character_refine_preprocess.cpp:71
character_refine_preprocesst::convert_is_supplementary_code_point
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....
Definition: character_refine_preprocess.cpp:862
character_refine_preprocesst::initialize_conversion_table
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
Definition: character_refine_preprocess.cpp:1303
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
character_refine_preprocesst::convert_is_ideographic
static codet convert_is_ideographic(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:584
character_refine_preprocesst::convert_to_upper_case_char
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....
Definition: character_refine_preprocess.cpp:1265
character_refine_preprocesst::convert_is_identifier_ignorable_int
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....
Definition: character_refine_preprocess.cpp:575