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 
136  conversion_inputt &target)
137 {
138  const code_function_callt &function_call=target;
139  const std::size_t nb_args=function_call.arguments().size();
140  PRECONDITION(nb_args==1 || nb_args==2);
141  const exprt &arg=function_call.arguments()[0];
142  // If there is no radix argument we set it to 36 which is the maximum possible
143  const exprt &radix=
144  nb_args>1?function_call.arguments()[1]:from_integer(36, arg.type());
145  const exprt &result=function_call.lhs();
146  const typet &type=result.type();
147 
148  // TODO: If the radix is not in the range MIN_RADIX <= radix <= MAX_RADIX or
149  // if the value of ch is not a valid digit in the specified radix,
150  // -1 is returned.
151 
152  // Case 1: The method isDigit is true of the character and the Unicode
153  // decimal digit value of the character (or its single-character
154  // decomposition) is less than the specified radix.
155  exprt invalid=from_integer(-1, arg.type());
156  exprt c0=from_integer('0', arg.type());
157  exprt latin_digit=in_interval_expr(arg, '0', '9');
158  minus_exprt value1(arg, c0);
159  // TODO: this is only valid for latin digits
160  if_exprt case1(
161  binary_relation_exprt(value1, ID_lt, radix), value1, invalid);
162 
163  // Case 2: The character is one of the uppercase Latin letters 'A'
164  // through 'Z' and its code is less than radix + 'A' - 10,
165  // then ch - 'A' + 10 is returned.
166  exprt cA=from_integer('A', arg.type());
167  exprt i10=from_integer(10, arg.type());
168  exprt upper_case=in_interval_expr(arg, 'A', 'Z');
169  plus_exprt value2(minus_exprt(arg, cA), i10);
170  if_exprt case2(
171  binary_relation_exprt(value2, ID_lt, radix), value2, invalid);
172 
173  // The character is one of the lowercase Latin letters 'a' through 'z' and
174  // its code is less than radix + 'a' - 10, then ch - 'a' + 10 is returned.
175  exprt ca=from_integer('a', arg.type());
176  exprt lower_case=in_interval_expr(arg, 'a', 'z');
177  plus_exprt value3(minus_exprt(arg, ca), i10);
178  if_exprt case3(
179  binary_relation_exprt(value3, ID_lt, radix), value3, invalid);
180 
181 
182  // The character is one of the fullwidth uppercase Latin letters A ('\uFF21')
183  // through Z ('\uFF3A') and its code is less than radix + '\uFF21' - 10.
184  // In this case, ch - '\uFF21' + 10 is returned.
185  exprt uFF21=from_integer(0xFF21, arg.type());
186  exprt fullwidth_upper_case=in_interval_expr(arg, 0xFF21, 0xFF3A);
187  plus_exprt value4(minus_exprt(arg, uFF21), i10);
188  if_exprt case4(
189  binary_relation_exprt(value4, ID_lt, radix), value4, invalid);
190 
191  // The character is one of the fullwidth lowercase Latin letters a ('\uFF41')
192  // through z ('\uFF5A') and its code is less than radix + '\uFF41' - 10.
193  // In this case, ch - '\uFF41' + 10 is returned.
194  exprt uFF41=from_integer(0xFF41, arg.type());
195  plus_exprt value5(minus_exprt(arg, uFF41), i10);
196  if_exprt case5(
197  binary_relation_exprt(value5, ID_lt, radix), value5, invalid);
198 
199  if_exprt fullwidth_cases(fullwidth_upper_case, case4, case5);
200  if_exprt expr(
201  latin_digit,
202  case1,
203  if_exprt(upper_case, case2, if_exprt(lower_case, case3, fullwidth_cases)));
204  typecast_exprt tc_expr(expr, type);
205 
206  return code_assignt(result, tc_expr);
207 }
208 
213 {
214  return convert_digit_char(target);
215 }
216 
223 {
224  const code_function_callt &function_call=target;
225  assert(function_call.arguments().size()==2);
226  const exprt &digit=function_call.arguments()[0];
227  const exprt &result=function_call.lhs();
228  const typet &type=result.type();
229  typecast_exprt casted_digit(digit, type);
230 
231  exprt d10=from_integer(10, type);
232  binary_relation_exprt small(casted_digit, ID_le, d10);
233  plus_exprt value1(casted_digit, from_integer('0', type));
234  plus_exprt value2(minus_exprt(casted_digit, d10), from_integer('a', type));
235  return code_assignt(result, if_exprt(small, value1, value2));
236 }
237 
242  conversion_inputt &target)
243 {
244  // TODO: This is unimplemented for now as it requires analyzing
245  // the UnicodeData file to find characters directionality.
246  return target;
247 }
248 
253  conversion_inputt &target)
254 {
255  return convert_get_directionality_char(target);
256 }
257 
263  conversion_inputt &target)
264 {
265  return convert_digit_char(target);
266 }
267 
274  conversion_inputt &target)
275 {
276  return convert_digit_int(target);
277 }
278 
283  conversion_inputt &target)
284 {
285  // TODO: This is unimplemented for now as it requires analyzing
286  // the UnicodeData file to categorize characters.
287  return target;
288 }
289 
294  conversion_inputt &target)
295 {
296  return convert_get_type_char(target);
297 }
298 
303 {
304  return convert_char_value(target);
305 }
306 
314  const exprt &chr, const typet &type)
315 {
316  exprt u10000=from_integer(0x010000, type);
317  exprt uD800=from_integer(0xD800, type);
318  exprt u400=from_integer(0x0400, type);
319 
320  plus_exprt high_surrogate(uD800, div_exprt(minus_exprt(chr, u10000), u400));
321  return std::move(high_surrogate);
322 }
323 
329  const exprt &chr, const typet &type)
330 {
331  (void)type; // unused parameter
332  return in_interval_expr(chr, 'a', 'z');
333 }
334 
340  const exprt &chr, const typet &type)
341 {
342  (void)type; // unused parameter
343  return in_interval_expr(chr, 'A', 'Z');
344 }
345 
355  const exprt &chr, const typet &type)
356 {
357  return or_exprt(
358  expr_of_is_ascii_upper_case(chr, type),
359  expr_of_is_ascii_lower_case(chr, type));
360 }
361 
373  const exprt &chr, const typet &type)
374 {
375  return expr_of_is_letter(chr, type);
376 }
377 
382  conversion_inputt &target)
383 {
384  return convert_char_function(
386 }
387 
395  const exprt &chr, const typet &type)
396 {
397  (void)type; // unused parameter
398  return and_exprt(
399  binary_relation_exprt(chr, ID_le, from_integer(0xFFFF, chr.type())),
400  binary_relation_exprt(chr, ID_ge, from_integer(0, chr.type())));
401 }
402 
407  conversion_inputt &target)
408 {
409  return convert_char_function(
411 }
412 
418  const exprt &chr, const typet &type)
419 {
420  (void)type; // unused parameter
421  // The following intervals are undefined in unicode, according to
422  // the Unicode Character Database: http://www.unicode.org/Public/UCD/latest/
423  exprt::operandst intervals;
424  intervals.push_back(in_interval_expr(chr, 0x0750, 0x077F));
425  intervals.push_back(in_interval_expr(chr, 0x07C0, 0x08FF));
426  intervals.push_back(in_interval_expr(chr, 0x1380, 0x139F));
427  intervals.push_back(in_interval_expr(chr, 0x18B0, 0x18FF));
428  intervals.push_back(in_interval_expr(chr, 0x1980, 0x19DF));
429  intervals.push_back(in_interval_expr(chr, 0x1A00, 0x1CFF));
430  intervals.push_back(in_interval_expr(chr, 0x1D80, 0x1DFF));
431  intervals.push_back(in_interval_expr(chr, 0x2C00, 0x2E7F));
432  intervals.push_back(in_interval_expr(chr, 0x2FE0, 0x2FEF));
433  intervals.push_back(in_interval_expr(chr, 0x31C0, 0x31EF));
434  intervals.push_back(in_interval_expr(chr, 0x9FB0, 0x9FFF));
435  intervals.push_back(in_interval_expr(chr, 0xA4D0, 0xABFF));
436  intervals.push_back(in_interval_expr(chr, 0xD7B0, 0xD7FF));
437  intervals.push_back(in_interval_expr(chr, 0xFE10, 0xFE1F));
438  intervals.push_back(in_interval_expr(chr, 0x10140, 0x102FF));
439  intervals.push_back(in_interval_expr(chr, 0x104B0, 0x107FF));
440  intervals.push_back(in_interval_expr(chr, 0x10840, 0x1CFFF));
441  intervals.push_back(in_interval_expr(chr, 0x1D200, 0x1D2FF));
442  intervals.push_back(in_interval_expr(chr, 0x1D360, 0x1D3FF));
443  intervals.push_back(
444  binary_relation_exprt(chr, ID_ge, from_integer(0x1D800, chr.type())));
445 
446  return not_exprt(disjunction(intervals));
447 }
448 
453  conversion_inputt &target)
454 {
455  return convert_char_function(
457 }
458 
463  conversion_inputt &target)
464 {
465  return convert_is_defined_char(target);
466 }
467 
483  const exprt &chr, const typet &type)
484 {
485  (void)type; // unused parameter
486  exprt latin_digit=in_interval_expr(chr, '0', '9');
487  exprt arabic_indic_digit=in_interval_expr(chr, 0x660, 0x669);
488  exprt extended_digit=in_interval_expr(chr, 0x6F0, 0x6F9);
489  exprt devanagari_digit=in_interval_expr(chr, 0x966, 0x96F);
490  exprt fullwidth_digit=in_interval_expr(chr, 0xFF10, 0xFF19);
491  or_exprt digit(
492  or_exprt(latin_digit, or_exprt(arabic_indic_digit, extended_digit)),
493  or_exprt(devanagari_digit, fullwidth_digit));
494  return std::move(digit);
495 }
496 
501  conversion_inputt &target)
502 {
503  return convert_char_function(
505 }
506 
511  conversion_inputt &target)
512 {
513  return convert_is_digit_char(target);
514 }
515 
522  const exprt &chr, const typet &type)
523 {
524  (void)type; // unused parameter
525  return in_interval_expr(chr, 0xD800, 0xDBFF);
526 }
527 
532  conversion_inputt &target)
533 {
534  return convert_char_function(
536 }
537 
547  const exprt &chr, const typet &type)
548 {
549  (void)type; // unused parameter
550  or_exprt ignorable(
551  in_interval_expr(chr, 0x0000, 0x0008),
552  or_exprt(
553  in_interval_expr(chr, 0x000E, 0x001B),
554  in_interval_expr(chr, 0x007F, 0x009F)));
555  return std::move(ignorable);
556 }
557 
564  conversion_inputt &target)
565 {
566  return convert_char_function(
568 }
569 
576  conversion_inputt &target)
577 {
579 }
580 
585  conversion_inputt &target)
586 {
587  const code_function_callt &function_call=target;
588  assert(function_call.arguments().size()==1);
589  const exprt &arg=function_call.arguments()[0];
590  const exprt &result=function_call.lhs();
591  exprt is_ideograph=in_interval_expr(arg, 0x4E00, 0x9FFF);
592  return code_assignt(result, is_ideograph);
593 }
594 
599  conversion_inputt &target)
600 {
601  const code_function_callt &function_call=target;
602  assert(function_call.arguments().size()==1);
603  const exprt &arg=function_call.arguments()[0];
604  const exprt &result=function_call.lhs();
605  or_exprt iso(
606  in_interval_expr(arg, 0x00, 0x1F), in_interval_expr(arg, 0x7F, 0x9F));
607  return code_assignt(result, iso);
608 }
609 
614  conversion_inputt &target)
615 {
616  return convert_is_ISO_control_char(target);
617 }
618 
626  conversion_inputt &target)
627 {
628  return convert_char_function(
630 }
631 
636  conversion_inputt &target)
637 {
639 }
640 
649  conversion_inputt &target)
650 {
651  return convert_char_function(
653 }
654 
659  conversion_inputt &target)
660 {
662 }
663 
668  conversion_inputt &target)
669 {
671 }
672 
677  conversion_inputt &target)
678 {
680 }
681 
686  conversion_inputt &target)
687 {
688  return convert_char_function(
690 }
691 
696  conversion_inputt &target)
697 {
698  return convert_is_letter_char(target);
699 }
700 
706  const exprt &chr, const typet &type)
707 {
708  return or_exprt(expr_of_is_letter(chr, type), expr_of_is_digit(chr, type));
709 }
710 
715  conversion_inputt &target)
716 {
717  return convert_char_function(
719 }
720 
725  conversion_inputt &target)
726 {
727  return convert_is_letter_or_digit_char(target);
728 }
729 
736  conversion_inputt &target)
737 {
738  return convert_char_function(
740 }
741 
748  conversion_inputt &target)
749 {
750  return convert_is_lower_case_char(target);
751 }
752 
757  conversion_inputt &target)
758 {
759  const code_function_callt &function_call=target;
760  assert(function_call.arguments().size()==1);
761  const exprt &arg=function_call.arguments()[0];
762  const exprt &result=function_call.lhs();
763  exprt is_low_surrogate=in_interval_expr(arg, 0xDC00, 0xDFFF);
764  return code_assignt(result, is_low_surrogate);
765 }
766 
775  const exprt &chr, const typet &type)
776 {
777  (void)type; // unused parameter
778  return in_list_expr(chr, {0x28, 0x29, 0x3C, 0x3E, 0x5B, 0x5D, 0x7B, 0x7D});
779 }
780 
787  conversion_inputt &target)
788 {
789  return convert_char_function(
791 }
792 
799  conversion_inputt &target)
800 {
801  return convert_is_mirrored_char(target);
802 }
803 
808 {
809  return convert_is_whitespace_char(target);
810 }
811 
818  const exprt &chr, const typet &type)
819 {
820  (void)type; // unused parameter
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  (void)type; // unused parameter
856  return binary_relation_exprt(chr, ID_gt, from_integer(0xFFFF, chr.type()));
857 }
858 
863  conversion_inputt &target)
864 {
865  return convert_char_function(
867 }
868 
874  const exprt &chr, const typet &type)
875 {
876  (void)type; // unused parameter
877  return in_interval_expr(chr, 0xD800, 0xDFFF);
878 }
879 
884  conversion_inputt &target)
885 {
886  return convert_char_function(
888 }
889 
894  conversion_inputt &target)
895 {
896  const code_function_callt &function_call=target;
897  assert(function_call.arguments().size()==2);
898  const exprt &arg0=function_call.arguments()[0];
899  const exprt &arg1=function_call.arguments()[1];
900  const exprt &result=function_call.lhs();
901  exprt is_low_surrogate=in_interval_expr(arg1, 0xDC00, 0xDFFF);
902  exprt is_high_surrogate=in_interval_expr(arg0, 0xD800, 0xDBFF);
904 }
905 
911  const exprt &chr, const typet &type)
912 {
913  (void)type; // unused parameter
914  std::list<mp_integer>title_case_chars=
915  {0x01C5, 0x01C8, 0x01CB, 0x01F2, 0x1FBC, 0x1FCC, 0x1FFC};
916  exprt::operandst conditions;
917  conditions.push_back(in_list_expr(chr, title_case_chars));
918  conditions.push_back(in_interval_expr(chr, 0x1F88, 0x1F8F));
919  conditions.push_back(in_interval_expr(chr, 0x1F98, 0x1F9F));
920  conditions.push_back(in_interval_expr(chr, 0x1FA8, 0x1FAF));
921  return disjunction(conditions);
922 }
923 
928  conversion_inputt &target)
929 {
930  return convert_char_function(
932 }
933 
938  conversion_inputt &target)
939 {
940  return convert_is_title_case_char(target);
941 }
942 
949  const exprt &chr, const typet &type)
950 {
951  (void)type; // unused parameter
952  // The following set of characters is the general category "Nl" in the
953  // Unicode specification.
954  exprt cond0=in_interval_expr(chr, 0x16EE, 0x16F0);
955  exprt cond1=in_interval_expr(chr, 0x2160, 0x2188);
956  exprt cond2=in_interval_expr(chr, 0x3021, 0x3029);
957  exprt cond3=in_interval_expr(chr, 0x3038, 0x303A);
958  exprt cond4=in_interval_expr(chr, 0xA6E6, 0xA6EF);
959  exprt cond5=in_interval_expr(chr, 0x10140, 0x10174);
960  exprt cond6=in_interval_expr(chr, 0x103D1, 0x103D5);
961  exprt cond7=in_interval_expr(chr, 0x12400, 0x1246E);
962  exprt cond8=in_list_expr(chr, {0x3007, 0x10341, 0x1034A});
963  return or_exprt(
964  or_exprt(or_exprt(cond0, cond1), or_exprt(cond2, cond3)),
965  or_exprt(or_exprt(cond4, cond5), or_exprt(cond6, or_exprt(cond7, cond8))));
966 }
967 
968 
977  const exprt &chr, const typet &type)
978 {
979  exprt::operandst conditions;
980  conditions.push_back(expr_of_is_unicode_identifier_start(chr, type));
981  conditions.push_back(expr_of_is_digit(chr, type));
982  conditions.push_back(expr_of_is_identifier_ignorable(chr, type));
983  return disjunction(conditions);
984 }
985 
990  conversion_inputt &target)
991 {
992  return convert_char_function(
994 }
995 
1000  conversion_inputt &target)
1001 {
1003 }
1004 
1011  const exprt &chr, const typet &type)
1012 {
1013  return or_exprt(
1014  expr_of_is_letter(chr, type), expr_of_is_letter_number(chr, type));
1015 }
1016 
1021  conversion_inputt &target)
1022 {
1023  return convert_char_function(
1025 }
1026 
1031  conversion_inputt &target)
1032 {
1034 }
1035 
1042  conversion_inputt &target)
1043 {
1044  return convert_char_function(
1046 }
1047 
1052  conversion_inputt &target)
1053 {
1054  return convert_is_upper_case_char(target);
1055 }
1056 
1063  const exprt &chr, const typet &type)
1064 {
1065  (void)type; // unused parameter
1066  return binary_relation_exprt(chr, ID_le, from_integer(0x10FFFF, chr.type()));
1067 }
1068 
1073  conversion_inputt &target)
1074 {
1075  return convert_char_function(
1077 }
1078 
1088  const exprt &chr, const typet &type)
1089 {
1090  (void)type; // unused parameter
1091  exprt::operandst conditions;
1092  std::list<mp_integer> space_characters=
1093  {0x20, 0x1680, 0x205F, 0x3000, 0x2028, 0x2029};
1094  conditions.push_back(in_list_expr(chr, space_characters));
1095  conditions.push_back(in_interval_expr(chr, 0x2000, 0x2006));
1096  conditions.push_back(in_interval_expr(chr, 0x2008, 0x200A));
1097  conditions.push_back(in_interval_expr(chr, 0x09, 0x0D));
1098  conditions.push_back(in_interval_expr(chr, 0x1C, 0x1F));
1099  return disjunction(conditions);
1100 }
1101 
1106  conversion_inputt &target)
1107 {
1108  return convert_char_function(
1110 }
1111 
1116  conversion_inputt &target)
1117 {
1118  return convert_is_whitespace_char(target);
1119 }
1120 
1128  const exprt &chr, const typet &type)
1129 {
1130  exprt uDC00=from_integer(0xDC00, type);
1131  exprt u0400=from_integer(0x0400, type);
1132  return plus_exprt(uDC00, mod_exprt(chr, u0400));
1133 }
1134 
1141  const exprt &chr, const typet &type)
1142 {
1143  shl_exprt first_byte(chr, from_integer(8, type));
1144  lshr_exprt second_byte(chr, from_integer(8, type));
1145  return plus_exprt(first_byte, second_byte);
1146 }
1147 
1152  conversion_inputt &target)
1153 {
1154  return convert_char_function(
1156 }
1157 
1167  const exprt &chr, const typet &type)
1168 {
1169  minus_exprt transformed(
1170  plus_exprt(chr, from_integer('a', type)), from_integer('A', type));
1171 
1172  return if_exprt(expr_of_is_ascii_upper_case(chr, type), transformed, chr);
1173 }
1174 
1179  conversion_inputt &target)
1180 {
1181  return convert_char_function(
1183 }
1184 
1189  conversion_inputt &target)
1190 {
1191  return convert_to_lower_case_char(target);
1192 }
1193 
1199  const exprt &chr, const typet &type)
1200 {
1201  std::list<mp_integer> increment_list={0x01C4, 0x01C7, 0x01CA, 0x01F1};
1202  std::list<mp_integer> decrement_list={0x01C6, 0x01C9, 0x01CC, 0x01F3};
1203  exprt plus_8_interval1=in_interval_expr(chr, 0x1F80, 0x1F87);
1204  exprt plus_8_interval2=in_interval_expr(chr, 0x1F90, 0x1F97);
1205  exprt plus_8_interval3=in_interval_expr(chr, 0x1FA0, 0x1FA7);
1206  std::list<mp_integer> plus_9_list={0x1FB3, 0x1FC3, 0x1FF3};
1207  minus_exprt minus_1(chr, from_integer(1, type));
1208  plus_exprt plus_1(chr, from_integer(1, type));
1209  plus_exprt plus_8(chr, from_integer(8, type));
1210  plus_exprt plus_9(chr, from_integer(9, type));
1211  or_exprt plus_8_set(
1212  plus_8_interval1, or_exprt(plus_8_interval2, plus_8_interval3));
1213 
1214  return if_exprt(
1215  in_list_expr(chr, increment_list),
1216  plus_1,
1217  if_exprt(
1218  in_list_expr(chr, decrement_list),
1219  minus_1,
1220  if_exprt(
1221  plus_8_set,
1222  plus_8,
1223  if_exprt(in_list_expr(chr, plus_9_list), plus_9, chr))));
1224 }
1225 
1230  conversion_inputt &target)
1231 {
1232  return convert_char_function(
1234 }
1235 
1240  conversion_inputt &target)
1241 {
1242  return convert_to_title_case_char(target);
1243 }
1244 
1254  const exprt &chr, const typet &type)
1255 {
1256  minus_exprt transformed(
1257  plus_exprt(chr, from_integer('A', type)), from_integer('a', type));
1258 
1259  return if_exprt(expr_of_is_ascii_lower_case(chr, type), transformed, chr);
1260 }
1261 
1266  conversion_inputt &target)
1267 {
1268  return convert_char_function(
1270 }
1271 
1276  conversion_inputt &target)
1277 {
1278  return convert_to_upper_case_char(target);
1279 }
1280 
1288  const code_function_callt &code) const
1289 {
1290  if(code.function().id()==ID_symbol)
1291  {
1292  const irep_idt &function_id=
1294  auto it=conversion_table.find(function_id);
1295  if(it!=conversion_table.end())
1296  return (it->second)(code);
1297  }
1298 
1299  return code;
1300 }
1301 
1304 {
1305  // All methods are listed here in alphabetic order
1306  // The ones that are not supported by this module (though they may be
1307  // supported by the string solver) have no entry in the conversion
1308  // table and are marked in this way:
1309  // Not supported "java::java.lang.Character.<init>()"
1310 
1311  conversion_table["java::java.lang.Character.charCount:(I)I"]=
1313  conversion_table["java::java.lang.Character.charValue:()C"]=
1315 
1316  // Not supported "java::java.lang.Character.codePointAt:([CI)I
1317  // Not supported "java::java.lang.Character.codePointAt:([CII)I"
1318  // Not supported "java::java.lang.Character.codePointAt:"
1319  // "(Ljava.lang.CharSequence;I)I"
1320  // Not supported "java::java.lang.Character.codePointBefore:([CI)I"
1321  // Not supported "java::java.lang.Character.codePointBefore:([CII)I"
1322  // Not supported "java::java.lang.Character.codePointBefore:"
1323  // "(Ljava.lang.CharSequence;I)I"
1324  // Not supported "java::java.lang.Character.codePointCount:([CII)I"
1325  // Not supported "java::java.lang.Character.codePointCount:"
1326  // "(Ljava.lang.CharSequence;II)I"
1327  // Not supported "java::java.lang.Character.compareTo:"
1328  // "(Ljava.lang.Character;)I"
1329 
1330  conversion_table["java::java.lang.Character.compare:(CC)I"]=
1332  conversion_table["java::java.lang.Character.digit:(CI)I"]=
1334  conversion_table["java::java.lang.Character.digit:(II)I"]=
1336 
1337  // Not supported "java::java.lang.Character.equals:(Ljava.lang.Object;)Z"
1338 
1339  conversion_table["java::java.lang.Character.forDigit:(II)C"]=
1341  conversion_table["java::java.lang.Character.getDirectionality:(C)B"]=
1343  conversion_table["java::java.lang.Character.getDirectionality:(I)B"]=
1345 
1346  // Not supported "java::java.lang.Character.getName:(I)Ljava.lang.String;"
1347 
1348  conversion_table["java::java.lang.Character.getNumericValue:(C)I"]=
1350  conversion_table["java::java.lang.Character.getNumericValue:(I)I"]=
1352  conversion_table["java::java.lang.Character.getType:(C)I"]=
1354  conversion_table["java::java.lang.Character.getType:(I)I"]=
1356  conversion_table["java::java.lang.Character.hashCode:()I"]=
1358  conversion_table["java::java.lang.Character.isAlphabetic:(I)Z"]=
1360  conversion_table["java::java.lang.Character.isBmpCodePoint:(I)Z"]=
1362  conversion_table["java::java.lang.Character.isDefined:(C)Z"]=
1364  conversion_table["java::java.lang.Character.isDefined:(I)Z"]=
1366  conversion_table["java::java.lang.Character.isDigit:(C)Z"]=
1368  conversion_table["java::java.lang.Character.isDigit:(I)Z"]=
1370  conversion_table["java::java.lang.Character.isHighSurrogate:(C)Z"]=
1372  conversion_table["java::java.lang.Character.isIdentifierIgnorable:(C)Z"]=
1374  conversion_table["java::java.lang.Character.isIdentifierIgnorable:(I)Z"]=
1376  conversion_table["java::java.lang.Character.isIdeographic:(I)Z"]=
1378  conversion_table["java::java.lang.Character.isISOControl:(C)Z"]=
1380  conversion_table["java::java.lang.Character.isISOControl:(I)Z"]=
1382  conversion_table["java::java.lang.Character.isJavaIdentifierPart:(C)Z"]=
1384  conversion_table["java::java.lang.Character.isJavaIdentifierPart:(I)Z"]=
1386  conversion_table["java::java.lang.Character.isJavaIdentifierStart:(C)Z"]=
1388  conversion_table["java::java.lang.Character.isJavaIdentifierStart:(I)Z"]=
1390  conversion_table["java::java.lang.Character.isJavaLetter:(C)Z"]=
1392  conversion_table["java::java.lang.Character.isJavaLetterOrDigit:(C)Z"]=
1394  conversion_table["java::java.lang.Character.isLetter:(C)Z"]=
1396  conversion_table["java::java.lang.Character.isLetter:(I)Z"]=
1398  conversion_table["java::java.lang.Character.isLetterOrDigit:(C)Z"]=
1400  conversion_table["java::java.lang.Character.isLetterOrDigit:(I)Z"]=
1402  conversion_table["java::java.lang.Character.isLowerCase:(C)Z"]=
1404  conversion_table["java::java.lang.Character.isLowerCase:(I)Z"]=
1406  conversion_table["java::java.lang.Character.isLowSurrogate:(C)Z"]=
1408  conversion_table["java::java.lang.Character.isMirrored:(C)Z"]=
1410  conversion_table["java::java.lang.Character.isMirrored:(I)Z"]=
1412  conversion_table["java::java.lang.Character.isSpace:(C)Z"]=
1414  conversion_table["java::java.lang.Character.isSpaceChar:(C)Z"]=
1416  conversion_table["java::java.lang.Character.isSpaceChar:(I)Z"]=
1418  conversion_table["java::java.lang.Character.isSupplementaryCodePoint:(I)Z"]=
1420  conversion_table["java::java.lang.Character.isSurrogate:(C)Z"]=
1422  conversion_table["java::java.lang.Character.isSurrogatePair:(CC)Z"]=
1424  conversion_table["java::java.lang.Character.isTitleCase:(C)Z"]=
1426  conversion_table["java::java.lang.Character.isTitleCase:(I)Z"]=
1428  conversion_table["java::java.lang.Character.isUnicodeIdentifierPart:(C)Z"]=
1430  conversion_table["java::java.lang.Character.isUnicodeIdentifierPart:(I)Z"]=
1432  conversion_table["java::java.lang.Character.isUnicodeIdentifierStart:(C)Z"]=
1434  conversion_table["java::java.lang.Character.isUnicodeIdentifierStart:(I)Z"]=
1436  conversion_table["java::java.lang.Character.isUpperCase:(C)Z"]=
1438  conversion_table["java::java.lang.Character.isUpperCase:(I)Z"]=
1440  conversion_table["java::java.lang.Character.isValidCodePoint:(I)Z"]=
1442  conversion_table["java::java.lang.Character.isWhitespace:(C)Z"]=
1444  conversion_table["java::java.lang.Character.isWhitespace:(I)Z"]=
1446 
1447  // Not supported "java::java.lang.Character.offsetByCodePoints:([CIIII)I"
1448  // Not supported "java::java.lang.Character.offsetByCodePoints:"
1449  // "(Ljava.lang.CharacterSequence;II)I"
1450 
1451  conversion_table["java::java.lang.Character.reverseBytes:(C)C"]=
1453 
1454  // Not supported "java::java.lang.Character.toChars:(I[CI)I"
1455 
1456  conversion_table["java::java.lang.Character.toLowerCase:(C)C"]=
1458  conversion_table["java::java.lang.Character.toLowerCase:(I)I"]=
1460 
1461  // Not supported "java::java.lang.Character.toString:()Ljava.lang.String;"
1462  // Not supported "java::java.lang.Character.toString:(C)Ljava.lang.String;"
1463 
1464  conversion_table["java::java.lang.Character.toTitleCase:(C)C"]=
1466  conversion_table["java::java.lang.Character.toTitleCase:(I)I"]=
1468  conversion_table["java::java.lang.Character.toUpperCase:(C)C"]=
1470  conversion_table["java::java.lang.Character.toUpperCase:(I)I"]=
1472 
1473  // Not supported "java::java.lang.Character.valueOf:(C)Ljava.lang.Character;"
1474 }
character_refine_preprocesst::convert_is_letter_or_digit_int
static codet convert_is_letter_or_digit_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:724
character_refine_preprocesst::expr_of_high_surrogate
static exprt expr_of_high_surrogate(const exprt &chr, const typet &type)
Returns the leading surrogate (a high surrogate code unit) of the surrogate pair representing the spe...
Definition: character_refine_preprocess.cpp:313
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
character_refine_preprocesst::convert_is_unicode_identifier_start_char
static codet convert_is_unicode_identifier_start_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1020
character_refine_preprocesst::expr_of_char_value
static exprt expr_of_char_value(const exprt &chr, const typet &type)
Casts the given expression to the given type.
Definition: character_refine_preprocess.cpp:91
character_refine_preprocesst::convert_is_digit_int
static codet convert_is_digit_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:510
character_refine_preprocesst::convert_compare
static codet convert_compare(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:110
character_refine_preprocesst::expr_of_is_supplementary_code_point
static exprt expr_of_is_supplementary_code_point(const exprt &chr, const typet &type)
Determines whether the specified character (Unicode code point) is in the supplementary character ran...
Definition: character_refine_preprocess.cpp:852
character_refine_preprocesst::convert_to_lower_case_char
static codet convert_to_lower_case_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1178
character_refine_preprocesst::convert_char_value
static codet convert_char_value(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:100
character_refine_preprocesst::convert_is_ISO_control_char
static codet convert_is_ISO_control_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:598
arith_tools.h
character_refine_preprocesst::convert_is_lower_case_int
static codet convert_is_lower_case_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:747
character_refine_preprocesst::convert_digit_int
static codet convert_digit_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:212
character_refine_preprocesst::convert_reverse_bytes
static codet convert_reverse_bytes(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1151
character_refine_preprocesst::convert_is_surrogate_pair
static codet convert_is_surrogate_pair(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:893
character_refine_preprocesst::convert_is_whitespace_int
static codet convert_is_whitespace_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1115
character_refine_preprocess.h
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
typet
The type of an expression, extends irept.
Definition: type.h:29
character_refine_preprocesst::convert_is_alphabetic
static codet convert_is_alphabetic(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:381
character_refine_preprocesst::expr_of_low_surrogate
static exprt expr_of_low_surrogate(const exprt &chr, const typet &type)
Returns the trailing surrogate (a low surrogate code unit) of the surrogate pair representing the spe...
Definition: character_refine_preprocess.cpp:1127
character_refine_preprocesst::expr_of_reverse_bytes
static exprt expr_of_reverse_bytes(const exprt &chr, const typet &type)
Returns the value obtained by reversing the order of the bytes in the specified char value.
Definition: character_refine_preprocess.cpp:1140
character_refine_preprocesst::convert_hash_code
static codet convert_hash_code(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:302
character_refine_preprocesst::convert_is_upper_case_char
static codet convert_is_upper_case_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1041
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
character_refine_preprocesst::expr_of_is_mirrored
static exprt expr_of_is_mirrored(const exprt &chr, const typet &type)
Determines whether the character is mirrored according to the Unicode specification.
Definition: character_refine_preprocess.cpp:774
character_refine_preprocesst::convert_is_unicode_identifier_part_int
static codet convert_is_unicode_identifier_part_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:999
and_exprt
Boolean AND.
Definition: std_expr.h:2137
character_refine_preprocesst::expr_of_is_identifier_ignorable
static exprt expr_of_is_identifier_ignorable(const exprt &chr, const typet &type)
Determines if the character is one of ignorable in a Java identifier, that is, it is in one of these ...
Definition: character_refine_preprocess.cpp:546
character_refine_preprocesst::convert_is_defined_char
static codet convert_is_defined_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:452
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
character_refine_preprocesst::expr_of_is_letter_number
static exprt expr_of_is_letter_number(const exprt &chr, const typet &type)
Determines if the specified character is in the LETTER_NUMBER category of Unicode.
Definition: character_refine_preprocess.cpp:948
is_low_surrogate
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....
Definition: string_constraint_generator_code_points.cpp:91
exprt
Base class for all expressions.
Definition: expr.h:53
character_refine_preprocesst::convert_to_upper_case_int
static codet convert_to_upper_case_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1275
character_refine_preprocesst::convert_is_lower_case_char
static codet convert_is_lower_case_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:735
character_refine_preprocesst::convert_is_whitespace_char
static codet convert_is_whitespace_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1105
character_refine_preprocesst::expr_of_is_surrogate
static exprt expr_of_is_surrogate(const exprt &chr, const typet &type)
Determines if the given char value is a Unicode surrogate code unit.
Definition: character_refine_preprocess.cpp:873
character_refine_preprocesst::convert_is_letter_or_digit_char
static codet convert_is_letter_or_digit_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:714
character_refine_preprocesst::convert_is_title_case_char
static codet convert_is_title_case_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:927
character_refine_preprocesst::expr_of_is_valid_code_point
static exprt expr_of_is_valid_code_point(const exprt &chr, const typet &type)
Determines whether the specified code point is a valid Unicode code point value.
Definition: character_refine_preprocess.cpp:1062
character_refine_preprocesst::convert_is_mirrored_char
static codet convert_is_mirrored_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:786
lshr_exprt
Logical right shift.
Definition: std_expr.h:2614
character_refine_preprocesst::expr_of_is_bmp_code_point
static exprt expr_of_is_bmp_code_point(const exprt &chr, const typet &type)
Determines whether the specified character (Unicode code point) is in the Basic Multilingual Plane (B...
Definition: character_refine_preprocess.cpp:394
character_refine_preprocesst::convert_is_unicode_identifier_start_int
static codet convert_is_unicode_identifier_start_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1030
character_refine_preprocesst::convert_is_valid_code_point
static codet convert_is_valid_code_point(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1072
div_exprt
Division.
Definition: std_expr.h:1031
character_refine_preprocesst::expr_of_is_digit
static exprt expr_of_is_digit(const exprt &chr, const typet &type)
Determines if the specified character is a digit.
Definition: character_refine_preprocess.cpp:482
character_refine_preprocesst::convert_is_surrogate
static codet convert_is_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:883
equal_exprt
Equality.
Definition: std_expr.h:1190
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
character_refine_preprocesst::convert_is_java_identifier_start_char
static codet convert_is_java_identifier_start_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaIdent...
Definition: character_refine_preprocess.cpp:648
character_refine_preprocesst::convert_get_directionality_int
static codet convert_get_directionality_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:252
character_refine_preprocesst::conversion_table
std::unordered_map< irep_idt, conversion_functiont > conversion_table
Definition: character_refine_preprocess.h:38
character_refine_preprocesst::convert_is_space
static codet convert_is_space(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:807
character_refine_preprocesst::expr_of_is_title_case
static exprt expr_of_is_title_case(const exprt &chr, const typet &type)
Determines if the specified character is a titlecase character.
Definition: character_refine_preprocess.cpp:910
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
character_refine_preprocesst::convert_for_digit
static codet convert_for_digit(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:222
character_refine_preprocesst::expr_of_is_letter_or_digit
static exprt expr_of_is_letter_or_digit(const exprt &chr, const typet &type)
Determines if the specified character is a letter or digit.
Definition: character_refine_preprocess.cpp:705
character_refine_preprocesst::convert_is_upper_case_int
static codet convert_is_upper_case_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1051
character_refine_preprocesst::expr_of_to_lower_case
static exprt expr_of_to_lower_case(const exprt &chr, const typet &type)
Converts the character argument to lowercase.
Definition: character_refine_preprocess.cpp:1166
character_refine_preprocesst::expr_of_is_high_surrogate
static exprt expr_of_is_high_surrogate(const exprt &chr, const typet &type)
Determines if the given char value is a Unicode high-surrogate code unit (also known as leading-surro...
Definition: character_refine_preprocess.cpp:521
character_refine_preprocesst::convert_get_type_char
static codet convert_get_type_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:282
disjunction
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:29
character_refine_preprocesst::expr_of_is_alphabetic
static exprt expr_of_is_alphabetic(const exprt &chr, const typet &type)
Determines if the specified character (Unicode code point) is alphabetic.
Definition: character_refine_preprocess.cpp:372
is_high_surrogate
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....
Definition: string_constraint_generator_code_points.cpp:78
or_exprt
Boolean OR.
Definition: std_expr.h:2245
character_refine_preprocesst::convert_get_directionality_char
static codet convert_get_directionality_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:241
character_refine_preprocesst::expr_of_to_upper_case
static exprt expr_of_to_upper_case(const exprt &chr, const typet &type)
Converts the character argument to uppercase.
Definition: character_refine_preprocess.cpp:1253
character_refine_preprocesst::convert_is_space_char
static codet convert_is_space_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:831
character_refine_preprocesst::expr_of_to_title_case
static exprt expr_of_to_title_case(const exprt &chr, const typet &type)
Converts the character argument to titlecase.
Definition: character_refine_preprocess.cpp:1198
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
character_refine_preprocesst::convert_is_defined_int
static codet convert_is_defined_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:462
character_refine_preprocesst::convert_is_high_surrogate
static codet convert_is_high_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:531
character_refine_preprocesst::in_interval_expr
static exprt in_interval_expr(const exprt &chr, const mp_integer &lower_bound, const mp_integer &upper_bound)
The returned expression is true when the first argument is in the interval defined by the lower and u...
Definition: character_refine_preprocess.cpp:42
character_refine_preprocesst::convert_get_numeric_value_char
static codet convert_get_numeric_value_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:262
character_refine_preprocesst::convert_to_lower_case_int
static codet convert_to_lower_case_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1188
character_refine_preprocesst::convert_is_space_char_int
static codet convert_is_space_char_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:841
character_refine_preprocesst::convert_is_letter_int
static codet convert_is_letter_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:695
character_refine_preprocesst::convert_is_bmp_code_point
static codet convert_is_bmp_code_point(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:406
character_refine_preprocesst::in_list_expr
static exprt in_list_expr(const exprt &chr, const std::list< mp_integer > &list)
The returned expression is true when the given character is equal to one of the element in the list.
Definition: character_refine_preprocess.cpp:57
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
character_refine_preprocesst::convert_is_java_identifier_part_char
static codet convert_is_java_identifier_part_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:625
irept::id
const irep_idt & id() const
Definition: irep.h:418
character_refine_preprocesst::convert_is_low_surrogate
static codet convert_is_low_surrogate(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:756
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
character_refine_preprocesst::expr_of_is_unicode_identifier_start
static exprt expr_of_is_unicode_identifier_start(const exprt &chr, const typet &type)
Determines if the specified character is permissible as the first character in a Unicode identifier.
Definition: character_refine_preprocess.cpp:1010
character_refine_preprocesst::expr_of_is_defined
static exprt expr_of_is_defined(const exprt &chr, const typet &type)
Determines if a character is defined in Unicode.
Definition: character_refine_preprocess.cpp:417
character_refine_preprocesst::convert_digit_char
static codet convert_digit_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:135
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
character_refine_preprocesst::convert_is_letter_char
static codet convert_is_letter_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:685
character_refine_preprocesst::convert_is_mirrored_int
static codet convert_is_mirrored_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:798
character_refine_preprocesst::expr_of_is_space_char
static exprt expr_of_is_space_char(const exprt &chr, const typet &type)
Determines if the specified character is white space according to Unicode (SPACE_SEPARATOR,...
Definition: character_refine_preprocess.cpp:817
minus_exprt
Binary minus.
Definition: std_expr.h:940
character_refine_preprocesst::convert_to_title_case_char
static codet convert_to_title_case_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1229
character_refine_preprocesst::expr_of_is_ascii_lower_case
static exprt expr_of_is_ascii_lower_case(const exprt &chr, const typet &type)
Determines if the specified character is an ASCII lowercase character.
Definition: character_refine_preprocess.cpp:328
character_refine_preprocesst::convert_get_numeric_value_int
static codet convert_get_numeric_value_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:273
character_refine_preprocesst::expr_of_is_letter
static exprt expr_of_is_letter(const exprt &chr, const typet &type)
Determines if the specified character is a letter.
Definition: character_refine_preprocess.cpp:354
character_refine_preprocesst::convert_char_count
static codet convert_char_count(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:82
character_refine_preprocesst::convert_get_type_int
static codet convert_get_type_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:293
character_refine_preprocesst::convert_is_ISO_control_int
static codet convert_is_ISO_control_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:613
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
character_refine_preprocesst::convert_char_function
static codet convert_char_function(exprt(*expr_function)(const exprt &chr, const typet &type), conversion_inputt &target)
converts based on a function on expressions
Definition: character_refine_preprocess.cpp:24
character_refine_preprocesst::expr_of_is_whitespace
static exprt expr_of_is_whitespace(const exprt &chr, const typet &type)
Determines if the specified character is white space according to Java.
Definition: character_refine_preprocess.cpp:1087
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
character_refine_preprocesst::convert_is_java_letter
static codet convert_is_java_letter(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:667
character_refine_preprocesst::convert_is_identifier_ignorable_char
static codet convert_is_identifier_ignorable_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:563
character_refine_preprocesst::convert_is_java_identifier_start_int
static codet convert_is_java_identifier_start_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaIdent...
Definition: character_refine_preprocess.cpp:658
character_refine_preprocesst::convert_is_title_case_int
static codet convert_is_title_case_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:937
character_refine_preprocesst::expr_of_is_ascii_upper_case
static exprt expr_of_is_ascii_upper_case(const exprt &chr, const typet &type)
Determines if the specified character is an ASCII uppercase character.
Definition: character_refine_preprocess.cpp:339
character_refine_preprocesst::convert_is_digit_char
static codet convert_is_digit_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:500
character_refine_preprocesst::convert_is_java_identifier_part_int
static codet convert_is_java_identifier_part_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaIdent...
Definition: character_refine_preprocess.cpp:635
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
character_refine_preprocesst::replace_character_call
codet replace_character_call(const code_function_callt &call) const
replace function calls to functions of the Character by an affectation if possible,...
Definition: character_refine_preprocess.cpp:1287
character_refine_preprocesst::expr_of_is_unicode_identifier_part
static exprt expr_of_is_unicode_identifier_part(const exprt &chr, const typet &type)
Determines if the character may be part of a Unicode identifier.
Definition: character_refine_preprocess.cpp:976
std_expr.h
API to expression classes.
character_refine_preprocesst::convert_to_title_case_int
static codet convert_to_title_case_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1239
character_refine_preprocesst::convert_is_unicode_identifier_part_char
static codet convert_is_unicode_identifier_part_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:989
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
character_refine_preprocesst::convert_is_java_letter_or_digit
static codet convert_is_java_letter_or_digit(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method isJavaLette...
Definition: character_refine_preprocess.cpp:676
character_refine_preprocesst::expr_of_char_count
static exprt expr_of_char_count(const exprt &chr, const typet &type)
Determines the number of char values needed to represent the specified character (Unicode code point)...
Definition: character_refine_preprocess.cpp:71
mod_exprt
Modulo.
Definition: std_expr.h:1100
character_refine_preprocesst::convert_is_supplementary_code_point
static codet convert_is_supplementary_code_point(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:862
shl_exprt
Left shift.
Definition: std_expr.h:2561
character_refine_preprocesst::initialize_conversion_table
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
Definition: character_refine_preprocess.cpp:1303
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
not_exprt
Boolean negation.
Definition: std_expr.h:2843
character_refine_preprocesst::convert_is_ideographic
static codet convert_is_ideographic(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:584
character_refine_preprocesst::convert_to_upper_case_char
static codet convert_to_upper_case_char(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:1265
character_refine_preprocesst::convert_is_identifier_ignorable_int
static codet convert_is_identifier_ignorable_int(conversion_inputt &target)
Converts function call to an assignment of an expression corresponding to the java method Character....
Definition: character_refine_preprocess.cpp:575