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_inputt &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  conversion_inputt &target)
84 {
85  return convert_char_function(
87 }
88 
92  const exprt &chr, const typet &type)
93 {
94  return typecast_exprt(chr, type);
95 }
96 
101  conversion_inputt &target)
102 {
103  return convert_char_function(
105 }
106 
111 {
112  const code_function_callt &function_call=target;
113  assert(function_call.arguments().size()==2);
114  const exprt &char1=function_call.arguments()[0];
115  const exprt &char2=function_call.arguments()[1];
116  const exprt &result=function_call.lhs();
117  const typet &type=result.type();
118  binary_relation_exprt smaller(char1, ID_lt, char2);
119  binary_relation_exprt greater(char1, ID_gt, char2);
120  if_exprt expr(
121  smaller,
122  from_integer(-1, type),
123  if_exprt(greater, from_integer(1, type), from_integer(0, type)));
124 
125  return code_assignt(result, expr);
126 }
127 
128 
137  conversion_inputt &target)
138 {
139  const code_function_callt &function_call=target;
140  const std::size_t nb_args=function_call.arguments().size();
141  PRECONDITION(nb_args==1 || nb_args==2);
142  const exprt &arg=function_call.arguments()[0];
143  // If there is no radix argument we set it to 36 which is the maximum possible
144  const exprt &radix=
145  nb_args>1?function_call.arguments()[1]:from_integer(36, arg.type());
146  const exprt &result=function_call.lhs();
147  const typet &type=result.type();
148 
149  // TODO: If the radix is not in the range MIN_RADIX <= radix <= MAX_RADIX or
150  // if the value of ch is not a valid digit in the specified radix,
151  // -1 is returned.
152 
153  // Case 1: The method isDigit is true of the character and the Unicode
154  // decimal digit value of the character (or its single-character
155  // decomposition) is less than the specified radix.
156  exprt invalid=from_integer(-1, arg.type());
157  exprt c0=from_integer('0', arg.type());
158  exprt latin_digit=in_interval_expr(arg, '0', '9');
159  minus_exprt value1(arg, c0);
160  // TODO: this is only valid for latin digits
161  if_exprt case1(
162  binary_relation_exprt(value1, ID_lt, radix), value1, invalid);
163 
164  // Case 2: The character is one of the uppercase Latin letters 'A'
165  // through 'Z' and its code is less than radix + 'A' - 10,
166  // then ch - 'A' + 10 is returned.
167  exprt cA=from_integer('A', arg.type());
168  exprt i10=from_integer(10, arg.type());
169  exprt upper_case=in_interval_expr(arg, 'A', 'Z');
170  plus_exprt value2(minus_exprt(arg, cA), i10);
171  if_exprt case2(
172  binary_relation_exprt(value2, ID_lt, radix), value2, invalid);
173 
174  // The character is one of the lowercase Latin letters 'a' through 'z' and
175  // its code is less than radix + 'a' - 10, then ch - 'a' + 10 is returned.
176  exprt ca=from_integer('a', arg.type());
177  exprt lower_case=in_interval_expr(arg, 'a', 'z');
178  plus_exprt value3(minus_exprt(arg, ca), i10);
179  if_exprt case3(
180  binary_relation_exprt(value3, ID_lt, radix), value3, invalid);
181 
182 
183  // The character is one of the fullwidth uppercase Latin letters A ('\uFF21')
184  // through Z ('\uFF3A') and its code is less than radix + '\uFF21' - 10.
185  // In this case, ch - '\uFF21' + 10 is returned.
186  exprt uFF21=from_integer(0xFF21, arg.type());
187  exprt fullwidth_upper_case=in_interval_expr(arg, 0xFF21, 0xFF3A);
188  plus_exprt value4(minus_exprt(arg, uFF21), i10);
189  if_exprt case4(
190  binary_relation_exprt(value4, ID_lt, radix), value4, invalid);
191 
192  // The character is one of the fullwidth lowercase Latin letters a ('\uFF41')
193  // through z ('\uFF5A') and its code is less than radix + '\uFF41' - 10.
194  // In this case, ch - '\uFF41' + 10 is returned.
195  exprt uFF41=from_integer(0xFF41, arg.type());
196  plus_exprt value5(minus_exprt(arg, uFF41), i10);
197  if_exprt case5(
198  binary_relation_exprt(value5, ID_lt, radix), value5, invalid);
199 
200  if_exprt fullwidth_cases(fullwidth_upper_case, case4, case5);
201  if_exprt expr(
202  latin_digit,
203  case1,
204  if_exprt(upper_case, case2, if_exprt(lower_case, case3, fullwidth_cases)));
205  typecast_exprt tc_expr(expr, type);
206 
207  return code_assignt(result, tc_expr);
208 }
209 
214 {
215  return convert_digit_char(target);
216 }
217 
224 {
225  const code_function_callt &function_call=target;
226  assert(function_call.arguments().size()==2);
227  const exprt &digit=function_call.arguments()[0];
228  const exprt &result=function_call.lhs();
229  const typet &type=result.type();
230  typecast_exprt casted_digit(digit, type);
231 
232  exprt d10=from_integer(10, type);
233  binary_relation_exprt small(casted_digit, ID_le, d10);
234  plus_exprt value1(casted_digit, from_integer('0', type));
235  plus_exprt value2(minus_exprt(casted_digit, d10), from_integer('a', type));
236  return code_assignt(result, if_exprt(small, value1, value2));
237 }
238 
243  conversion_inputt &target)
244 {
245  // TODO: This is unimplemented for now as it requires analyzing
246  // the UnicodeData file to find characters directionality.
247  return target;
248 }
249 
254  conversion_inputt &target)
255 {
256  return convert_get_directionality_char(target);
257 }
258 
264  conversion_inputt &target)
265 {
266  return convert_digit_char(target);
267 }
268 
275  conversion_inputt &target)
276 {
277  return convert_digit_int(target);
278 }
279 
284  conversion_inputt &target)
285 {
286  // TODO: This is unimplemented for now as it requires analyzing
287  // the UnicodeData file to categorize characters.
288  return target;
289 }
290 
295  conversion_inputt &target)
296 {
297  return convert_get_type_char(target);
298 }
299 
304 {
305  return convert_char_value(target);
306 }
307 
315  const exprt &chr, const typet &type)
316 {
317  exprt u10000=from_integer(0x010000, type);
318  exprt uD800=from_integer(0xD800, type);
319  exprt u400=from_integer(0x0400, type);
320 
321  plus_exprt high_surrogate(uD800, div_exprt(minus_exprt(chr, u10000), u400));
322  return high_surrogate;
323 }
324 
328  conversion_inputt &target)
329 {
330  return convert_char_function(
332 }
333 
339  const exprt &chr, const typet &type)
340 {
341  return in_interval_expr(chr, 'a', 'z');
342 }
343 
349  const exprt &chr, const typet &type)
350 {
351  return in_interval_expr(chr, 'A', 'Z');
352 }
353 
363  const exprt &chr, const typet &type)
364 {
365  return or_exprt(
366  expr_of_is_ascii_upper_case(chr, type),
367  expr_of_is_ascii_lower_case(chr, type));
368 }
369 
381  const exprt &chr, const typet &type)
382 {
383  return expr_of_is_letter(chr, type);
384 }
385 
390  conversion_inputt &target)
391 {
392  return convert_char_function(
394 }
395 
403  const exprt &chr, const typet &type)
404 {
405  binary_relation_exprt is_bmp(chr, ID_le, from_integer(0xFFFF, chr.type()));
406  return is_bmp;
407 }
408 
413  conversion_inputt &target)
414 {
415  return convert_char_function(
417 }
418 
424  const exprt &chr, const typet &type)
425 {
426  // The following intervals are undefined in unicode, according to
427  // the Unicode Character Database: http://www.unicode.org/Public/UCD/latest/
428  exprt::operandst intervals;
429  intervals.push_back(in_interval_expr(chr, 0x0750, 0x077F));
430  intervals.push_back(in_interval_expr(chr, 0x07C0, 0x08FF));
431  intervals.push_back(in_interval_expr(chr, 0x1380, 0x139F));
432  intervals.push_back(in_interval_expr(chr, 0x18B0, 0x18FF));
433  intervals.push_back(in_interval_expr(chr, 0x1980, 0x19DF));
434  intervals.push_back(in_interval_expr(chr, 0x1A00, 0x1CFF));
435  intervals.push_back(in_interval_expr(chr, 0x1D80, 0x1DFF));
436  intervals.push_back(in_interval_expr(chr, 0x2C00, 0x2E7F));
437  intervals.push_back(in_interval_expr(chr, 0x2FE0, 0x2FEF));
438  intervals.push_back(in_interval_expr(chr, 0x31C0, 0x31EF));
439  intervals.push_back(in_interval_expr(chr, 0x9FB0, 0x9FFF));
440  intervals.push_back(in_interval_expr(chr, 0xA4D0, 0xABFF));
441  intervals.push_back(in_interval_expr(chr, 0xD7B0, 0xD7FF));
442  intervals.push_back(in_interval_expr(chr, 0xFE10, 0xFE1F));
443  intervals.push_back(in_interval_expr(chr, 0x10140, 0x102FF));
444  intervals.push_back(in_interval_expr(chr, 0x104B0, 0x107FF));
445  intervals.push_back(in_interval_expr(chr, 0x10840, 0x1CFFF));
446  intervals.push_back(in_interval_expr(chr, 0x1D200, 0x1D2FF));
447  intervals.push_back(in_interval_expr(chr, 0x1D360, 0x1D3FF));
448  intervals.push_back(
449  binary_relation_exprt(chr, ID_ge, from_integer(0x1D800, chr.type())));
450 
451  return not_exprt(disjunction(intervals));
452 }
453 
458  conversion_inputt &target)
459 {
460  return convert_char_function(
462 }
463 
468  conversion_inputt &target)
469 {
470  return convert_is_defined_char(target);
471 }
472 
488  const exprt &chr, const typet &type)
489 {
490  exprt latin_digit=in_interval_expr(chr, '0', '9');
491  exprt arabic_indic_digit=in_interval_expr(chr, 0x660, 0x669);
492  exprt extended_digit=in_interval_expr(chr, 0x6F0, 0x6F9);
493  exprt devanagari_digit=in_interval_expr(chr, 0x966, 0x96F);
494  exprt fullwidth_digit=in_interval_expr(chr, 0xFF10, 0xFF19);
495  or_exprt digit(
496  or_exprt(latin_digit, or_exprt(arabic_indic_digit, extended_digit)),
497  or_exprt(devanagari_digit, fullwidth_digit));
498  return digit;
499 }
500 
505  conversion_inputt &target)
506 {
507  return convert_char_function(
509 }
510 
515  conversion_inputt &target)
516 {
517  return convert_is_digit_char(target);
518 }
519 
526  const exprt &chr, const typet &type)
527 {
528  return in_interval_expr(chr, 0xD800, 0xDBFF);
529 }
530 
535  conversion_inputt &target)
536 {
537  return convert_char_function(
539 }
540 
550  const exprt &chr, const typet &type)
551 {
552  or_exprt ignorable(
553  in_interval_expr(chr, 0x0000, 0x0008),
554  or_exprt(
555  in_interval_expr(chr, 0x000E, 0x001B),
556  in_interval_expr(chr, 0x007F, 0x009F)));
557  return ignorable;
558 }
559 
566  conversion_inputt &target)
567 {
568  return convert_char_function(
570 }
571 
578  conversion_inputt &target)
579 {
581 }
582 
587  conversion_inputt &target)
588 {
589  const code_function_callt &function_call=target;
590  assert(function_call.arguments().size()==1);
591  const exprt &arg=function_call.arguments()[0];
592  const exprt &result=function_call.lhs();
593  exprt is_ideograph=in_interval_expr(arg, 0x4E00, 0x9FFF);
594  return code_assignt(result, is_ideograph);
595 }
596 
601  conversion_inputt &target)
602 {
603  const code_function_callt &function_call=target;
604  assert(function_call.arguments().size()==1);
605  const exprt &arg=function_call.arguments()[0];
606  const exprt &result=function_call.lhs();
607  or_exprt iso(
608  in_interval_expr(arg, 0x00, 0x1F), in_interval_expr(arg, 0x7F, 0x9F));
609  return code_assignt(result, iso);
610 }
611 
616  conversion_inputt &target)
617 {
618  return convert_is_ISO_control_char(target);
619 }
620 
628  conversion_inputt &target)
629 {
630  return convert_char_function(
632 }
633 
638  conversion_inputt &target)
639 {
641 }
642 
651  conversion_inputt &target)
652 {
653  return convert_char_function(
655 }
656 
661  conversion_inputt &target)
662 {
664 }
665 
670  conversion_inputt &target)
671 {
673 }
674 
679  conversion_inputt &target)
680 {
682 }
683 
688  conversion_inputt &target)
689 {
690  return convert_char_function(
692 }
693 
698  conversion_inputt &target)
699 {
700  return convert_is_letter_char(target);
701 }
702 
708  const exprt &chr, const typet &type)
709 {
710  return or_exprt(expr_of_is_letter(chr, type), expr_of_is_digit(chr, type));
711 }
712 
717  conversion_inputt &target)
718 {
719  return convert_char_function(
721 }
722 
727  conversion_inputt &target)
728 {
729  return convert_is_letter_or_digit_char(target);
730 }
731 
738  conversion_inputt &target)
739 {
740  return convert_char_function(
742 }
743 
750  conversion_inputt &target)
751 {
752  return convert_is_lower_case_char(target);
753 }
754 
759  conversion_inputt &target)
760 {
761  const code_function_callt &function_call=target;
762  assert(function_call.arguments().size()==1);
763  const exprt &arg=function_call.arguments()[0];
764  const exprt &result=function_call.lhs();
765  exprt is_low_surrogate=in_interval_expr(arg, 0xDC00, 0xDFFF);
766  return code_assignt(result, is_low_surrogate);
767 }
768 
777  const exprt &chr, const typet &type)
778 {
779  return in_list_expr(chr, {0x28, 0x29, 0x3C, 0x3E, 0x5B, 0x5D, 0x7B, 0x7D});
780 }
781 
788  conversion_inputt &target)
789 {
790  return convert_char_function(
792 }
793 
800  conversion_inputt &target)
801 {
802  return convert_is_mirrored_char(target);
803 }
804 
809 {
810  return convert_is_whitespace_char(target);
811 }
812 
819  const exprt &chr, const typet &type)
820 {
821  std::list<mp_integer> space_characters=
822  {0x20, 0x00A0, 0x1680, 0x202F, 0x205F, 0x3000, 0x2028, 0x2029};
823  exprt condition0=in_list_expr(chr, space_characters);
824  exprt condition1=in_interval_expr(chr, 0x2000, 0x200A);
825  return or_exprt(condition0, condition1);
826 }
827 
832  conversion_inputt &target)
833 {
834  return convert_char_function(
836 }
837 
842  conversion_inputt &target)
843 {
844  return convert_is_space_char(target);
845 }
846 
853  const exprt &chr, const typet &type)
854 {
855  return binary_relation_exprt(chr, ID_gt, from_integer(0xFFFF, chr.type()));
856 }
857 
862  conversion_inputt &target)
863 {
864  return convert_char_function(
866 }
867 
873  const exprt &chr, const typet &type)
874 {
875  return in_interval_expr(chr, 0xD800, 0xDFFF);
876 }
877 
882  conversion_inputt &target)
883 {
884  return convert_char_function(
886 }
887 
892  conversion_inputt &target)
893 {
894  const code_function_callt &function_call=target;
895  assert(function_call.arguments().size()==2);
896  const exprt &arg0=function_call.arguments()[0];
897  const exprt &arg1=function_call.arguments()[1];
898  const exprt &result=function_call.lhs();
899  exprt is_low_surrogate=in_interval_expr(arg1, 0xDC00, 0xDFFF);
900  exprt is_high_surrogate=in_interval_expr(arg0, 0xD800, 0xDBFF);
901  return code_assignt(result, and_exprt(is_high_surrogate, is_low_surrogate));
902 }
903 
909  const exprt &chr, const typet &type)
910 {
911  std::list<mp_integer>title_case_chars=
912  {0x01C5, 0x01C8, 0x01CB, 0x01F2, 0x1FBC, 0x1FCC, 0x1FFC};
913  exprt::operandst conditions;
914  conditions.push_back(in_list_expr(chr, title_case_chars));
915  conditions.push_back(in_interval_expr(chr, 0x1F88, 0x1F8F));
916  conditions.push_back(in_interval_expr(chr, 0x1F98, 0x1F9F));
917  conditions.push_back(in_interval_expr(chr, 0x1FA8, 0x1FAF));
918  return disjunction(conditions);
919 }
920 
925  conversion_inputt &target)
926 {
927  return convert_char_function(
929 }
930 
935  conversion_inputt &target)
936 {
937  return convert_is_title_case_char(target);
938 }
939 
946  const exprt &chr, const typet &type)
947 {
948  // The following set of characters is the general category "Nl" in the
949  // Unicode specification.
950  exprt cond0=in_interval_expr(chr, 0x16EE, 0x16F0);
951  exprt cond1=in_interval_expr(chr, 0x2160, 0x2188);
952  exprt cond2=in_interval_expr(chr, 0x3021, 0x3029);
953  exprt cond3=in_interval_expr(chr, 0x3038, 0x303A);
954  exprt cond4=in_interval_expr(chr, 0xA6E6, 0xA6EF);
955  exprt cond5=in_interval_expr(chr, 0x10140, 0x10174);
956  exprt cond6=in_interval_expr(chr, 0x103D1, 0x103D5);
957  exprt cond7=in_interval_expr(chr, 0x12400, 0x1246E);
958  exprt cond8=in_list_expr(chr, {0x3007, 0x10341, 0x1034A});
959  return or_exprt(
960  or_exprt(or_exprt(cond0, cond1), or_exprt(cond2, cond3)),
961  or_exprt(or_exprt(cond4, cond5), or_exprt(cond6, or_exprt(cond7, cond8))));
962 }
963 
964 
973  const exprt &chr, const typet &type)
974 {
975  exprt::operandst conditions;
976  conditions.push_back(expr_of_is_unicode_identifier_start(chr, type));
977  conditions.push_back(expr_of_is_digit(chr, type));
978  conditions.push_back(expr_of_is_identifier_ignorable(chr, type));
979  return disjunction(conditions);
980 }
981 
986  conversion_inputt &target)
987 {
988  return convert_char_function(
990 }
991 
996  conversion_inputt &target)
997 {
999 }
1000 
1007  const exprt &chr, const typet &type)
1008 {
1009  return or_exprt(
1010  expr_of_is_letter(chr, type), expr_of_is_letter_number(chr, type));
1011 }
1012 
1017  conversion_inputt &target)
1018 {
1019  return convert_char_function(
1021 }
1022 
1027  conversion_inputt &target)
1028 {
1030 }
1031 
1038  conversion_inputt &target)
1039 {
1040  return convert_char_function(
1042 }
1043 
1048  conversion_inputt &target)
1049 {
1050  return convert_is_upper_case_char(target);
1051 }
1052 
1059  const exprt &chr, const typet &type)
1060 {
1061  return binary_relation_exprt(chr, ID_le, from_integer(0x10FFFF, chr.type()));
1062 }
1063 
1068  conversion_inputt &target)
1069 {
1070  return convert_char_function(
1072 }
1073 
1083  const exprt &chr, const typet &type)
1084 {
1085  exprt::operandst conditions;
1086  std::list<mp_integer> space_characters=
1087  {0x20, 0x1680, 0x205F, 0x3000, 0x2028, 0x2029};
1088  conditions.push_back(in_list_expr(chr, space_characters));
1089  conditions.push_back(in_interval_expr(chr, 0x2000, 0x2006));
1090  conditions.push_back(in_interval_expr(chr, 0x2008, 0x200A));
1091  conditions.push_back(in_interval_expr(chr, 0x09, 0x0D));
1092  conditions.push_back(in_interval_expr(chr, 0x1C, 0x1F));
1093  return disjunction(conditions);
1094 }
1095 
1100  conversion_inputt &target)
1101 {
1102  return convert_char_function(
1104 }
1105 
1110  conversion_inputt &target)
1111 {
1112  return convert_is_whitespace_char(target);
1113 }
1114 
1122  const exprt &chr, const typet &type)
1123 {
1124  exprt uDC00=from_integer(0xDC00, type);
1125  exprt u0400=from_integer(0x0400, type);
1126  return plus_exprt(uDC00, mod_exprt(chr, u0400));
1127 }
1128 
1133  conversion_inputt &target)
1134 {
1135  return convert_char_function(
1137 }
1138 
1145  const exprt &chr, const typet &type)
1146 {
1147  shl_exprt first_byte(chr, from_integer(8, type));
1148  lshr_exprt second_byte(chr, from_integer(8, type));
1149  return plus_exprt(first_byte, second_byte);
1150 }
1151 
1156  conversion_inputt &target)
1157 {
1158  return convert_char_function(
1160 }
1161 
1171  const exprt &chr, const typet &type)
1172 {
1173  array_typet array_type=to_array_type(type);
1174  const typet &char_type=array_type.subtype();
1175  array_exprt case1(array_type);
1176  array_exprt case2(array_type);
1177  exprt low_surrogate=expr_of_low_surrogate(chr, char_type);
1178  case1.copy_to_operands(low_surrogate);
1179  case2.move_to_operands(low_surrogate);
1180  exprt high_surrogate=expr_of_high_surrogate(chr, char_type);
1181  case2.move_to_operands(high_surrogate);
1182  return if_exprt(expr_of_is_bmp_code_point(chr, type), case1, case2);
1183 }
1184 
1189 {
1190  return convert_char_function(
1192 }
1193 
1198  conversion_inputt &target)
1199 {
1200  const code_function_callt &function_call=target;
1201  assert(function_call.arguments().size()==2);
1202  const exprt &arg0=function_call.arguments()[0];
1203  const exprt &arg1=function_call.arguments()[1];
1204  const exprt &result=function_call.lhs();
1205  const typet &type=result.type();
1206 
1207  // These operations implement the decoding of a unicode symbol encoded
1208  // in UTF16 for the supplementary planes (above U+10000).
1209  // The low ten bits of the first character give the bits 10 to 19 of
1210  // code point and the low ten bits of the second give the bits 0 to 9,
1211  // then 0x10000 is added to the result. For more explenations see:
1212  // https://en.wikipedia.org/wiki/UTF-16
1213 
1214  exprt u010000=from_integer(0x010000, type);
1215  exprt mask10bit=from_integer(0x03FF, type);
1216  shl_exprt m1(bitand_exprt(arg0, mask10bit), from_integer(10, type));
1217  bitand_exprt m2(arg1, mask10bit);
1218  bitor_exprt pair_value(u010000, bitor_exprt(m1, m2));
1219  return code_assignt(result, pair_value);
1220 }
1221 
1231  const exprt &chr, const typet &type)
1232 {
1233  minus_exprt transformed(
1234  plus_exprt(chr, from_integer('a', type)), from_integer('A', type));
1235 
1236  if_exprt res(expr_of_is_ascii_upper_case(chr, type), transformed, chr);
1237  return res;
1238 }
1239 
1244  conversion_inputt &target)
1245 {
1246  return convert_char_function(
1248 }
1249 
1254  conversion_inputt &target)
1255 {
1256  return convert_to_lower_case_char(target);
1257 }
1258 
1264  const exprt &chr, const typet &type)
1265 {
1266  std::list<mp_integer> increment_list={0x01C4, 0x01C7, 0x01CA, 0x01F1};
1267  std::list<mp_integer> decrement_list={0x01C6, 0x01C9, 0x01CC, 0x01F3};
1268  exprt plus_8_interval1=in_interval_expr(chr, 0x1F80, 0x1F87);
1269  exprt plus_8_interval2=in_interval_expr(chr, 0x1F90, 0x1F97);
1270  exprt plus_8_interval3=in_interval_expr(chr, 0x1FA0, 0x1FA7);
1271  std::list<mp_integer> plus_9_list={0x1FB3, 0x1FC3, 0x1FF3};
1272  minus_exprt minus_1(chr, from_integer(1, type));
1273  plus_exprt plus_1(chr, from_integer(1, type));
1274  plus_exprt plus_8(chr, from_integer(8, type));
1275  plus_exprt plus_9(chr, from_integer(9, type));
1276  or_exprt plus_8_set(
1277  plus_8_interval1, or_exprt(plus_8_interval2, plus_8_interval3));
1278 
1279  if_exprt res(
1280  in_list_expr(chr, increment_list),
1281  plus_1,
1282  if_exprt(
1283  in_list_expr(chr, decrement_list),
1284  minus_1,
1285  if_exprt(
1286  plus_8_set,
1287  plus_8,
1288  if_exprt(
1289  in_list_expr(chr, plus_9_list),
1290  plus_9,
1291  chr))));
1292 
1293  return res;
1294 }
1295 
1300  conversion_inputt &target)
1301 {
1302  return convert_char_function(
1304 }
1305 
1310  conversion_inputt &target)
1311 {
1312  return convert_to_title_case_char(target);
1313 }
1314 
1324  const exprt &chr, const typet &type)
1325 {
1326  minus_exprt transformed(
1327  plus_exprt(chr, from_integer('A', type)), from_integer('a', type));
1328 
1329  if_exprt res(expr_of_is_ascii_lower_case(chr, type), transformed, chr);
1330  return res;
1331 }
1332 
1337  conversion_inputt &target)
1338 {
1339  return convert_char_function(
1341 }
1342 
1347  conversion_inputt &target)
1348 {
1349  return convert_to_upper_case_char(target);
1350 }
1351 
1359  const code_function_callt &code) const
1360 {
1361  if(code.function().id()==ID_symbol)
1362  {
1363  const irep_idt &function_id=
1364  to_symbol_expr(code.function()).get_identifier();
1365  auto it=conversion_table.find(function_id);
1366  if(it!=conversion_table.end())
1367  return (it->second)(code);
1368  }
1369 
1370  return code;
1371 }
1372 
1375 {
1376  // All methods are listed here in alphabetic order
1377  // The ones that are not supported by this module (though they may be
1378  // supported by the string solver) have no entry in the conversion
1379  // table and are marked in this way:
1380  // Not supported "java::java.lang.Character.<init>()"
1381 
1382  conversion_table["java::java.lang.Character.charCount:(I)I"]=
1384  conversion_table["java::java.lang.Character.charValue:()C"]=
1386 
1387  // Not supported "java::java.lang.Character.codePointAt:([CI)I
1388  // Not supported "java::java.lang.Character.codePointAt:([CII)I"
1389  // Not supported "java::java.lang.Character.codePointAt:"
1390  // "(Ljava.lang.CharSequence;I)I"
1391  // Not supported "java::java.lang.Character.codePointBefore:([CI)I"
1392  // Not supported "java::java.lang.Character.codePointBefore:([CII)I"
1393  // Not supported "java::java.lang.Character.codePointBefore:"
1394  // "(Ljava.lang.CharSequence;I)I"
1395  // Not supported "java::java.lang.Character.codePointCount:([CII)I"
1396  // Not supported "java::java.lang.Character.codePointCount:"
1397  // "(Ljava.lang.CharSequence;II)I"
1398  // Not supported "java::java.lang.Character.compareTo:"
1399  // "(Ljava.lang.Character;)I"
1400 
1401  conversion_table["java::java.lang.Character.compare:(CC)I"]=
1403  conversion_table["java::java.lang.Character.digit:(CI)I"]=
1405  conversion_table["java::java.lang.Character.digit:(II)I"]=
1407 
1408  // Not supported "java::java.lang.Character.equals:(Ljava.lang.Object;)Z"
1409 
1410  conversion_table["java::java.lang.Character.forDigit:(II)C"]=
1412  conversion_table["java::java.lang.Character.getDirectionality:(C)B"]=
1414  conversion_table["java::java.lang.Character.getDirectionality:(I)B"]=
1416 
1417  // Not supported "java::java.lang.Character.getName:(I)Ljava.lang.String;"
1418 
1419  conversion_table["java::java.lang.Character.getNumericValue:(C)I"]=
1421  conversion_table["java::java.lang.Character.getNumericValue:(I)I"]=
1423  conversion_table["java::java.lang.Character.getType:(C)I"]=
1425  conversion_table["java::java.lang.Character.getType:(I)I"]=
1427  conversion_table["java::java.lang.Character.hashCode:()I"]=
1429  conversion_table["java::java.lang.Character.highSurrogate:(I)C"]=
1431  conversion_table["java::java.lang.Character.isAlphabetic:(I)Z"]=
1433  conversion_table["java::java.lang.Character.isBmpCodePoint:(I)Z"]=
1435  conversion_table["java::java.lang.Character.isDefined:(C)Z"]=
1437  conversion_table["java::java.lang.Character.isDefined:(I)Z"]=
1439  conversion_table["java::java.lang.Character.isDigit:(C)Z"]=
1441  conversion_table["java::java.lang.Character.isDigit:(I)Z"]=
1443  conversion_table["java::java.lang.Character.isHighSurrogate:(C)Z"]=
1445  conversion_table["java::java.lang.Character.isIdentifierIgnorable:(C)Z"]=
1447  conversion_table["java::java.lang.Character.isIdentifierIgnorable:(I)Z"]=
1449  conversion_table["java::java.lang.Character.isIdeographic:(I)Z"]=
1451  conversion_table["java::java.lang.Character.isISOControl:(C)Z"]=
1453  conversion_table["java::java.lang.Character.isISOControl:(I)Z"]=
1455  conversion_table["java::java.lang.Character.isJavaIdentifierPart:(C)Z"]=
1457  conversion_table["java::java.lang.Character.isJavaIdentifierPart:(I)Z"]=
1459  conversion_table["java::java.lang.Character.isJavaIdentifierStart:(C)Z"]=
1461  conversion_table["java::java.lang.Character.isJavaIdentifierStart:(I)Z"]=
1463  conversion_table["java::java.lang.Character.isJavaLetter:(C)Z"]=
1465  conversion_table["java::java.lang.Character.isJavaLetterOrDigit:(C)Z"]=
1467  conversion_table["java::java.lang.Character.isLetter:(C)Z"]=
1469  conversion_table["java::java.lang.Character.isLetter:(I)Z"]=
1471  conversion_table["java::java.lang.Character.isLetterOrDigit:(C)Z"]=
1473  conversion_table["java::java.lang.Character.isLetterOrDigit:(I)Z"]=
1475  conversion_table["java::java.lang.Character.isLowerCase:(C)Z"]=
1477  conversion_table["java::java.lang.Character.isLowerCase:(I)Z"]=
1479  conversion_table["java::java.lang.Character.isLowSurrogate:(C)Z"]=
1481  conversion_table["java::java.lang.Character.isMirrored:(C)Z"]=
1483  conversion_table["java::java.lang.Character.isMirrored:(I)Z"]=
1485  conversion_table["java::java.lang.Character.isSpace:(C)Z"]=
1487  conversion_table["java::java.lang.Character.isSpaceChar:(C)Z"]=
1489  conversion_table["java::java.lang.Character.isSpaceChar:(I)Z"]=
1491  conversion_table["java::java.lang.Character.isSupplementaryCodePoint:(I)Z"]=
1493  conversion_table["java::java.lang.Character.isSurrogate:(C)Z"]=
1495  conversion_table["java::java.lang.Character.isSurrogatePair:(CC)Z"]=
1497  conversion_table["java::java.lang.Character.isTitleCase:(C)Z"]=
1499  conversion_table["java::java.lang.Character.isTitleCase:(I)Z"]=
1501  conversion_table["java::java.lang.Character.isUnicodeIdentifierPart:(C)Z"]=
1503  conversion_table["java::java.lang.Character.isUnicodeIdentifierPart:(I)Z"]=
1505  conversion_table["java::java.lang.Character.isUnicodeIdentifierStart:(C)Z"]=
1507  conversion_table["java::java.lang.Character.isUnicodeIdentifierStart:(I)Z"]=
1509  conversion_table["java::java.lang.Character.isUpperCase:(C)Z"]=
1511  conversion_table["java::java.lang.Character.isUpperCase:(I)Z"]=
1513  conversion_table["java::java.lang.Character.isValidCodePoint:(I)Z"]=
1515  conversion_table["java::java.lang.Character.isWhitespace:(C)Z"]=
1517  conversion_table["java::java.lang.Character.isWhitespace:(I)Z"]=
1519  conversion_table["java::java.lang.Character.lowSurrogate:(I)C"]=
1521 
1522  // Not supported "java::java.lang.Character.offsetByCodePoints:([CIIII)I"
1523  // Not supported "java::java.lang.Character.offsetByCodePoints:"
1524  // "(Ljava.lang.CharacterSequence;II)I"
1525 
1526  conversion_table["java::java.lang.Character.reverseBytes:(C)C"]=
1528  conversion_table["java::java.lang.Character.toChars:(I)[C"]=
1530 
1531  // Not supported "java::java.lang.Character.toChars:(I[CI)I"
1532 
1533  conversion_table["java::java.lang.Character.toCodePoint:(CC)I"]=
1535  conversion_table["java::java.lang.Character.toLowerCase:(C)C"]=
1537  conversion_table["java::java.lang.Character.toLowerCase:(I)I"]=
1539 
1540  // Not supported "java::java.lang.Character.toString:()Ljava.lang.String;"
1541  // Not supported "java::java.lang.Character.toString:(C)Ljava.lang.String;"
1542 
1543  conversion_table["java::java.lang.Character.toTitleCase:(C)C"]=
1545  conversion_table["java::java.lang.Character.toTitleCase:(I)I"]=
1547  conversion_table["java::java.lang.Character.toUpperCase:(C)C"]=
1549  conversion_table["java::java.lang.Character.toUpperCase:(I)I"]=
1551 
1552  // Not supported "java::java.lang.Character.valueOf:(C)Ljava.lang.Character;"
1553 }
The type of an expression.
Definition: type.h:22
static codet convert_is_alphabetic(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
Boolean negation.
Definition: std_expr.h:3228
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
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_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_high_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
boolean OR
Definition: std_expr.h:2391
static exprt expr_of_is_title_case(const exprt &chr, const typet &type)
Determines if the specified character is a titlecase character.
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_mirrored(const exprt &chr, const typet &type)
Determines whether the character is mirrored according to the Unicode specification.
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...
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_ISO_control_int(conversion_inputt &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_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_java_identifier_part_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaIdent...
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:55
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_to_lower_case(const exprt &chr, const typet &type)
Converts the character argument to lowercase.
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
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 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 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 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.
Definition: std_expr.h:3359
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_is_title_case_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
typet & type()
Definition: expr.h:56
static codet convert_low_surrogate(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_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_digit_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
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.
static codet convert_get_type_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
static codet convert_is_defined_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_space(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
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_to_code_point(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.
equality
Definition: std_expr.h:1354
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 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.
static codet convert_compare(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
const irep_idt & id() const
Definition: irep.h:259
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...
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_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
Bit-wise OR.
Definition: std_expr.h:2583
argumentst & arguments()
Definition: std_code.h:890
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:1075
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 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_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_is_unicode_identifier_start_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_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_title_case_int(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...
boolean AND
Definition: std_expr.h:2255
API to expression classes.
static codet convert_char_value(conversion_inputt &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 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.
Left shift.
Definition: std_expr.h:2848
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
static codet convert_to_chars(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
A function call.
Definition: std_code.h:858
The plus expression.
Definition: std_expr.h:893
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
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_get_directionality_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
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_title_case_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
Logical right shift.
Definition: std_expr.h:2888
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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...
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:24
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...
std::vector< exprt > operandst
Definition: expr.h:45
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_mirrored_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_digit_char(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_unicode_identifier_part_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
mstreamt & result() const
Definition: message.h:312
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...
exprt & function()
Definition: std_code.h:878
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
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...
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...
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
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_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_java_identifier_part_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
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 codet convert_is_high_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
arrays with given size
Definition: std_types.h:1013
binary minus
Definition: std_expr.h:959
Bit-wise AND.
Definition: std_expr.h:2704
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 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_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_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_letter_int(conversion_inputt &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:21
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_for_digit(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
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_hash_code(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
const typet & subtype() const
Definition: type.h:33
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 codet convert_is_whitespace_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
static codet convert_is_ideographic(conversion_inputt &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_is_java_identifier_start_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaIdent...
static codet convert_is_low_surrogate(conversion_inputt &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 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_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
bitvector_typet char_type()
Definition: c_types.cpp:114
array constructor from list of elements
Definition: std_expr.h:1617
binary modulo
Definition: std_expr.h:1133
static codet convert_reverse_bytes(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
Assignment.
Definition: std_code.h:196
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_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_letter_or_digit_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...