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  };
287 
288  using methodst = std::vector<methodt>;
289 
290  const methodst &methods() const
291  {
292  return (const methodst &)(find(ID_methods).get_sub());
293  }
294 
296  {
297  return (methodst &)(add(ID_methods).get_sub());
298  }
299 
301  using static_memberst = std::vector<componentt>;
302 
304  {
306  }
307 
309  {
311  }
312 
313  const irep_idt &get_access() const
314  {
315  return get(ID_access);
316  }
317 
318  void set_access(const irep_idt &access)
319  {
320  return set(ID_access, access);
321  }
322 
323  bool get_is_inner_class() const
324  {
325  return get_bool(ID_is_inner_class);
326  }
327 
328  void set_is_inner_class(const bool &is_inner_class)
329  {
330  return set(ID_is_inner_class, is_inner_class);
331  }
332 
333  const irep_idt &get_outer_class() const
334  {
335  return get(ID_outer_class);
336  }
337 
338  void set_outer_class(const irep_idt &outer_class)
339  {
340  return set(ID_outer_class, outer_class);
341  }
342 
343  const irep_idt &get_super_class() const
344  {
345  return get(ID_super_class);
346  }
347 
348  void set_super_class(const irep_idt &super_class)
349  {
350  return set(ID_super_class, super_class);
351  }
352 
353  bool get_is_static_class() const
354  {
355  return get_bool(ID_is_static);
356  }
357 
358  void set_is_static_class(const bool &is_static_class)
359  {
360  return set(ID_is_static, is_static_class);
361  }
362 
364  {
365  return get_bool(ID_is_anonymous);
366  }
367 
368  void set_is_anonymous_class(const bool &is_anonymous_class)
369  {
370  return set(ID_is_anonymous, is_anonymous_class);
371  }
372 
373  bool get_final() const
374  {
375  return get_bool(ID_final);
376  }
377 
378  void set_final(bool is_final)
379  {
380  set(ID_final, is_final);
381  }
382 
383  void set_is_stub(bool is_stub)
384  {
385  set(ID_incomplete_class, is_stub);
386  }
387 
388  bool get_is_stub() const
389  {
390  return get_bool(ID_incomplete_class);
391  }
392 
394  bool get_is_enumeration() const
395  {
396  return get_bool(ID_enumeration);
397  }
398 
400  void set_is_enumeration(const bool is_enumeration)
401  {
402  set(ID_enumeration, is_enumeration);
403  }
404 
406  bool get_abstract() const
407  {
408  return get_bool(ID_abstract);
409  }
410 
412  void set_abstract(bool abstract)
413  {
414  set(ID_abstract, abstract);
415  }
416 
418  bool get_synthetic() const
419  {
420  return get_bool(ID_synthetic);
421  }
422 
424  void set_synthetic(bool synthetic)
425  {
426  set(ID_synthetic, synthetic);
427  }
428 
430  bool get_is_annotation() const
431  {
432  return get_bool(ID_is_annotation);
433  }
434 
436  void set_is_annotation(bool is_annotation)
437  {
438  set(ID_is_annotation, is_annotation);
439  }
440 
442  bool get_interface() const
443  {
444  return get_bool(ID_interface);
445  }
446 
448  void set_interface(bool interface)
449  {
450  set(ID_interface, interface);
451  }
452 
453  // it may be better to introduce a class like
454  // class java_lambda_method_handlet : private irept
455  // {
456  // java_lambda_method_handlet(const irep_idt &id) : irept(id)
457  // {
458  // }
459  //
460  // const irep_idt &get_lambda_method_handle() const
461  // {
462  // return id();
463  // }
464  // };
466 
468  {
469  return find(ID_java_lambda_method_handles).get_sub();
470  }
471 
473  {
474  return add(ID_java_lambda_method_handles).get_sub();
475  }
476 
477  void add_lambda_method_handle(const irep_idt &identifier)
478  {
479  // creates a symbol_exprt for the identifier and pushes it in the vector
480  lambda_method_handles().emplace_back(identifier);
481  }
483  {
484  // creates empty symbol_exprt and pushes it in the vector
485  lambda_method_handles().emplace_back();
486  }
487 
488  const std::vector<java_annotationt> &get_annotations() const
489  {
490  return static_cast<const annotated_typet &>(
491  static_cast<const typet &>(*this)).get_annotations();
492  }
493 
494  std::vector<java_annotationt> &get_annotations()
495  {
496  return type_checked_cast<annotated_typet>(
497  static_cast<typet &>(*this)).get_annotations();
498  }
499 
502  const irep_idt &get_name() const
503  {
504  return get(ID_name);
505  }
506 
509  void set_name(const irep_idt &name)
510  {
511  set(ID_name, name);
512  }
513 
515  const irep_idt &get_inner_name() const
516  {
517  return get(ID_inner_name);
518  }
519 
521  void set_inner_name(const irep_idt &name)
522  {
523  set(ID_inner_name, name);
524  }
525 };
526 
527 inline const java_class_typet &to_java_class_type(const typet &type)
528 {
529  assert(type.id()==ID_struct);
530  return static_cast<const java_class_typet &>(type);
531 }
532 
534 {
535  assert(type.id()==ID_struct);
536  return static_cast<java_class_typet &>(type);
537 }
538 
539 template <>
540 inline bool can_cast_type<java_class_typet>(const typet &type)
541 {
542  return can_cast_type<class_typet>(type);
543 }
544 
548 {
549 public:
551  const struct_tag_typet &_subtype,
552  std::size_t _width)
553  : reference_typet(_subtype, _width)
554  {
555  }
556 
558  {
559  return static_cast<struct_tag_typet &>(reference_typet::subtype());
560  }
561 
562  const struct_tag_typet &subtype() const
563  {
564  return static_cast<const struct_tag_typet &>(reference_typet::subtype());
565  }
566 };
567 
568 template <>
570 {
571  return type.id() == ID_pointer &&
572  to_type_with_subtype(type).subtype().id() == ID_struct_tag;
573 }
574 
576 {
578  return static_cast<const java_reference_typet &>(type);
579 }
580 
582 {
584  return static_cast<java_reference_typet &>(type);
585 }
586 
599 struct_tag_typet java_classname(const std::string &);
600 
601 #define JAVA_REFERENCE_ARRAY_CLASSID "java::array[reference]"
602 
603 java_reference_typet java_array_type(const char subtype);
605 java_reference_array_type(const struct_tag_typet &element_type);
606 const typet &java_array_element_type(const struct_tag_typet &array_symbol);
608 bool is_java_array_type(const typet &type);
609 bool is_multidim_java_array_type(const typet &type);
610 
611 std::pair<typet, std::size_t>
613 
614 #define JAVA_ARRAY_DIMENSION_FIELD_NAME "@array_dimensions"
616 #define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME "@element_class_identifier"
618 
619 typet java_type_from_char(char t);
621  const std::string &,
622  const std::string &class_name_prefix = "");
623 char java_char_from_type(const typet &type);
624 std::vector<typet> java_generic_type_from_string(
625  const std::string &,
626  const std::string &);
627 
631  const std::string src,
632  size_t starting_point = 0);
633 
634 std::vector<std::string> parse_raw_list_types(
635  std::string src,
636  char opening_bracket,
637  char closing_bracket);
638 
639 bool is_java_array_tag(const irep_idt &tag);
640 bool is_valid_java_array(const struct_typet &);
641 
642 bool equal_java_types(const typet &type1, const typet &type2);
643 
648 {
649 public:
651 
653  const irep_idt &_type_var_name,
654  const struct_tag_typet &_bound)
655  : struct_tag_typet(_bound)
656  {
657  set(ID_C_java_generic_parameter, true);
658  type_variables().push_back(struct_tag_typet(_type_var_name));
659  }
660 
663  {
664  PRECONDITION(!type_variables().empty());
665  return type_variables().front();
666  }
667 
669  {
670  PRECONDITION(!type_variables().empty());
671  return type_variables().front();
672  }
673 
674  const irep_idt get_name() const
675  {
676  return type_variable().get_identifier();
677  }
678 
679 private:
680  typedef std::vector<type_variablet> type_variablest;
682  {
683  return (const type_variablest &)(find(ID_type_variables).get_sub());
684  }
685 
687  {
688  return (type_variablest &)(add(ID_type_variables).get_sub());
689  }
690 };
691 
696 inline bool is_java_generic_parameter_tag(const typet &type)
697 {
698  return type.get_bool(ID_C_java_generic_parameter);
699 }
700 
703 inline const java_generic_parameter_tagt &
705 {
707  return static_cast<const java_generic_parameter_tagt &>(type);
708 }
709 
713 {
715  return static_cast<java_generic_parameter_tagt &>(type);
716 }
717 
721 {
722 public:
724 
726  const irep_idt &_type_var_name,
727  const struct_tag_typet &_bound)
729  java_generic_parameter_tagt(_type_var_name, _bound)))
730  {
731  }
732 
735  {
737  }
738 
740  {
742  }
743 
744  const irep_idt get_name() const
745  {
747  }
748 };
749 
754 template <>
756 {
757  return is_reference(base) && is_java_generic_parameter_tag(base.subtype());
758 }
759 
764 inline bool is_java_generic_parameter(const typet &type)
765 {
767 }
768 
772  const typet &type)
773 {
775  return static_cast<const java_generic_parametert &>(type);
776 }
777 
781 {
783  return static_cast<java_generic_parametert &>(type);
784 }
785 
802 {
803 public:
804  typedef std::vector<reference_typet> generic_typest;
805 
807  : struct_tag_typet(type)
808  {
809  set(ID_C_java_generic_symbol, true);
810  }
811 
813  const struct_tag_typet &type,
814  const std::string &base_ref,
815  const std::string &class_name_prefix);
816 
818  {
819  return (const generic_typest &)(find(ID_generic_types).get_sub());
820  }
821 
823  {
824  return (generic_typest &)(add(ID_generic_types).get_sub());
825  }
826 
828  generic_type_index(const java_generic_parametert &type) const;
829 };
830 
833 inline bool is_java_generic_struct_tag_type(const typet &type)
834 {
835  return type.get_bool(ID_C_java_generic_symbol);
836 }
837 
840 inline const java_generic_struct_tag_typet &
842 {
844  return static_cast<const java_generic_struct_tag_typet &>(type);
845 }
846 
851 {
853  return static_cast<java_generic_struct_tag_typet &>(type);
854 }
855 
859 {
860 public:
862 
863  explicit java_generic_typet(const typet &_type)
866  {
867  }
868 
871  {
873  }
874 
877  {
879  }
880 };
881 
882 template <>
883 inline bool can_cast_type<java_generic_typet>(const typet &type)
884 {
885  return is_reference(type) && is_java_generic_struct_tag_type(type.subtype());
886 }
887 
890 inline bool is_java_generic_type(const typet &type)
891 {
893 }
894 
898  const typet &type)
899 {
901  return static_cast<const java_generic_typet &>(type);
902 }
903 
907 {
909  return static_cast<java_generic_typet &>(type);
910 }
911 
916 {
917  public:
918  typedef std::vector<java_generic_parametert> generic_typest;
919 
921  {
922  set(ID_C_java_generics_class_type, true);
923  }
924 
926  {
927  return (const generic_typest &)(find(ID_generic_types).get_sub());
928  }
929 
931  {
932  return (generic_typest &)(add(ID_generic_types).get_sub());
933  }
934 };
935 
938 inline bool is_java_generic_class_type(const typet &type)
939 {
940  return type.get_bool(ID_C_java_generics_class_type);
941 }
942 
945 inline const java_generic_class_typet &
947 {
949  return static_cast<const java_generic_class_typet &>(type);
950 }
951 
956 {
958  return static_cast<java_generic_class_typet &>(type);
959 }
960 
966  size_t index,
967  const java_generic_typet &type)
968 {
969  const std::vector<reference_typet> &type_arguments =
970  type.generic_type_arguments();
971  PRECONDITION(index<type_arguments.size());
972  return type_arguments[index];
973 }
974 
979 inline const irep_idt &
981 {
982  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
983 
984  PRECONDITION(index<gen_types.size());
985  const java_generic_parametert &gen_type=gen_types[index];
986 
987  return gen_type.type_variable().get_identifier();
988 }
989 
994 inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
995 {
997  const java_generic_class_typet &type =
999  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
1000 
1001  PRECONDITION(index<gen_types.size());
1002  const java_generic_parametert &gen_type=gen_types[index];
1003 
1004  return gen_type.subtype();
1005 }
1006 
1011 {
1012 public:
1013  typedef std::vector<java_generic_parametert> implicit_generic_typest;
1014 
1016  const java_class_typet &class_type,
1017  const implicit_generic_typest &generic_types)
1018  : java_class_typet(class_type)
1019  {
1020  set(ID_C_java_implicitly_generic_class_type, true);
1021  for(const auto &type : generic_types)
1022  {
1023  implicit_generic_types().push_back(type);
1024  }
1025  }
1026 
1028  {
1029  return (
1031  &)(find(ID_implicit_generic_types).get_sub());
1032  }
1033 
1035  {
1036  return (
1037  implicit_generic_typest &)(add(ID_implicit_generic_types).get_sub());
1038  }
1039 };
1040 
1044 {
1045  return type.get_bool(ID_C_java_implicitly_generic_class_type);
1046 }
1047 
1052 {
1054  return static_cast<const java_implicitly_generic_class_typet &>(type);
1055 }
1056 
1061 {
1063  return static_cast<java_implicitly_generic_class_typet &>(type);
1064 }
1065 
1069 std::vector<java_generic_parametert>
1070 get_all_generic_parameters(const typet &type);
1071 
1074 class unsupported_java_class_signature_exceptiont:public std::logic_error
1075 {
1076 public:
1078  std::logic_error(
1079  "Unsupported class signature: "+type)
1080  {
1081  }
1082 };
1083 
1085  const std::string &descriptor,
1086  const optionalt<std::string> &signature,
1087  const std::string &class_name)
1088 {
1089  try
1090  {
1091  return java_type_from_string(signature.value(), class_name);
1092  }
1094  {
1095  return java_type_from_string(descriptor, class_name);
1096  }
1097 }
1098 
1104  const std::vector<java_generic_parametert> &gen_types,
1105  const irep_idt &identifier)
1106 {
1107  const auto iter = std::find_if(
1108  gen_types.cbegin(),
1109  gen_types.cend(),
1110  [&identifier](const java_generic_parametert &ref)
1111  {
1112  return ref.type_variable().get_identifier() == identifier;
1113  });
1114 
1115  if(iter == gen_types.cend())
1116  {
1117  return {};
1118  }
1119 
1120  return narrow_cast<size_t>(std::distance(gen_types.cbegin(), iter));
1121 }
1122 
1124  const std::string &,
1125  std::set<irep_idt> &);
1127  const typet &,
1128  std::set<irep_idt> &);
1129 
1134 std::string erase_type_arguments(const std::string &);
1140 std::string gather_full_class_name(const std::string &);
1141 
1142 // turn java type into string
1143 std::string pretty_java_type(const typet &);
1144 
1145 // pretty signature for methods
1146 std::string pretty_signature(const java_method_typet &);
1147 
1148 #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:938
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:569
java_generic_typet::java_generic_typet
java_generic_typet(const typet &_type)
Definition: java_types.h:863
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:515
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:859
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:424
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:358
java_class_typet::set_is_anonymous_class
void set_is_anonymous_class(const bool &is_anonymous_class)
Definition: java_types.h:368
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:442
java_implicitly_generic_class_typet::implicit_generic_types
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:1027
java_generic_class_typet::generic_typest
std::vector< java_generic_parametert > generic_typest
Definition: java_types.h:918
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
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:394
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:1075
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:482
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:721
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:436
can_cast_type< java_generic_typet >
bool can_cast_type< java_generic_typet >(const typet &type)
Definition: java_types.h:883
is_java_implicitly_generic_class_type
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:1043
java_class_typet::static_members
const static_memberst & static_members() const
Definition: java_types.h:303
java_generic_parametert::type_variablet
struct_tag_typet type_variablet
Definition: java_types.h:723
to_java_generic_class_type
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:946
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:930
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:290
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:861
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:817
java_generic_class_typet::java_generic_class_typet
java_generic_class_typet()
Definition: java_types.h:920
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:323
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:739
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:521
type.h
java_class_typet
Definition: java_types.h:199
java_generic_class_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:925
get_array_dimension_field
exprt get_array_dimension_field(const exprt &pointer)
Definition: java_types.cpp:205
narrow.h
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_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:1084
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:965
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:652
java_class_typet::set_is_enumeration
void set_is_enumeration(const bool is_enumeration)
marks class as an enumeration
Definition: java_types.h:400
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:363
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:744
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:488
java_reference_typet::subtype
struct_tag_typet & subtype()
Definition: java_types.h:557
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:806
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:430
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:841
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:870
java_void_type
empty_typet java_void_type()
Definition: java_types.cpp:38
java_class_typet::methods
methodst & methods()
Definition: java_types.h:295
java_generic_parameter_tagt::type_variables
type_variablest & type_variables()
Definition: java_types.h:686
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:764
java_generic_parametert::java_generic_parametert
java_generic_parametert(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
Definition: java_types.h:725
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:575
std_types.h
is_java_generic_struct_tag_type
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:833
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:890
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:1011
java_implicitly_generic_class_typet::implicit_generic_types
implicit_generic_typest & implicit_generic_types()
Definition: java_types.h:1034
java_generic_typet::generic_type_arguments
generic_type_argumentst & generic_type_arguments()
Definition: java_types.h:876
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
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:681
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:418
irept::id
const irep_idt & id() const
Definition: irep.h:418
can_cast_type< java_class_typet >
bool can_cast_type< java_class_typet >(const typet &type)
Definition: java_types.h:540
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_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:755
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:648
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:406
java_class_typet::get_final
bool get_final() const
Definition: java_types.h:373
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:897
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:668
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:378
sharing_treet< irept, std::map< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:182
java_generic_parameter_tagt::type_variable
const type_variablet & type_variable() const
Definition: java_types.h:662
java_class_typet::set_interface
void set_interface(bool interface)
marks class an interface
Definition: java_types.h:448
java_class_typet::set_outer_class
void set_outer_class(const irep_idt &outer_class)
Definition: java_types.h:338
java_class_typet::java_lambda_method_handlest
irept::subt java_lambda_method_handlest
Definition: java_types.h:465
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:502
java_class_typet::get_annotations
std::vector< java_annotationt > & get_annotations()
Definition: java_types.h:494
java_class_typet::set_is_stub
void set_is_stub(bool is_stub)
Definition: java_types.h:383
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:348
java_generic_struct_tag_typet::generic_typest
std::vector< reference_typet > generic_typest
Definition: java_types.h:804
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_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:994
java_class_typet::lambda_method_handles
java_lambda_method_handlest & lambda_method_handles()
Definition: java_types.h:472
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:650
java_class_typet::set_access
void set_access(const irep_idt &access)
Definition: java_types.h:318
java_reference_typet::java_reference_typet
java_reference_typet(const struct_tag_typet &_subtype, std::size_t _width)
Definition: java_types.h:550
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:562
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:1015
to_java_generic_parameter
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:771
java_implicitly_generic_class_typet::implicit_generic_typest
std::vector< java_generic_parametert > implicit_generic_typest
Definition: java_types.h:1013
java_class_typet::get_outer_class
const irep_idt & get_outer_class() const
Definition: java_types.h:333
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:696
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:980
to_java_generic_parameter_tag
const java_generic_parameter_tagt & to_java_generic_parameter_tag(const typet &type)
Definition: java_types.h:704
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:680
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:822
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::add_lambda_method_handle
void add_lambda_method_handle(const irep_idt &identifier)
Definition: java_types.h:477
java_class_typet::set_is_inner_class
void set_is_inner_class(const bool &is_inner_class)
Definition: java_types.h:328
irept::get_sub
subt & get_sub()
Definition: irep.h:477
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
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:509
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:1051
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:802
java_method_typet::get_is_varargs
bool get_is_varargs() const
Definition: java_types.h:159
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:674
java_class_typet::set_abstract
void set_abstract(bool abstract)
marks class abstract
Definition: java_types.h:412
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:548
unsupported_java_class_signature_exceptiont::unsupported_java_class_signature_exceptiont
unsupported_java_class_signature_exceptiont(std::string type)
Definition: java_types.h:1077
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:916
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:527
java_class_typet::get_super_class
const irep_idt & get_super_class() const
Definition: java_types.h:343
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:388
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:467
java_classname
struct_tag_typet java_classname(const std::string &)
Definition: java_types.cpp:806
std_expr.h
java_class_typet::get_access
const irep_idt & get_access() const
Definition: java_types.h:313
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:1103
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:308
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:734
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:353
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