cprover
java_types.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
10 #define CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
11 
12 #include <util/invariant.h>
13 #include <algorithm>
14 #include <set>
15 
16 #include <util/c_types.h>
17 #include <util/narrow.h>
18 #include <util/optional.h>
19 #include <util/std_expr.h>
20 #include <util/std_types.h>
21 #include <util/type.h>
22 
23 class java_annotationt : public irept
24 {
25 public:
26  class valuet : public irept
27  {
28  public:
29  valuet(irep_idt name, const exprt &value) : irept(name)
30  {
31  get_sub().push_back(value);
32  }
33 
34  const irep_idt &get_name() const
35  {
36  return id();
37  }
38 
39  const exprt &get_value() const
40  {
41  return static_cast<const exprt &>(get_sub().front());
42  }
43  };
44 
45  explicit java_annotationt(const typet &type)
46  {
47  set(ID_type, type);
48  }
49 
50  const typet &get_type() const
51  {
52  return static_cast<const typet &>(find(ID_type));
53  }
54 
55  const std::vector<valuet> &get_values() const
56  {
57  // This cast should be safe as valuet doesn't add data to irept
58  return reinterpret_cast<const std::vector<valuet> &>(get_sub());
59  }
60 
61  std::vector<valuet> &get_values()
62  {
63  // This cast should be safe as valuet doesn't add data to irept
64  return reinterpret_cast<std::vector<valuet> &>(get_sub());
65  }
66 };
67 
68 class annotated_typet : public typet
69 {
70 public:
71  const std::vector<java_annotationt> &get_annotations() const
72  {
73  // This cast should be safe as java_annotationt doesn't add data to irept
74  return reinterpret_cast<const std::vector<java_annotationt> &>(
75  find(ID_C_annotations).get_sub());
76  }
77 
78  std::vector<java_annotationt> &get_annotations()
79  {
80  // This cast should be safe as java_annotationt doesn't add data to irept
81  return reinterpret_cast<std::vector<java_annotationt> &>(
82  add(ID_C_annotations).get_sub());
83  }
84 };
85 
86 inline const annotated_typet &to_annotated_type(const typet &type)
87 {
88  return static_cast<const annotated_typet &>(type);
89 }
90 
92 {
93  return static_cast<annotated_typet &>(type);
94 }
95 
96 template <>
98 {
99  return true;
100 }
101 
103 {
104 public:
107 
111  java_method_typet(parameterst &&_parameters, typet &&_return_type)
112  : code_typet(std::move(_parameters), std::move(_return_type))
113  {
114  set(ID_C_java_method_type, true);
115  }
116 
120  java_method_typet(parameterst &&_parameters, const typet &_return_type)
121  : code_typet(std::move(_parameters), _return_type)
122  {
123  set(ID_C_java_method_type, true);
124  }
125 
126  const std::vector<irep_idt> throws_exceptions() const
127  {
128  std::vector<irep_idt> exceptions;
129  for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
130  exceptions.push_back(e.id());
131  return exceptions;
132  }
133 
135  {
136  add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
137  }
138 
139  bool get_is_final() const
140  {
141  return get_bool(ID_final);
142  }
143 
144  void set_is_final(bool is_final)
145  {
146  set(ID_final, is_final);
147  }
148 
149  bool get_native() const
150  {
151  return get_bool(ID_is_native_method);
152  }
153 
154  void set_native(bool is_native)
155  {
156  set(ID_is_native_method, is_native);
157  }
158 
159  bool get_is_varargs() const
160  {
161  return get_bool(ID_is_varargs_method);
162  }
163 
164  void set_is_varargs(bool is_varargs)
165  {
166  set(ID_is_varargs_method, is_varargs);
167  }
168 
169  bool is_synthetic() const
170  {
171  return get_bool(ID_synthetic);
172  }
173 
175  {
176  set(ID_synthetic, is_synthetic);
177  }
178 };
179 
180 template <>
181 inline bool can_cast_type<java_method_typet>(const typet &type)
182 {
183  return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
184 }
185 
186 inline const java_method_typet &to_java_method_type(const typet &type)
187 {
189  return static_cast<const java_method_typet &>(type);
190 }
191 
193 {
195  return static_cast<java_method_typet &>(type);
196 }
197 
199 {
200 public:
201  class componentt : public class_typet::componentt
202  {
203  public:
204  componentt() = default;
205 
206  componentt(const irep_idt &_name, typet _type)
207  : class_typet::componentt(_name, std::move(_type))
208  {
209  }
210 
212  bool get_is_final() const
213  {
214  return get_bool(ID_final);
215  }
216 
218  void set_is_final(const bool is_final)
219  {
220  set(ID_final, is_final);
221  }
222  };
223 
224  using componentst = std::vector<componentt>;
225 
226  const componentst &components() const
227  {
228  return (const componentst &)(find(ID_components).get_sub());
229  }
230 
232  {
233  return (componentst &)(add(ID_components).get_sub());
234  }
235 
236  const componentt &get_component(const irep_idt &component_name) const
237  {
238  return static_cast<const componentt &>(
239  class_typet::get_component(component_name));
240  }
241 
243  {
244  public:
245  methodt() = delete;
246 
247  methodt(const irep_idt &_name, java_method_typet _type)
248  : class_typet::methodt(_name, std::move(_type))
249  {
250  }
251 
252  const java_method_typet &type() const
253  {
254  return static_cast<const java_method_typet &>(
256  }
257 
259  {
260  return static_cast<java_method_typet &>(class_typet::methodt::type());
261  }
262 
264  bool get_is_final() const
265  {
266  return get_bool(ID_final);
267  }
268 
270  void set_is_final(const bool is_final)
271  {
272  set(ID_final, is_final);
273  }
274 
276  bool get_is_native() const
277  {
278  return get_bool(ID_is_native_method);
279  }
280 
282  void set_is_native(const bool is_native)
283  {
284  set(ID_is_native_method, is_native);
285  }
286 
288  const irep_idt &get_descriptor() const
289  {
290  return get(ID_object_descriptor);
291  }
292 
294  void set_descriptor(const irep_idt &id)
295  {
296  set(ID_object_descriptor, id);
297  }
298  };
299 
300  using methodst = std::vector<methodt>;
301 
302  const methodst &methods() const
303  {
304  return (const methodst &)(find(ID_methods).get_sub());
305  }
306 
308  {
309  return (methodst &)(add(ID_methods).get_sub());
310  }
311 
313  using static_memberst = std::vector<componentt>;
314 
316  {
318  }
319 
321  {
323  }
324 
325  const irep_idt &get_access() const
326  {
327  return get(ID_access);
328  }
329 
330  void set_access(const irep_idt &access)
331  {
332  return set(ID_access, access);
333  }
334 
335  bool get_is_inner_class() const
336  {
337  return get_bool(ID_is_inner_class);
338  }
339 
340  void set_is_inner_class(const bool &is_inner_class)
341  {
342  return set(ID_is_inner_class, is_inner_class);
343  }
344 
345  const irep_idt &get_outer_class() const
346  {
347  return get(ID_outer_class);
348  }
349 
350  void set_outer_class(const irep_idt &outer_class)
351  {
352  return set(ID_outer_class, outer_class);
353  }
354 
355  const irep_idt &get_super_class() const
356  {
357  return get(ID_super_class);
358  }
359 
360  void set_super_class(const irep_idt &super_class)
361  {
362  return set(ID_super_class, super_class);
363  }
364 
365  bool get_is_static_class() const
366  {
367  return get_bool(ID_is_static);
368  }
369 
370  void set_is_static_class(const bool &is_static_class)
371  {
372  return set(ID_is_static, is_static_class);
373  }
374 
376  {
377  return get_bool(ID_is_anonymous);
378  }
379 
380  void set_is_anonymous_class(const bool &is_anonymous_class)
381  {
382  return set(ID_is_anonymous, is_anonymous_class);
383  }
384 
385  bool get_final() const
386  {
387  return get_bool(ID_final);
388  }
389 
390  void set_final(bool is_final)
391  {
392  set(ID_final, is_final);
393  }
394 
395  void set_is_stub(bool is_stub)
396  {
397  set(ID_incomplete_class, is_stub);
398  }
399 
400  bool get_is_stub() const
401  {
402  return get_bool(ID_incomplete_class);
403  }
404 
406  bool get_is_enumeration() const
407  {
408  return get_bool(ID_enumeration);
409  }
410 
412  void set_is_enumeration(const bool is_enumeration)
413  {
414  set(ID_enumeration, is_enumeration);
415  }
416 
418  bool get_abstract() const
419  {
420  return get_bool(ID_abstract);
421  }
422 
424  void set_abstract(bool abstract)
425  {
426  set(ID_abstract, abstract);
427  }
428 
430  bool get_synthetic() const
431  {
432  return get_bool(ID_synthetic);
433  }
434 
436  void set_synthetic(bool synthetic)
437  {
438  set(ID_synthetic, synthetic);
439  }
440 
442  bool get_is_annotation() const
443  {
444  return get_bool(ID_is_annotation);
445  }
446 
448  void set_is_annotation(bool is_annotation)
449  {
450  set(ID_is_annotation, is_annotation);
451  }
452 
454  bool get_interface() const
455  {
456  return get_bool(ID_interface);
457  }
458 
460  void set_interface(bool interface)
461  {
462  set(ID_interface, interface);
463  }
464 
467  {
476  };
477 
484  {
485  public:
487  const class_method_descriptor_exprt &method_descriptor,
488  method_handle_kindt handle_kind)
489  {
490  set(ID_object_descriptor, method_descriptor);
491  set(ID_handle_type, static_cast<int>(handle_kind));
492  }
493 
495  {
496  set(
497  ID_handle_type, static_cast<int>(method_handle_kindt::UNKNOWN_HANDLE));
498  }
499 
501  {
502  return static_cast<const class_method_descriptor_exprt &>(
503  find(ID_object_descriptor));
504  }
505 
507  {
509  }
510 
512  {
513  return (method_handle_kindt)get_int(ID_handle_type);
514  }
515  };
516 
517  using java_lambda_method_handlest = std::vector<java_lambda_method_handlet>;
518 
520  {
521  return (const java_lambda_method_handlest &)find(
522  ID_java_lambda_method_handles)
523  .get_sub();
524  }
525 
527  {
528  return (java_lambda_method_handlest &)add(ID_java_lambda_method_handles)
529  .get_sub();
530  }
531 
533  const class_method_descriptor_exprt &method_descriptor,
534  method_handle_kindt handle_kind)
535  {
536  // creates a symbol_exprt for the identifier and pushes it in the vector
537  lambda_method_handles().emplace_back(method_descriptor, handle_kind);
538  }
540  {
541  // creates empty symbol_exprt and pushes it in the vector
542  lambda_method_handles().emplace_back();
543  }
544 
545  const std::vector<java_annotationt> &get_annotations() const
546  {
547  return static_cast<const annotated_typet &>(
548  static_cast<const typet &>(*this)).get_annotations();
549  }
550 
551  std::vector<java_annotationt> &get_annotations()
552  {
553  return type_checked_cast<annotated_typet>(
554  static_cast<typet &>(*this)).get_annotations();
555  }
556 
559  const irep_idt &get_name() const
560  {
561  return get(ID_name);
562  }
563 
566  void set_name(const irep_idt &name)
567  {
568  set(ID_name, name);
569  }
570 
572  const irep_idt &get_inner_name() const
573  {
574  return get(ID_inner_name);
575  }
576 
578  void set_inner_name(const irep_idt &name)
579  {
580  set(ID_inner_name, name);
581  }
582 };
583 
584 inline const java_class_typet &to_java_class_type(const typet &type)
585 {
586  assert(type.id()==ID_struct);
587  return static_cast<const java_class_typet &>(type);
588 }
589 
591 {
592  assert(type.id()==ID_struct);
593  return static_cast<java_class_typet &>(type);
594 }
595 
596 template <>
597 inline bool can_cast_type<java_class_typet>(const typet &type)
598 {
599  return can_cast_type<class_typet>(type);
600 }
601 
605 {
606 public:
608  const struct_tag_typet &_subtype,
609  std::size_t _width)
610  : reference_typet(_subtype, _width)
611  {
612  }
613 
615  {
616  return static_cast<struct_tag_typet &>(reference_typet::subtype());
617  }
618 
619  const struct_tag_typet &subtype() const
620  {
621  return static_cast<const struct_tag_typet &>(reference_typet::subtype());
622  }
623 };
624 
625 template <>
627 {
628  return type.id() == ID_pointer &&
629  to_type_with_subtype(type).subtype().id() == ID_struct_tag;
630 }
631 
633 {
635  return static_cast<const java_reference_typet &>(type);
636 }
637 
639 {
641  return static_cast<java_reference_typet &>(type);
642 }
643 
656 struct_tag_typet java_classname(const std::string &);
657 
658 #define JAVA_REFERENCE_ARRAY_CLASSID "java::array[reference]"
659 
660 java_reference_typet java_array_type(const char subtype);
662 java_reference_array_type(const struct_tag_typet &element_type);
663 const typet &java_array_element_type(const struct_tag_typet &array_symbol);
665 bool is_java_array_type(const typet &type);
666 bool is_multidim_java_array_type(const typet &type);
667 
668 std::pair<typet, std::size_t>
670 
671 #define JAVA_ARRAY_DIMENSION_FIELD_NAME "@array_dimensions"
672 exprt get_array_dimension_field(const exprt &pointer);
673 #define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME "@element_class_identifier"
675 
676 typet java_type_from_char(char t);
678  const std::string &,
679  const std::string &class_name_prefix = "");
680 char java_char_from_type(const typet &type);
681 std::vector<typet> java_generic_type_from_string(
682  const std::string &,
683  const std::string &);
684 
688  const std::string src,
689  size_t starting_point = 0);
690 
691 std::vector<std::string> parse_raw_list_types(
692  std::string src,
693  char opening_bracket,
694  char closing_bracket);
695 
696 bool is_java_array_tag(const irep_idt &tag);
697 bool is_valid_java_array(const struct_typet &);
698 
699 bool equal_java_types(const typet &type1, const typet &type2);
700 
705 {
706 public:
708 
710  const irep_idt &_type_var_name,
711  const struct_tag_typet &_bound)
712  : struct_tag_typet(_bound)
713  {
714  set(ID_C_java_generic_parameter, true);
715  type_variables().push_back(struct_tag_typet(_type_var_name));
716  }
717 
720  {
721  PRECONDITION(!type_variables().empty());
722  return type_variables().front();
723  }
724 
726  {
727  PRECONDITION(!type_variables().empty());
728  return type_variables().front();
729  }
730 
731  const irep_idt get_name() const
732  {
733  return type_variable().get_identifier();
734  }
735 
736 private:
737  typedef std::vector<type_variablet> type_variablest;
739  {
740  return (const type_variablest &)(find(ID_type_variables).get_sub());
741  }
742 
744  {
745  return (type_variablest &)(add(ID_type_variables).get_sub());
746  }
747 };
748 
753 inline bool is_java_generic_parameter_tag(const typet &type)
754 {
755  return type.get_bool(ID_C_java_generic_parameter);
756 }
757 
760 inline const java_generic_parameter_tagt &
762 {
764  return static_cast<const java_generic_parameter_tagt &>(type);
765 }
766 
770 {
772  return static_cast<java_generic_parameter_tagt &>(type);
773 }
774 
778 {
779 public:
781 
783  const irep_idt &_type_var_name,
784  const struct_tag_typet &_bound)
786  java_generic_parameter_tagt(_type_var_name, _bound)))
787  {
788  }
789 
792  {
794  }
795 
797  {
799  }
800 
801  const irep_idt get_name() const
802  {
804  }
805 };
806 
811 template <>
813 {
814  return is_reference(base) && is_java_generic_parameter_tag(base.subtype());
815 }
816 
821 inline bool is_java_generic_parameter(const typet &type)
822 {
824 }
825 
829  const typet &type)
830 {
832  return static_cast<const java_generic_parametert &>(type);
833 }
834 
838 {
840  return static_cast<java_generic_parametert &>(type);
841 }
842 
859 {
860 public:
861  typedef std::vector<reference_typet> generic_typest;
862 
864  : struct_tag_typet(type)
865  {
866  set(ID_C_java_generic_symbol, true);
867  }
868 
870  const struct_tag_typet &type,
871  const std::string &base_ref,
872  const std::string &class_name_prefix);
873 
875  {
876  return (const generic_typest &)(find(ID_generic_types).get_sub());
877  }
878 
880  {
881  return (generic_typest &)(add(ID_generic_types).get_sub());
882  }
883 
885  generic_type_index(const java_generic_parametert &type) const;
886 };
887 
890 inline bool is_java_generic_struct_tag_type(const typet &type)
891 {
892  return type.get_bool(ID_C_java_generic_symbol);
893 }
894 
897 inline const java_generic_struct_tag_typet &
899 {
901  return static_cast<const java_generic_struct_tag_typet &>(type);
902 }
903 
908 {
910  return static_cast<java_generic_struct_tag_typet &>(type);
911 }
912 
916 {
917 public:
919 
920  explicit java_generic_typet(const typet &_type)
923  {
924  }
925 
928  {
930  }
931 
934  {
936  }
937 };
938 
939 template <>
940 inline bool can_cast_type<java_generic_typet>(const typet &type)
941 {
942  return is_reference(type) && is_java_generic_struct_tag_type(type.subtype());
943 }
944 
947 inline bool is_java_generic_type(const typet &type)
948 {
950 }
951 
955  const typet &type)
956 {
958  return static_cast<const java_generic_typet &>(type);
959 }
960 
964 {
966  return static_cast<java_generic_typet &>(type);
967 }
968 
973 {
974  public:
975  typedef std::vector<java_generic_parametert> generic_typest;
976 
978  {
979  set(ID_C_java_generics_class_type, true);
980  }
981 
983  {
984  return (const generic_typest &)(find(ID_generic_types).get_sub());
985  }
986 
988  {
989  return (generic_typest &)(add(ID_generic_types).get_sub());
990  }
991 };
992 
995 inline bool is_java_generic_class_type(const typet &type)
996 {
997  return type.get_bool(ID_C_java_generics_class_type);
998 }
999 
1002 inline const java_generic_class_typet &
1004 {
1006  return static_cast<const java_generic_class_typet &>(type);
1007 }
1008 
1011 inline java_generic_class_typet &
1013 {
1015  return static_cast<java_generic_class_typet &>(type);
1016 }
1017 
1023  size_t index,
1024  const java_generic_typet &type)
1025 {
1026  const std::vector<reference_typet> &type_arguments =
1027  type.generic_type_arguments();
1028  PRECONDITION(index<type_arguments.size());
1029  return type_arguments[index];
1030 }
1031 
1036 inline const irep_idt &
1038 {
1039  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
1040 
1041  PRECONDITION(index<gen_types.size());
1042  const java_generic_parametert &gen_type=gen_types[index];
1043 
1044  return gen_type.type_variable().get_identifier();
1045 }
1046 
1051 inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
1052 {
1054  const java_generic_class_typet &type =
1056  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
1057 
1058  PRECONDITION(index<gen_types.size());
1059  const java_generic_parametert &gen_type=gen_types[index];
1060 
1061  return gen_type.subtype();
1062 }
1063 
1068 {
1069 public:
1070  typedef std::vector<java_generic_parametert> implicit_generic_typest;
1071 
1073  const java_class_typet &class_type,
1074  const implicit_generic_typest &generic_types)
1075  : java_class_typet(class_type)
1076  {
1077  set(ID_C_java_implicitly_generic_class_type, true);
1078  for(const auto &type : generic_types)
1079  {
1080  implicit_generic_types().push_back(type);
1081  }
1082  }
1083 
1085  {
1086  return (
1088  &)(find(ID_implicit_generic_types).get_sub());
1089  }
1090 
1092  {
1093  return (
1094  implicit_generic_typest &)(add(ID_implicit_generic_types).get_sub());
1095  }
1096 };
1097 
1101 {
1102  return type.get_bool(ID_C_java_implicitly_generic_class_type);
1103 }
1104 
1109 {
1111  return static_cast<const java_implicitly_generic_class_typet &>(type);
1112 }
1113 
1118 {
1120  return static_cast<java_implicitly_generic_class_typet &>(type);
1121 }
1122 
1126 std::vector<java_generic_parametert>
1127 get_all_generic_parameters(const typet &type);
1128 
1131 class unsupported_java_class_signature_exceptiont:public std::logic_error
1132 {
1133 public:
1135  std::logic_error(
1136  "Unsupported class signature: "+type)
1137  {
1138  }
1139 };
1140 
1142  const std::string &descriptor,
1143  const optionalt<std::string> &signature,
1144  const std::string &class_name)
1145 {
1146  try
1147  {
1148  return java_type_from_string(signature.value(), class_name);
1149  }
1151  {
1152  return java_type_from_string(descriptor, class_name);
1153  }
1154 }
1155 
1161  const std::vector<java_generic_parametert> &gen_types,
1162  const irep_idt &identifier)
1163 {
1164  const auto iter = std::find_if(
1165  gen_types.cbegin(),
1166  gen_types.cend(),
1167  [&identifier](const java_generic_parametert &ref)
1168  {
1169  return ref.type_variable().get_identifier() == identifier;
1170  });
1171 
1172  if(iter == gen_types.cend())
1173  {
1174  return {};
1175  }
1176 
1177  return narrow_cast<size_t>(std::distance(gen_types.cbegin(), iter));
1178 }
1179 
1181  const std::string &,
1182  std::set<irep_idt> &);
1184  const typet &,
1185  std::set<irep_idt> &);
1186 
1191 std::string erase_type_arguments(const std::string &);
1197 std::string gather_full_class_name(const std::string &);
1198 
1199 // turn java type into string
1200 std::string pretty_java_type(const typet &);
1201 
1202 // pretty signature for methods
1203 std::string pretty_signature(const java_method_typet &);
1204 
1205 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
is_java_generic_class_type
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:995
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
can_cast_type< java_reference_typet >
bool can_cast_type< java_reference_typet >(const typet &type)
Definition: java_types.h:626
java_generic_typet::java_generic_typet
java_generic_typet(const typet &_type)
Definition: java_types.h:920
irept::get_int
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:69
struct_tag_typet::struct_tag_typet
struct_tag_typet(const irep_idt &identifier)
Definition: std_types.h:492
java_method_typet::add_throws_exception
void add_throws_exception(irep_idt exception)
Definition: java_types.h:134
java_class_typet::componentt
Definition: java_types.h:202
class_typet::methodst
componentst methodst
Definition: std_types.h:328
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_class_typet::get_inner_name
const irep_idt & get_inner_name() const
Get the name of a java inner class.
Definition: java_types.h:572
class_typet
Class type.
Definition: std_types.h:320
java_double_type
floatbv_typet java_double_type()
Definition: java_types.cpp:74
java_generic_typet
Reference that points to a java_generic_struct_tag_typet.
Definition: java_types.h:916
java_class_typet::method_handle_kindt::LAMBDA_VIRTUAL_METHOD_HANDLE
@ LAMBDA_VIRTUAL_METHOD_HANDLE
Virtual call to the given interface or method.
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
java_method_typet::get_is_final
bool get_is_final() const
Definition: java_types.h:139
java_class_typet::set_synthetic
void set_synthetic(bool synthetic)
marks class synthetic
Definition: java_types.h:436
java_class_typet::java_lambda_method_handlet::java_lambda_method_handlet
java_lambda_method_handlet()
Definition: java_types.h:494
java_byte_type
signedbv_typet java_byte_type()
Definition: java_types.cpp:56
java_class_typet::set_is_static_class
void set_is_static_class(const bool &is_static_class)
Definition: java_types.h:370
java_class_typet::set_is_anonymous_class
void set_is_anonymous_class(const bool &is_anonymous_class)
Definition: java_types.h:380
can_cast_type< annotated_typet >
bool can_cast_type< annotated_typet >(const typet &)
Definition: java_types.h:97
reference_typet
The reference type.
Definition: std_types.h:1553
java_class_typet::get_interface
bool get_interface() const
is class an interface?
Definition: java_types.h:454
java_implicitly_generic_class_typet::implicit_generic_types
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:1084
java_generic_class_typet::generic_typest
std::vector< java_generic_parametert > generic_typest
Definition: java_types.h:975
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
java_class_typet::method_handle_kindt::LAMBDA_STATIC_METHOD_HANDLE
@ LAMBDA_STATIC_METHOD_HANDLE
Direct call to the given method.
optional.h
java_annotationt::valuet::get_name
const irep_idt & get_name() const
Definition: java_types.h:34
java_class_typet::get_is_enumeration
bool get_is_enumeration() const
is class an enumeration?
Definition: java_types.h:406
java_class_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Definition: java_types.h:236
unsupported_java_class_signature_exceptiont
An exception that is raised for unsupported class signature.
Definition: java_types.h:1132
java_class_typet::methodt::get_is_native
bool get_is_native() const
is a method 'native'?
Definition: java_types.h:276
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
java_class_typet::methodt::methodt
methodt(const irep_idt &_name, java_method_typet _type)
Definition: java_types.h:247
java_long_type
signedbv_typet java_long_type()
Definition: java_types.cpp:44
java_class_typet::add_unknown_lambda_method_handle
void add_unknown_lambda_method_handle()
Definition: java_types.h:539
java_method_typet::is_synthetic
bool is_synthetic() const
Definition: java_types.h:169
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1379
to_annotated_type
const annotated_typet & to_annotated_type(const typet &type)
Definition: java_types.h:86
is_multidim_java_array_type
bool is_multidim_java_array_type(const typet &type)
Checks whether the given type is a multi-dimensional array pointer type, i.e., a pointer to an array ...
Definition: java_types.cpp:179
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:232
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
annotated_typet::get_annotations
std::vector< java_annotationt > & get_annotations()
Definition: java_types.h:78
java_method_typet::get_native
bool get_native() const
Definition: java_types.h:149
java_class_typet::methodt
Definition: java_types.h:243
java_class_typet::methodt::type
java_method_typet & type()
Definition: java_types.h:258
java_generic_parametert
Reference that points to a java_generic_parameter_tagt.
Definition: java_types.h:778
java_class_typet::add_lambda_method_handle
void add_lambda_method_handle(const class_method_descriptor_exprt &method_descriptor, method_handle_kindt handle_kind)
Definition: java_types.h:532
invariant.h
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:162
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
java_array_element_type
const typet & java_array_element_type(const struct_tag_typet &array_symbol)
Return a const reference to the element type of a given java array type.
Definition: java_types.cpp:145
java_class_typet::set_is_annotation
void set_is_annotation(bool is_annotation)
marks class an annotation
Definition: java_types.h:448
can_cast_type< java_generic_typet >
bool can_cast_type< java_generic_typet >(const typet &type)
Definition: java_types.h:940
is_java_implicitly_generic_class_type
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:1100
java_class_typet::static_members
const static_memberst & static_members() const
Definition: java_types.h:315
java_generic_parametert::type_variablet
struct_tag_typet type_variablet
Definition: java_types.h:780
to_java_generic_class_type
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:1003
pretty_java_type
std::string pretty_java_type(const typet &)
Definition: java_types.cpp:1082
java_generic_class_typet::generic_types
generic_typest & generic_types()
Definition: java_types.h:987
gather_full_class_name
std::string gather_full_class_name(const std::string &)
Returns the full class name, skipping over the generics.
Definition: java_types.cpp:364
java_class_typet::methods
const methodst & methods() const
Definition: java_types.h:302
java_method_typet::set_is_varargs
void set_is_varargs(bool is_varargs)
Definition: java_types.h:164
java_generic_typet::generic_type_argumentst
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
Definition: java_types.h:918
is_java_array_type
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
Definition: java_types.cpp:164
java_generic_struct_tag_typet::generic_type_index
optionalt< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
Definition: java_types.cpp:1068
java_annotationt::valuet::valuet
valuet(irep_idt name, const exprt &value)
Definition: java_types.h:29
java_generic_struct_tag_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:874
java_generic_class_typet::java_generic_class_typet
java_generic_class_typet()
Definition: java_types.h:977
java_array_dimension_and_element_type
std::pair< typet, std::size_t > java_array_dimension_and_element_type(const struct_tag_typet &type)
Returns the underlying element type and array dimensionality of Java struct type.
Definition: java_types.cpp:188
java_class_typet::get_is_inner_class
bool get_is_inner_class() const
Definition: java_types.h:335
irept::irept
irept()=default
pretty_signature
std::string pretty_signature(const java_method_typet &)
Definition: java_types.cpp:1123
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
java_generic_parametert::type_variable_ref
type_variablet & type_variable_ref()
Definition: java_types.h:796
java_class_typet::set_inner_name
void set_inner_name(const irep_idt &name)
Set the name of a java inner class.
Definition: java_types.h:578
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
java_class_typet
Definition: java_types.h:199
java_generic_class_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:982
get_array_dimension_field
exprt get_array_dimension_field(const exprt &pointer)
Definition: java_types.cpp:205
narrow.h
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:4508
java_type_from_string
optionalt< typet > java_type_from_string(const std::string &, const std::string &class_name_prefix="")
Transforms a string representation of a Java type into an internal type representation thereof.
Definition: java_types.cpp:560
java_class_typet::java_lambda_method_handlet
Represents a lambda call to a method.
Definition: java_types.h:484
java_type_from_string_with_exception
optionalt< typet > java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
Definition: java_types.h:1141
java_generic_get_inst_type
const typet & java_generic_get_inst_type(size_t index, const java_generic_typet &type)
Access information of type arguments of java instantiated type.
Definition: java_types.h:1022
c_bool_typet
The C/C++ Booleans.
Definition: std_types.h:1604
java_array_type
java_reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:110
java_generic_parameter_tagt::java_generic_parameter_tagt
java_generic_parameter_tagt(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
Definition: java_types.h:709
class_method_descriptor_exprt::get_identifier
const irep_idt & get_identifier() const
A unique identifier of the combination of class and method overload to which this expression refers.
Definition: std_expr.h:4568
java_class_typet::set_is_enumeration
void set_is_enumeration(const bool is_enumeration)
marks class as an enumeration
Definition: java_types.h:412
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
java_class_typet::get_is_anonymous_class
bool get_is_anonymous_class() const
Definition: java_types.h:375
java_class_typet::methodt::type
const java_method_typet & type() const
Definition: java_types.h:252
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
java_annotationt::get_values
const std::vector< valuet > & get_values() const
Definition: java_types.h:55
java_method_typet::set_native
void set_native(bool is_native)
Definition: java_types.h:154
java_generic_parametert::get_name
const irep_idt get_name() const
Definition: java_types.h:801
java_annotationt::java_annotationt
java_annotationt(const typet &type)
Definition: java_types.h:45
java_class_typet::get_annotations
const std::vector< java_annotationt > & get_annotations() const
Definition: java_types.h:545
java_reference_typet::subtype
struct_tag_typet & subtype()
Definition: java_types.h:614
class_typet::static_memberst
componentst static_memberst
Definition: std_types.h:341
java_generic_struct_tag_typet::java_generic_struct_tag_typet
java_generic_struct_tag_typet(const struct_tag_typet &type)
Definition: java_types.h:863
empty_typet
The empty type.
Definition: std_types.h:46
java_annotationt::valuet
Definition: java_types.h:27
java_class_typet::get_is_annotation
bool get_is_annotation() const
is class an annotation?
Definition: java_types.h:442
to_java_generic_struct_tag_type
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:898
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:927
java_void_type
empty_typet java_void_type()
Definition: java_types.cpp:38
java_class_typet::methods
methodst & methods()
Definition: java_types.h:307
java_generic_parameter_tagt::type_variables
type_variablest & type_variables()
Definition: java_types.h:743
java_class_typet::java_lambda_method_handlest
std::vector< java_lambda_method_handlet > java_lambda_method_handlest
Definition: java_types.h:517
get_all_generic_parameters
std::vector< java_generic_parametert > get_all_generic_parameters(const typet &type)
Definition: java_types.cpp:918
java_class_typet::methodt::methodt
methodt()=delete
java_class_typet::methodt::set_is_final
void set_is_final(const bool is_final)
is a method 'final'?
Definition: java_types.h:270
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
is_java_generic_parameter
bool is_java_generic_parameter(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.
Definition: java_types.h:821
java_generic_parametert::java_generic_parametert
java_generic_parametert(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
Definition: java_types.h:782
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
to_java_reference_type
const java_reference_typet & to_java_reference_type(const typet &type)
Definition: java_types.h:632
std_types.h
Pre-defined types.
is_java_generic_struct_tag_type
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:890
equal_java_types
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
Definition: java_types.cpp:891
annotated_typet
Definition: java_types.h:69
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition: java_types.h:947
class_typet::static_members
const static_memberst & static_members() const
Definition: std_types.h:343
java_implicitly_generic_class_typet
Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class o...
Definition: java_types.h:1068
java_implicitly_generic_class_typet::implicit_generic_types
implicit_generic_typest & implicit_generic_types()
Definition: java_types.h:1091
java_class_typet::method_handle_kindt::LAMBDA_CONSTRUCTOR_HANDLE
@ LAMBDA_CONSTRUCTOR_HANDLE
Instantiate the needed type then call a constructor.
java_generic_typet::generic_type_arguments
generic_type_argumentst & generic_type_arguments()
Definition: java_types.h:933
java_class_typet::methodt::set_is_native
void set_is_native(const bool is_native)
marks a method as 'native'
Definition: java_types.h:282
java_class_typet::java_lambda_method_handlet::get_lambda_method_identifier
const irep_idt & get_lambda_method_identifier() const
Definition: java_types.h:506
code_typet
Base type of functions.
Definition: std_types.h:736
java_generic_parameter_tagt::type_variables
const type_variablest & type_variables() const
Definition: java_types.h:738
java_method_typet::java_method_typet
java_method_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e.
Definition: java_types.h:111
java_class_typet::get_synthetic
bool get_synthetic() const
is class synthetic?
Definition: java_types.h:430
irept::id
const irep_idt & id() const
Definition: irep.h:418
java_class_typet::method_handle_kindt::UNKNOWN_HANDLE
@ UNKNOWN_HANDLE
Can't be called.
can_cast_type< java_class_typet >
bool can_cast_type< java_class_typet >(const typet &type)
Definition: java_types.h:597
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
java_class_typet::components
componentst & components()
Definition: java_types.h:231
java_class_typet::java_lambda_method_handlet::get_handle_kind
method_handle_kindt get_handle_kind() const
Definition: java_types.h:511
java_short_type
signedbv_typet java_short_type()
Definition: java_types.cpp:50
can_cast_type< java_generic_parametert >
bool can_cast_type< java_generic_parametert >(const typet &base)
Check whether a reference to a typet is a Java generic parameter/variable, e.g., T in List<T>.
Definition: java_types.h:812
java_generic_parameter_tagt
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
Definition: java_types.h:705
get_array_element_type_field
exprt get_array_element_type_field(const exprt &pointer)
Definition: java_types.cpp:217
java_annotationt::get_type
const typet & get_type() const
Definition: java_types.h:50
java_class_typet::get_abstract
bool get_abstract() const
is class abstract?
Definition: java_types.h:418
java_class_typet::get_final
bool get_final() const
Definition: java_types.h:385
class_typet::methodt
componentt methodt
Definition: std_types.h:327
java_type_from_char
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
Definition: java_types.cpp:247
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:954
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_generic_parameter_tagt::type_variable_ref
type_variablet & type_variable_ref()
Definition: java_types.h:725
java_bytecode_promotion
typet java_bytecode_promotion(const typet &)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:268
java_class_typet::set_final
void set_final(bool is_final)
Definition: java_types.h:390
java_generic_parameter_tagt::type_variable
const type_variablet & type_variable() const
Definition: java_types.h:719
java_class_typet::set_interface
void set_interface(bool interface)
marks class an interface
Definition: java_types.h:460
java_class_typet::set_outer_class
void set_outer_class(const irep_idt &outer_class)
Definition: java_types.h:350
java_class_typet::componentt::componentt
componentt(const irep_idt &_name, typet _type)
Definition: java_types.h:206
java_annotationt::valuet::get_value
const exprt & get_value() const
Definition: java_types.h:39
java_class_typet::get_name
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:559
java_class_typet::get_annotations
std::vector< java_annotationt > & get_annotations()
Definition: java_types.h:551
java_class_typet::set_is_stub
void set_is_stub(bool is_stub)
Definition: java_types.h:395
struct_union_typet::componentt
Definition: std_types.h:64
java_class_typet::set_super_class
void set_super_class(const irep_idt &super_class)
Definition: java_types.h:360
java_generic_struct_tag_typet::generic_typest
std::vector< reference_typet > generic_typest
Definition: java_types.h:861
java_method_typet::set_is_final
void set_is_final(bool is_final)
Definition: java_types.h:144
java_class_typet::components
const componentst & components() const
Definition: java_types.h:226
java_class_typet::methodt::get_descriptor
const irep_idt & get_descriptor() const
Gets the method's descriptor – the mangled form of its type.
Definition: java_types.h:288
java_generic_class_type_bound
const typet & java_generic_class_type_bound(size_t index, const typet &t)
Access information of the type bound of a generic java class type.
Definition: java_types.h:1051
java_class_typet::lambda_method_handles
java_lambda_method_handlest & lambda_method_handles()
Definition: java_types.h:526
java_class_typet::methodt::get_is_final
bool get_is_final() const
is a method 'final'?
Definition: java_types.h:264
java_generic_parameter_tagt::type_variablet
struct_tag_typet type_variablet
Definition: java_types.h:707
java_class_typet::set_access
void set_access(const irep_idt &access)
Definition: java_types.h:330
java_reference_typet::java_reference_typet
java_reference_typet(const struct_tag_typet &_subtype, std::size_t _width)
Definition: java_types.h:607
is_valid_java_array
bool is_valid_java_array(const struct_typet &)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
Definition: java_types.cpp:834
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
java_reference_typet::subtype
const struct_tag_typet & subtype() const
Definition: java_types.h:619
java_implicitly_generic_class_typet::java_implicitly_generic_class_typet
java_implicitly_generic_class_typet(const java_class_typet &class_type, const implicit_generic_typest &generic_types)
Definition: java_types.h:1072
to_java_generic_parameter
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:828
java_implicitly_generic_class_typet::implicit_generic_typest
std::vector< java_generic_parametert > implicit_generic_typest
Definition: java_types.h:1070
java_class_typet::get_outer_class
const irep_idt & get_outer_class() const
Definition: java_types.h:345
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
is_java_generic_parameter_tag
bool is_java_generic_parameter_tag(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.
Definition: java_types.h:753
java_generic_class_type_var
const irep_idt & java_generic_class_type_var(size_t index, const java_generic_class_typet &type)
Access information of type variables of a generic java class type.
Definition: java_types.h:1037
to_java_generic_parameter_tag
const java_generic_parameter_tagt & to_java_generic_parameter_tag(const typet &type)
Definition: java_types.h:761
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
java_generic_parameter_tagt::type_variablest
std::vector< type_variablet > type_variablest
Definition: java_types.h:737
java_reference_type
java_reference_typet java_reference_type(const struct_tag_typet &subtype)
Definition: java_types.cpp:94
get_dependencies_from_generic_parameters
void get_dependencies_from_generic_parameters(const std::string &, std::set< irep_idt > &)
Collect information about generic type parameters from a given signature.
Definition: java_types.cpp:989
java_generic_struct_tag_typet::generic_types
generic_typest & generic_types()
Definition: java_types.h:879
find_closing_semi_colon_for_reference_type
size_t find_closing_semi_colon_for_reference_type(const std::string src, size_t starting_point=0)
Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point.
Definition: java_types.cpp:515
java_generic_type_from_string
std::vector< typet > java_generic_type_from_string(const std::string &, const std::string &)
Converts the content of a generic class type into a vector of Java types, that is each type variable ...
Definition: java_types.cpp:747
java_annotationt::get_values
std::vector< valuet > & get_values()
Definition: java_types.h:61
erase_type_arguments
std::string erase_type_arguments(const std::string &)
Take a signature string and remove everything in angle brackets allowing for the type to be parsed no...
Definition: java_types.cpp:333
java_class_typet::set_is_inner_class
void set_is_inner_class(const bool &is_inner_class)
Definition: java_types.h:340
irept::get_sub
subt & get_sub()
Definition: irep.h:477
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
java_class_typet::java_lambda_method_handlet::java_lambda_method_handlet
java_lambda_method_handlet(const class_method_descriptor_exprt &method_descriptor, method_handle_kindt handle_kind)
Definition: java_types.h:486
code_typet::parametert
Definition: std_types.h:753
can_cast_type< java_method_typet >
bool can_cast_type< java_method_typet >(const typet &type)
Definition: java_types.h:181
java_class_typet::set_name
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:566
to_java_implicitly_generic_class_type
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
Definition: java_types.h:1108
java_reference_array_type
java_reference_typet java_reference_array_type(const struct_tag_typet &element_type)
Definition: java_types.cpp:540
java_method_typet::java_method_typet
java_method_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e.
Definition: java_types.h:120
java_class_typet::componentt::get_is_final
bool get_is_final() const
is a field 'final'?
Definition: java_types.h:212
java_generic_struct_tag_typet
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:859
java_method_typet::get_is_varargs
bool get_is_varargs() const
Definition: java_types.h:159
java_class_typet::java_lambda_method_handlet::get_lambda_method_descriptor
const class_method_descriptor_exprt & get_lambda_method_descriptor() const
Definition: java_types.h:500
java_method_typet::set_is_synthetic
void set_is_synthetic(bool is_synthetic)
Definition: java_types.h:174
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
java_generic_parameter_tagt::get_name
const irep_idt get_name() const
Definition: java_types.h:731
java_class_typet::set_abstract
void set_abstract(bool abstract)
marks class abstract
Definition: java_types.h:424
java_class_typet::componentt::set_is_final
void set_is_final(const bool is_final)
is a field 'final'?
Definition: java_types.h:218
java_reference_typet
This is a specialization of reference_typet.
Definition: java_types.h:605
java_class_typet::method_handle_kindt
method_handle_kindt
Indicates what sort of code should be synthesised for a lambda call:
Definition: java_types.h:467
unsupported_java_class_signature_exceptiont::unsupported_java_class_signature_exceptiont
unsupported_java_class_signature_exceptiont(std::string type)
Definition: java_types.h:1134
java_generic_class_typet
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:973
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
java_class_typet::get_super_class
const irep_idt & get_super_class() const
Definition: java_types.h:355
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:400
annotated_typet::get_annotations
const std::vector< java_annotationt > & get_annotations() const
Definition: java_types.h:71
can_cast_type< class_typet >
bool can_cast_type< class_typet >(const typet &type)
Check whether a reference to a typet is a class_typet.
Definition: std_types.h:363
java_class_typet::lambda_method_handles
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:519
java_classname
struct_tag_typet java_classname(const std::string &)
Definition: java_types.cpp:806
std_expr.h
API to expression classes.
java_class_typet::get_access
const irep_idt & get_access() const
Definition: java_types.h:325
java_annotationt
Definition: java_types.h:24
java_method_typet
Definition: java_types.h:103
java_float_type
floatbv_typet java_float_type()
Definition: java_types.cpp:68
java_generics_get_index_for_subtype
const optionalt< size_t > java_generics_get_index_for_subtype(const std::vector< java_generic_parametert > &gen_types, const irep_idt &identifier)
Get the index in the subtypes array for a given component.
Definition: java_types.h:1160
c_types.h
java_method_typet::throws_exceptions
const std::vector< irep_idt > throws_exceptions() const
Definition: java_types.h:126
java_class_typet::static_members
static_memberst & static_members()
Definition: java_types.h:320
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:80
java_class_typet::componentt::componentt
componentt()=default
java_generic_parametert::type_variable
const type_variablet & type_variable() const
Definition: java_types.h:791
parse_raw_list_types
std::vector< std::string > parse_raw_list_types(std::string src, char opening_bracket, char closing_bracket)
Given a substring of a descriptor or signature that contains one or more types parse out the individu...
Definition: java_types.cpp:418
java_class_typet::get_is_static_class
bool get_is_static_class() const
Definition: java_types.h:365
java_lang_object_type
java_reference_typet java_lang_object_type()
Definition: java_types.cpp:99
java_char_from_type
char java_char_from_type(const typet &type)
Definition: java_types.cpp:706
java_class_typet::methodt::set_descriptor
void set_descriptor(const irep_idt &id)
Sets the method's descriptor – the mangled form of its type.
Definition: java_types.h:294