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 std::move(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  (void)type; // unused parameter
342  return in_interval_expr(chr, 'a', 'z');
343 }
344 
350  const exprt &chr, const typet &type)
351 {
352  (void)type; // unused parameter
353  return in_interval_expr(chr, 'A', 'Z');
354 }
355 
365  const exprt &chr, const typet &type)
366 {
367  return or_exprt(
368  expr_of_is_ascii_upper_case(chr, type),
369  expr_of_is_ascii_lower_case(chr, type));
370 }
371 
383  const exprt &chr, const typet &type)
384 {
385  return expr_of_is_letter(chr, type);
386 }
387 
392  conversion_inputt &target)
393 {
394  return convert_char_function(
396 }
397 
405  const exprt &chr, const typet &type)
406 {
407  (void)type; // unused parameter
408  return and_exprt(
409  binary_relation_exprt(chr, ID_le, from_integer(0xFFFF, chr.type())),
410  binary_relation_exprt(chr, ID_ge, from_integer(0, chr.type())));
411 }
412 
417  conversion_inputt &target)
418 {
419  return convert_char_function(
421 }
422 
428  const exprt &chr, const typet &type)
429 {
430  (void)type; // unused parameter
431  // The following intervals are undefined in unicode, according to
432  // the Unicode Character Database: http://www.unicode.org/Public/UCD/latest/
433  exprt::operandst intervals;
434  intervals.push_back(in_interval_expr(chr, 0x0750, 0x077F));
435  intervals.push_back(in_interval_expr(chr, 0x07C0, 0x08FF));
436  intervals.push_back(in_interval_expr(chr, 0x1380, 0x139F));
437  intervals.push_back(in_interval_expr(chr, 0x18B0, 0x18FF));
438  intervals.push_back(in_interval_expr(chr, 0x1980, 0x19DF));
439  intervals.push_back(in_interval_expr(chr, 0x1A00, 0x1CFF));
440  intervals.push_back(in_interval_expr(chr, 0x1D80, 0x1DFF));
441  intervals.push_back(in_interval_expr(chr, 0x2C00, 0x2E7F));
442  intervals.push_back(in_interval_expr(chr, 0x2FE0, 0x2FEF));
443  intervals.push_back(in_interval_expr(chr, 0x31C0, 0x31EF));
444  intervals.push_back(in_interval_expr(chr, 0x9FB0, 0x9FFF));
445  intervals.push_back(in_interval_expr(chr, 0xA4D0, 0xABFF));
446  intervals.push_back(in_interval_expr(chr, 0xD7B0, 0xD7FF));
447  intervals.push_back(in_interval_expr(chr, 0xFE10, 0xFE1F));
448  intervals.push_back(in_interval_expr(chr, 0x10140, 0x102FF));
449  intervals.push_back(in_interval_expr(chr, 0x104B0, 0x107FF));
450  intervals.push_back(in_interval_expr(chr, 0x10840, 0x1CFFF));
451  intervals.push_back(in_interval_expr(chr, 0x1D200, 0x1D2FF));
452  intervals.push_back(in_interval_expr(chr, 0x1D360, 0x1D3FF));
453  intervals.push_back(
454  binary_relation_exprt(chr, ID_ge, from_integer(0x1D800, chr.type())));
455 
456  return not_exprt(disjunction(intervals));
457 }
458 
463  conversion_inputt &target)
464 {
465  return convert_char_function(
467 }
468 
473  conversion_inputt &target)
474 {
475  return convert_is_defined_char(target);
476 }
477 
493  const exprt &chr, const typet &type)
494 {
495  (void)type; // unused parameter
496  exprt latin_digit=in_interval_expr(chr, '0', '9');
497  exprt arabic_indic_digit=in_interval_expr(chr, 0x660, 0x669);
498  exprt extended_digit=in_interval_expr(chr, 0x6F0, 0x6F9);
499  exprt devanagari_digit=in_interval_expr(chr, 0x966, 0x96F);
500  exprt fullwidth_digit=in_interval_expr(chr, 0xFF10, 0xFF19);
501  or_exprt digit(
502  or_exprt(latin_digit, or_exprt(arabic_indic_digit, extended_digit)),
503  or_exprt(devanagari_digit, fullwidth_digit));
504  return std::move(digit);
505 }
506 
511  conversion_inputt &target)
512 {
513  return convert_char_function(
515 }
516 
521  conversion_inputt &target)
522 {
523  return convert_is_digit_char(target);
524 }
525 
532  const exprt &chr, const typet &type)
533 {
534  (void)type; // unused parameter
535  return in_interval_expr(chr, 0xD800, 0xDBFF);
536 }
537 
542  conversion_inputt &target)
543 {
544  return convert_char_function(
546 }
547 
557  const exprt &chr, const typet &type)
558 {
559  (void)type; // unused parameter
560  or_exprt ignorable(
561  in_interval_expr(chr, 0x0000, 0x0008),
562  or_exprt(
563  in_interval_expr(chr, 0x000E, 0x001B),
564  in_interval_expr(chr, 0x007F, 0x009F)));
565  return std::move(ignorable);
566 }
567 
574  conversion_inputt &target)
575 {
576  return convert_char_function(
578 }
579 
586  conversion_inputt &target)
587 {
589 }
590 
595  conversion_inputt &target)
596 {
597  const code_function_callt &function_call=target;
598  assert(function_call.arguments().size()==1);
599  const exprt &arg=function_call.arguments()[0];
600  const exprt &result=function_call.lhs();
601  exprt is_ideograph=in_interval_expr(arg, 0x4E00, 0x9FFF);
602  return code_assignt(result, is_ideograph);
603 }
604 
609  conversion_inputt &target)
610 {
611  const code_function_callt &function_call=target;
612  assert(function_call.arguments().size()==1);
613  const exprt &arg=function_call.arguments()[0];
614  const exprt &result=function_call.lhs();
615  or_exprt iso(
616  in_interval_expr(arg, 0x00, 0x1F), in_interval_expr(arg, 0x7F, 0x9F));
617  return code_assignt(result, iso);
618 }
619 
624  conversion_inputt &target)
625 {
626  return convert_is_ISO_control_char(target);
627 }
628 
636  conversion_inputt &target)
637 {
638  return convert_char_function(
640 }
641 
646  conversion_inputt &target)
647 {
649 }
650 
659  conversion_inputt &target)
660 {
661  return convert_char_function(
663 }
664 
669  conversion_inputt &target)
670 {
672 }
673 
678  conversion_inputt &target)
679 {
681 }
682 
687  conversion_inputt &target)
688 {
690 }
691 
696  conversion_inputt &target)
697 {
698  return convert_char_function(
700 }
701 
706  conversion_inputt &target)
707 {
708  return convert_is_letter_char(target);
709 }
710 
716  const exprt &chr, const typet &type)
717 {
718  return or_exprt(expr_of_is_letter(chr, type), expr_of_is_digit(chr, type));
719 }
720 
725  conversion_inputt &target)
726 {
727  return convert_char_function(
729 }
730 
735  conversion_inputt &target)
736 {
737  return convert_is_letter_or_digit_char(target);
738 }
739 
746  conversion_inputt &target)
747 {
748  return convert_char_function(
750 }
751 
758  conversion_inputt &target)
759 {
760  return convert_is_lower_case_char(target);
761 }
762 
767  conversion_inputt &target)
768 {
769  const code_function_callt &function_call=target;
770  assert(function_call.arguments().size()==1);
771  const exprt &arg=function_call.arguments()[0];
772  const exprt &result=function_call.lhs();
773  exprt is_low_surrogate=in_interval_expr(arg, 0xDC00, 0xDFFF);
775 }
776 
785  const exprt &chr, const typet &type)
786 {
787  (void)type; // unused parameter
788  return in_list_expr(chr, {0x28, 0x29, 0x3C, 0x3E, 0x5B, 0x5D, 0x7B, 0x7D});
789 }
790 
797  conversion_inputt &target)
798 {
799  return convert_char_function(
801 }
802 
809  conversion_inputt &target)
810 {
811  return convert_is_mirrored_char(target);
812 }
813 
818 {
819  return convert_is_whitespace_char(target);
820 }
821 
828  const exprt &chr, const typet &type)
829 {
830  (void)type; // unused parameter
831  std::list<mp_integer> space_characters=
832  {0x20, 0x00A0, 0x1680, 0x202F, 0x205F, 0x3000, 0x2028, 0x2029};
833  exprt condition0=in_list_expr(chr, space_characters);
834  exprt condition1=in_interval_expr(chr, 0x2000, 0x200A);
835  return or_exprt(condition0, condition1);
836 }
837 
842  conversion_inputt &target)
843 {
844  return convert_char_function(
846 }
847 
852  conversion_inputt &target)
853 {
854  return convert_is_space_char(target);
855 }
856 
863  const exprt &chr, const typet &type)
864 {
865  (void)type; // unused parameter
866  return binary_relation_exprt(chr, ID_gt, from_integer(0xFFFF, chr.type()));
867 }
868 
873  conversion_inputt &target)
874 {
875  return convert_char_function(
877 }
878 
884  const exprt &chr, const typet &type)
885 {
886  (void)type; // unused parameter
887  return in_interval_expr(chr, 0xD800, 0xDFFF);
888 }
889 
894  conversion_inputt &target)
895 {
896  return convert_char_function(
898 }
899 
904  conversion_inputt &target)
905 {
906  const code_function_callt &function_call=target;
907  assert(function_call.arguments().size()==2);
908  const exprt &arg0=function_call.arguments()[0];
909  const exprt &arg1=function_call.arguments()[1];
910  const exprt &result=function_call.lhs();
911  exprt is_low_surrogate=in_interval_expr(arg1, 0xDC00, 0xDFFF);
912  exprt is_high_surrogate=in_interval_expr(arg0, 0xD800, 0xDBFF);
914 }
915 
921  const exprt &chr, const typet &type)
922 {
923  (void)type; // unused parameter
924  std::list<mp_integer>title_case_chars=
925  {0x01C5, 0x01C8, 0x01CB, 0x01F2, 0x1FBC, 0x1FCC, 0x1FFC};
926  exprt::operandst conditions;
927  conditions.push_back(in_list_expr(chr, title_case_chars));
928  conditions.push_back(in_interval_expr(chr, 0x1F88, 0x1F8F));
929  conditions.push_back(in_interval_expr(chr, 0x1F98, 0x1F9F));
930  conditions.push_back(in_interval_expr(chr, 0x1FA8, 0x1FAF));
931  return disjunction(conditions);
932 }
933 
938  conversion_inputt &target)
939 {
940  return convert_char_function(
942 }
943 
948  conversion_inputt &target)
949 {
950  return convert_is_title_case_char(target);
951 }
952 
959  const exprt &chr, const typet &type)
960 {
961  (void)type; // unused parameter
962  // The following set of characters is the general category "Nl" in the
963  // Unicode specification.
964  exprt cond0=in_interval_expr(chr, 0x16EE, 0x16F0);
965  exprt cond1=in_interval_expr(chr, 0x2160, 0x2188);
966  exprt cond2=in_interval_expr(chr, 0x3021, 0x3029);
967  exprt cond3=in_interval_expr(chr, 0x3038, 0x303A);
968  exprt cond4=in_interval_expr(chr, 0xA6E6, 0xA6EF);
969  exprt cond5=in_interval_expr(chr, 0x10140, 0x10174);
970  exprt cond6=in_interval_expr(chr, 0x103D1, 0x103D5);
971  exprt cond7=in_interval_expr(chr, 0x12400, 0x1246E);
972  exprt cond8=in_list_expr(chr, {0x3007, 0x10341, 0x1034A});
973  return or_exprt(
974  or_exprt(or_exprt(cond0, cond1), or_exprt(cond2, cond3)),
975  or_exprt(or_exprt(cond4, cond5), or_exprt(cond6, or_exprt(cond7, cond8))));
976 }
977 
978 
987  const exprt &chr, const typet &type)
988 {
989  exprt::operandst conditions;
990  conditions.push_back(expr_of_is_unicode_identifier_start(chr, type));
991  conditions.push_back(expr_of_is_digit(chr, type));
992  conditions.push_back(expr_of_is_identifier_ignorable(chr, type));
993  return disjunction(conditions);
994 }
995 
1000  conversion_inputt &target)
1001 {
1002  return convert_char_function(
1004 }
1005 
1010  conversion_inputt &target)
1011 {
1013 }
1014 
1021  const exprt &chr, const typet &type)
1022 {
1023  return or_exprt(
1024  expr_of_is_letter(chr, type), expr_of_is_letter_number(chr, type));
1025 }
1026 
1031  conversion_inputt &target)
1032 {
1033  return convert_char_function(
1035 }
1036 
1041  conversion_inputt &target)
1042 {
1044 }
1045 
1052  conversion_inputt &target)
1053 {
1054  return convert_char_function(
1056 }
1057 
1062  conversion_inputt &target)
1063 {
1064  return convert_is_upper_case_char(target);
1065 }
1066 
1073  const exprt &chr, const typet &type)
1074 {
1075  (void)type; // unused parameter
1076  return binary_relation_exprt(chr, ID_le, from_integer(0x10FFFF, chr.type()));
1077 }
1078 
1083  conversion_inputt &target)
1084 {
1085  return convert_char_function(
1087 }
1088 
1098  const exprt &chr, const typet &type)
1099 {
1100  (void)type; // unused parameter
1101  exprt::operandst conditions;
1102  std::list<mp_integer> space_characters=
1103  {0x20, 0x1680, 0x205F, 0x3000, 0x2028, 0x2029};
1104  conditions.push_back(in_list_expr(chr, space_characters));
1105  conditions.push_back(in_interval_expr(chr, 0x2000, 0x2006));
1106  conditions.push_back(in_interval_expr(chr, 0x2008, 0x200A));
1107  conditions.push_back(in_interval_expr(chr, 0x09, 0x0D));
1108  conditions.push_back(in_interval_expr(chr, 0x1C, 0x1F));
1109  return disjunction(conditions);
1110 }
1111 
1116  conversion_inputt &target)
1117 {
1118  return convert_char_function(
1120 }
1121 
1126  conversion_inputt &target)
1127 {
1128  return convert_is_whitespace_char(target);
1129 }
1130 
1138  const exprt &chr, const typet &type)
1139 {
1140  exprt uDC00=from_integer(0xDC00, type);
1141  exprt u0400=from_integer(0x0400, type);
1142  return plus_exprt(uDC00, mod_exprt(chr, u0400));
1143 }
1144 
1149  conversion_inputt &target)
1150 {
1151  return convert_char_function(
1153 }
1154 
1161  const exprt &chr, const typet &type)
1162 {
1163  shl_exprt first_byte(chr, from_integer(8, type));
1164  lshr_exprt second_byte(chr, from_integer(8, type));
1165  return plus_exprt(first_byte, second_byte);
1166 }
1167 
1172  conversion_inputt &target)
1173 {
1174  return convert_char_function(
1176 }
1177 
1187  const exprt &chr, const typet &type)
1188 {
1189  array_typet array_type=to_array_type(type);
1190  const typet &char_type=array_type.subtype();
1191  array_exprt case1(array_type);
1192  array_exprt case2(array_type);
1193  exprt low_surrogate=expr_of_low_surrogate(chr, char_type);
1194  case1.copy_to_operands(low_surrogate);
1195  case2.move_to_operands(low_surrogate);
1196  exprt high_surrogate=expr_of_high_surrogate(chr, char_type);
1197  case2.move_to_operands(high_surrogate);
1198  return if_exprt(expr_of_is_bmp_code_point(chr, type), case1, case2);
1199 }
1200 
1205 {
1206  return convert_char_function(
1208 }
1209 
1214  conversion_inputt &target)
1215 {
1216  const code_function_callt &function_call=target;
1217  assert(function_call.arguments().size()==2);
1218  const exprt &arg0=function_call.arguments()[0];
1219  const exprt &arg1=function_call.arguments()[1];
1220  const exprt &result=function_call.lhs();
1221  const typet &type=result.type();
1222 
1223  // These operations implement the decoding of a unicode symbol encoded
1224  // in UTF16 for the supplementary planes (above U+10000).
1225  // The low ten bits of the first character give the bits 10 to 19 of
1226  // code point and the low ten bits of the second give the bits 0 to 9,
1227  // then 0x10000 is added to the result. For more explenations see:
1228  // https://en.wikipedia.org/wiki/UTF-16
1229 
1230  exprt u010000=from_integer(0x010000, type);
1231  exprt mask10bit=from_integer(0x03FF, type);
1232  shl_exprt m1(bitand_exprt(arg0, mask10bit), from_integer(10, type));
1233  bitand_exprt m2(arg1, mask10bit);
1234  bitor_exprt pair_value(u010000, bitor_exprt(m1, m2));
1235  return code_assignt(result, pair_value);
1236 }
1237 
1247  const exprt &chr, const typet &type)
1248 {
1249  minus_exprt transformed(
1250  plus_exprt(chr, from_integer('a', type)), from_integer('A', type));
1251 
1252  if_exprt res(expr_of_is_ascii_upper_case(chr, type), transformed, chr);
1253  return std::move(res);
1254 }
1255 
1260  conversion_inputt &target)
1261 {
1262  return convert_char_function(
1264 }
1265 
1270  conversion_inputt &target)
1271 {
1272  return convert_to_lower_case_char(target);
1273 }
1274 
1280  const exprt &chr, const typet &type)
1281 {
1282  std::list<mp_integer> increment_list={0x01C4, 0x01C7, 0x01CA, 0x01F1};
1283  std::list<mp_integer> decrement_list={0x01C6, 0x01C9, 0x01CC, 0x01F3};
1284  exprt plus_8_interval1=in_interval_expr(chr, 0x1F80, 0x1F87);
1285  exprt plus_8_interval2=in_interval_expr(chr, 0x1F90, 0x1F97);
1286  exprt plus_8_interval3=in_interval_expr(chr, 0x1FA0, 0x1FA7);
1287  std::list<mp_integer> plus_9_list={0x1FB3, 0x1FC3, 0x1FF3};
1288  minus_exprt minus_1(chr, from_integer(1, type));
1289  plus_exprt plus_1(chr, from_integer(1, type));
1290  plus_exprt plus_8(chr, from_integer(8, type));
1291  plus_exprt plus_9(chr, from_integer(9, type));
1292  or_exprt plus_8_set(
1293  plus_8_interval1, or_exprt(plus_8_interval2, plus_8_interval3));
1294 
1295  if_exprt res(
1296  in_list_expr(chr, increment_list),
1297  plus_1,
1298  if_exprt(
1299  in_list_expr(chr, decrement_list),
1300  minus_1,
1301  if_exprt(
1302  plus_8_set,
1303  plus_8,
1304  if_exprt(
1305  in_list_expr(chr, plus_9_list),
1306  plus_9,
1307  chr))));
1308 
1309  return std::move(res);
1310 }
1311 
1316  conversion_inputt &target)
1317 {
1318  return convert_char_function(
1320 }
1321 
1326  conversion_inputt &target)
1327 {
1328  return convert_to_title_case_char(target);
1329 }
1330 
1340  const exprt &chr, const typet &type)
1341 {
1342  minus_exprt transformed(
1343  plus_exprt(chr, from_integer('A', type)), from_integer('a', type));
1344 
1345  if_exprt res(expr_of_is_ascii_lower_case(chr, type), transformed, chr);
1346  return std::move(res);
1347 }
1348 
1353  conversion_inputt &target)
1354 {
1355  return convert_char_function(
1357 }
1358 
1363  conversion_inputt &target)
1364 {
1365  return convert_to_upper_case_char(target);
1366 }
1367 
1375  const code_function_callt &code) const
1376 {
1377  if(code.function().id()==ID_symbol)
1378  {
1379  const irep_idt &function_id=
1380  to_symbol_expr(code.function()).get_identifier();
1381  auto it=conversion_table.find(function_id);
1382  if(it!=conversion_table.end())
1383  return (it->second)(code);
1384  }
1385 
1386  return code;
1387 }
1388 
1391 {
1392  // All methods are listed here in alphabetic order
1393  // The ones that are not supported by this module (though they may be
1394  // supported by the string solver) have no entry in the conversion
1395  // table and are marked in this way:
1396  // Not supported "java::java.lang.Character.<init>()"
1397 
1398  conversion_table["java::java.lang.Character.charCount:(I)I"]=
1400  conversion_table["java::java.lang.Character.charValue:()C"]=
1402 
1403  // Not supported "java::java.lang.Character.codePointAt:([CI)I
1404  // Not supported "java::java.lang.Character.codePointAt:([CII)I"
1405  // Not supported "java::java.lang.Character.codePointAt:"
1406  // "(Ljava.lang.CharSequence;I)I"
1407  // Not supported "java::java.lang.Character.codePointBefore:([CI)I"
1408  // Not supported "java::java.lang.Character.codePointBefore:([CII)I"
1409  // Not supported "java::java.lang.Character.codePointBefore:"
1410  // "(Ljava.lang.CharSequence;I)I"
1411  // Not supported "java::java.lang.Character.codePointCount:([CII)I"
1412  // Not supported "java::java.lang.Character.codePointCount:"
1413  // "(Ljava.lang.CharSequence;II)I"
1414  // Not supported "java::java.lang.Character.compareTo:"
1415  // "(Ljava.lang.Character;)I"
1416 
1417  conversion_table["java::java.lang.Character.compare:(CC)I"]=
1419  conversion_table["java::java.lang.Character.digit:(CI)I"]=
1421  conversion_table["java::java.lang.Character.digit:(II)I"]=
1423 
1424  // Not supported "java::java.lang.Character.equals:(Ljava.lang.Object;)Z"
1425 
1426  conversion_table["java::java.lang.Character.forDigit:(II)C"]=
1428  conversion_table["java::java.lang.Character.getDirectionality:(C)B"]=
1430  conversion_table["java::java.lang.Character.getDirectionality:(I)B"]=
1432 
1433  // Not supported "java::java.lang.Character.getName:(I)Ljava.lang.String;"
1434 
1435  conversion_table["java::java.lang.Character.getNumericValue:(C)I"]=
1437  conversion_table["java::java.lang.Character.getNumericValue:(I)I"]=
1439  conversion_table["java::java.lang.Character.getType:(C)I"]=
1441  conversion_table["java::java.lang.Character.getType:(I)I"]=
1443  conversion_table["java::java.lang.Character.hashCode:()I"]=
1445  conversion_table["java::java.lang.Character.highSurrogate:(I)C"]=
1447  conversion_table["java::java.lang.Character.isAlphabetic:(I)Z"]=
1449  conversion_table["java::java.lang.Character.isBmpCodePoint:(I)Z"]=
1451  conversion_table["java::java.lang.Character.isDefined:(C)Z"]=
1453  conversion_table["java::java.lang.Character.isDefined:(I)Z"]=
1455  conversion_table["java::java.lang.Character.isDigit:(C)Z"]=
1457  conversion_table["java::java.lang.Character.isDigit:(I)Z"]=
1459  conversion_table["java::java.lang.Character.isHighSurrogate:(C)Z"]=
1461  conversion_table["java::java.lang.Character.isIdentifierIgnorable:(C)Z"]=
1463  conversion_table["java::java.lang.Character.isIdentifierIgnorable:(I)Z"]=
1465  conversion_table["java::java.lang.Character.isIdeographic:(I)Z"]=
1467  conversion_table["java::java.lang.Character.isISOControl:(C)Z"]=
1469  conversion_table["java::java.lang.Character.isISOControl:(I)Z"]=
1471  conversion_table["java::java.lang.Character.isJavaIdentifierPart:(C)Z"]=
1473  conversion_table["java::java.lang.Character.isJavaIdentifierPart:(I)Z"]=
1475  conversion_table["java::java.lang.Character.isJavaIdentifierStart:(C)Z"]=
1477  conversion_table["java::java.lang.Character.isJavaIdentifierStart:(I)Z"]=
1479  conversion_table["java::java.lang.Character.isJavaLetter:(C)Z"]=
1481  conversion_table["java::java.lang.Character.isJavaLetterOrDigit:(C)Z"]=
1483  conversion_table["java::java.lang.Character.isLetter:(C)Z"]=
1485  conversion_table["java::java.lang.Character.isLetter:(I)Z"]=
1487  conversion_table["java::java.lang.Character.isLetterOrDigit:(C)Z"]=
1489  conversion_table["java::java.lang.Character.isLetterOrDigit:(I)Z"]=
1491  conversion_table["java::java.lang.Character.isLowerCase:(C)Z"]=
1493  conversion_table["java::java.lang.Character.isLowerCase:(I)Z"]=
1495  conversion_table["java::java.lang.Character.isLowSurrogate:(C)Z"]=
1497  conversion_table["java::java.lang.Character.isMirrored:(C)Z"]=
1499  conversion_table["java::java.lang.Character.isMirrored:(I)Z"]=
1501  conversion_table["java::java.lang.Character.isSpace:(C)Z"]=
1503  conversion_table["java::java.lang.Character.isSpaceChar:(C)Z"]=
1505  conversion_table["java::java.lang.Character.isSpaceChar:(I)Z"]=
1507  conversion_table["java::java.lang.Character.isSupplementaryCodePoint:(I)Z"]=
1509  conversion_table["java::java.lang.Character.isSurrogate:(C)Z"]=
1511  conversion_table["java::java.lang.Character.isSurrogatePair:(CC)Z"]=
1513  conversion_table["java::java.lang.Character.isTitleCase:(C)Z"]=
1515  conversion_table["java::java.lang.Character.isTitleCase:(I)Z"]=
1517  conversion_table["java::java.lang.Character.isUnicodeIdentifierPart:(C)Z"]=
1519  conversion_table["java::java.lang.Character.isUnicodeIdentifierPart:(I)Z"]=
1521  conversion_table["java::java.lang.Character.isUnicodeIdentifierStart:(C)Z"]=
1523  conversion_table["java::java.lang.Character.isUnicodeIdentifierStart:(I)Z"]=
1525  conversion_table["java::java.lang.Character.isUpperCase:(C)Z"]=
1527  conversion_table["java::java.lang.Character.isUpperCase:(I)Z"]=
1529  conversion_table["java::java.lang.Character.isValidCodePoint:(I)Z"]=
1531  conversion_table["java::java.lang.Character.isWhitespace:(C)Z"]=
1533  conversion_table["java::java.lang.Character.isWhitespace:(I)Z"]=
1535  conversion_table["java::java.lang.Character.lowSurrogate:(I)C"]=
1537 
1538  // Not supported "java::java.lang.Character.offsetByCodePoints:([CIIII)I"
1539  // Not supported "java::java.lang.Character.offsetByCodePoints:"
1540  // "(Ljava.lang.CharacterSequence;II)I"
1541 
1542  conversion_table["java::java.lang.Character.reverseBytes:(C)C"]=
1544  conversion_table["java::java.lang.Character.toChars:(I)[C"]=
1546 
1547  // Not supported "java::java.lang.Character.toChars:(I[CI)I"
1548 
1549  conversion_table["java::java.lang.Character.toCodePoint:(CC)I"]=
1551  conversion_table["java::java.lang.Character.toLowerCase:(C)C"]=
1553  conversion_table["java::java.lang.Character.toLowerCase:(I)I"]=
1555 
1556  // Not supported "java::java.lang.Character.toString:()Ljava.lang.String;"
1557  // Not supported "java::java.lang.Character.toString:(C)Ljava.lang.String;"
1558 
1559  conversion_table["java::java.lang.Character.toTitleCase:(C)C"]=
1561  conversion_table["java::java.lang.Character.toTitleCase:(I)I"]=
1563  conversion_table["java::java.lang.Character.toUpperCase:(C)C"]=
1565  conversion_table["java::java.lang.Character.toUpperCase:(I)I"]=
1567 
1568  // Not supported "java::java.lang.Character.valueOf:(C)Ljava.lang.Character;"
1569 }
The type of an expression, extends irept.
Definition: type.h:27
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:3308
Semantic type conversion.
Definition: std_expr.h:2277
BigInt mp_integer
Definition: mp_arith.h:22
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
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:2531
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)
Copy the given argument to the end of exprt&#39;s operands.
Definition: expr.h:123
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)
Move the given argument to the end of exprt&#39;s operands.
Definition: expr.cpp:29
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:3427
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()
Return the type of the expression.
Definition: expr.h:68
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:1484
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:2702
static exprt is_high_surrogate(const exprt &chr)
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en...
argumentst & arguments()
Definition: std_code.h:1109
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.
Definition: std_expr.h:1211
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:2409
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:2944
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
static codet convert_to_chars(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
codet representation of a function call statement.
Definition: std_code.h:1036
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
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:2984
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:35
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)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:26
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:57
static exprt is_low_surrogate(const exprt &chr)
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en...
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:396
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:1099
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
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:1000
Binary minus.
Definition: std_expr.h:1106
Bit-wise AND.
Definition: std_expr.h:2811
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...
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
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:38
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:1739
Modulo.
Definition: std_expr.h:1287
static codet convert_reverse_bytes(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character...
A codet representing an assignment in the program.
Definition: std_code.h:256
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...