CBMC
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/std_expr.h>
19
20class java_annotationt : public irept
21{
22public:
23 class valuet : public irept
24 {
25 public:
26 valuet(irep_idt name, const exprt &value) : irept(name)
27 {
28 get_sub().push_back(value);
29 }
30
31 const irep_idt &get_name() const
32 {
33 return id();
34 }
35
36 const exprt &get_value() const
37 {
38 return static_cast<const exprt &>(get_sub().front());
39 }
40 };
41
42 explicit java_annotationt(const typet &type)
43 {
44 set(ID_type, type);
45 }
46
47 const typet &get_type() const
48 {
49 return static_cast<const typet &>(find(ID_type));
50 }
51
52 const std::vector<valuet> &get_values() const
53 {
54 // This cast should be safe as valuet doesn't add data to irept
55 return reinterpret_cast<const std::vector<valuet> &>(get_sub());
56 }
57
58 std::vector<valuet> &get_values()
59 {
60 // This cast should be safe as valuet doesn't add data to irept
61 return reinterpret_cast<std::vector<valuet> &>(get_sub());
62 }
63};
64
65class annotated_typet : public typet
66{
67public:
68 const std::vector<java_annotationt> &get_annotations() const
69 {
70 // This cast should be safe as java_annotationt doesn't add data to irept
71 return reinterpret_cast<const std::vector<java_annotationt> &>(
72 find(ID_C_annotations).get_sub());
73 }
74
75 std::vector<java_annotationt> &get_annotations()
76 {
77 // This cast should be safe as java_annotationt doesn't add data to irept
78 return reinterpret_cast<std::vector<java_annotationt> &>(
80 }
81};
82
83inline const annotated_typet &to_annotated_type(const typet &type)
84{
85 return static_cast<const annotated_typet &>(type);
86}
87
89{
90 return static_cast<annotated_typet &>(type);
91}
92
93template <>
95{
96 return true;
97}
98
100{
101public:
104
113
122
123 const std::vector<irep_idt> throws_exceptions() const
124 {
125 std::vector<irep_idt> exceptions;
126 for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
127 exceptions.push_back(e.id());
128 return exceptions;
129 }
130
132 {
133 add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
134 }
135
136 bool get_is_final() const
137 {
138 return get_bool(ID_final);
139 }
140
141 void set_is_final(bool is_final)
142 {
143 set(ID_final, is_final);
144 }
145
146 bool get_native() const
147 {
149 }
150
151 void set_native(bool is_native)
152 {
153 set(ID_is_native_method, is_native);
154 }
155
156 bool get_is_varargs() const
157 {
159 }
160
161 void set_is_varargs(bool is_varargs)
162 {
163 set(ID_is_varargs_method, is_varargs);
164 }
165
166 bool is_synthetic() const
167 {
168 return get_bool(ID_synthetic);
169 }
170
175};
176
177template <>
179{
180 return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
181}
182
184{
186 return static_cast<const java_method_typet &>(type);
187}
188
190{
192 return static_cast<java_method_typet &>(type);
193}
194
196{
197public:
198 class componentt : public class_typet::componentt
199 {
200 public:
201 componentt() = default;
202
204 : class_typet::componentt(_name, std::move(_type))
205 {
206 }
207
209 bool get_is_final() const
210 {
211 return get_bool(ID_final);
212 }
213
215 void set_is_final(const bool is_final)
216 {
217 set(ID_final, is_final);
218 }
219 };
220
221 using componentst = std::vector<componentt>;
222
223 const componentst &components() const
224 {
225 return (const componentst &)(find(ID_components).get_sub());
226 }
227
229 {
230 return (componentst &)(add(ID_components).get_sub());
231 }
232
233 const componentt &get_component(const irep_idt &component_name) const
234 {
235 return static_cast<const componentt &>(
236 class_typet::get_component(component_name));
237 }
238
240 {
241 public:
242 methodt() = delete;
243
245 : class_typet::methodt(_name, std::move(_type))
246 {
247 }
248
249 const java_method_typet &type() const
250 {
251 return static_cast<const java_method_typet &>(
252 class_typet::methodt::type());
253 }
254
256 {
257 return static_cast<java_method_typet &>(class_typet::methodt::type());
258 }
259
261 bool get_is_final() const
262 {
263 return get_bool(ID_final);
264 }
265
267 void set_is_final(const bool is_final)
268 {
269 set(ID_final, is_final);
270 }
271
273 bool get_is_native() const
274 {
276 }
277
279 void set_is_native(const bool is_native)
280 {
281 set(ID_is_native_method, is_native);
282 }
283
286 {
288 }
289
291 void set_descriptor(const irep_idt &id)
292 {
294 }
295 };
296
297 using methodst = std::vector<methodt>;
298
299 const methodst &methods() const
300 {
301 return (const methodst &)(find(ID_methods).get_sub());
302 }
303
305 {
306 return (methodst &)(add(ID_methods).get_sub());
307 }
308
310 using static_memberst = std::vector<componentt>;
311
313 {
315 }
316
321
322 const irep_idt &get_access() const
323 {
324 return get(ID_access);
325 }
326
328 {
329 return set(ID_access, access);
330 }
331
333 {
335 }
336
337 void set_is_inner_class(const bool &is_inner_class)
338 {
339 return set(ID_is_inner_class, is_inner_class);
340 }
341
343 {
344 return get(ID_outer_class);
345 }
346
347 void set_outer_class(const irep_idt &outer_class)
348 {
349 return set(ID_outer_class, outer_class);
350 }
351
353 {
354 return get(ID_super_class);
355 }
356
357 void set_super_class(const irep_idt &super_class)
358 {
359 return set(ID_super_class, super_class);
360 }
361
363 {
364 return get_bool(ID_is_static);
365 }
366
367 void set_is_static_class(const bool &is_static_class)
368 {
369 return set(ID_is_static, is_static_class);
370 }
371
373 {
375 }
376
377 void set_is_anonymous_class(const bool &is_anonymous_class)
378 {
379 return set(ID_is_anonymous, is_anonymous_class);
380 }
381
382 bool get_final() const
383 {
384 return get_bool(ID_final);
385 }
386
387 void set_final(bool is_final)
388 {
389 set(ID_final, is_final);
390 }
391
393 {
395 }
396
397 bool get_is_stub() const
398 {
400 }
401
404 {
405 return get_bool(ID_enumeration);
406 }
407
413
415 bool get_abstract() const
416 {
417 return get_bool(ID_abstract);
418 }
419
421 void set_abstract(bool abstract)
422 {
423 set(ID_abstract, abstract);
424 }
425
427 bool get_synthetic() const
428 {
429 return get_bool(ID_synthetic);
430 }
431
434 {
436 }
437
439 bool get_is_annotation() const
440 {
442 }
443
445 void set_is_annotation(bool is_annotation)
446 {
447 set(ID_is_annotation, is_annotation);
448 }
449
451 bool get_interface() const
452 {
453 return get_bool(ID_interface);
454 }
455
458 {
460 }
461
474
481 {
482 public:
484 const class_method_descriptor_exprt &method_descriptor,
485 method_handle_kindt handle_kind)
486 {
487 set(ID_object_descriptor, method_descriptor);
488 set(ID_handle_type, static_cast<int>(handle_kind));
489 }
490
496
502
504 {
505 return get_lambda_method_descriptor().get_identifier();
506 }
507
512 };
513
514 using java_lambda_method_handlest = std::vector<java_lambda_method_handlet>;
515
517 {
518 return (const java_lambda_method_handlest &)find(
520 .get_sub();
521 }
522
528
530 const class_method_descriptor_exprt &method_descriptor,
531 method_handle_kindt handle_kind)
532 {
533 // creates a symbol_exprt for the identifier and pushes it in the vector
534 lambda_method_handles().emplace_back(method_descriptor, handle_kind);
535 }
537 {
538 // creates empty symbol_exprt and pushes it in the vector
539 lambda_method_handles().emplace_back();
540 }
541
542 const std::vector<java_annotationt> &get_annotations() const
543 {
544 return static_cast<const annotated_typet &>(
545 static_cast<const typet &>(*this)).get_annotations();
546 }
547
548 std::vector<java_annotationt> &get_annotations()
549 {
551 static_cast<typet &>(*this)).get_annotations();
552 }
553
556 const irep_idt &get_name() const
557 {
558 return get(ID_name);
559 }
560
563 void set_name(const irep_idt &name)
564 {
565 set(ID_name, name);
566 }
567
570 {
571 return get(ID_inner_name);
572 }
573
575 void set_inner_name(const irep_idt &name)
576 {
577 set(ID_inner_name, name);
578 }
579};
580
581inline const java_class_typet &to_java_class_type(const typet &type)
582{
583 PRECONDITION(type.id() == ID_struct);
584 return static_cast<const java_class_typet &>(type);
585}
586
588{
589 PRECONDITION(type.id() == ID_struct);
590 return static_cast<java_class_typet &>(type);
591}
592
593template <>
595{
596 return can_cast_type<class_typet>(type);
597}
598
602{
603public:
606 std::size_t _width)
607 : reference_typet(_subtype, _width)
608 {
609 }
610
612 {
613 return static_cast<struct_tag_typet &>(reference_typet::subtype());
614 }
615
617 {
618 return static_cast<const struct_tag_typet &>(reference_typet::subtype());
619 }
620};
621
622template <>
624{
625 return type.id() == ID_pointer &&
626 to_type_with_subtype(type).subtype().id() == ID_struct_tag;
627}
628
630{
632 return static_cast<const java_reference_typet &>(type);
633}
634
640
653struct_tag_typet java_classname(const std::string &);
654
655#define JAVA_REFERENCE_ARRAY_CLASSID "java::array[reference]"
656
657java_reference_typet java_array_type(const char subtype);
660const typet &java_array_element_type(const struct_tag_typet &array_symbol);
662bool is_java_array_type(const typet &type);
663bool is_multidim_java_array_type(const typet &type);
664
665std::pair<typet, std::size_t>
667
668#define JAVA_ARRAY_DIMENSION_FIELD_NAME "@array_dimensions"
670#define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME "@element_class_identifier"
672
674std::optional<typet> java_type_from_string(
675 const std::string &,
676 const std::string &class_name_prefix = "");
677char java_char_from_type(const typet &type);
678std::vector<typet> java_generic_type_from_string(
679 const std::string &,
680 const std::string &);
681
685 const std::string src,
686 size_t starting_point = 0);
687
688std::vector<std::string> parse_raw_list_types(
689 std::string src,
690 char opening_bracket,
691 char closing_bracket);
692
693bool is_java_array_tag(const irep_idt &tag);
695
696bool equal_java_types(const typet &type1, const typet &type2);
697
702{
703public:
705
714
717 {
718 PRECONDITION(!type_variables().empty());
719 return type_variables().front();
720 }
721
723 {
724 PRECONDITION(!type_variables().empty());
725 return type_variables().front();
726 }
727
728 const irep_idt get_name() const
729 {
730 return type_variable().get_identifier();
731 }
732
733private:
734 typedef std::vector<type_variablet> type_variablest;
736 {
737 return (const type_variablest &)(find(ID_type_variables).get_sub());
738 }
739
744};
745
750inline bool is_java_generic_parameter_tag(const typet &type)
751{
753}
754
757inline const java_generic_parameter_tagt &
759{
761 return static_cast<const java_generic_parameter_tagt &>(type);
762}
763
771
775{
776public:
778
786
789 {
790 return to_java_generic_parameter_tag(subtype()).type_variable();
791 }
792
794 {
795 return to_java_generic_parameter_tag(subtype()).type_variable_ref();
796 }
797
798 const irep_idt get_name() const
799 {
800 return to_java_generic_parameter_tag(subtype()).get_name();
801 }
802};
803
808template <>
810{
811 return is_reference(base) &&
813}
814
819inline bool is_java_generic_parameter(const typet &type)
820{
822}
823
827 const typet &type)
828{
830 return static_cast<const java_generic_parametert &>(type);
831}
832
840
857{
858public:
859 typedef std::vector<reference_typet> generic_typest;
860
862 : struct_tag_typet(type)
863 {
865 }
866
868 const struct_tag_typet &type,
869 const std::string &base_ref,
870 const std::string &class_name_prefix);
871
873 {
874 return (const generic_typest &)(find(ID_generic_types).get_sub());
875 }
876
881
882 std::optional<size_t>
884};
885
889{
891}
892
897{
899 return static_cast<const java_generic_struct_tag_typet &>(type);
900}
901
910
936
937template <>
939{
940 return is_reference(type) &&
942}
943
946inline bool is_java_generic_type(const typet &type)
947{
949}
950
954 const typet &type)
955{
957 return static_cast<const java_generic_typet &>(type);
958}
959
963{
965 return static_cast<java_generic_typet &>(type);
966}
967
972{
973 public:
974 typedef std::vector<java_generic_parametert> generic_typest;
975
980
982 {
983 return (const generic_typest &)(find(ID_generic_types).get_sub());
984 }
985
990};
991
994inline bool is_java_generic_class_type(const typet &type)
995{
997}
998
1001inline const java_generic_class_typet &
1003{
1005 return static_cast<const java_generic_class_typet &>(type);
1006}
1007
1016
1022 size_t index,
1023 const java_generic_typet &type)
1024{
1025 const std::vector<reference_typet> &type_arguments =
1027 PRECONDITION(index<type_arguments.size());
1028 return type_arguments[index];
1029}
1030
1035inline const irep_idt &
1037{
1038 const std::vector<java_generic_parametert> &gen_types=type.generic_types();
1039
1040 PRECONDITION(index<gen_types.size());
1042
1043 return gen_type.type_variable().get_identifier();
1044}
1045
1050inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
1051{
1053 const java_generic_class_typet &type =
1055 const std::vector<java_generic_parametert> &gen_types=type.generic_types();
1056
1057 PRECONDITION(index<gen_types.size());
1059
1060 return gen_type.base_type();
1061}
1062
1067{
1068public:
1069 typedef std::vector<java_generic_parametert> implicit_generic_typest;
1070
1073 const implicit_generic_typest &generic_types)
1075 {
1077 for(const auto &type : generic_types)
1078 {
1079 implicit_generic_types().push_back(type);
1080 }
1081 }
1082
1084 {
1085 return (
1087 &)(find(ID_implicit_generic_types).get_sub());
1088 }
1089
1095};
1096
1103
1112
1121
1125std::vector<java_generic_parametert>
1127
1131{
1132public:
1134 std::logic_error(
1135 "Unsupported class signature: "+type)
1136 {
1137 }
1138};
1139
1140inline std::optional<typet> java_type_from_string_with_exception(
1141 const std::string &descriptor,
1142 const std::optional<std::string> &signature,
1143 const std::string &class_name)
1144{
1145 try
1146 {
1147 return java_type_from_string(signature.value(), class_name);
1148 }
1150 {
1151 return java_type_from_string(descriptor, class_name);
1152 }
1153}
1154
1159inline const std::optional<size_t> java_generics_get_index_for_subtype(
1160 const std::vector<java_generic_parametert> &gen_types,
1161 const irep_idt &identifier)
1162{
1163 const auto iter = std::find_if(
1164 gen_types.cbegin(),
1165 gen_types.cend(),
1166 [&identifier](const java_generic_parametert &ref)
1167 {
1168 return ref.type_variable().get_identifier() == identifier;
1169 });
1170
1171 if(iter == gen_types.cend())
1172 {
1173 return {};
1174 }
1175
1176 return narrow_cast<size_t>(std::distance(gen_types.cbegin(), iter));
1177}
1178
1180 const std::string &,
1181 std::set<irep_idt> &);
1183 const typet &,
1184 std::set<irep_idt> &);
1185
1190std::string erase_type_arguments(const std::string &);
1196std::string gather_full_class_name(const std::string &);
1197
1198// turn java type into string
1199std::string pretty_java_type(const typet &);
1200
1201// pretty signature for methods
1202std::string pretty_signature(const java_method_typet &);
1203
1204#endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::vector< java_annotationt > & get_annotations()
Definition java_types.h:75
const std::vector< java_annotationt > & get_annotations() const
Definition java_types.h:68
The C/C++ Booleans.
Definition c_types.h:97
An expression describing a method on a class.
Definition std_expr.h:3634
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:583
std::vector< parametert > parameterst
Definition std_types.h:586
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
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:364
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
irept()=default
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
subt & get_sub()
Definition irep.h:448
signed int get_int(const irep_idt &name) const
Definition irep.cpp:62
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
valuet(irep_idt name, const exprt &value)
Definition java_types.h:26
const irep_idt & get_name() const
Definition java_types.h:31
const exprt & get_value() const
Definition java_types.h:36
const typet & get_type() const
Definition java_types.h:47
java_annotationt(const typet &type)
Definition java_types.h:42
const std::vector< valuet > & get_values() const
Definition java_types.h:52
std::vector< valuet > & get_values()
Definition java_types.h:58
void set_is_final(const bool is_final)
is a field 'final'?
Definition java_types.h:215
componentt(const irep_idt &_name, typet _type)
Definition java_types.h:203
bool get_is_final() const
is a field 'final'?
Definition java_types.h:209
Represents a lambda call to a method.
Definition java_types.h:481
method_handle_kindt get_handle_kind() const
Definition java_types.h:508
const class_method_descriptor_exprt & get_lambda_method_descriptor() const
Definition java_types.h:497
const irep_idt & get_lambda_method_identifier() const
Definition java_types.h:503
java_lambda_method_handlet(const class_method_descriptor_exprt &method_descriptor, method_handle_kindt handle_kind)
Definition java_types.h:483
const java_method_typet & type() const
Definition java_types.h:249
bool get_is_final() const
is a method 'final'?
Definition java_types.h:261
void set_is_native(const bool is_native)
marks a method as 'native'
Definition java_types.h:279
bool get_is_native() const
is a method 'native'?
Definition java_types.h:273
void set_is_final(const bool is_final)
is a method 'final'?
Definition java_types.h:267
java_method_typet & type()
Definition java_types.h:255
const irep_idt & get_descriptor() const
Gets the method's descriptor – the mangled form of its type.
Definition java_types.h:285
void set_descriptor(const irep_idt &id)
Sets the method's descriptor – the mangled form of its type.
Definition java_types.h:291
methodt(const irep_idt &_name, java_method_typet _type)
Definition java_types.h:244
void set_is_annotation(bool is_annotation)
marks class an annotation
Definition java_types.h:445
bool get_interface() const
is class an interface?
Definition java_types.h:451
const std::vector< java_annotationt > & get_annotations() const
Definition java_types.h:542
const irep_idt & get_outer_class() const
Definition java_types.h:342
std::vector< componentt > static_memberst
Definition java_types.h:310
void set_is_stub(bool is_stub)
Definition java_types.h:392
componentst & components()
Definition java_types.h:228
void set_inner_name(const irep_idt &name)
Set the name of a java inner class.
Definition java_types.h:575
methodst & methods()
Definition java_types.h:304
void add_unknown_lambda_method_handle()
Definition java_types.h:536
void set_final(bool is_final)
Definition java_types.h:387
bool get_abstract() const
is class abstract?
Definition java_types.h:415
bool get_is_static_class() const
Definition java_types.h:362
bool get_final() const
Definition java_types.h:382
bool get_is_stub() const
Definition java_types.h:397
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:556
void set_is_anonymous_class(const bool &is_anonymous_class)
Definition java_types.h:377
bool get_is_inner_class() const
Definition java_types.h:332
static_memberst & static_members()
Definition java_types.h:317
const componentt & get_component(const irep_idt &component_name) const
Definition java_types.h:233
void add_lambda_method_handle(const class_method_descriptor_exprt &method_descriptor, method_handle_kindt handle_kind)
Definition java_types.h:529
const static_memberst & static_members() const
Definition java_types.h:312
const componentst & components() const
Definition java_types.h:223
void set_abstract(bool abstract)
marks class abstract
Definition java_types.h:421
const java_lambda_method_handlest & lambda_method_handles() const
Definition java_types.h:516
java_lambda_method_handlest & lambda_method_handles()
Definition java_types.h:523
void set_super_class(const irep_idt &super_class)
Definition java_types.h:357
void set_synthetic(bool synthetic)
marks class synthetic
Definition java_types.h:433
bool get_is_enumeration() const
is class an enumeration?
Definition java_types.h:403
bool get_synthetic() const
is class synthetic?
Definition java_types.h:427
void set_is_inner_class(const bool &is_inner_class)
Definition java_types.h:337
const irep_idt & get_inner_name() const
Get the name of a java inner class.
Definition java_types.h:569
void set_is_static_class(const bool &is_static_class)
Definition java_types.h:367
void set_is_enumeration(const bool is_enumeration)
marks class as an enumeration
Definition java_types.h:409
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:563
bool get_is_anonymous_class() const
Definition java_types.h:372
bool get_is_annotation() const
is class an annotation?
Definition java_types.h:439
const irep_idt & get_access() const
Definition java_types.h:322
void set_access(const irep_idt &access)
Definition java_types.h:327
std::vector< methodt > methodst
Definition java_types.h:297
std::vector< java_lambda_method_handlet > java_lambda_method_handlest
Definition java_types.h:514
void set_interface(bool interface)
marks class an interface
Definition java_types.h:457
method_handle_kindt
Indicates what sort of code should be synthesised for a lambda call:
Definition java_types.h:464
@ 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:299
std::vector< componentt > componentst
Definition java_types.h:221
const irep_idt & get_super_class() const
Definition java_types.h:352
std::vector< java_annotationt > & get_annotations()
Definition java_types.h:548
void set_outer_class(const irep_idt &outer_class)
Definition java_types.h:347
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition java_types.h:972
generic_typest & generic_types()
Definition java_types.h:986
std::vector< java_generic_parametert > generic_typest
Definition java_types.h:974
const generic_typest & generic_types() const
Definition java_types.h:981
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
Definition java_types.h:702
java_generic_parameter_tagt(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
Definition java_types.h:706
struct_tag_typet type_variablet
Definition java_types.h:704
type_variablest & type_variables()
Definition java_types.h:740
const type_variablest & type_variables() const
Definition java_types.h:735
std::vector< type_variablet > type_variablest
Definition java_types.h:734
type_variablet & type_variable_ref()
Definition java_types.h:722
const irep_idt get_name() const
Definition java_types.h:728
const type_variablet & type_variable() const
Definition java_types.h:716
Reference that points to a java_generic_parameter_tagt.
Definition java_types.h:775
struct_tag_typet type_variablet
Definition java_types.h:777
type_variablet & type_variable_ref()
Definition java_types.h:793
java_generic_parametert(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
Definition java_types.h:779
const type_variablet & type_variable() const
Definition java_types.h:788
const irep_idt get_name() const
Definition java_types.h:798
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition java_types.h:857
generic_typest & generic_types()
Definition java_types.h:877
std::vector< reference_typet > generic_typest
Definition java_types.h:859
java_generic_struct_tag_typet(const struct_tag_typet &type)
Definition java_types.h:861
const generic_typest & generic_types() const
Definition java_types.h:872
std::optional< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
Reference that points to a java_generic_struct_tag_typet.
Definition java_types.h:914
const generic_type_argumentst & generic_type_arguments() const
Definition java_types.h:925
java_generic_typet(const typet &_type)
Definition java_types.h:918
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
Definition java_types.h:916
generic_type_argumentst & generic_type_arguments()
Definition java_types.h:931
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:131
std::vector< parametert > parameterst
Definition std_types.h:586
bool is_synthetic() const
Definition java_types.h:166
const std::vector< irep_idt > throws_exceptions() const
Definition java_types.h:123
java_method_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e.
Definition java_types.h:117
bool get_is_final() const
Definition java_types.h:136
java_method_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e.
Definition java_types.h:108
bool get_is_varargs() const
Definition java_types.h:156
void set_is_varargs(bool is_varargs)
Definition java_types.h:161
void set_is_synthetic(bool is_synthetic)
Definition java_types.h:171
bool get_native() const
Definition java_types.h:146
void set_is_final(bool is_final)
Definition java_types.h:141
void set_native(bool is_native)
Definition java_types.h:151
This is a specialization of reference_typet.
Definition java_types.h:602
const struct_tag_typet & subtype() const
Definition java_types.h:616
java_reference_typet(const struct_tag_typet &_subtype, std::size_t _width)
Definition java_types.h:604
struct_tag_typet & subtype()
Definition java_types.h:611
const typet & subtype() const
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:493
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:64
The type of an expression, extends irept.
Definition type.h:29
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:183
signedbv_typet java_int_type()
const java_reference_typet & to_java_reference_type(const typet &type)
Definition java_types.h:629
std::optional< typet > java_type_from_string_with_exception(const std::string &descriptor, const std::optional< std::string > &signature, const std::string &class_name)
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:953
empty_typet java_void_type()
const std::optional< 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.
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:809
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:896
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:581
bool is_java_generic_type(const typet &type)
Definition java_types.h:946
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:758
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:819
signedbv_typet java_byte_type()
bool can_cast_type< java_method_typet >(const typet &type)
Definition java_types.h:178
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:83
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:938
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:826
std::optional< 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.
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:594
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:888
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:994
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:623
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:94
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:750
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:518
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208