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  const 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  const 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 
154  const bool get_is_anonymous_class() const
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()
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  typedef std::vector<symbol_exprt> java_lambda_method_handlest;
175 
177  {
178  return (const java_lambda_method_handlest &)find(
179  ID_java_lambda_method_handles)
180  .get_sub();
181  }
182 
184  {
185  return (java_lambda_method_handlest &)add(ID_java_lambda_method_handles)
186  .get_sub();
187  }
188 
189  void add_lambda_method_handle(const irep_idt &identifier)
190  {
191  // creates a symbol_exprt for the identifier and pushes it in the vector
192  lambda_method_handles().emplace_back(identifier);
193  }
195  {
196  // creates empty symbol_exprt and pushes it in the vector
197  lambda_method_handles().emplace_back();
198  }
199 
200  const std::vector<java_annotationt> &get_annotations() const
201  {
202  return static_cast<const annotated_typet &>(
203  static_cast<const typet &>(*this)).get_annotations();
204  }
205 
206  std::vector<java_annotationt> &get_annotations()
207  {
209  static_cast<typet &>(*this)).get_annotations();
210  }
211 
214  const irep_idt &get_name() const
215  {
216  return get(ID_name);
217  }
218 
221  void set_name(const irep_idt &name)
222  {
223  set(ID_name, name);
224  }
225 };
226 
227 inline const java_class_typet &to_java_class_type(const typet &type)
228 {
229  assert(type.id()==ID_struct);
230  return static_cast<const java_class_typet &>(type);
231 }
232 
234 {
235  assert(type.id()==ID_struct);
236  return static_cast<java_class_typet &>(type);
237 }
238 
239 template <>
240 inline bool can_cast_type<java_class_typet>(const typet &type)
241 {
242  return can_cast_type<class_typet>(type);
243 }
244 
246 {
247 public:
250 
254  java_method_typet(parameterst &&_parameters, typet &&_return_type)
255  : code_typet(std::move(_parameters), std::move(_return_type))
256  {
257  set(ID_C_java_method_type, true);
258  }
259 
263  java_method_typet(parameterst &&_parameters, const typet &_return_type)
264  : code_typet(std::move(_parameters), _return_type)
265  {
266  set(ID_C_java_method_type, true);
267  }
268 
269  const std::vector<irep_idt> throws_exceptions() const
270  {
271  std::vector<irep_idt> exceptions;
272  for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
273  exceptions.push_back(e.id());
274  return exceptions;
275  }
276 
278  {
279  add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
280  }
281 };
282 
283 template <>
284 inline bool can_cast_type<java_method_typet>(const typet &type)
285 {
286  return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
287 }
288 
289 inline const java_method_typet &to_java_method_type(const typet &type)
290 {
292  return static_cast<const java_method_typet &>(type);
293 }
294 
296 {
298  return static_cast<java_method_typet &>(type);
299 }
300 
311 symbol_typet java_classname(const std::string &);
312 
313 reference_typet java_array_type(const char subtype);
314 const typet &java_array_element_type(const symbol_typet &array_symbol);
316 bool is_java_array_type(const typet &type);
317 bool is_multidim_java_array_type(const typet &type);
318 
319 typet java_type_from_char(char t);
321  const std::string &,
322  const std::string &class_name_prefix="");
323 char java_char_from_type(const typet &type);
324 std::vector<typet> java_generic_type_from_string(
325  const std::string &,
326  const std::string &);
327 
331  const std::string src,
332  size_t starting_point = 0);
333 
334 
335 bool is_java_array_tag(const irep_idt &tag);
336 bool is_valid_java_array(const struct_typet &);
337 
338 bool equal_java_types(const typet &type1, const typet &type2);
339 
344 {
345 public:
347 
349  const irep_idt &_type_var_name,
350  const symbol_typet &_bound):
352  {
353  set(ID_C_java_generic_parameter, true);
354  type_variables().push_back(symbol_typet(_type_var_name));
355  }
356 
359  {
360  PRECONDITION(!type_variables().empty());
361  return type_variables().front();
362  }
363 
365  {
366  PRECONDITION(!type_variables().empty());
367  return const_cast<type_variablet &>(type_variables().front());
368  }
369 
370  const irep_idt get_name() const
371  {
372  return type_variable().get_identifier();
373  }
374 
375 private:
376  typedef std::vector<type_variablet> type_variablest;
378  {
379  return (const type_variablest &)(find(ID_type_variables).get_sub());
380  }
381 
383  {
384  return (type_variablest &)(add(ID_type_variables).get_sub());
385  }
386 };
387 
392 inline bool is_java_generic_parameter(const typet &type)
393 {
394  return type.get_bool(ID_C_java_generic_parameter);
395 }
396 
400  const typet &type)
401 {
403  return static_cast<const java_generic_parametert &>(type);
404 }
405 
409 {
411  return static_cast<java_generic_parametert &>(type);
412 }
413 
430 {
431 public:
432  typedef std::vector<reference_typet> generic_type_argumentst;
433 
434  explicit java_generic_typet(const typet &_type):
436  {
437  set(ID_C_java_generic_type, true);
438  }
439 
442  {
443  return (const generic_type_argumentst &)(
444  find(ID_type_variables).get_sub());
445  }
446 
449  {
450  return (generic_type_argumentst &)(
451  add(ID_type_variables).get_sub());
452  }
453 };
454 
457 inline bool is_java_generic_type(const typet &type)
458 {
459  return type.get_bool(ID_C_java_generic_type);
460 }
461 
465  const typet &type)
466 {
467  PRECONDITION(
468  type.id()==ID_pointer &&
469  is_java_generic_type(type));
470  return static_cast<const java_generic_typet &>(type);
471 }
472 
476 {
477  PRECONDITION(
478  type.id()==ID_pointer &&
479  is_java_generic_type(type));
480  return static_cast<java_generic_typet &>(type);
481 }
482 
487 {
488  public:
489  typedef std::vector<java_generic_parametert> generic_typest;
490 
492  {
493  set(ID_C_java_generics_class_type, true);
494  }
495 
497  {
498  return (const generic_typest &)(find(ID_generic_types).get_sub());
499  }
500 
502  {
503  return (generic_typest &)(add(ID_generic_types).get_sub());
504  }
505 };
506 
509 inline bool is_java_generic_class_type(const typet &type)
510 {
511  return type.get_bool(ID_C_java_generics_class_type);
512 }
513 
516 inline const java_generic_class_typet &
518 {
520  return static_cast<const java_generic_class_typet &>(type);
521 }
522 
527 {
529  return static_cast<java_generic_class_typet &>(type);
530 }
531 
537  size_t index,
538  const java_generic_typet &type)
539 {
540  const std::vector<reference_typet> &type_arguments =
541  type.generic_type_arguments();
542  PRECONDITION(index<type_arguments.size());
543  return type_arguments[index];
544 }
545 
550 inline const irep_idt &
552 {
553  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
554 
555  PRECONDITION(index<gen_types.size());
556  const java_generic_parametert &gen_type=gen_types[index];
557 
558  return gen_type.type_variable().get_identifier();
559 }
560 
565 inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
566 {
568  const java_generic_class_typet &type =
570  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
571 
572  PRECONDITION(index<gen_types.size());
573  const java_generic_parametert &gen_type=gen_types[index];
574 
575  return gen_type.subtype();
576 }
577 
582 {
583 public:
584  typedef std::vector<java_generic_parametert> implicit_generic_typest;
585 
587  const java_class_typet &class_type,
588  const implicit_generic_typest &generic_types)
589  : java_class_typet(class_type)
590  {
591  set(ID_C_java_implicitly_generic_class_type, true);
592  for(const auto &type : generic_types)
593  {
594  implicit_generic_types().push_back(type);
595  }
596  }
597 
599  {
600  return (
602  &)(find(ID_implicit_generic_types).get_sub());
603  }
604 
606  {
607  return (
608  implicit_generic_typest &)(add(ID_implicit_generic_types).get_sub());
609  }
610 };
611 
615 {
616  return type.get_bool(ID_C_java_implicitly_generic_class_type);
617 }
618 
623 {
625  return static_cast<const java_implicitly_generic_class_typet &>(type);
626 }
627 
632 {
634  return static_cast<java_implicitly_generic_class_typet &>(type);
635 }
636 
639 class unsupported_java_class_signature_exceptiont:public std::logic_error
640 {
641 public:
643  std::logic_error(
644  "Unsupported class signature: "+type)
645  {
646  }
647 };
648 
650  const std::string &descriptor,
651  const optionalt<std::string> &signature,
652  const std::string &class_name)
653 {
654  try
655  {
656  return java_type_from_string(signature.value(), class_name);
657  }
659  {
660  return java_type_from_string(descriptor, class_name);
661  }
662 }
663 
669  const std::vector<java_generic_parametert> &gen_types,
670  const irep_idt &identifier)
671 {
672  const auto iter = std::find_if(
673  gen_types.cbegin(),
674  gen_types.cend(),
675  [&identifier](const java_generic_parametert &ref)
676  {
677  return ref.type_variable().get_identifier() == identifier;
678  });
679 
680  if(iter == gen_types.cend())
681  {
682  return {};
683  }
684 
685  return std::distance(gen_types.cbegin(), iter);
686 }
687 
689  const std::string &,
690  std::set<irep_idt> &);
692  const typet &,
693  std::set<irep_idt> &);
694 
699 {
700 public:
701  typedef std::vector<reference_typet> generic_typest;
702 
704  const symbol_typet &type,
705  const std::string &base_ref,
706  const std::string &class_name_prefix);
707 
709  {
710  return (const generic_typest &)(find(ID_generic_types).get_sub());
711  }
712 
714  {
715  return (generic_typest &)(add(ID_generic_types).get_sub());
716  }
717 
719  generic_type_index(const java_generic_parametert &type) const;
720 };
721 
724 inline bool is_java_generic_symbol_type(const typet &type)
725 {
726  return type.get_bool(ID_C_java_generic_symbol);
727 }
728 
731 inline const java_generic_symbol_typet &
733 {
735  return static_cast<const java_generic_symbol_typet &>(type);
736 }
737 
741 {
743  return static_cast<java_generic_symbol_typet &>(type);
744 }
745 
750 std::string erase_type_arguments(const std::string &);
756 std::string gather_full_class_name(const std::string &);
757 
758 // turn java type into string
759 std::string pretty_java_type(const typet &);
760 
761 // pretty signature for methods
762 std::string pretty_signature(const java_method_typet &);
763 
764 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
std::vector< java_annotationt > & get_annotations()
Definition: java_types.h:206
The type of an expression.
Definition: type.h:22
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:221
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:652
unsupported_java_class_signature_exceptiont(std::string type)
Definition: java_types.h:642
std::vector< java_generic_parametert > implicit_generic_typest
Definition: java_types.h:584
char java_char_from_type(const typet &type)
Definition: java_types.cpp:611
java_implicitly_generic_class_typet(const java_class_typet &class_type, const implicit_generic_typest &generic_types)
Definition: java_types.h:586
Base type of functions.
Definition: std_types.h:764
symbol_typet type_variablet
Definition: java_types.h:346
std::vector< symbol_exprt > java_lambda_method_handlest
Definition: java_types.h:174
std::vector< valuet > & get_values()
Definition: java_types.h:60
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:924
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
const irep_idt & get_outer_class() const
Definition: java_types.h:124
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
Definition: java_types.cpp:148
void add_lambda_method_handle(const irep_idt &identifier)
Definition: java_types.h:189
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:176
bool is_java_generic_symbol_type(const typet &type)
Definition: java_types.h:724
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:517
typet java_char_type()
Definition: java_types.cpp:57
generic_typest & generic_types()
Definition: java_types.h:713
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:392
typet java_double_type()
Definition: java_types.cpp:67
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:565
std::vector< parametert > parameterst
Definition: std_types.h:767
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:399
void set_final(bool is_final)
Definition: java_types.h:169
typet java_float_type()
Definition: java_types.cpp:62
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Definition: expr_cast.h:198
std::string pretty_java_type(const typet &)
Definition: java_types.cpp:939
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:847
An exception that is raised for unsupported class signature.
Definition: java_types.h:639
STL namespace.
typet java_byte_type()
Definition: java_types.cpp:52
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:214
java_generic_typet(const typet &_type)
Definition: java_types.h:434
Structure type.
Definition: std_types.h:297
const std::vector< irep_idt > throws_exceptions() const
Definition: java_types.h:269
void set_access(const irep_idt &access)
Definition: java_types.h:109
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
java_generic_parametert(const irep_idt &_type_var_name, const symbol_typet &_bound)
Definition: java_types.h:348
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:738
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:432
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:470
subt & get_sub()
Definition: irep.h:317
valuet(irep_idt name, const exprt &value)
Definition: java_types.h:28
const irep_idt & get_super_class() const
Definition: java_types.h:134
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:441
java_method_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e.
Definition: java_types.h:254
const irep_idt & id() const
Definition: irep.h:259
typet java_short_type()
Definition: java_types.cpp:47
void set_outer_class(const irep_idt &outer_class)
Definition: java_types.h:129
const java_generic_symbol_typet & to_java_generic_symbol_type(const typet &type)
Definition: java_types.h:732
void set_super_class(const irep_idt &super_class)
Definition: java_types.h:139
const type_variablet & type_variable() const
Definition: java_types.h:358
std::vector< reference_typet > generic_type_argumentst
Definition: java_types.h:432
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:174
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:486
const irep_idt & get_access() const
Definition: java_types.h:104
java_lambda_method_handlest & lambda_method_handles()
Definition: java_types.h:183
void add_throws_exceptions(irep_idt exception)
Definition: java_types.h:277
std::vector< reference_typet > generic_typest
Definition: java_types.h:701
const exprt & get_value() const
Definition: java_types.h:38
A reference into the symbol table.
Definition: std_types.h:110
void set_is_inner_class(const bool &is_inner_class)
Definition: java_types.h:119
implicit_generic_typest & implicit_generic_types()
Definition: java_types.h:605
typet java_long_type()
Definition: java_types.cpp:42
typet java_int_type()
Definition: java_types.cpp:32
const std::vector< java_annotationt > & get_annotations() const
Definition: java_types.h:70
symbol_typet java_classname(const std::string &)
Definition: java_types.cpp:710
nonstd::optional< T > optionalt
Definition: optional.h:35
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
Definition: java_types.h:622
API to expression classes.
std::string pretty_signature(const java_method_typet &)
Definition: java_types.cpp:977
bool can_cast_type< java_class_typet >(const typet &type)
Definition: java_types.h:240
const typet & java_array_element_type(const symbol_typet &array_symbol)
Return a const reference to the element type of a given java array type.
Definition: java_types.cpp:129
typet java_bytecode_promotion(const typet &)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:208
void add_unknown_lambda_method_handle()
Definition: java_types.h:194
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const generic_typest & generic_types() const
Definition: java_types.h:708
Base class for tree-like data structures with sharing.
Definition: irep.h:156
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:509
bool can_cast_type< annotated_typet >(const typet &)
Definition: java_types.h:96
Type for a generic symbol, extends symbol_typet with a vector of java generic types.
Definition: java_types.h:698
irept()
Definition: irep.h:185
bool can_cast_type< java_method_typet >(const typet &type)
Definition: java_types.h:284
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:551
reference_typet java_lang_object_type()
Definition: java_types.cpp:85
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:598
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:536
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:649
The reference type.
Definition: std_types.h:1492
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:429
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:273
const irep_idt & get_name() const
Definition: java_types.h:33
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:464
const type_variablest & type_variables() const
Definition: java_types.h:377
API to type classes.
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:289
std::vector< type_variablet > type_variablest
Definition: java_types.h:376
type_variablest & type_variables()
Definition: java_types.h:382
Base class for all expressions.
Definition: expr.h:42
void set_is_static_class(const bool &is_static_class)
Definition: java_types.h:149
std::vector< java_annotationt > & get_annotations()
Definition: java_types.h:77
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:775
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>...
Definition: java_types.h:343
typet java_boolean_type()
Definition: java_types.cpp:72
void set_is_anonymous_class(const bool &is_anonymous_class)
Definition: java_types.h:159
const irep_idt get_name() const
Definition: java_types.h:370
java_method_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e.
Definition: java_types.h:263
java_annotationt(const typet &type)
Definition: java_types.h:44
irept & add(const irep_namet &name)
Definition: irep.cpp:306
std::string gather_full_class_name(const std::string &)
Returns the full class name, skipping over the generics.
Definition: java_types.cpp:304
generic_typest & generic_types()
Definition: java_types.h:501
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:668
generic_type_argumentst & generic_type_arguments()
Definition: java_types.h:448
const std::vector< valuet > & get_values() const
Definition: java_types.h:54
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
Definition: java_types.cpp:189
const bool get_is_static_class() const
Definition: java_types.h:144
bool is_java_generic_type(const typet &type)
Definition: java_types.h:457
java_generic_symbol_typet(const symbol_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:899
const bool get_is_inner_class() const
Definition: java_types.h:114
C++ class type.
Definition: std_types.h:341
const typet & get_type() const
Definition: java_types.h:49
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
const bool get_is_anonymous_class() const
Definition: java_types.h:154
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:614
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:94
const std::vector< java_annotationt > & get_annotations() const
Definition: java_types.h:200
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:581
type_variablet & type_variable_ref()
Definition: java_types.h:364
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const annotated_typet & to_annotated_type(const typet &type)
Definition: java_types.h:85
bool can_cast_type< class_typet >(const typet &type)
Definition: std_types.h:451
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:227
const irep_idt & get_identifier() const
Definition: std_types.h:123
const generic_typest & generic_types() const
Definition: java_types.h:496
std::vector< java_generic_parametert > generic_typest
Definition: java_types.h:489