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/type.h>
17 #include <util/std_types.h>
18 #include <util/c_types.h>
19 #include <util/optional.h>
20 #include <util/std_expr.h>
21 
22 class java_annotationt : public irept
23 {
24 public:
25  class valuet : public irept
26  {
27  public:
28  valuet(irep_idt name, const exprt &value) : irept(name)
29  {
30  get_sub().push_back(value);
31  }
32 
33  const irep_idt &get_name() const
34  {
35  return id();
36  }
37 
38  const exprt &get_value() const
39  {
40  return static_cast<const exprt &>(get_sub().front());
41  }
42  };
43 
44  explicit java_annotationt(const typet &type)
45  {
46  set(ID_type, type);
47  }
48 
49  const typet &get_type() const
50  {
51  return static_cast<const typet &>(find(ID_type));
52  }
53 
54  const std::vector<valuet> &get_values() const
55  {
56  // This cast should be safe as valuet doesn't add data to irept
57  return reinterpret_cast<const std::vector<valuet> &>(get_sub());
58  }
59 
60  std::vector<valuet> &get_values()
61  {
62  // This cast should be safe as valuet doesn't add data to irept
63  return reinterpret_cast<std::vector<valuet> &>(get_sub());
64  }
65 };
66 
67 class annotated_typet : public typet
68 {
69 public:
70  const std::vector<java_annotationt> &get_annotations() const
71  {
72  // This cast should be safe as java_annotationt doesn't add data to irept
73  return reinterpret_cast<const std::vector<java_annotationt> &>(
74  find(ID_C_annotations).get_sub());
75  }
76 
77  std::vector<java_annotationt> &get_annotations()
78  {
79  // This cast should be safe as java_annotationt doesn't add data to irept
80  return reinterpret_cast<std::vector<java_annotationt> &>(
81  add(ID_C_annotations).get_sub());
82  }
83 };
84 
85 inline const annotated_typet &to_annotated_type(const typet &type)
86 {
87  return static_cast<const annotated_typet &>(type);
88 }
89 
91 {
92  return static_cast<annotated_typet &>(type);
93 }
94 
95 template <>
97 {
98  return true;
99 }
100 
102 {
103  public:
104  const irep_idt &get_access() const
105  {
106  return get(ID_access);
107  }
108 
109  void set_access(const irep_idt &access)
110  {
111  return set(ID_access, access);
112  }
113 
114  bool get_is_inner_class() const
115  {
116  return get_bool(ID_is_inner_class);
117  }
118 
119  void set_is_inner_class(const bool &is_inner_class)
120  {
121  return set(ID_is_inner_class, is_inner_class);
122  }
123 
124  const irep_idt &get_outer_class() const
125  {
126  return get(ID_outer_class);
127  }
128 
129  void set_outer_class(const irep_idt &outer_class)
130  {
131  return set(ID_outer_class, outer_class);
132  }
133 
134  const irep_idt &get_super_class() const
135  {
136  return get(ID_super_class);
137  }
138 
139  void set_super_class(const irep_idt &super_class)
140  {
141  return set(ID_super_class, super_class);
142  }
143 
144  bool get_is_static_class() const
145  {
146  return get_bool(ID_is_static);
147  }
148 
149  void set_is_static_class(const bool &is_static_class)
150  {
151  return set(ID_is_static, is_static_class);
152  }
153 
155  {
156  return get_bool(ID_is_anonymous);
157  }
158 
159  void set_is_anonymous_class(const bool &is_anonymous_class)
160  {
161  return set(ID_is_anonymous, is_anonymous_class);
162  }
163 
164  bool get_final() const
165  {
166  return get_bool(ID_final);
167  }
168 
169  void set_final(bool is_final)
170  {
171  set(ID_final, is_final);
172  }
173 
174  void set_is_stub(const bool &is_stub)
175  {
176  set(ID_incomplete_class, true);
177  }
178 
179  bool get_is_stub() const
180  {
181  return get_bool(ID_incomplete_class);
182  }
183 
184  // it may be better to introduce a class like
185  // class java_lambda_method_handlet : private irept
186  // {
187  // java_lambda_method_handlet(const irep_idt &id) : irept(id)
188  // {
189  // }
190  //
191  // const irep_idt &get_lambda_method_handle() const
192  // {
193  // return id();
194  // }
195  // };
197 
199  {
200  return find(ID_java_lambda_method_handles).get_sub();
201  }
202 
204  {
205  return add(ID_java_lambda_method_handles).get_sub();
206  }
207 
208  void add_lambda_method_handle(const irep_idt &identifier)
209  {
210  // creates a symbol_exprt for the identifier and pushes it in the vector
211  lambda_method_handles().emplace_back(identifier);
212  }
214  {
215  // creates empty symbol_exprt and pushes it in the vector
216  lambda_method_handles().emplace_back();
217  }
218 
219  const std::vector<java_annotationt> &get_annotations() const
220  {
221  return static_cast<const annotated_typet &>(
222  static_cast<const typet &>(*this)).get_annotations();
223  }
224 
225  std::vector<java_annotationt> &get_annotations()
226  {
227  return type_checked_cast<annotated_typet>(
228  static_cast<typet &>(*this)).get_annotations();
229  }
230 
233  const irep_idt &get_name() const
234  {
235  return get(ID_name);
236  }
237 
240  void set_name(const irep_idt &name)
241  {
242  set(ID_name, name);
243  }
244 };
245 
246 inline const java_class_typet &to_java_class_type(const typet &type)
247 {
248  assert(type.id()==ID_struct);
249  return static_cast<const java_class_typet &>(type);
250 }
251 
253 {
254  assert(type.id()==ID_struct);
255  return static_cast<java_class_typet &>(type);
256 }
257 
258 template <>
259 inline bool can_cast_type<java_class_typet>(const typet &type)
260 {
261  return can_cast_type<class_typet>(type);
262 }
263 
265 {
266 public:
269 
273  java_method_typet(parameterst &&_parameters, typet &&_return_type)
274  : code_typet(std::move(_parameters), std::move(_return_type))
275  {
276  set(ID_C_java_method_type, true);
277  }
278 
282  java_method_typet(parameterst &&_parameters, const typet &_return_type)
283  : code_typet(std::move(_parameters), _return_type)
284  {
285  set(ID_C_java_method_type, true);
286  }
287 
288  const std::vector<irep_idt> throws_exceptions() const
289  {
290  std::vector<irep_idt> exceptions;
291  for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
292  exceptions.push_back(e.id());
293  return exceptions;
294  }
295 
297  {
298  add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
299  }
300 
301  bool get_is_final() const
302  {
303  return get_bool(ID_final);
304  }
305 
306  void set_is_final(bool is_final)
307  {
308  set(ID_final, is_final);
309  }
310 
311  bool get_native() const
312  {
313  return get_bool(ID_is_native_method);
314  }
315 
316  void set_native(bool is_native)
317  {
318  set(ID_is_native_method, is_native);
319  }
320 
321  bool get_is_varargs() const
322  {
323  return get_bool(ID_is_varargs_method);
324  }
325 
326  void set_is_varargs(bool is_varargs)
327  {
328  set(ID_is_varargs_method, is_varargs);
329  }
330 };
331 
332 template <>
333 inline bool can_cast_type<java_method_typet>(const typet &type)
334 {
335  return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
336 }
337 
338 inline const java_method_typet &to_java_method_type(const typet &type)
339 {
341  return static_cast<const java_method_typet &>(type);
342 }
343 
345 {
347  return static_cast<java_method_typet &>(type);
348 }
349 
361 struct_tag_typet java_classname(const std::string &);
362 
363 reference_typet java_array_type(const char subtype);
364 const typet &java_array_element_type(const struct_tag_typet &array_symbol);
366 bool is_java_array_type(const typet &type);
367 bool is_multidim_java_array_type(const typet &type);
368 
369 typet java_type_from_char(char t);
371  const std::string &,
372  const std::string &class_name_prefix="");
373 char java_char_from_type(const typet &type);
374 std::vector<typet> java_generic_type_from_string(
375  const std::string &,
376  const std::string &);
377 
381  const std::string src,
382  size_t starting_point = 0);
383 
384 std::vector<std::string> parse_raw_list_types(
385  std::string src,
386  char opening_bracket,
387  char closing_bracket);
388 
389 bool is_java_array_tag(const irep_idt &tag);
390 bool is_valid_java_array(const struct_typet &);
391 
392 bool equal_java_types(const typet &type1, const typet &type2);
393 
398 {
399 public:
401 
403  const irep_idt &_type_var_name,
404  const struct_tag_typet &_bound)
406  {
407  set(ID_C_java_generic_parameter, true);
408  type_variables().push_back(struct_tag_typet(_type_var_name));
409  }
410 
413  {
414  PRECONDITION(!type_variables().empty());
415  return type_variables().front();
416  }
417 
419  {
420  PRECONDITION(!type_variables().empty());
421  return const_cast<type_variablet &>(type_variables().front());
422  }
423 
424  const irep_idt get_name() const
425  {
426  return type_variable().get_identifier();
427  }
428 
429 private:
430  typedef std::vector<type_variablet> type_variablest;
432  {
433  return (const type_variablest &)(find(ID_type_variables).get_sub());
434  }
435 
437  {
438  return (type_variablest &)(add(ID_type_variables).get_sub());
439  }
440 };
441 
446 inline bool is_java_generic_parameter(const typet &type)
447 {
448  return type.get_bool(ID_C_java_generic_parameter);
449 }
450 
454  const typet &type)
455 {
457  return static_cast<const java_generic_parametert &>(type);
458 }
459 
463 {
465  return static_cast<java_generic_parametert &>(type);
466 }
467 
484 {
485 public:
486  typedef std::vector<reference_typet> generic_type_argumentst;
487 
488  explicit java_generic_typet(const typet &_type):
490  {
491  set(ID_C_java_generic_type, true);
492  }
493 
496  {
497  return (const generic_type_argumentst &)(
498  find(ID_type_variables).get_sub());
499  }
500 
503  {
504  return (generic_type_argumentst &)(
505  add(ID_type_variables).get_sub());
506  }
507 };
508 
509 template <>
510 inline bool can_cast_type<java_generic_typet>(const typet &type)
511 {
512  return is_reference(type) && type.get_bool(ID_C_java_generic_type);
513 }
514 
517 inline bool is_java_generic_type(const typet &type)
518 {
520 }
521 
525  const typet &type)
526 {
528  return static_cast<const java_generic_typet &>(type);
529 }
530 
534 {
536  return static_cast<java_generic_typet &>(type);
537 }
538 
543 {
544  public:
545  typedef std::vector<java_generic_parametert> generic_typest;
546 
548  {
549  set(ID_C_java_generics_class_type, true);
550  }
551 
553  {
554  return (const generic_typest &)(find(ID_generic_types).get_sub());
555  }
556 
558  {
559  return (generic_typest &)(add(ID_generic_types).get_sub());
560  }
561 };
562 
565 inline bool is_java_generic_class_type(const typet &type)
566 {
567  return type.get_bool(ID_C_java_generics_class_type);
568 }
569 
572 inline const java_generic_class_typet &
574 {
576  return static_cast<const java_generic_class_typet &>(type);
577 }
578 
583 {
585  return static_cast<java_generic_class_typet &>(type);
586 }
587 
593  size_t index,
594  const java_generic_typet &type)
595 {
596  const std::vector<reference_typet> &type_arguments =
597  type.generic_type_arguments();
598  PRECONDITION(index<type_arguments.size());
599  return type_arguments[index];
600 }
601 
606 inline const irep_idt &
608 {
609  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
610 
611  PRECONDITION(index<gen_types.size());
612  const java_generic_parametert &gen_type=gen_types[index];
613 
614  return gen_type.type_variable().get_identifier();
615 }
616 
621 inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
622 {
624  const java_generic_class_typet &type =
626  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
627 
628  PRECONDITION(index<gen_types.size());
629  const java_generic_parametert &gen_type=gen_types[index];
630 
631  return gen_type.subtype();
632 }
633 
638 {
639 public:
640  typedef std::vector<java_generic_parametert> implicit_generic_typest;
641 
643  const java_class_typet &class_type,
644  const implicit_generic_typest &generic_types)
645  : java_class_typet(class_type)
646  {
647  set(ID_C_java_implicitly_generic_class_type, true);
648  for(const auto &type : generic_types)
649  {
650  implicit_generic_types().push_back(type);
651  }
652  }
653 
655  {
656  return (
658  &)(find(ID_implicit_generic_types).get_sub());
659  }
660 
662  {
663  return (
664  implicit_generic_typest &)(add(ID_implicit_generic_types).get_sub());
665  }
666 };
667 
671 {
672  return type.get_bool(ID_C_java_implicitly_generic_class_type);
673 }
674 
679 {
681  return static_cast<const java_implicitly_generic_class_typet &>(type);
682 }
683 
688 {
690  return static_cast<java_implicitly_generic_class_typet &>(type);
691 }
692 
695 class unsupported_java_class_signature_exceptiont:public std::logic_error
696 {
697 public:
699  std::logic_error(
700  "Unsupported class signature: "+type)
701  {
702  }
703 };
704 
706  const std::string &descriptor,
707  const optionalt<std::string> &signature,
708  const std::string &class_name)
709 {
710  try
711  {
712  return java_type_from_string(signature.value(), class_name);
713  }
715  {
716  return java_type_from_string(descriptor, class_name);
717  }
718 }
719 
725  const std::vector<java_generic_parametert> &gen_types,
726  const irep_idt &identifier)
727 {
728  const auto iter = std::find_if(
729  gen_types.cbegin(),
730  gen_types.cend(),
731  [&identifier](const java_generic_parametert &ref)
732  {
733  return ref.type_variable().get_identifier() == identifier;
734  });
735 
736  if(iter == gen_types.cend())
737  {
738  return {};
739  }
740 
741  return std::distance(gen_types.cbegin(), iter);
742 }
743 
745  const std::string &,
746  std::set<irep_idt> &);
748  const typet &,
749  std::set<irep_idt> &);
750 
755 {
756 public:
757  typedef std::vector<reference_typet> generic_typest;
758 
760  const struct_tag_typet &type,
761  const std::string &base_ref,
762  const std::string &class_name_prefix);
763 
765  {
766  return (const generic_typest &)(find(ID_generic_types).get_sub());
767  }
768 
770  {
771  return (generic_typest &)(add(ID_generic_types).get_sub());
772  }
773 
775  generic_type_index(const java_generic_parametert &type) const;
776 };
777 
780 inline bool is_java_generic_struct_tag_type(const typet &type)
781 {
782  return type.get_bool(ID_C_java_generic_symbol);
783 }
784 
787 inline const java_generic_struct_tag_typet &
789 {
791  return static_cast<const java_generic_struct_tag_typet &>(type);
792 }
793 
798 {
800  return static_cast<java_generic_struct_tag_typet &>(type);
801 }
802 
807 std::string erase_type_arguments(const std::string &);
813 std::string gather_full_class_name(const std::string &);
814 
815 // turn java type into string
816 std::string pretty_java_type(const typet &);
817 
818 // pretty signature for methods
819 std::string pretty_signature(const java_method_typet &);
820 
821 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:479
is_java_generic_class_type
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:565
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
java_generic_typet::java_generic_typet
java_generic_typet(const typet &_type)
Definition: java_types.h:488
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
java_generic_parametert::type_variables
type_variablest & type_variables()
Definition: java_types.h:436
class_typet
Class type.
Definition: std_types.h:365
java_generic_typet
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:483
java_generic_typet::generic_type_argumentst
std::vector< reference_typet > generic_type_argumentst
Definition: java_types.h:486
java_method_typet::get_is_final
bool get_is_final() const
Definition: java_types.h:301
java_class_typet::set_is_static_class
void set_is_static_class(const bool &is_static_class)
Definition: java_types.h:149
java_class_typet::set_is_anonymous_class
void set_is_anonymous_class(const bool &is_anonymous_class)
Definition: java_types.h:159
can_cast_type< annotated_typet >
bool can_cast_type< annotated_typet >(const typet &)
Definition: java_types.h:96
java_void_type
typet java_void_type()
Definition: java_types.cpp:37
reference_typet
The reference type.
Definition: std_types.h:1565
java_implicitly_generic_class_typet::implicit_generic_types
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:654
java_generic_class_typet::generic_typest
std::vector< java_generic_parametert > generic_typest
Definition: java_types.h:545
typet
The type of an expression, extends irept.
Definition: type.h:27
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
optional.h
java_annotationt::valuet::get_name
const irep_idt & get_name() const
Definition: java_types.h:33
unsupported_java_class_signature_exceptiont
An exception that is raised for unsupported class signature.
Definition: java_types.h:695
java_class_typet::add_unknown_lambda_method_handle
void add_unknown_lambda_method_handle()
Definition: java_types.h:213
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
to_annotated_type
const annotated_typet & to_annotated_type(const typet &type)
Definition: java_types.h:85
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,.
Definition: java_types.cpp:163
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:173
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
annotated_typet::get_annotations
std::vector< java_annotationt > & get_annotations()
Definition: java_types.h:77
java_method_typet::get_native
bool get_native() const
Definition: java_types.h:311
java_generic_parametert
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
Definition: java_types.h:397
java_short_type
typet java_short_type()
Definition: java_types.cpp:47
exprt
Base class for all expressions.
Definition: expr.h:54
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
java_generic_struct_tag_typet::java_generic_struct_tag_typet
java_generic_struct_tag_typet(const struct_tag_typet &type, const std::string &base_ref, const std::string &class_name_prefix)
Construct a generic symbol type by extending the symbol type type with generic types extracted from t...
Definition: java_types.cpp:924
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:129
invariant.h
can_cast_type< java_generic_typet >
bool can_cast_type< java_generic_typet >(const typet &type)
Definition: java_types.h:510
is_java_implicitly_generic_class_type
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:670
java_generic_parametert::type_variablet
struct_tag_typet type_variablet
Definition: java_types.h:400
to_java_generic_class_type
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:573
pretty_java_type
std::string pretty_java_type(const typet &)
Definition: java_types.cpp:966
java_generic_class_typet::generic_types
generic_typest & generic_types()
Definition: java_types.h:557
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:303
java_method_typet::set_is_varargs
void set_is_varargs(bool is_varargs)
Definition: java_types.h:326
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:148
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:951
java_annotationt::valuet::valuet
valuet(irep_idt name, const exprt &value)
Definition: java_types.h:28
java_generic_struct_tag_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:764
java_generic_class_typet::java_generic_class_typet
java_generic_class_typet()
Definition: java_types.h:547
java_class_typet::get_is_inner_class
bool get_is_inner_class() const
Definition: java_types.h:114
pretty_signature
std::string pretty_signature(const java_method_typet &)
Definition: java_types.cpp:1007
java_generic_parametert::type_variable_ref
type_variablet & type_variable_ref()
Definition: java_types.h:418
type.h
java_class_typet
Definition: java_types.h:101
java_generic_class_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:552
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:592
java_class_typet::get_is_anonymous_class
bool get_is_anonymous_class() const
Definition: java_types.h:154
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
java_annotationt::get_values
const std::vector< valuet > & get_values() const
Definition: java_types.h:54
java_method_typet::set_native
void set_native(bool is_native)
Definition: java_types.h:316
irept::irept
irept()
Definition: irep.h:185
java_generic_parametert::get_name
const irep_idt get_name() const
Definition: java_types.h:424
java_annotationt::java_annotationt
java_annotationt(const typet &type)
Definition: java_types.h:44
java_class_typet::get_annotations
const std::vector< java_annotationt > & get_annotations() const
Definition: java_types.h:219
java_lang_object_type
reference_typet java_lang_object_type()
Definition: java_types.cpp:85
java_annotationt::valuet
Definition: java_types.h:25
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:788
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:495
java_generic_parametert::type_variables
const type_variablest & type_variables() const
Definition: java_types.h:431
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:446
java_array_type
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:94
java_byte_type
typet java_byte_type()
Definition: java_types.cpp:52
java_generic_parametert::java_generic_parametert
java_generic_parametert(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
Definition: java_types.h:402
std_types.h
is_java_generic_struct_tag_type
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:780
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:799
annotated_typet
Definition: java_types.h:67
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition: java_types.h:517
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:637
java_implicitly_generic_class_typet::implicit_generic_types
implicit_generic_typest & implicit_generic_types()
Definition: java_types.h:661
java_type_from_string
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:492
java_generic_typet::generic_type_arguments
generic_type_argumentst & generic_type_arguments()
Definition: java_types.h:502
code_typet
Base type of functions.
Definition: std_types.h:751
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:273
irept::id
const irep_idt & id() const
Definition: irep.h:259
can_cast_type< java_class_typet >
bool can_cast_type< java_class_typet >(const typet &type)
Definition: java_types.h:259
java_method_typet::add_throws_exceptions
void add_throws_exceptions(irep_idt exception)
Definition: java_types.h:296
java_annotationt::get_type
const typet & get_type() const
Definition: java_types.h:49
java_class_typet::get_final
bool get_final() const
Definition: java_types.h:164
java_type_from_char
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
Definition: java_types.cpp:188
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:524
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
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:207
java_class_typet::set_final
void set_final(bool is_final)
Definition: java_types.h:169
java_class_typet::set_outer_class
void set_outer_class(const irep_idt &outer_class)
Definition: java_types.h:129
java_class_typet::java_lambda_method_handlest
irept::subt java_lambda_method_handlest
Definition: java_types.h:196
java_annotationt::valuet::get_value
const exprt & get_value() const
Definition: java_types.h:38
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:233
java_class_typet::get_annotations
std::vector< java_annotationt > & get_annotations()
Definition: java_types.h:225
java_class_typet::set_super_class
void set_super_class(const irep_idt &super_class)
Definition: java_types.h:139
java_generic_struct_tag_typet::generic_typest
std::vector< reference_typet > generic_typest
Definition: java_types.h:757
java_method_typet::set_is_final
void set_is_final(bool is_final)
Definition: java_types.h:306
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:621
java_class_typet::lambda_method_handles
java_lambda_method_handlest & lambda_method_handles()
Definition: java_types.h:203
java_class_typet::set_access
void set_access(const irep_idt &access)
Definition: java_types.h:109
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:762
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
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:642
to_java_generic_parameter
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:453
java_reference_type
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
java_implicitly_generic_class_typet::implicit_generic_typest
std::vector< java_generic_parametert > implicit_generic_typest
Definition: java_types.h:640
java_class_typet::get_outer_class
const irep_idt & get_outer_class() const
Definition: java_types.h:124
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
java_class_typet::set_is_stub
void set_is_stub(const bool &is_stub)
Definition: java_types.h:174
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:607
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
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:872
java_generic_struct_tag_typet::generic_types
generic_typest & generic_types()
Definition: java_types.h:769
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:454
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:675
java_annotationt::get_values
std::vector< valuet > & get_values()
Definition: java_types.h:60
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:272
java_class_typet::add_lambda_method_handle
void add_lambda_method_handle(const irep_idt &identifier)
Definition: java_types.h:208
java_class_typet::set_is_inner_class
void set_is_inner_class(const bool &is_inner_class)
Definition: java_types.h:119
java_float_type
typet java_float_type()
Definition: java_types.cpp:62
irept::get_sub
subt & get_sub()
Definition: irep.h:317
java_char_type
typet java_char_type()
Definition: java_types.cpp:57
code_typet::parametert
Definition: std_types.h:788
can_cast_type< java_method_typet >
bool can_cast_type< java_method_typet >(const typet &type)
Definition: java_types.h:333
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:240
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:678
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:282
java_generic_struct_tag_typet
Type for a generic symbol, extends struct_tag_typet with a vector of java generic types.
Definition: java_types.h:754
java_method_typet::get_is_varargs
bool get_is_varargs() const
Definition: java_types.h:321
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
java_type_from_string_with_exception
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:705
unsupported_java_class_signature_exceptiont::unsupported_java_class_signature_exceptiont
unsupported_java_class_signature_exceptiont(std::string type)
Definition: java_types.h:698
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:542
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
java_class_typet::get_super_class
const irep_idt & get_super_class() const
Definition: java_types.h:134
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:179
annotated_typet::get_annotations
const std::vector< java_annotationt > & get_annotations() const
Definition: java_types.h:70
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:396
java_int_type
typet java_int_type()
Definition: java_types.cpp:32
java_boolean_type
typet java_boolean_type()
Definition: java_types.cpp:72
java_class_typet::lambda_method_handles
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:198
java_classname
struct_tag_typet java_classname(const std::string &)
Definition: java_types.cpp:734
irept::subt
std::vector< irept > subt
Definition: irep.h:160
java_generic_parametert::type_variablest
std::vector< type_variablet > type_variablest
Definition: java_types.h:430
std_expr.h
java_double_type
typet java_double_type()
Definition: java_types.cpp:67
java_class_typet::get_access
const irep_idt & get_access() const
Definition: java_types.h:104
java_annotationt
Definition: java_types.h:22
java_method_typet
Definition: java_types.h:264
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:724
c_types.h
java_method_typet::throws_exceptions
const std::vector< irep_idt > throws_exceptions() const
Definition: java_types.h:288
java_generic_parametert::type_variable
const type_variablet & type_variable() const
Definition: java_types.h:412
java_long_type
typet java_long_type()
Definition: java_types.cpp:42
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:357
java_class_typet::get_is_static_class
bool get_is_static_class() const
Definition: java_types.h:144
java_char_from_type
char java_char_from_type(const typet &type)
Definition: java_types.cpp:634