cprover
Loading...
Searching...
No Matches
java_types.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
21class java_annotationt : public irept
22{
23public:
24 class valuet : public irept
25 {
26 public:
27 valuet(irep_idt name, const exprt &value) : irept(name)
28 {
29 get_sub().push_back(value);
30 }
31
32 const irep_idt &get_name() const
33 {
34 return id();
35 }
36
37 const exprt &get_value() const
38 {
39 return static_cast<const exprt &>(get_sub().front());
40 }
41 };
42
43 explicit java_annotationt(const typet &type)
44 {
45 set(ID_type, type);
46 }
47
48 const typet &get_type() const
49 {
50 return static_cast<const typet &>(find(ID_type));
51 }
52
53 const std::vector<valuet> &get_values() const
54 {
55 // This cast should be safe as valuet doesn't add data to irept
56 return reinterpret_cast<const std::vector<valuet> &>(get_sub());
57 }
58
59 std::vector<valuet> &get_values()
60 {
61 // This cast should be safe as valuet doesn't add data to irept
62 return reinterpret_cast<std::vector<valuet> &>(get_sub());
63 }
64};
65
66class annotated_typet : public typet
67{
68public:
69 const std::vector<java_annotationt> &get_annotations() const
70 {
71 // This cast should be safe as java_annotationt doesn't add data to irept
72 return reinterpret_cast<const std::vector<java_annotationt> &>(
74 }
75
76 std::vector<java_annotationt> &get_annotations()
77 {
78 // This cast should be safe as java_annotationt doesn't add data to irept
79 return reinterpret_cast<std::vector<java_annotationt> &>(
81 }
82};
83
84inline const annotated_typet &to_annotated_type(const typet &type)
85{
86 return static_cast<const annotated_typet &>(type);
87}
88
90{
91 return static_cast<annotated_typet &>(type);
92}
93
94template <>
96{
97 return true;
98}
99
101{
102public:
105
114
123
124 const std::vector<irep_idt> throws_exceptions() const
125 {
126 std::vector<irep_idt> exceptions;
127 for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
128 exceptions.push_back(e.id());
129 return exceptions;
130 }
131
133 {
134 add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
135 }
136
137 bool get_is_final() const
138 {
139 return get_bool(ID_final);
140 }
141
142 void set_is_final(bool is_final)
143 {
144 set(ID_final, is_final);
145 }
146
147 bool get_native() const
148 {
150 }
151
152 void set_native(bool is_native)
153 {
154 set(ID_is_native_method, is_native);
155 }
156
157 bool get_is_varargs() const
158 {
160 }
161
162 void set_is_varargs(bool is_varargs)
163 {
164 set(ID_is_varargs_method, is_varargs);
165 }
166
167 bool is_synthetic() const
168 {
169 return get_bool(ID_synthetic);
170 }
171
176};
177
178template <>
180{
181 return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
182}
183
185{
187 return static_cast<const java_method_typet &>(type);
188}
189
191{
193 return static_cast<java_method_typet &>(type);
194}
195
197{
198public:
199 class componentt : public class_typet::componentt
200 {
201 public:
202 componentt() = default;
203
205 : class_typet::componentt(_name, std::move(_type))
206 {
207 }
208
210 bool get_is_final() const
211 {
212 return get_bool(ID_final);
213 }
214
216 void set_is_final(const bool is_final)
217 {
218 set(ID_final, is_final);
219 }
220 };
221
222 using componentst = std::vector<componentt>;
223
224 const componentst &components() const
225 {
226 return (const componentst &)(find(ID_components).get_sub());
227 }
228
230 {
231 return (componentst &)(add(ID_components).get_sub());
232 }
233
234 const componentt &get_component(const irep_idt &component_name) const
235 {
236 return static_cast<const componentt &>(
237 class_typet::get_component(component_name));
238 }
239
241 {
242 public:
243 methodt() = delete;
244
246 : class_typet::methodt(_name, std::move(_type))
247 {
248 }
249
250 const java_method_typet &type() const
251 {
252 return static_cast<const java_method_typet &>(
253 class_typet::methodt::type());
254 }
255
257 {
258 return static_cast<java_method_typet &>(class_typet::methodt::type());
259 }
260
262 bool get_is_final() const
263 {
264 return get_bool(ID_final);
265 }
266
268 void set_is_final(const bool is_final)
269 {
270 set(ID_final, is_final);
271 }
272
274 bool get_is_native() const
275 {
277 }
278
280 void set_is_native(const bool is_native)
281 {
282 set(ID_is_native_method, is_native);
283 }
284
287 {
289 }
290
292 void set_descriptor(const irep_idt &id)
293 {
295 }
296 };
297
298 using methodst = std::vector<methodt>;
299
300 const methodst &methods() const
301 {
302 return (const methodst &)(find(ID_methods).get_sub());
303 }
304
306 {
307 return (methodst &)(add(ID_methods).get_sub());
308 }
309
311 using static_memberst = std::vector<componentt>;
312
314 {
316 }
317
322
323 const irep_idt &get_access() const
324 {
325 return get(ID_access);
326 }
327
329 {
330 return set(ID_access, access);
331 }
332
334 {
336 }
337
338 void set_is_inner_class(const bool &is_inner_class)
339 {
340 return set(ID_is_inner_class, is_inner_class);
341 }
342
344 {
345 return get(ID_outer_class);
346 }
347
348 void set_outer_class(const irep_idt &outer_class)
349 {
350 return set(ID_outer_class, outer_class);
351 }
352
354 {
355 return get(ID_super_class);
356 }
357
358 void set_super_class(const irep_idt &super_class)
359 {
360 return set(ID_super_class, super_class);
361 }
362
364 {
365 return get_bool(ID_is_static);
366 }
367
368 void set_is_static_class(const bool &is_static_class)
369 {
370 return set(ID_is_static, is_static_class);
371 }
372
374 {
376 }
377
378 void set_is_anonymous_class(const bool &is_anonymous_class)
379 {
380 return set(ID_is_anonymous, is_anonymous_class);
381 }
382
383 bool get_final() const
384 {
385 return get_bool(ID_final);
386 }
387
388 void set_final(bool is_final)
389 {
390 set(ID_final, is_final);
391 }
392
394 {
396 }
397
398 bool get_is_stub() const
399 {
401 }
402
405 {
406 return get_bool(ID_enumeration);
407 }
408
414
416 bool get_abstract() const
417 {
418 return get_bool(ID_abstract);
419 }
420
422 void set_abstract(bool abstract)
423 {
424 set(ID_abstract, abstract);
425 }
426
428 bool get_synthetic() const
429 {
430 return get_bool(ID_synthetic);
431 }
432
435 {
437 }
438
440 bool get_is_annotation() const
441 {
443 }
444
446 void set_is_annotation(bool is_annotation)
447 {
448 set(ID_is_annotation, is_annotation);
449 }
450
452 bool get_interface() const
453 {
454 return get_bool(ID_interface);
455 }
456
459 {
461 }
462
475
482 {
483 public:
485 const class_method_descriptor_exprt &method_descriptor,
486 method_handle_kindt handle_kind)
487 {
488 set(ID_object_descriptor, method_descriptor);
489 set(ID_handle_type, static_cast<int>(handle_kind));
490 }
491
497
503
508
513 };
514
515 using java_lambda_method_handlest = std::vector<java_lambda_method_handlet>;
516
523
529
531 const class_method_descriptor_exprt &method_descriptor,
532 method_handle_kindt handle_kind)
533 {
534 // creates a symbol_exprt for the identifier and pushes it in the vector
535 lambda_method_handles().emplace_back(method_descriptor, handle_kind);
536 }
538 {
539 // creates empty symbol_exprt and pushes it in the vector
540 lambda_method_handles().emplace_back();
541 }
542
543 const std::vector<java_annotationt> &get_annotations() const
544 {
545 return static_cast<const annotated_typet &>(
546 static_cast<const typet &>(*this)).get_annotations();
547 }
548
549 std::vector<java_annotationt> &get_annotations()
550 {
552 static_cast<typet &>(*this)).get_annotations();
553 }
554
557 const irep_idt &get_name() const
558 {
559 return get(ID_name);
560 }
561
564 void set_name(const irep_idt &name)
565 {
566 set(ID_name, name);
567 }
568
571 {
572 return get(ID_inner_name);
573 }
574
576 void set_inner_name(const irep_idt &name)
577 {
578 set(ID_inner_name, name);
579 }
580};
581
582inline const java_class_typet &to_java_class_type(const typet &type)
583{
584 assert(type.id()==ID_struct);
585 return static_cast<const java_class_typet &>(type);
586}
587
589{
590 assert(type.id()==ID_struct);
591 return static_cast<java_class_typet &>(type);
592}
593
594template <>
596{
597 return can_cast_type<class_typet>(type);
598}
599
603{
604public:
607 std::size_t _width)
609 {
610 }
611
613 {
614 return static_cast<struct_tag_typet &>(reference_typet::subtype());
615 }
616
618 {
619 return static_cast<const struct_tag_typet &>(reference_typet::subtype());
620 }
621};
622
623template <>
625{
626 return type.id() == ID_pointer &&
628}
629
631{
633 return static_cast<const java_reference_typet &>(type);
634}
635
641
654struct_tag_typet java_classname(const std::string &);
655
656#define JAVA_REFERENCE_ARRAY_CLASSID "java::array[reference]"
657
658java_reference_typet java_array_type(const char subtype);
661const typet &java_array_element_type(const struct_tag_typet &array_symbol);
663bool is_java_array_type(const typet &type);
664bool is_multidim_java_array_type(const typet &type);
665
666std::pair<typet, std::size_t>
668
669#define JAVA_ARRAY_DIMENSION_FIELD_NAME "@array_dimensions"
671#define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME "@element_class_identifier"
673
676 const std::string &,
677 const std::string &class_name_prefix = "");
678char java_char_from_type(const typet &type);
679std::vector<typet> java_generic_type_from_string(
680 const std::string &,
681 const std::string &);
682
686 const std::string src,
687 size_t starting_point = 0);
688
689std::vector<std::string> parse_raw_list_types(
690 std::string src,
691 char opening_bracket,
692 char closing_bracket);
693
694bool is_java_array_tag(const irep_idt &tag);
696
697bool equal_java_types(const typet &type1, const typet &type2);
698
703{
704public:
706
715
718 {
719 PRECONDITION(!type_variables().empty());
720 return type_variables().front();
721 }
722
724 {
725 PRECONDITION(!type_variables().empty());
726 return type_variables().front();
727 }
728
729 const irep_idt get_name() const
730 {
731 return type_variable().get_identifier();
732 }
733
734private:
735 typedef std::vector<type_variablet> type_variablest;
737 {
738 return (const type_variablest &)(find(ID_type_variables).get_sub());
739 }
740
745};
746
751inline bool is_java_generic_parameter_tag(const typet &type)
752{
754}
755
758inline const java_generic_parameter_tagt &
760{
762 return static_cast<const java_generic_parameter_tagt &>(type);
763}
764
772
804
809template <>
815
820inline bool is_java_generic_parameter(const typet &type)
821{
823}
824
828 const typet &type)
829{
831 return static_cast<const java_generic_parametert &>(type);
832}
833
841
858{
859public:
860 typedef std::vector<reference_typet> generic_typest;
861
863 : struct_tag_typet(type)
864 {
866 }
867
869 const struct_tag_typet &type,
870 const std::string &base_ref,
871 const std::string &class_name_prefix);
872
874 {
875 return (const generic_typest &)(find(ID_generic_types).get_sub());
876 }
877
882
885};
886
890{
892}
893
898{
900 return static_cast<const java_generic_struct_tag_typet &>(type);
901}
902
911
937
938template <>
940{
941 return is_reference(type) &&
943}
944
947inline bool is_java_generic_type(const typet &type)
948{
950}
951
955 const typet &type)
956{
958 return static_cast<const java_generic_typet &>(type);
959}
960
964{
966 return static_cast<java_generic_typet &>(type);
967}
968
973{
974 public:
975 typedef std::vector<java_generic_parametert> generic_typest;
976
981
983 {
984 return (const generic_typest &)(find(ID_generic_types).get_sub());
985 }
986
991};
992
995inline bool is_java_generic_class_type(const typet &type)
996{
998}
999
1002inline const java_generic_class_typet &
1004{
1006 return static_cast<const java_generic_class_typet &>(type);
1007}
1008
1017
1023 size_t index,
1024 const java_generic_typet &type)
1025{
1026 const std::vector<reference_typet> &type_arguments =
1028 PRECONDITION(index<type_arguments.size());
1029 return type_arguments[index];
1030}
1031
1036inline const irep_idt &
1038{
1039 const std::vector<java_generic_parametert> &gen_types=type.generic_types();
1040
1041 PRECONDITION(index<gen_types.size());
1043
1044 return gen_type.type_variable().get_identifier();
1045}
1046
1051inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
1052{
1054 const java_generic_class_typet &type =
1056 const std::vector<java_generic_parametert> &gen_types=type.generic_types();
1057
1058 PRECONDITION(index<gen_types.size());
1060
1061 return gen_type.base_type();
1062}
1063
1068{
1069public:
1070 typedef std::vector<java_generic_parametert> implicit_generic_typest;
1071
1074 const implicit_generic_typest &generic_types)
1076 {
1078 for(const auto &type : generic_types)
1079 {
1080 implicit_generic_types().push_back(type);
1081 }
1082 }
1083
1085 {
1086 return (
1089 }
1090
1096};
1097
1104
1113
1122
1126std::vector<java_generic_parametert>
1128
1132{
1133public:
1135 std::logic_error(
1136 "Unsupported class signature: "+type)
1137 {
1138 }
1139};
1140
1142 const std::string &descriptor,
1143 const optionalt<std::string> &signature,
1144 const std::string &class_name)
1145{
1146 try
1147 {
1148 return java_type_from_string(signature.value(), class_name);
1149 }
1151 {
1152 return java_type_from_string(descriptor, class_name);
1153 }
1154}
1155
1161 const std::vector<java_generic_parametert> &gen_types,
1162 const irep_idt &identifier)
1163{
1164 const auto iter = std::find_if(
1165 gen_types.cbegin(),
1166 gen_types.cend(),
1167 [&identifier](const java_generic_parametert &ref)
1168 {
1169 return ref.type_variable().get_identifier() == identifier;
1170 });
1171
1172 if(iter == gen_types.cend())
1173 {
1174 return {};
1175 }
1176
1177 return narrow_cast<size_t>(std::distance(gen_types.cbegin(), iter));
1178}
1179
1181 const std::string &,
1182 std::set<irep_idt> &);
1184 const typet &,
1185 std::set<irep_idt> &);
1186
1191std::string erase_type_arguments(const std::string &);
1197std::string gather_full_class_name(const std::string &);
1198
1199// turn java type into string
1200std::string pretty_java_type(const typet &);
1201
1202// pretty signature for methods
1203std::string pretty_signature(const java_method_typet &);
1204
1205#endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
void base_type(typet &type, const namespacet &ns)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
std::vector< java_annotationt > & get_annotations()
Definition java_types.h:76
const std::vector< java_annotationt > & get_annotations() const
Definition java_types.h:69
The C/C++ Booleans.
Definition c_types.h:75
An expression describing a method on a class.
Definition std_expr.h:3272
const irep_idt & get_identifier() const
A unique identifier of the combination of class and method overload to which this expression refers.
Definition std_expr.h:3332
Class type.
Definition std_types.h:325
componentt methodt
Definition std_types.h:332
const static_memberst & static_members() const
Definition std_types.h:348
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:54
Fixed-width bit-vector with IEEE floating-point interpretation.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
irept()=default
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
subt & get_sub()
Definition irep.h:456
signed int get_int(const irep_idt &name) const
Definition irep.cpp:63
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:116
valuet(irep_idt name, const exprt &value)
Definition java_types.h:27
const irep_idt & get_name() const
Definition java_types.h:32
const exprt & get_value() const
Definition java_types.h:37
const typet & get_type() const
Definition java_types.h:48
java_annotationt(const typet &type)
Definition java_types.h:43
const std::vector< valuet > & get_values() const
Definition java_types.h:53
std::vector< valuet > & get_values()
Definition java_types.h:59
void set_is_final(const bool is_final)
is a field 'final'?
Definition java_types.h:216
componentt(const irep_idt &_name, typet _type)
Definition java_types.h:204
bool get_is_final() const
is a field 'final'?
Definition java_types.h:210
Represents a lambda call to a method.
Definition java_types.h:482
method_handle_kindt get_handle_kind() const
Definition java_types.h:509
const class_method_descriptor_exprt & get_lambda_method_descriptor() const
Definition java_types.h:498
const irep_idt & get_lambda_method_identifier() const
Definition java_types.h:504
java_lambda_method_handlet(const class_method_descriptor_exprt &method_descriptor, method_handle_kindt handle_kind)
Definition java_types.h:484
const java_method_typet & type() const
Definition java_types.h:250
bool get_is_final() const
is a method 'final'?
Definition java_types.h:262
void set_is_native(const bool is_native)
marks a method as 'native'
Definition java_types.h:280
bool get_is_native() const
is a method 'native'?
Definition java_types.h:274
void set_is_final(const bool is_final)
is a method 'final'?
Definition java_types.h:268
java_method_typet & type()
Definition java_types.h:256
const irep_idt & get_descriptor() const
Gets the method's descriptor – the mangled form of its type.
Definition java_types.h:286
void set_descriptor(const irep_idt &id)
Sets the method's descriptor – the mangled form of its type.
Definition java_types.h:292
methodt(const irep_idt &_name, java_method_typet _type)
Definition java_types.h:245
void set_is_annotation(bool is_annotation)
marks class an annotation
Definition java_types.h:446
bool get_interface() const
is class an interface?
Definition java_types.h:452
const std::vector< java_annotationt > & get_annotations() const
Definition java_types.h:543
const irep_idt & get_outer_class() const
Definition java_types.h:343
std::vector< componentt > static_memberst
Definition java_types.h:311
void set_is_stub(bool is_stub)
Definition java_types.h:393
componentst & components()
Definition java_types.h:229
void set_inner_name(const irep_idt &name)
Set the name of a java inner class.
Definition java_types.h:576
methodst & methods()
Definition java_types.h:305
void add_unknown_lambda_method_handle()
Definition java_types.h:537
void set_final(bool is_final)
Definition java_types.h:388
bool get_abstract() const
is class abstract?
Definition java_types.h:416
bool get_is_static_class() const
Definition java_types.h:363
bool get_final() const
Definition java_types.h:383
bool get_is_stub() const
Definition java_types.h:398
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:557
void set_is_anonymous_class(const bool &is_anonymous_class)
Definition java_types.h:378
bool get_is_inner_class() const
Definition java_types.h:333
static_memberst & static_members()
Definition java_types.h:318
const componentt & get_component(const irep_idt &component_name) const
Definition java_types.h:234
void add_lambda_method_handle(const class_method_descriptor_exprt &method_descriptor, method_handle_kindt handle_kind)
Definition java_types.h:530
const static_memberst & static_members() const
Definition java_types.h:313
const componentst & components() const
Definition java_types.h:224
void set_abstract(bool abstract)
marks class abstract
Definition java_types.h:422
const java_lambda_method_handlest & lambda_method_handles() const
Definition java_types.h:517
java_lambda_method_handlest & lambda_method_handles()
Definition java_types.h:524
void set_super_class(const irep_idt &super_class)
Definition java_types.h:358
void set_synthetic(bool synthetic)
marks class synthetic
Definition java_types.h:434
bool get_is_enumeration() const
is class an enumeration?
Definition java_types.h:404
bool get_synthetic() const
is class synthetic?
Definition java_types.h:428
void set_is_inner_class(const bool &is_inner_class)
Definition java_types.h:338
const irep_idt & get_inner_name() const
Get the name of a java inner class.
Definition java_types.h:570
void set_is_static_class(const bool &is_static_class)
Definition java_types.h:368
void set_is_enumeration(const bool is_enumeration)
marks class as an enumeration
Definition java_types.h:410
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:564
bool get_is_anonymous_class() const
Definition java_types.h:373
bool get_is_annotation() const
is class an annotation?
Definition java_types.h:440
const irep_idt & get_access() const
Definition java_types.h:323
void set_access(const irep_idt &access)
Definition java_types.h:328
std::vector< methodt > methodst
Definition java_types.h:298
std::vector< java_lambda_method_handlet > java_lambda_method_handlest
Definition java_types.h:515
void set_interface(bool interface)
marks class an interface
Definition java_types.h:458
method_handle_kindt
Indicates what sort of code should be synthesised for a lambda call:
Definition java_types.h:465
@ LAMBDA_STATIC_METHOD_HANDLE
Direct call to the given method.
@ LAMBDA_VIRTUAL_METHOD_HANDLE
Virtual call to the given interface or method.
@ LAMBDA_CONSTRUCTOR_HANDLE
Instantiate the needed type then call a constructor.
const methodst & methods() const
Definition java_types.h:300
std::vector< componentt > componentst
Definition java_types.h:222
const irep_idt & get_super_class() const
Definition java_types.h:353
std::vector< java_annotationt > & get_annotations()
Definition java_types.h:549
void set_outer_class(const irep_idt &outer_class)
Definition java_types.h:348
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition java_types.h:973
generic_typest & generic_types()
Definition java_types.h:987
std::vector< java_generic_parametert > generic_typest
Definition java_types.h:975
const generic_typest & generic_types() const
Definition java_types.h:982
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
Definition java_types.h:703
java_generic_parameter_tagt(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
Definition java_types.h:707
struct_tag_typet type_variablet
Definition java_types.h:705
type_variablest & type_variables()
Definition java_types.h:741
const type_variablest & type_variables() const
Definition java_types.h:736
std::vector< type_variablet > type_variablest
Definition java_types.h:735
type_variablet & type_variable_ref()
Definition java_types.h:723
const irep_idt get_name() const
Definition java_types.h:729
const type_variablet & type_variable() const
Definition java_types.h:717
Reference that points to a java_generic_parameter_tagt.
Definition java_types.h:776
struct_tag_typet type_variablet
Definition java_types.h:778
type_variablet & type_variable_ref()
Definition java_types.h:794
java_generic_parametert(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
Definition java_types.h:780
const type_variablet & type_variable() const
Definition java_types.h:789
const irep_idt get_name() const
Definition java_types.h:799
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition java_types.h:858
generic_typest & generic_types()
Definition java_types.h:878
std::vector< reference_typet > generic_typest
Definition java_types.h:860
java_generic_struct_tag_typet(const struct_tag_typet &type)
Definition java_types.h:862
optionalt< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
const generic_typest & generic_types() const
Definition java_types.h:873
Reference that points to a java_generic_struct_tag_typet.
Definition java_types.h:915
const generic_type_argumentst & generic_type_arguments() const
Definition java_types.h:926
java_generic_typet(const typet &_type)
Definition java_types.h:919
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
Definition java_types.h:917
generic_type_argumentst & generic_type_arguments()
Definition java_types.h:932
Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class o...
implicit_generic_typest & implicit_generic_types()
java_implicitly_generic_class_typet(const java_class_typet &class_type, const implicit_generic_typest &generic_types)
const implicit_generic_typest & implicit_generic_types() const
std::vector< java_generic_parametert > implicit_generic_typest
void add_throws_exception(irep_idt exception)
Definition java_types.h:132
std::vector< parametert > parameterst
Definition std_types.h:542
bool is_synthetic() const
Definition java_types.h:167
const std::vector< irep_idt > throws_exceptions() const
Definition java_types.h:124
java_method_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e.
Definition java_types.h:118
bool get_is_final() const
Definition java_types.h:137
java_method_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e.
Definition java_types.h:109
bool get_is_varargs() const
Definition java_types.h:157
void set_is_varargs(bool is_varargs)
Definition java_types.h:162
void set_is_synthetic(bool is_synthetic)
Definition java_types.h:172
bool get_native() const
Definition java_types.h:147
void set_is_final(bool is_final)
Definition java_types.h:142
void set_native(bool is_native)
Definition java_types.h:152
This is a specialization of reference_typet.
Definition java_types.h:603
const struct_tag_typet & subtype() const
Definition java_types.h:617
java_reference_typet(const struct_tag_typet &_subtype, std::size_t _width)
Definition java_types.h:605
struct_tag_typet & subtype()
Definition java_types.h:612
The reference type.
Fixed-width bit-vector with two's complement interpretation.
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition std_types.cpp:57
const irep_idt & get_identifier() const
Definition std_types.h:410
const typet & subtype() const
Definition type.h:156
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
Fixed-width bit-vector with unsigned binary interpretation.
An exception that is raised for unsupported class signature.
unsupported_java_class_signature_exceptiont(std::string type)
const java_method_typet & to_java_method_type(const typet &type)
Definition java_types.h:184
signedbv_typet java_int_type()
const java_reference_typet & to_java_reference_type(const typet &type)
Definition java_types.h:630
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
const java_generic_typet & to_java_generic_type(const typet &type)
Definition java_types.h:954
empty_typet java_void_type()
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.
char java_char_from_type(const typet &type)
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:810
std::string pretty_java_type(const typet &)
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
Definition java_types.h:897
java_reference_typet java_reference_type(const struct_tag_typet &subtype)
struct_tag_typet java_classname(const std::string &)
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:582
bool is_java_generic_type(const typet &type)
Definition java_types.h:947
std::string gather_full_class_name(const std::string &)
Returns the full class name, skipping over the generics.
const java_generic_parameter_tagt & to_java_generic_parameter_tag(const typet &type)
Definition java_types.h:759
optionalt< typet > java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
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:820
signedbv_typet java_byte_type()
bool can_cast_type< java_method_typet >(const typet &type)
Definition java_types.h:179
std::vector< java_generic_parametert > get_all_generic_parameters(const typet &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.
void get_dependencies_from_generic_parameters(const std::string &, std::set< irep_idt > &)
Collect information about generic type parameters from a given signature.
const annotated_typet & to_annotated_type(const typet &type)
Definition java_types.h:84
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.
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...
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
bool can_cast_type< java_generic_typet >(const typet &type)
Definition java_types.h:939
java_reference_typet java_array_type(const char subtype)
Construct an array pointer type.
typet java_bytecode_promotion(const typet &)
Java does not support byte/short return types. These are always promoted.
signedbv_typet java_short_type()
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition java_types.h:827
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.
const typet & java_generic_get_inst_type(size_t index, const java_generic_typet &type)
Access information of type arguments of java instantiated type.
bool can_cast_type< java_class_typet >(const typet &type)
Definition java_types.h:595
java_reference_typet java_reference_array_type(const struct_tag_typet &element_type)
floatbv_typet java_double_type()
bool is_java_generic_struct_tag_type(const typet &type)
Definition java_types.h:889
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 ...
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.
bool is_java_generic_class_type(const typet &type)
Definition java_types.h:995
bool is_java_implicitly_generic_class_type(const typet &type)
floatbv_typet java_float_type()
bool can_cast_type< java_reference_typet >(const typet &type)
Definition java_types.h:624
c_bool_typet java_boolean_type()
unsignedbv_typet java_char_type()
exprt get_array_element_type_field(const exprt &pointer)
std::string pretty_signature(const java_method_typet &)
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.
bool is_valid_java_array(const struct_typet &)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
bool can_cast_type< annotated_typet >(const typet &)
Definition java_types.h:95
bool is_java_array_tag(const irep_idt &tag)
See above.
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
signedbv_typet java_long_type()
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...
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:751
exprt get_array_dimension_field(const exprt &pointer)
java_reference_typet java_lang_object_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.
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 ...
STL namespace.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
bool can_cast_type< class_typet >(const typet &type)
Check whether a reference to a typet is a class_typet.
Definition std_types.h:368
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177