Go to the documentation of this file.
26 conversion_inputt &target)
29 assert(function_call.
arguments().size()==1);
58 const exprt &chr,
const std::list<mp_integer> &list)
61 for(
const auto &i : list)
83 conversion_inputt &target)
101 conversion_inputt &target)
113 assert(function_call.
arguments().size()==2);
137 conversion_inputt &target)
140 const std::size_t nb_args=function_call.
arguments().size();
200 if_exprt fullwidth_cases(fullwidth_upper_case, case4, case5);
226 assert(function_call.
arguments().size()==2);
243 conversion_inputt &target)
254 conversion_inputt &target)
264 conversion_inputt &target)
275 conversion_inputt &target)
284 conversion_inputt &target)
295 conversion_inputt &target)
322 return std::move(high_surrogate);
328 conversion_inputt &target)
392 conversion_inputt &target)
417 conversion_inputt &target)
463 conversion_inputt &target)
473 conversion_inputt &target)
503 or_exprt(devanagari_digit, fullwidth_digit));
504 return std::move(digit);
511 conversion_inputt &target)
521 conversion_inputt &target)
542 conversion_inputt &target)
565 return std::move(ignorable);
574 conversion_inputt &target)
586 conversion_inputt &target)
595 conversion_inputt &target)
598 assert(function_call.
arguments().size()==1);
609 conversion_inputt &target)
612 assert(function_call.
arguments().size()==1);
624 conversion_inputt &target)
636 conversion_inputt &target)
646 conversion_inputt &target)
659 conversion_inputt &target)
669 conversion_inputt &target)
678 conversion_inputt &target)
687 conversion_inputt &target)
696 conversion_inputt &target)
706 conversion_inputt &target)
725 conversion_inputt &target)
735 conversion_inputt &target)
746 conversion_inputt &target)
758 conversion_inputt &target)
767 conversion_inputt &target)
770 assert(function_call.
arguments().size()==1);
788 return in_list_expr(chr, {0x28, 0x29, 0x3C, 0x3E, 0x5B, 0x5D, 0x7B, 0x7D});
797 conversion_inputt &target)
809 conversion_inputt &target)
831 std::list<mp_integer> space_characters=
832 {0x20, 0x00A0, 0x1680, 0x202F, 0x205F, 0x3000, 0x2028, 0x2029};
835 return or_exprt(condition0, condition1);
842 conversion_inputt &target)
852 conversion_inputt &target)
873 conversion_inputt &target)
894 conversion_inputt &target)
904 conversion_inputt &target)
907 assert(function_call.
arguments().size()==2);
924 std::list<mp_integer>title_case_chars=
925 {0x01C5, 0x01C8, 0x01CB, 0x01F2, 0x1FBC, 0x1FCC, 0x1FFC};
927 conditions.push_back(
in_list_expr(chr, title_case_chars));
938 conversion_inputt &target)
948 conversion_inputt &target)
1000 conversion_inputt &target)
1010 conversion_inputt &target)
1031 conversion_inputt &target)
1041 conversion_inputt &target)
1052 conversion_inputt &target)
1062 conversion_inputt &target)
1083 conversion_inputt &target)
1102 std::list<mp_integer> space_characters=
1103 {0x20, 0x1680, 0x205F, 0x3000, 0x2028, 0x2029};
1104 conditions.push_back(
in_list_expr(chr, space_characters));
1116 conversion_inputt &target)
1126 conversion_inputt &target)
1149 conversion_inputt &target)
1172 conversion_inputt &target)
1214 conversion_inputt &target)
1217 assert(function_call.
arguments().size()==2);
1253 return std::move(res);
1260 conversion_inputt &target)
1270 conversion_inputt &target)
1282 std::list<mp_integer> increment_list={0x01C4, 0x01C7, 0x01CA, 0x01F1};
1283 std::list<mp_integer> decrement_list={0x01C6, 0x01C9, 0x01CC, 0x01F3};
1287 std::list<mp_integer> plus_9_list={0x1FB3, 0x1FC3, 0x1FF3};
1293 plus_8_interval1,
or_exprt(plus_8_interval2, plus_8_interval3));
1309 return std::move(res);
1316 conversion_inputt &target)
1326 conversion_inputt &target)
1346 return std::move(res);
1353 conversion_inputt &target)
1363 conversion_inputt &target)
1383 return (it->second)(code);
1507 conversion_table[
"java::java.lang.Character.isSupplementaryCodePoint:(I)Z"]=
1517 conversion_table[
"java::java.lang.Character.isUnicodeIdentifierPart:(C)Z"]=
1519 conversion_table[
"java::java.lang.Character.isUnicodeIdentifierPart:(I)Z"]=
1521 conversion_table[
"java::java.lang.Character.isUnicodeIdentifierStart:(C)Z"]=
1523 conversion_table[
"java::java.lang.Character.isUnicodeIdentifierStart:(I)Z"]=
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....
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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....
#define PRECONDITION(CONDITION)
static exprt expr_of_char_value(const exprt &chr, const typet &type)
Casts the given expression to the given type.
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
static codet convert_is_digit_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_compare(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
const typet & subtype() const
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...
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....
static codet convert_char_value(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_low_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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....
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....
static codet convert_digit_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_reverse_bytes(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_is_surrogate_pair(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_is_whitespace_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
The type of an expression, extends irept.
static codet convert_is_alphabetic(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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...
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.
static codet convert_hash_code(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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....
The trinary if-then-else operator.
static exprt expr_of_is_mirrored(const exprt &chr, const typet &type)
Determines whether the character is mirrored according to the Unicode specification.
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....
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 ...
static codet convert_is_defined_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
The plus expression Associativity is not specified.
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.
static exprt is_low_surrogate(const exprt &chr)
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en....
Base class for all expressions.
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....
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....
static codet convert_is_whitespace_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static exprt expr_of_is_surrogate(const exprt &chr, const typet &type)
Determines if the given char value is a Unicode surrogate code unit.
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....
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....
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.
static codet convert_is_mirrored_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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...
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....
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....
static exprt expr_of_is_digit(const exprt &chr, const typet &type)
Determines if the specified character is a digit.
static codet convert_is_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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...
static codet convert_get_directionality_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
std::unordered_map< irep_idt, conversion_functiont > conversion_table
static codet convert_is_space(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static exprt expr_of_is_title_case(const exprt &chr, const typet &type)
Determines if the specified character is a titlecase character.
typet & type()
Return the type of the expression.
codet representation of a function call statement.
static codet convert_for_digit(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static exprt expr_of_is_letter_or_digit(const exprt &chr, const typet &type)
Determines if the specified character is a letter or digit.
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....
static exprt expr_of_to_lower_case(const exprt &chr, const typet &type)
Converts the character argument to lowercase.
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...
static codet convert_get_type_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
static exprt expr_of_is_alphabetic(const exprt &chr, const typet &type)
Determines if the specified character (Unicode code point) is alphabetic.
mstreamt & result() const
static exprt is_high_surrogate(const exprt &chr)
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en....
static codet convert_get_directionality_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static exprt expr_of_to_upper_case(const exprt &chr, const typet &type)
Converts the character argument to uppercase.
static codet convert_is_space_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static exprt expr_of_to_title_case(const exprt &chr, const typet &type)
Converts the character argument to titlecase.
static codet convert_high_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_is_defined_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_is_high_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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...
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....
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....
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....
static codet convert_is_letter_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_to_code_point(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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....
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.
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 a...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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....
const irep_idt & id() const
static codet convert_is_low_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
std::vector< exprt > operandst
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.
static exprt expr_of_is_defined(const exprt &chr, const typet &type)
Determines if a character is defined in Unicode.
static codet convert_digit_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_is_letter_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_is_mirrored_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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,...
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....
static exprt expr_of_is_ascii_lower_case(const exprt &chr, const typet &type)
Determines if the specified character is an ASCII lowercase character.
bitvector_typet char_type()
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....
static exprt expr_of_is_letter(const exprt &chr, const typet &type)
Determines if the specified character is a letter.
static codet convert_char_count(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_get_type_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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....
static codet convert_char_function(exprt(*expr_function)(const exprt &chr, const typet &type), conversion_inputt &target)
converts based on a function on expressions
static exprt expr_of_is_whitespace(const exprt &chr, const typet &type)
Determines if the specified character is white space according to Java.
A base class for relations, i.e., binary predicates.
static codet convert_to_chars(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
static codet convert_is_java_letter(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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....
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...
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
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....
static exprt expr_of_is_ascii_upper_case(const exprt &chr, const typet &type)
Determines if the specified character is an ASCII uppercase character.
static codet convert_is_digit_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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...
exprt pair_value(exprt char1, exprt char2, typet return_type)
the output corresponds to the unicode character given by the pair of characters of inputs assuming it...
Semantic type conversion.
A codet representing an assignment in the program.
codet replace_character_call(const code_function_callt &call) const
replace function calls to functions of the Character by an affectation if possible,...
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.
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....
Array constructor from list of elements.
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....
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...
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)...
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....
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
Data structure for representing an arbitrary statement in a program.
static codet convert_is_ideographic(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
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....
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....