cprover
character_refine_preprocess.cpp
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 
6 Author: Romain Brenguier
7 
8 Date: March 2017
9 
10 \*******************************************************************/
11 
15 
17 
18 #include <util/arith_tools.h>
19 #include <util/std_expr.h>
20 
25  exprt (*expr_function)(const exprt &chr, const typet &type),
26  conversion_input &target)
27 {
28  const code_function_callt &function_call=target;
29  assert(function_call.arguments().size()==1);
30  const exprt &arg=function_call.arguments()[0];
31  const exprt &result=function_call.lhs();
32  const typet &type=result.type();
33  return code_assignt(result, expr_function(arg, type));
34 }
35 
43  const exprt &chr,
44  const mp_integer &lower_bound,
45  const mp_integer &upper_bound)
46 {
47  return and_exprt(
48  binary_relation_exprt(chr, ID_ge, from_integer(lower_bound, chr.type())),
49  binary_relation_exprt(chr, ID_le, from_integer(upper_bound, chr.type())));
50 }
51 
58  const exprt &chr, const std::list<mp_integer> &list)
59 {
60  exprt::operandst ops;
61  for(const auto &i : list)
62  ops.push_back(equal_exprt(chr, from_integer(i, chr.type())));
63  return disjunction(ops);
64 }
65 
72  const exprt &chr, const typet &type)
73 {
74  exprt u010000=from_integer(0x010000, type);
75  binary_relation_exprt small(chr, ID_lt, u010000);
76  return if_exprt(small, from_integer(1, type), from_integer(2, type));
77 }
78 
83 {
84  return convert_char_function(
86 }
87 
91  const exprt &chr, const typet &type)
92 {
93  return typecast_exprt(chr, type);
94 }
95 
100 {
101  return convert_char_function(
103 }
104 
109 {
110  const code_function_callt &function_call=target;
111  assert(function_call.arguments().size()==2);
112  const exprt &char1=function_call.arguments()[0];
113  const exprt &char2=function_call.arguments()[1];
114  const exprt &result=function_call.lhs();
115  const typet &type=result.type();
116  binary_relation_exprt smaller(char1, ID_lt, char2);
117  binary_relation_exprt greater(char1, ID_gt, char2);
118  if_exprt expr(
119  smaller,
120  from_integer(-1, type),
121  if_exprt(greater, from_integer(1, type), from_integer(0, type)));
122 
123  return code_assignt(result, expr);
124 }
125 
126 
131 {
132  const code_function_callt &function_call=target;
133  assert(function_call.arguments().size()==2);
134  const exprt &arg=function_call.arguments()[0];
135  const exprt &radix=function_call.arguments()[1];
136  const exprt &result=function_call.lhs();
137  const typet &type=result.type();
138 
139  // TODO: If the radix is not in the range MIN_RADIX <= radix <= MAX_RADIX or
140  // if the value of ch is not a valid digit in the specified radix,
141  // -1 is returned.
142 
143  // Case 1: The method isDigit is true of the character and the Unicode
144  // decimal digit value of the character (or its single-character
145  // decomposition) is less than the specified radix.
146  exprt invalid=from_integer(-1, arg.type());
147  exprt c0=from_integer('0', arg.type());
148  exprt latin_digit=in_interval_expr(arg, '0', '9');
149  minus_exprt value1(arg, c0);
150  // TODO: this is only valid for latin digits
151  if_exprt case1(
152  binary_relation_exprt(value1, ID_lt, radix), value1, invalid);
153 
154  // Case 2: The character is one of the uppercase Latin letters 'A'
155  // through 'Z' and its code is less than radix + 'A' - 10,
156  // then ch - 'A' + 10 is returned.
157  exprt cA=from_integer('A', arg.type());
158  exprt i10=from_integer(10, arg.type());
159  exprt upper_case=in_interval_expr(arg, 'A', 'Z');
160  plus_exprt value2(minus_exprt(arg, cA), i10);
161  if_exprt case2(
162  binary_relation_exprt(value2, ID_lt, radix), value2, invalid);
163 
164  // The character is one of the lowercase Latin letters 'a' through 'z' and
165  // its code is less than radix + 'a' - 10, then ch - 'a' + 10 is returned.
166  exprt ca=from_integer('a', arg.type());
167  exprt lower_case=in_interval_expr(arg, 'a', 'z');
168  plus_exprt value3(minus_exprt(arg, ca), i10);
169  if_exprt case3(
170  binary_relation_exprt(value3, ID_lt, radix), value3, invalid);
171 
172 
173  // The character is one of the fullwidth uppercase Latin letters A ('\uFF21')
174  // through Z ('\uFF3A') and its code is less than radix + '\uFF21' - 10.
175  // In this case, ch - '\uFF21' + 10 is returned.
176  exprt uFF21=from_integer(0xFF21, arg.type());
177  exprt fullwidth_upper_case=in_interval_expr(arg, 0xFF21, 0xFF3A);
178  plus_exprt value4(minus_exprt(arg, uFF21), i10);
179  if_exprt case4(
180  binary_relation_exprt(value4, ID_lt, radix), value4, invalid);
181 
182  // The character is one of the fullwidth lowercase Latin letters a ('\uFF41')
183  // through z ('\uFF5A') and its code is less than radix + '\uFF41' - 10.
184  // In this case, ch - '\uFF41' + 10 is returned.
185  exprt uFF41=from_integer(0xFF41, arg.type());
186  plus_exprt value5(minus_exprt(arg, uFF41), i10);
187  if_exprt case5(
188  binary_relation_exprt(value5, ID_lt, radix), value5, invalid);
189 
190  if_exprt fullwidth_cases(fullwidth_upper_case, case4, case5);
191  if_exprt expr(
192  latin_digit,
193  case1,
194  if_exprt(upper_case, case2, if_exprt(lower_case, case3, fullwidth_cases)));
195  typecast_exprt tc_expr(expr, type);
196 
197  return code_assignt(result, tc_expr);
198 }
199 
204 {
205  return convert_digit_char(target);
206 }
207 
214 {
215  const code_function_callt &function_call=target;
216  assert(function_call.arguments().size()==2);
217  const exprt &digit=function_call.arguments()[0];
218  const exprt &result=function_call.lhs();
219  const typet &type=result.type();
220 
221  exprt d10=from_integer(10, type);
222  binary_relation_exprt small(digit, ID_le, d10);
223  plus_exprt value1(digit, from_integer('0', type));
224  minus_exprt value2(plus_exprt(digit, from_integer('a', digit.type())), d10);
225  return code_assignt(result, if_exprt(small, value1, value2));
226 }
227 
232  conversion_input &target)
233 {
234  // TODO: This is unimplemented for now as it requires analyzing
235  // the UnicodeData file to find characters directionality.
236  return target;
237 }
238 
243  conversion_input &target)
244 {
245  return convert_get_directionality_char(target);
246 }
247 
253  conversion_input &target)
254 {
255  return convert_digit_char(target);
256 }
257 
264  conversion_input &target)
265 {
266  return convert_digit_int(target);
267 }
268 
273  conversion_input &target)
274 {
275  // TODO: This is unimplemented for now as it requires analyzing
276  // the UnicodeData file to categorize characters.
277  return target;
278 }
279 
284  conversion_input &target)
285 {
286  return convert_get_type_char(target);
287 }
288 
293 {
294  return convert_char_value(target);
295 }
296 
304  const exprt &chr, const typet &type)
305 {
306  exprt u10000=from_integer(0x010000, type);
307  exprt uD800=from_integer(0xD800, type);
308  exprt u400=from_integer(0x0400, type);
309 
310  plus_exprt high_surrogate(uD800, div_exprt(minus_exprt(chr, u10000), u400));
311  return high_surrogate;
312 }
313 
317  conversion_input &target)
318 {
319  return convert_char_function(
321 }
322 
328  const exprt &chr, const typet &type)
329 {
330  return in_interval_expr(chr, 'a', 'z');
331 }
332 
338  const exprt &chr, const typet &type)
339 {
340  return in_interval_expr(chr, 'A', 'Z');
341 }
342 
352  const exprt &chr, const typet &type)
353 {
354  return or_exprt(
355  expr_of_is_ascii_upper_case(chr, type),
356  expr_of_is_ascii_lower_case(chr, type));
357 }
358 
370  const exprt &chr, const typet &type)
371 {
372  return expr_of_is_letter(chr, type);
373 }
374 
379  conversion_input &target)
380 {
381  return convert_char_function(
383 }
384 
392  const exprt &chr, const typet &type)
393 {
394  binary_relation_exprt is_bmp(chr, ID_le, from_integer(0xFFFF, chr.type()));
395  return is_bmp;
396 }
397 
402  conversion_input &target)
403 {
404  return convert_char_function(
406 }
407 
413  const exprt &chr, const typet &type)
414 {
415  // The following intervals are undefined in unicode, according to
416  // the Unicode Character Database: http://www.unicode.org/Public/UCD/latest/
417  exprt::operandst intervals;
418  intervals.push_back(in_interval_expr(chr, 0x0750, 0x077F));
419  intervals.push_back(in_interval_expr(chr, 0x07C0, 0x08FF));
420  intervals.push_back(in_interval_expr(chr, 0x1380, 0x139F));
421  intervals.push_back(in_interval_expr(chr, 0x18B0, 0x18FF));
422  intervals.push_back(in_interval_expr(chr, 0x1980, 0x19DF));
423  intervals.push_back(in_interval_expr(chr, 0x1A00, 0x1CFF));
424  intervals.push_back(in_interval_expr(chr, 0x1D80, 0x1DFF));
425  intervals.push_back(in_interval_expr(chr, 0x2C00, 0x2E7F));
426  intervals.push_back(in_interval_expr(chr, 0x2FE0, 0x2FEF));
427  intervals.push_back(in_interval_expr(chr, 0x31C0, 0x31EF));
428  intervals.push_back(in_interval_expr(chr, 0x9FB0, 0x9FFF));
429  intervals.push_back(in_interval_expr(chr, 0xA4D0, 0xABFF));
430  intervals.push_back(in_interval_expr(chr, 0xD7B0, 0xD7FF));
431  intervals.push_back(in_interval_expr(chr, 0xFE10, 0xFE1F));
432  intervals.push_back(in_interval_expr(chr, 0x10140, 0x102FF));
433  intervals.push_back(in_interval_expr(chr, 0x104B0, 0x107FF));
434  intervals.push_back(in_interval_expr(chr, 0x10840, 0x1CFFF));
435  intervals.push_back(in_interval_expr(chr, 0x1D200, 0x1D2FF));
436  intervals.push_back(in_interval_expr(chr, 0x1D360, 0x1D3FF));
437  intervals.push_back(
438  binary_relation_exprt(chr, ID_ge, from_integer(0x1D800, chr.type())));
439 
440  return not_exprt(disjunction(intervals));
441 }
442 
447  conversion_input &target)
448 {
449  return convert_char_function(
451 }
452 
457  conversion_input &target)
458 {
459  return convert_is_defined_char(target);
460 }
461 
477  const exprt &chr, const typet &type)
478 {
479  exprt latin_digit=in_interval_expr(chr, '0', '9');
480  exprt arabic_indic_digit=in_interval_expr(chr, 0x660, 0x669);
481  exprt extended_digit=in_interval_expr(chr, 0x6F0, 0x6F9);
482  exprt devanagari_digit=in_interval_expr(chr, 0x966, 0x96F);
483  exprt fullwidth_digit=in_interval_expr(chr, 0xFF10, 0xFF19);
484  or_exprt digit(
485  or_exprt(latin_digit, or_exprt(arabic_indic_digit, extended_digit)),
486  or_exprt(devanagari_digit, fullwidth_digit));
487  return digit;
488 }
489 
494  conversion_input &target)
495 {
496  return convert_char_function(
498 }
499 
504  conversion_input &target)
505 {
506  return convert_is_digit_char(target);
507 }
508 
515  const exprt &chr, const typet &type)
516 {
517  return in_interval_expr(chr, 0xD800, 0xDBFF);
518 }
519 
524  conversion_input &target)
525 {
526  return convert_char_function(
528 }
529 
539  const exprt &chr, const typet &type)
540 {
541  or_exprt ignorable(
542  in_interval_expr(chr, 0x0000, 0x0008),
543  or_exprt(
544  in_interval_expr(chr, 0x000E, 0x001B),
545  in_interval_expr(chr, 0x007F, 0x009F)));
546  return ignorable;
547 }
548 
555  conversion_input &target)
556 {
557  return convert_char_function(
559 }
560 
567  conversion_input &target)
568 {
570 }
571 
576  conversion_input &target)
577 {
578  const code_function_callt &function_call=target;
579  assert(function_call.arguments().size()==1);
580  const exprt &arg=function_call.arguments()[0];
581  const exprt &result=function_call.lhs();
582  exprt is_ideograph=in_interval_expr(arg, 0x4E00, 0x9FFF);
583  return code_assignt(result, is_ideograph);
584 }
585 
590  conversion_input &target)
591 {
592  const code_function_callt &function_call=target;
593  assert(function_call.arguments().size()==1);
594  const exprt &arg=function_call.arguments()[0];
595  const exprt &result=function_call.lhs();
596  or_exprt iso(
597  in_interval_expr(arg, 0x00, 0x1F), in_interval_expr(arg, 0x7F, 0x9F));
598  return code_assignt(result, iso);
599 }
600 
605  conversion_input &target)
606 {
607  return convert_is_ISO_control_char(target);
608 }
609 
617  conversion_input &target)
618 {
619  return convert_char_function(
621 }
622 
627  conversion_input &target)
628 {
630 }
631 
640  conversion_input &target)
641 {
642  return convert_char_function(
644 }
645 
650  conversion_input &target)
651 {
653 }
654 
659  conversion_input &target)
660 {
662 }
663 
668  conversion_input &target)
669 {
671 }
672 
677  conversion_input &target)
678 {
679  return convert_char_function(
681 }
682 
687  conversion_input &target)
688 {
689  return convert_is_letter_char(target);
690 }
691 
697  const exprt &chr, const typet &type)
698 {
699  return or_exprt(expr_of_is_letter(chr, type), expr_of_is_digit(chr, type));
700 }
701 
706  conversion_input &target)
707 {
708  return convert_char_function(
710 }
711 
716  conversion_input &target)
717 {
718  return convert_is_letter_or_digit_char(target);
719 }
720 
727  conversion_input &target)
728 {
729  return convert_char_function(
731 }
732 
739  conversion_input &target)
740 {
741  return convert_is_lower_case_char(target);
742 }
743 
748  conversion_input &target)
749 {
750  const code_function_callt &function_call=target;
751  assert(function_call.arguments().size()==1);
752  const exprt &arg=function_call.arguments()[0];
753  const exprt &result=function_call.lhs();
754  exprt is_low_surrogate=in_interval_expr(arg, 0xDC00, 0xDFFF);
755  return code_assignt(result, is_low_surrogate);
756 }
757 
766  const exprt &chr, const typet &type)
767 {
768  return in_list_expr(chr, {0x28, 0x29, 0x3C, 0x3E, 0x5B, 0x5D, 0x7B, 0x7D});
769 }
770 
777  conversion_input &target)
778 {
779  return convert_char_function(
781 }
782 
789  conversion_input &target)
790 {
791  return convert_is_mirrored_char(target);
792 }
793 
798 {
799  return convert_is_whitespace_char(target);
800 }
801 
808  const exprt &chr, const typet &type)
809 {
810  std::list<mp_integer> space_characters=
811  {0x20, 0x00A0, 0x1680, 0x202F, 0x205F, 0x3000, 0x2028, 0x2029};
812  exprt condition0=in_list_expr(chr, space_characters);
813  exprt condition1=in_interval_expr(chr, 0x2000, 0x200A);
814  return or_exprt(condition0, condition1);
815 }
816 
821  conversion_input &target)
822 {
823  return convert_char_function(
825 }
826 
831  conversion_input &target)
832 {
833  return convert_is_space_char(target);
834 }
835 
842  const exprt &chr, const typet &type)
843 {
844  return binary_relation_exprt(chr, ID_gt, from_integer(0xFFFF, chr.type()));
845 }
846 
851  conversion_input &target)
852 {
853  return convert_char_function(
855 }
856 
862  const exprt &chr, const typet &type)
863 {
864  return in_interval_expr(chr, 0xD800, 0xDFFF);
865 }
866 
871  conversion_input &target)
872 {
873  return convert_char_function(
875 }
876 
881  conversion_input &target)
882 {
883  const code_function_callt &function_call=target;
884  assert(function_call.arguments().size()==2);
885  const exprt &arg0=function_call.arguments()[0];
886  const exprt &arg1=function_call.arguments()[1];
887  const exprt &result=function_call.lhs();
888  exprt is_low_surrogate=in_interval_expr(arg1, 0xDC00, 0xDFFF);
889  exprt is_high_surrogate=in_interval_expr(arg0, 0xD800, 0xDBFF);
890  return code_assignt(result, and_exprt(is_high_surrogate, is_low_surrogate));
891 }
892 
898  const exprt &chr, const typet &type)
899 {
900  std::list<mp_integer>title_case_chars=
901  {0x01C5, 0x01C8, 0x01CB, 0x01F2, 0x1FBC, 0x1FCC, 0x1FFC};
902  exprt::operandst conditions;
903  conditions.push_back(in_list_expr(chr, title_case_chars));
904  conditions.push_back(in_interval_expr(chr, 0x1F88, 0x1F8F));
905  conditions.push_back(in_interval_expr(chr, 0x1F98, 0x1F9F));
906  conditions.push_back(in_interval_expr(chr, 0x1FA8, 0x1FAF));
907  return disjunction(conditions);
908 }
909 
914  conversion_input &target)
915 {
916  return convert_char_function(
918 }
919 
924  conversion_input &target)
925 {
926  return convert_is_title_case_char(target);
927 }
928 
935  const exprt &chr, const typet &type)
936 {
937  // The following set of characters is the general category "Nl" in the
938  // Unicode specification.
939  exprt cond0=in_interval_expr(chr, 0x16EE, 0x16F0);
940  exprt cond1=in_interval_expr(chr, 0x2160, 0x2188);
941  exprt cond2=in_interval_expr(chr, 0x3021, 0x3029);
942  exprt cond3=in_interval_expr(chr, 0x3038, 0x303A);
943  exprt cond4=in_interval_expr(chr, 0xA6E6, 0xA6EF);
944  exprt cond5=in_interval_expr(chr, 0x10140, 0x10174);
945  exprt cond6=in_interval_expr(chr, 0x103D1, 0x103D5);
946  exprt cond7=in_interval_expr(chr, 0x12400, 0x1246E);
947  exprt cond8=in_list_expr(chr, {0x3007, 0x10341, 0x1034A});
948  return or_exprt(
949  or_exprt(or_exprt(cond0, cond1), or_exprt(cond2, cond3)),
950  or_exprt(or_exprt(cond4, cond5), or_exprt(cond6, or_exprt(cond7, cond8))));
951 }
952 
953 
962  const exprt &chr, const typet &type)
963 {
964  exprt::operandst conditions;
965  conditions.push_back(expr_of_is_unicode_identifier_start(chr, type));
966  conditions.push_back(expr_of_is_digit(chr, type));
967  conditions.push_back(expr_of_is_identifier_ignorable(chr, type));
968  return disjunction(conditions);
969 }
970 
975  conversion_input &target)
976 {
977  return convert_char_function(
979 }
980 
985  conversion_input &target)
986 {
988 }
989 
996  const exprt &chr, const typet &type)
997 {
998  return or_exprt(
999  expr_of_is_letter(chr, type), expr_of_is_letter_number(chr, type));
1000 }
1001 
1006  conversion_input &target)
1007 {
1008  return convert_char_function(
1010 }
1011 
1016  conversion_input &target)
1017 {
1019 }
1020 
1027  conversion_input &target)
1028 {
1029  return convert_char_function(
1031 }
1032 
1037  conversion_input &target)
1038 {
1039  return convert_is_upper_case_char(target);
1040 }
1041 
1048  const exprt &chr, const typet &type)
1049 {
1050  return binary_relation_exprt(chr, ID_le, from_integer(0x10FFFF, chr.type()));
1051 }
1052 
1057  conversion_input &target)
1058 {
1059  return convert_char_function(
1061 }
1062 
1072  const exprt &chr, const typet &type)
1073 {
1074  exprt::operandst conditions;
1075  std::list<mp_integer> space_characters=
1076  {0x20, 0x1680, 0x205F, 0x3000, 0x2028, 0x2029};
1077  conditions.push_back(in_list_expr(chr, space_characters));
1078  conditions.push_back(in_interval_expr(chr, 0x2000, 0x2006));
1079  conditions.push_back(in_interval_expr(chr, 0x2008, 0x200A));
1080  conditions.push_back(in_interval_expr(chr, 0x09, 0x0D));
1081  conditions.push_back(in_interval_expr(chr, 0x1C, 0x1F));
1082  return disjunction(conditions);
1083 }
1084 
1089  conversion_input &target)
1090 {
1091  return convert_char_function(
1093 }
1094 
1099  conversion_input &target)
1100 {
1101  return convert_is_whitespace_char(target);
1102 }
1103 
1111  const exprt &chr, const typet &type)
1112 {
1113  exprt uDC00=from_integer(0xDC00, type);
1114  exprt u0400=from_integer(0x0400, type);
1115  return plus_exprt(uDC00, mod_exprt(chr, u0400));
1116 }
1117 
1122  conversion_input &target)
1123 {
1124  return convert_char_function(
1126 }
1127 
1134  const exprt &chr, const typet &type)
1135 {
1136  shl_exprt first_byte(chr, from_integer(8, type));
1137  lshr_exprt second_byte(chr, from_integer(8, type));
1138  return plus_exprt(first_byte, second_byte);
1139 }
1140 
1145  conversion_input &target)
1146 {
1147  return convert_char_function(
1149 }
1150 
1160  const exprt &chr, const typet &type)
1161 {
1162  array_typet array_type=to_array_type(type);
1163  const typet &char_type=array_type.subtype();
1164  array_exprt case1(array_type);
1165  array_exprt case2(array_type);
1166  exprt low_surrogate=expr_of_low_surrogate(chr, char_type);
1167  case1.copy_to_operands(low_surrogate);
1168  case2.move_to_operands(low_surrogate);
1169  exprt high_surrogate=expr_of_high_surrogate(chr, char_type);
1170  case2.move_to_operands(high_surrogate);
1171  return if_exprt(expr_of_is_bmp_code_point(chr, type), case1, case2);
1172 }
1173 
1178 {
1179  return convert_char_function(
1181 }
1182 
1187  conversion_input &target)
1188 {
1189  const code_function_callt &function_call=target;
1190  assert(function_call.arguments().size()==2);
1191  const exprt &arg0=function_call.arguments()[0];
1192  const exprt &arg1=function_call.arguments()[1];
1193  const exprt &result=function_call.lhs();
1194  const typet &type=result.type();
1195 
1196  // These operations implement the decoding of a unicode symbol encoded
1197  // in UTF16 for the supplementary planes (above U+10000).
1198  // The low ten bits of the first character give the bits 10 to 19 of
1199  // code point and the low ten bits of the second give the bits 0 to 9,
1200  // then 0x10000 is added to the result. For more explenations see:
1201  // https://en.wikipedia.org/wiki/UTF-16
1202 
1203  exprt u010000=from_integer(0x010000, type);
1204  exprt mask10bit=from_integer(0x03FF, type);
1205  shl_exprt m1(bitand_exprt(arg0, mask10bit), from_integer(10, type));
1206  bitand_exprt m2(arg1, mask10bit);
1207  bitor_exprt pair_value(u010000, bitor_exprt(m1, m2));
1208  return code_assignt(result, pair_value);
1209 }
1210 
1220  const exprt &chr, const typet &type)
1221 {
1222  minus_exprt transformed(
1223  plus_exprt(chr, from_integer('a', type)), from_integer('A', type));
1224 
1225  if_exprt res(expr_of_is_ascii_upper_case(chr, type), transformed, chr);
1226  return res;
1227 }
1228 
1233  conversion_input &target)
1234 {
1235  return convert_char_function(
1237 }
1238 
1243  conversion_input &target)
1244 {
1245  return convert_to_lower_case_char(target);
1246 }
1247 
1253  const exprt &chr, const typet &type)
1254 {
1255  std::list<mp_integer> increment_list={0x01C4, 0x01C7, 0x01CA, 0x01F1};
1256  std::list<mp_integer> decrement_list={0x01C6, 0x01C9, 0x01CC, 0x01F3};
1257  exprt plus_8_interval1=in_interval_expr(chr, 0x1F80, 0x1F87);
1258  exprt plus_8_interval2=in_interval_expr(chr, 0x1F90, 0x1F97);
1259  exprt plus_8_interval3=in_interval_expr(chr, 0x1FA0, 0x1FA7);
1260  std::list<mp_integer> plus_9_list={0x1FB3, 0x1FC3, 0x1FF3};
1261  minus_exprt minus_1(chr, from_integer(1, type));
1262  plus_exprt plus_1(chr, from_integer(1, type));
1263  plus_exprt plus_8(chr, from_integer(8, type));
1264  plus_exprt plus_9(chr, from_integer(9, type));
1265  or_exprt plus_8_set(
1266  plus_8_interval1, or_exprt(plus_8_interval2, plus_8_interval3));
1267 
1268  if_exprt res(
1269  in_list_expr(chr, increment_list),
1270  plus_1,
1271  if_exprt(
1272  in_list_expr(chr, decrement_list),
1273  minus_1,
1274  if_exprt(
1275  plus_8_set,
1276  plus_8,
1277  if_exprt(
1278  in_list_expr(chr, plus_9_list),
1279  plus_9,
1280  chr))));
1281 
1282  return res;
1283 }
1284 
1289  conversion_input &target)
1290 {
1291  return convert_char_function(
1293 }
1294 
1299  conversion_input &target)
1300 {
1301  return convert_to_title_case_char(target);
1302 }
1303 
1313  const exprt &chr, const typet &type)
1314 {
1315  minus_exprt transformed(
1316  plus_exprt(chr, from_integer('A', type)), from_integer('a', type));
1317 
1318  if_exprt res(expr_of_is_ascii_lower_case(chr, type), transformed, chr);
1319  return res;
1320 }
1321 
1326  conversion_input &target)
1327 {
1328  return convert_char_function(
1330 }
1331 
1336  conversion_input &target)
1337 {
1338  return convert_to_upper_case_char(target);
1339 }
1340 
1348  const code_function_callt &code) const
1349 {
1350  if(code.function().id()==ID_symbol)
1351  {
1352  const irep_idt &function_id=
1353  to_symbol_expr(code.function()).get_identifier();
1354  auto it=conversion_table.find(function_id);
1355  if(it!=conversion_table.end())
1356  return (it->second)(code);
1357  }
1358 
1359  return code;
1360 }
1361 
1364 {
1365  // All methods are listed here in alphabetic order
1366  // The ones that are not supported by this module (though they may be
1367  // supported by the string solver) have no entry in the conversion
1368  // table and are marked in this way:
1369  // Not supported "java::java.lang.Character.<init>()"
1370 
1371  conversion_table["java::java.lang.Character.charCount:(I)I"]=
1373  conversion_table["java::java.lang.Character.charValue:()C"]=
1375 
1376  // Not supported "java::java.lang.Character.codePointAt:([CI)I
1377  // Not supported "java::java.lang.Character.codePointAt:([CII)I"
1378  // Not supported "java::java.lang.Character.codePointAt:"
1379  // "(Ljava.lang.CharSequence;I)I"
1380  // Not supported "java::java.lang.Character.codePointBefore:([CI)I"
1381  // Not supported "java::java.lang.Character.codePointBefore:([CII)I"
1382  // Not supported "java::java.lang.Character.codePointBefore:"
1383  // "(Ljava.lang.CharSequence;I)I"
1384  // Not supported "java::java.lang.Character.codePointCount:([CII)I"
1385  // Not supported "java::java.lang.Character.codePointCount:"
1386  // "(Ljava.lang.CharSequence;I)I"
1387  // Not supported "java::java.lang.Character.compareTo:"
1388  // "(Ljava.lang.Character;)I"
1389 
1390  conversion_table["java::java.lang.Character.compare:(CC)I"]=
1392  conversion_table["java::java.lang.Character.digit:(CI)I"]=
1394  conversion_table["java::java.lang.Character.digit:(II)I"]=
1396 
1397  // Not supported "java::java.lang.Character.equals:(Ljava.lang.Object;)Z"
1398 
1399  conversion_table["java::java.lang.Character.forDigit:(II)C"]=
1401  conversion_table["java::java.lang.Character.getDirectionality:(C)B"]=
1403  conversion_table["java::java.lang.Character.getDirectionality:(I)B"]=
1405 
1406  // Not supported "java::java.lang.Character.getName:(I)Ljava.lang.String;"
1407 
1408  conversion_table["java::java.lang.Character.getNumericValue:(C)I"]=
1410  conversion_table["java::java.lang.Character.getNumericValue:(I)I"]=
1412  conversion_table["java::java.lang.Character.getType:(C)I"]=
1414  conversion_table["java::java.lang.Character.getType:(I)Z"]=
1416  conversion_table["java::java.lang.Character.hashCode:()I"]=
1418  conversion_table["java::java.lang.Character.highSurrogate:(C)Z"]=
1420  conversion_table["java::java.lang.Character.isAlphabetic:(I)Z"]=
1422  conversion_table["java::java.lang.Character.isBmpCodePoint:(I)Z"]=
1424  conversion_table["java::java.lang.Character.isDefined:(C)Z"]=
1426  conversion_table["java::java.lang.Character.isDefined:(I)Z"]=
1428  conversion_table["java::java.lang.Character.isDigit:(C)Z"]=
1430  conversion_table["java::java.lang.Character.isDigit:(I)Z"]=
1432  conversion_table["java::java.lang.Character.isHighSurrogate:(C)Z"]=
1434  conversion_table["java::java.lang.Character.isIdentifierIgnorable:(C)Z"]=
1436  conversion_table["java::java.lang.Character.isIdentifierIgnorable:(I)Z"]=
1438  conversion_table["java::java.lang.Character.isIdeographic:(C)Z"]=
1440  conversion_table["java::java.lang.Character.isISOControl:(C)Z"]=
1442  conversion_table["java::java.lang.Character.isISOControl:(I)Z"]=
1444  conversion_table["java::java.lang.Character.isJavaIdentifierPart:(C)Z"]=
1446  conversion_table["java::java.lang.Character.isJavaIdentifierPart:(I)Z"]=
1448  conversion_table["java::java.lang.Character.isJavaIdentifierStart:(C)Z"]=
1450  conversion_table["java::java.lang.Character.isJavaIdentifierStart:(I)Z"]=
1452  conversion_table["java::java.lang.Character.isJavaLetter:(C)Z"]=
1454  conversion_table["java::java.lang.Character.isJavaLetterOrDigit:(C)Z"]=
1456  conversion_table["java::java.lang.Character.isLetter:(C)Z"]=
1458  conversion_table["java::java.lang.Character.isLetter:(I)Z"]=
1460  conversion_table["java::java.lang.Character.isLetterOrDigit:(C)Z"]=
1462  conversion_table["java::java.lang.Character.isLetterOrDigit:(I)Z"]=
1464  conversion_table["java::java.lang.Character.isLowerCase:(C)Z"]=
1466  conversion_table["java::java.lang.Character.isLowerCase:(I)Z"]=
1468  conversion_table["java::java.lang.Character.isLowSurrogate:(I)Z"]=
1470  conversion_table["java::java.lang.Character.isMirrored:(C)Z"]=
1472  conversion_table["java::java.lang.Character.isMirrored:(I)Z"]=
1474  conversion_table["java::java.lang.Character.isSpace:(C)Z"]=
1476  conversion_table["java::java.lang.Character.isSpaceChar:(C)Z"]=
1478  conversion_table["java::java.lang.Character.isSpaceChar:(I)Z"]=
1480  conversion_table["java::java.lang.Character.isSupplementaryCodePoint:(I)Z"]=
1482  conversion_table["java::java.lang.Character.isSurrogate:(C)Z"]=
1484  conversion_table["java::java.lang.Character.isSurrogatePair:(CC)Z"]=
1486  conversion_table["java::java.lang.Character.isTitleCase:(C)Z"]=
1488  conversion_table["java::java.lang.Character.isTitleCase:(I)Z"]=
1490  conversion_table["java::java.lang.Character.isUnicodeIdentifierPart:(C)Z"]=
1492  conversion_table["java::java.lang.Character.isUnicodeIdentifierPart:(I)Z"]=
1494  conversion_table["java::java.lang.Character.isUnicodeIdentifierStart:(C)Z"]=
1496  conversion_table["java::java.lang.Character.isUnicodeIdentifierStart:(I)Z"]=
1498  conversion_table["java::java.lang.Character.isUpperCase:(C)Z"]=
1500  conversion_table["java::java.lang.Character.isUpperCase:(I)Z"]=
1502  conversion_table["java::java.lang.Character.isValidCodePoint:(I)Z"]=
1504  conversion_table["java::java.lang.Character.isWhitespace:(C)Z"]=
1506  conversion_table["java::java.lang.Character.isWhitespace:(I)Z"]=
1508  conversion_table["java::java.lang.Character.lowSurrogate:(I)Z"]=
1510 
1511  // Not supported "java::java.lang.Character.offsetByCodePoints:([CIIII)I"
1512  // Not supported "java::java.lang.Character.offsetByCodePoints:"
1513  // "(Ljava.lang.CharacterSequence;II)I"
1514 
1515  conversion_table["java::java.lang.Character.reverseBytes:(C)C"]=
1517  conversion_table["java::java.lang.Character.toChars:(I)[C"]=
1519 
1520  // Not supported "java::java.lang.Character.toChars:(I[CI])I"
1521 
1522  conversion_table["java::java.lang.Character.toCodePoint:(CC)I"]=
1524  conversion_table["java::java.lang.Character.toLowerCase:(C)C"]=
1526  conversion_table["java::java.lang.Character.toLowerCase:(I)I"]=
1528 
1529  // Not supported "java::java.lang.Character.toString:()Ljava.lang.String;"
1530  // Not supported "java::java.lang.Character.toString:(C)Ljava.lang.String;"
1531 
1532  conversion_table["java::java.lang.Character.toTitleCase:(C)C"]=
1534  conversion_table["java::java.lang.Character.toTitleCase:(I)I"]=
1536  conversion_table["java::java.lang.Character.toUpperCase:(C)C"]=
1538  conversion_table["java::java.lang.Character.toUpperCase:(I)I"]=
1540 
1541  // Not supported "java::java.lang.Character.valueOf:(C)Ljava.lang.Character;"
1542 }
static codet convert_is_lower_case_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
The type of an expression.
Definition: type.h:20
mstreamt & result()
Definition: message.h:233
Boolean negation.
Definition: std_expr.h:2648
semantic type conversion
Definition: std_expr.h:1725
static codet convert_is_unicode_identifier_part_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
BigInt mp_integer
Definition: mp_arith.h:19
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
static codet convert_is_unicode_identifier_part_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_get_directionality_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
boolean OR
Definition: std_expr.h:1968
static exprt expr_of_is_title_case(const exprt &chr, const typet &type)
Determines if the specified character is a titlecase character.
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_high_surrogate(conversion_input &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 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_bmp_code_point(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_defined_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static exprt expr_of_char_value(const exprt &chr, const typet &type)
Casts the given expression to the given type.
static codet convert_is_digit_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_whitespace_char(conversion_input &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.
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
static codet convert_for_digit(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_digit_char(conversion_input &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.
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
static exprt expr_of_is_ascii_lower_case(const exprt &chr, const typet &type)
Determines if the specified character is an ASCII lowercase character.
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...
static codet convert_compare(conversion_input &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...
The trinary if-then-else operator.
Definition: std_expr.h:2771
static codet convert_is_java_letter(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
typet & type()
Definition: expr.h:60
static codet convert_is_alphabetic(conversion_input &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 exprt expr_of_is_alphabetic(const exprt &chr, const typet &type)
Determines if the specified character (Unicode code point) is alphabetic.
static exprt expr_of_is_surrogate(const exprt &chr, const typet &type)
Determines if the given char value is a Unicode surrogate code unit.
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
static codet convert_hash_code(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_high_surrogate(conversion_input &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_is_java_letter_or_digit(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaLette...
static exprt expr_of_to_upper_case(const exprt &chr, const typet &type)
Converts the character argument to uppercase.
equality
Definition: std_expr.h:1082
static codet convert_is_letter_or_digit_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
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 expr_of_is_defined(const exprt &chr, const typet &type)
Determines if a character is defined in Unicode.
const irep_idt & id() const
Definition: irep.h:189
static codet convert_is_letter_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
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...
static codet convert_is_defined_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
Bit-wise OR.
Definition: std_expr.h:2087
static codet convert_is_low_surrogate(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
argumentst & arguments()
Definition: std_code.h:689
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...
division (integer and real)
Definition: std_expr.h:854
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_high_surrogate(const exprt &chr, const typet &type)
Returns the leading surrogate (a high surrogate code unit) of the surrogate pair representing the spe...
static codet convert_to_upper_case_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_unicode_identifier_start_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_surrogate(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_to_code_point(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_to_lower_case_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_title_case_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_to_title_case_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
boolean AND
Definition: std_expr.h:1852
static codet convert_get_directionality_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
API to expression classes.
static codet convert_is_lower_case_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
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_chars(conversion_input &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...
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.
static codet convert_is_supplementary_code_point(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
Left shift.
Definition: std_expr.h:2301
static codet convert_low_surrogate(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
std::unordered_map< irep_idt, conversion_functiont, irep_id_hash > conversion_table
static codet convert_is_identifier_ignorable_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
A function call.
Definition: std_code.h:657
The plus expression.
Definition: std_expr.h:702
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 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_is_whitespace_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_to_upper_case_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
Logical right shift.
Definition: std_expr.h:2341
static codet convert_is_letter_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_char_count(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:26
static codet convert_is_java_identifier_start_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaIdent...
static codet convert_is_java_identifier_start_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaIdent...
std::vector< exprt > operandst
Definition: expr.h:49
static codet convert_is_surrogate_pair(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_get_type_char(conversion_input &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_title_case_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_java_identifier_part_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_digit_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_upper_case_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
static codet convert_is_letter_or_digit_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_identifier_ignorable_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
static codet convert_char_value(conversion_input &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
static codet convert_is_ISO_control_char(conversion_input &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_input &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaIdent...
arrays with given size
Definition: std_types.h:901
binary minus
Definition: std_expr.h:758
Bit-wise AND.
Definition: std_expr.h:2180
static codet convert_digit_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_get_type_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
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 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)
static codet convert_reverse_bytes(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_space_char_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_mirrored_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
A statement in a programming language.
Definition: std_code.h:19
static codet convert_is_space(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
const typet & subtype() const
Definition: type.h:31
static codet convert_to_lower_case_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_valid_code_point(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static codet convert_get_numeric_value_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_unicode_identifier_start_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_upper_case_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
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_char_function(exprt(*expr_function)(const exprt &chr, const typet &type), conversion_input &target)
converts based on a function on expressions
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 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_is_whitespace(const exprt &chr, const typet &type)
Determines if the specified character is white space according to Java.
static codet convert_is_ISO_control_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_to_title_case_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
bitvector_typet char_type()
Definition: c_types.cpp:113
array constructor from list of elements
Definition: std_expr.h:1309
binary modulo
Definition: std_expr.h:902
static codet convert_is_space_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
Assignment.
Definition: std_code.h:144
static codet convert_is_mirrored_char(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_get_numeric_value_int(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_ideographic(conversion_input &target)
Converts function call to an assignment of an expression corresponding to the java method Character...