CBMC
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/mp_arith.h>
24 #include <util/std_code_base.h>
25 
26 #include <list>
27 #include <unordered_map>
28 
29 class code_function_callt;
30 
31 class character_refine_preprocesst
32 {
33 public:
34  void initialize_conversion_table();
35  codet replace_character_call(const code_function_callt &call) const;
36 
37 private:
38  typedef const code_function_callt &conversion_inputt;
39  typedef codet (*conversion_functiont)(conversion_inputt &target);
40  // A table tells us what method to call for each java method signature
41  std::unordered_map<irep_idt, conversion_functiont> conversion_table;
42 
43  // Conversion functions
44  static exprt expr_of_char_count(const exprt &chr, const typet &type);
45  static codet convert_char_count(conversion_inputt &target);
46  static exprt expr_of_char_value(const exprt &chr, const typet &type);
47  static codet convert_char_value(conversion_inputt &target);
48  static codet convert_compare(conversion_inputt &target);
49  static codet convert_digit_char(conversion_inputt &target);
50  static codet convert_digit_int(conversion_inputt &target);
51  static codet convert_for_digit(conversion_inputt &target);
52  static codet convert_get_directionality_char(conversion_inputt &target);
53  static codet convert_get_directionality_int(conversion_inputt &target);
54  static codet convert_get_numeric_value_char(conversion_inputt &target);
55  static codet convert_get_numeric_value_int(conversion_inputt &target);
56  static codet convert_get_type_char(conversion_inputt &target);
57  static codet convert_get_type_int(conversion_inputt &target);
58  static codet convert_hash_code(conversion_inputt &target);
59  static exprt expr_of_high_surrogate(const exprt &chr, const typet &type);
60  static codet convert_high_surrogate(conversion_inputt &target);
61  static exprt expr_of_is_alphabetic(const exprt &chr, const typet &type);
62  static codet convert_is_alphabetic(conversion_inputt &target);
63  static exprt expr_of_is_bmp_code_point(const exprt &chr, const typet &type);
64  static codet convert_is_bmp_code_point(conversion_inputt &target);
65  static exprt expr_of_is_defined(const exprt &chr, const typet &type);
66  static codet convert_is_defined_char(conversion_inputt &target);
67  static codet convert_is_defined_int(conversion_inputt &target);
68  static exprt expr_of_is_digit(const exprt &chr, const typet &type);
69  static codet convert_is_digit_char(conversion_inputt &target);
70  static codet convert_is_digit_int(conversion_inputt &target);
71  static exprt expr_of_is_high_surrogate(const exprt &chr, const typet &type);
72  static codet convert_is_high_surrogate(conversion_inputt &target);
73  static exprt expr_of_is_identifier_ignorable(
74  const exprt &chr, const typet &type);
75  static codet convert_is_identifier_ignorable_char(conversion_inputt &target);
76  static codet convert_is_identifier_ignorable_int(conversion_inputt &target);
77  static codet convert_is_ideographic(conversion_inputt &target);
78  static codet convert_is_ISO_control_char(conversion_inputt &target);
79  static codet convert_is_ISO_control_int(conversion_inputt &target);
80  static codet convert_is_java_identifier_part_char(conversion_inputt &target);
81  static codet convert_is_java_identifier_part_int(conversion_inputt &target);
82  static codet convert_is_java_identifier_start_char(conversion_inputt &target);
83  static codet convert_is_java_identifier_start_int(conversion_inputt &target);
84  static codet convert_is_java_letter(conversion_inputt &target);
85  static codet convert_is_java_letter_or_digit(conversion_inputt &target);
86  static exprt expr_of_is_letter(const exprt &chr, const typet &type);
87  static codet convert_is_letter_char(conversion_inputt &target);
88  static codet convert_is_letter_int(conversion_inputt &target);
89  static exprt expr_of_is_letter_or_digit(const exprt &chr, const typet &type);
90  static codet convert_is_letter_or_digit_char(conversion_inputt &target);
91  static codet convert_is_letter_or_digit_int(conversion_inputt &target);
92  static exprt expr_of_is_ascii_lower_case(const exprt &chr, const typet &type);
93  static codet convert_is_lower_case_char(conversion_inputt &target);
94  static codet convert_is_lower_case_int(conversion_inputt &target);
95  static codet convert_is_low_surrogate(conversion_inputt &target);
96  static exprt expr_of_is_mirrored(const exprt &chr, const typet &type);
97  static codet convert_is_mirrored_char(conversion_inputt &target);
98  static codet convert_is_mirrored_int(conversion_inputt &target);
99  static codet convert_is_space(conversion_inputt &target);
100  static exprt expr_of_is_space_char(const exprt &chr, const typet &type);
101  static codet convert_is_space_char(conversion_inputt &target);
102  static codet convert_is_space_char_int(conversion_inputt &target);
103  static exprt expr_of_is_supplementary_code_point(
104  const exprt &chr, const typet &type);
105  static codet convert_is_supplementary_code_point(conversion_inputt &target);
106  static exprt expr_of_is_surrogate(const exprt &chr, const typet &type);
107  static codet convert_is_surrogate(conversion_inputt &target);
108  static codet convert_is_surrogate_pair(conversion_inputt &target);
109  static exprt expr_of_is_title_case(const exprt &chr, const typet &type);
110  static codet convert_is_title_case_char(conversion_inputt &target);
111  static codet convert_is_title_case_int(conversion_inputt &target);
112  static exprt expr_of_is_letter_number(const exprt &chr, const typet &type);
113  static exprt expr_of_is_unicode_identifier_part(
114  const exprt &chr, const typet &type);
115  static codet convert_is_unicode_identifier_part_char(
116  conversion_inputt &target);
117  static codet convert_is_unicode_identifier_part_int(
118  conversion_inputt &target);
119  static exprt expr_of_is_unicode_identifier_start(
120  const exprt &chr, const typet &type);
121  static codet convert_is_unicode_identifier_start_char(
122  conversion_inputt &target);
123  static codet convert_is_unicode_identifier_start_int(
124  conversion_inputt &target);
125  static exprt expr_of_is_ascii_upper_case(const exprt &chr, const typet &type);
126  static codet convert_is_upper_case_char(conversion_inputt &target);
127  static codet convert_is_upper_case_int(conversion_inputt &target);
128  static exprt expr_of_is_valid_code_point(const exprt &chr, const typet &type);
129  static codet convert_is_valid_code_point(conversion_inputt &target);
130  static exprt expr_of_is_whitespace(const exprt &chr, const typet &type);
131  static codet convert_is_whitespace_char(conversion_inputt &target);
132  static codet convert_is_whitespace_int(conversion_inputt &target);
133  static exprt expr_of_low_surrogate(const exprt &chr, const typet &type);
134  static codet convert_low_surrogate(conversion_inputt &target);
135  static exprt expr_of_reverse_bytes(const exprt &chr, const typet &type);
136  static codet convert_reverse_bytes(conversion_inputt &target);
137  static exprt expr_of_to_chars(const exprt &chr, const typet &type);
138  static codet convert_to_chars(conversion_inputt &target);
139  static exprt expr_of_to_lower_case(const exprt &chr, const typet &type);
140  static codet convert_to_lower_case_char(conversion_inputt &target);
141  static codet convert_to_lower_case_int(conversion_inputt &target);
142  static exprt expr_of_to_title_case(const exprt &chr, const typet &type);
143  static codet convert_to_title_case_char(conversion_inputt &target);
144  static codet convert_to_title_case_int(conversion_inputt &target);
145  static exprt expr_of_to_upper_case(const exprt &chr, const typet &type);
146  static codet convert_to_upper_case_char(conversion_inputt &target);
147  static codet convert_to_upper_case_int(conversion_inputt &target);
148 
149  // Helper functions
150  static codet convert_char_function(
151  exprt (*expr_function)(const exprt &chr, const typet &type),
152  conversion_inputt &target);
153  static exprt in_interval_expr(
154  const exprt &chr,
155  const mp_integer &lower_bound,
156  const mp_integer &upper_bound);
157  static exprt in_list_expr(
158  const exprt &chr, const std::list<mp_integer> &list);
159 };
160 
161 #endif // CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
character_refine_preprocesst
Definition: character_refine_preprocess.h:32
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:1044
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:215
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:750
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:534
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:27
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:1118
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:951
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:375
character_refine_preprocesst::conversion_inputt
const code_function_callt & conversion_inputt
Definition: character_refine_preprocess.h:38
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:616
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:738
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:265
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:549
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:930
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:1002
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:342
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:420
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:1013
character_refine_preprocesst::conversion_table
std::unordered_map< irep_idt, conversion_functiont > conversion_table
Definition: character_refine_preprocess.h:41
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:896
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:1242
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:113
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:844
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:85
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:94
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:524
character_refine_preprocesst::convert_high_surrogate
static codet convert_high_surrogate(conversion_inputt &target)
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:810
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:834
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:1065
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:45
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:1306
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:708
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:992
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:777
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:1278
character_refine_preprocesst::convert_low_surrogate
static codet convert_low_surrogate(conversion_inputt &target)
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:789
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:670
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:465
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:578
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:1090
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:1290
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:717
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:979
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:587
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:296
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:1169
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:409
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:855
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:1143
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:455
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:1201
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:865
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:886
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:103
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:1191
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:801
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:940
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:1232
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:759
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:255
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:331
character_refine_preprocesst::conversion_functiont
codet(* conversion_functiont)(conversion_inputt &target)
Definition: character_refine_preprocess.h:39
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:305
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:1033
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:60
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:651
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:225
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:285
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:316
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:1054
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:513
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:628
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:661
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:566
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:601
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:1023
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:74
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:679
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:820
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:485
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:397
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:1154
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:876
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:276
character_refine_preprocesst::convert_to_chars
static codet convert_to_chars(conversion_inputt &target)
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:1268
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:727
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:698
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:503
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:244
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:1181
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:688
character_refine_preprocesst::expr_of_to_chars
static exprt expr_of_to_chars(const exprt &chr, const typet &type)
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:1108
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:357
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:913
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:138
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:1256
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:1075
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:384
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:638
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:1130
code_function_callt
goto_instruction_codet representation of a function call statement.
Definition: goto_instruction_code.h:271
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt
Base class for all expressions.
Definition: expr.h:56
typet
The type of an expression, extends irept.
Definition: type.h:29
mp_arith.h
mp_integer
BigInt mp_integer
Definition: smt_terms.h:17
std_code_base.h