37 size_t _max_array_length,
74 const bool loading_success =
75 parse_tree.loading_successful &&
80 for(
auto overlay_class_it = std::next(parse_trees.begin());
81 overlay_class_it != parse_trees.end();
84 overlay_classes.push_front(std::cref(overlay_class_it->parsed_class));
86 convert(parse_tree.parsed_class, overlay_classes);
90 const irep_idt &class_name = parse_tree.parsed_class.name;
93 else if(!loading_success)
166 const irep_idt &qualified_fieldname,
185 if(signature.has_value())
190 signature.value().front() ==
'<' 197 const std::string superclass_ref =
198 signature.value().substr(start, (end - start) + 1);
204 if(superclass_ref.find(
'<') != std::string::npos)
205 return superclass_ref;
224 const std::string &interface_name)
226 if(signature.has_value())
231 signature.value().front() ==
'<' 241 std::string interface_name_slash_to_dot = interface_name;
243 interface_name_slash_to_dot.begin(),
244 interface_name_slash_to_dot.end(),
249 signature.value().find(
"L" + interface_name_slash_to_dot +
"<", start);
250 if(start != std::string::npos)
254 return signature.value().substr(start, (end - start) + 1);
270 debug() <<
"Skip class " << c.
name <<
" (already loaded)" <<
eom;
279 std::cout <<
"INFO: found generic class signature " 281 <<
" in parsed class " 289 for(
const typet &t : generic_types)
294 class_type=generic_class_type;
299 <<
"\n could not parse signature: " << c.
signature.value()
300 <<
"\n " << e.what() <<
"\n ignoring that the class is generic" 320 warning() <<
"Java Enum " << c.
name <<
" won't work properly because max " 325 ID_java_enum_static_unwind,
327 class_type.
set(ID_enumeration,
true);
349 if(superclass_ref.has_value())
354 base, superclass_ref.value(), qualified_classname);
360 <<
"\n could not parse signature: " << superclass_ref.value()
362 <<
"\n ignoring that the superclass is generic" <<
eom;
371 base_class_field.
type() = class_type.
bases().at(0).type();
375 class_type.
components().push_back(base_class_field);
389 if(interface_ref.has_value())
394 base, interface_ref.value(), qualified_classname);
399 warning() <<
"Interface: " <<
interface << " of class: " << c.name
400 << "\n could not parse signature: " << interface_ref.value()
402 << "\n ignoring that the interface is generic" << eom;
403 class_type.add_base(base);
408 class_type.add_base(base);
413 for(const auto &lambda_entry : c.lambda_method_handle_map)
418 lambda_entry.second.is_unknown_handle()
419 ? class_type.add_unknown_lambda_method_handle()
420 : class_type.add_lambda_method_handle(
421 "java::" + id2string(lambda_entry.second.lambda_method_ref));
425 if(!c.annotations.empty())
426 convert_annotations(c.annotations, class_type.get_annotations());
429 const irep_idt base_name = [](const std::string &full_name) {
430 const size_t last_dot = full_name.find_last_of('.');
431 return last_dot == std::string::npos
433 : std::string(full_name, last_dot + 1, std::string::npos);
434 }(id2string(c.name));
438 new_symbol.base_name = base_name;
439 new_symbol.pretty_name=c.name;
440 new_symbol.name=qualified_classname;
441 class_type.set_name(new_symbol.name);
442 new_symbol.type=class_type;
443 new_symbol.mode=ID_java;
444 new_symbol.is_type=true;
446 symbolt *class_symbol;
449 debug() << "Adding symbol: class '" << c.name << "'" << eom;
450 if(symbol_table.move(new_symbol, class_symbol))
452 error() << "failed to add class symbol " << new_symbol.name << eom;
457 const class_typet::componentst &fields =
458 to_class_type(class_symbol->type).components();
461 for(auto overlay_class : overlay_classes)
463 for(const auto &field : overlay_class.get().fields)
465 std::string field_id = qualified_classname + "." + id2string(field.name);
466 if(check_field_exists(field, field_id, fields))
469 "Duplicate field definition for " + field_id + " in overlay class";
471 error() << err << eom;
475 << "Adding symbol from overlay class: field '" << field.name << "'"
477 convert(*class_symbol, field);
478 POSTCONDITION(check_field_exists(field, field_id, fields));
481 for(const auto &field : c.fields)
483 std::string field_id = qualified_classname + "." + id2string(field.name);
484 if(check_field_exists(field, field_id, fields))
488 << "Field definition for " << field_id
489 << " already loaded from overlay class" << eom;
492 debug() << "Adding symbol: field '" << field.name << "'" << eom;
493 convert(*class_symbol, field);
494 POSTCONDITION(check_field_exists(field, field_id, fields));
498 std::set<irep_idt> overlay_methods;
499 for(auto overlay_class : overlay_classes)
501 for(const methodt &method : overlay_class.get().methods)
503 const irep_idt method_identifier =
504 qualified_classname + "." + id2string(method.name)
505 + ":" + method.descriptor;
506 if(is_ignored_method(method))
509 << "Ignoring method: '" << method_identifier << "'"
513 if(method_bytecode.contains_method(method_identifier))
520 if(overlay_methods.count(method_identifier) == 0)
525 << "Method " << method_identifier
526 << " exists in an overlay class without being marked as an "
527 "overlay and also exists in another overlay class that appears "
528 "earlier in the classpath"
536 << "Adding symbol from overlay class: method '" << method_identifier
538 java_bytecode_convert_method_lazy(
543 get_message_handler());
544 method_bytecode.add(qualified_classname, method_identifier, method);
545 if(is_overlay_method(method))
546 overlay_methods.insert(method_identifier);
549 for(const methodt &method : c.methods)
551 const irep_idt method_identifier=
552 qualified_classname + "." + id2string(method.name)
553 + ":" + method.descriptor;
554 if(is_ignored_method(method))
557 << "Ignoring method: '" << method_identifier << "'"
561 if(method_bytecode.contains_method(method_identifier))
567 if(overlay_methods.erase(method_identifier) == 0)
572 << "Method " << method_identifier
573 << " exists in an overlay class without being marked as an overlay "
574 "and also exists in the underlying class"
581 debug() << "Adding symbol: method '" << method_identifier << "'" << eom;
582 java_bytecode_convert_method_lazy(
587 get_message_handler());
588 method_bytecode.add(qualified_classname, method_identifier, method);
589 if(is_overlay_method(method))
592 << "Method " << method_identifier
593 << " marked as an overlay where defined in the underlying class" << eom;
596 if(!overlay_methods.empty())
599 << "Overlay methods defined in overlay classes did not exist in the "
600 "underlying class:\n";
601 for(const irep_idt &method_id : overlay_methods)
602 error() << " " << method_id << "\n";
607 if(c.super_class.empty())
608 java_root_class(*class_symbol);
611 bool java_bytecode_convert_classt::check_field_exists(
612 const java_bytecode_parse_treet::fieldt &field,
613 const irep_idt &qualified_fieldname,
614 const struct_union_typet::componentst &fields) const
617 return symbol_table.has_symbol(qualified_fieldname);
619 auto existing_field = std::find_if(
622 [&field](const struct_union_typet::componentt &f)
624 return f.get_name() == field.name;
626 return existing_field != fields.end();
632 void java_bytecode_convert_classt::convert(
633 symbolt &class_symbol,
637 if(f.signature.has_value())
639 field_type=java_type_from_string_with_exception(
642 id2string(class_symbol.name));
645 if(is_java_generic_parameter(field_type))
648 std::cout << "fieldtype: generic "
649 << to_java_generic_parameter(field_type).type_variable()
651 << " name " << f.name << "\n";
657 else if(is_java_generic_type(field_type))
659 java_generic_typet &with_gen_type=
660 to_java_generic_type(field_type);
662 std::cout << "fieldtype: generic container type "
663 << std::to_string(with_gen_type.generic_type_arguments().size())
664 << " type " << with_gen_type.id()
665 << " name " << f.name
666 << " subtype id " << with_gen_type.subtype().id() << "\n";
668 field_type=with_gen_type;
672 field_type=java_type_from_string(f.descriptor);
680 new_symbol.is_static_lifetime=true;
681 new_symbol.is_lvalue=true;
682 new_symbol.is_state_var=true;
683 new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name);
684 new_symbol.base_name=f.name;
685 new_symbol.type=field_type;
689 new_symbol.type.set(ID_C_class, class_symbol.name);
690 new_symbol.type.set(ID_C_field, f.name);
691 new_symbol.type.set(ID_C_constant, f.is_final);
692 new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
693 "."+id2string(f.name);
694 new_symbol.mode=ID_java;
695 new_symbol.is_type=false;
702 new_symbol.type.set(ID_C_access, ID_public);
703 else if(f.is_protected)
704 new_symbol.type.set(ID_C_access, ID_protected);
705 else if(f.is_private)
706 new_symbol.type.set(ID_C_access, ID_private);
708 new_symbol.type.set(ID_C_access, ID_default);
710 const namespacet ns(symbol_table);
711 const auto value = zero_initializer(field_type, class_symbol.location, ns);
712 if(!value.has_value())
714 error().source_location = class_symbol.location;
715 error() << "failed to zero-initialize " << f.name << eom;
718 new_symbol.value = *value;
721 if(!f.annotations.empty())
725 type_checked_cast<annotated_typet>(new_symbol.type).get_annotations());
729 const auto s_it=symbol_table.symbols.find(new_symbol.name);
730 if(s_it!=symbol_table.symbols.end())
731 symbol_table.erase(s_it);
733 if(symbol_table.add(new_symbol))
734 assert(false && "failed to add static field symbol");
738 class_typet &class_type=to_class_type(class_symbol.type);
740 class_type.components().emplace_back();
741 class_typet::componentt &component=class_type.components().back();
743 component.set_name(f.name);
744 component.set_base_name(f.name);
745 component.set_pretty_name(f.name);
746 component.type()=field_type;
749 component.set_access(ID_private);
750 else if(f.is_protected)
751 component.set_access(ID_protected);
753 component.set_access(ID_public);
755 component.set_access(ID_default);
757 component.set_is_final(f.is_final);
760 if(!f.annotations.empty())
764 static_cast<annotated_typet &>(component.type()).get_annotations());
771 void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
773 const std::string letters="ijsbcfdza";
775 for(const char l : letters)
777 struct_tag_typet struct_tag_type =
778 to_struct_tag_type(java_array_type(l).subtype());
780 const irep_idt &struct_tag_type_identifier =
781 struct_tag_type.get_identifier();
782 if(symbol_table.has_symbol(struct_tag_type_identifier))
785 java_class_typet class_type;
788 class_type.set_tag(struct_tag_type_identifier);
793 class_type.set_name(struct_tag_type_identifier);
795 class_type.components().reserve(3);
796 class_typet::componentt base_class_component(
797 "@java.lang.Object", struct_tag_typet("java::java.lang.Object"));
798 base_class_component.set_pretty_name("@java.lang.Object");
799 base_class_component.set_base_name("@java.lang.Object");
800 class_type.components().push_back(base_class_component);
802 class_typet::componentt length_component("length", java_int_type());
803 length_component.set_pretty_name("length");
804 length_component.set_base_name("length");
805 class_type.components().push_back(length_component);
807 class_typet::componentt data_component(
808 "data", java_reference_type(java_type_from_char(l)));
809 data_component.set_pretty_name("data");
810 data_component.set_base_name("data");
811 class_type.components().push_back(data_component);
813 class_type.add_base(struct_tag_typet("java::java.lang.Object"));
816 is_valid_java_array(class_type),
817 "Constructed a new type representing a Java Array "
818 "object that doesn't match expectations");
821 symbol.name = struct_tag_type_identifier;
822 symbol.base_name = struct_tag_type.get(ID_C_base_name);
824 symbol.type = class_type;
825 symbol.mode = ID_java;
826 symbol_table.add(symbol);
831 const irep_idt clone_name =
832 id2string(struct_tag_type_identifier) + ".clone:()Ljava/lang/Object;";
833 java_method_typet::parametert this_param;
834 this_param.set_identifier(id2string(clone_name)+"::this");
835 this_param.set_base_name("this");
836 this_param.set_this();
837 this_param.type() = java_reference_type(struct_tag_type);
838 const java_method_typet clone_type({this_param}, java_lang_object_type());
840 parameter_symbolt this_symbol;
841 this_symbol.name=this_param.get_identifier();
842 this_symbol.base_name=this_param.get_base_name();
843 this_symbol.pretty_name=this_symbol.base_name;
844 this_symbol.type=this_param.type();
845 this_symbol.mode=ID_java;
846 symbol_table.add(this_symbol);
848 const irep_idt local_name=
849 id2string(clone_name)+"::cloned_array";
850 auxiliary_symbolt local_symbol;
851 local_symbol.name=local_name;
852 local_symbol.base_name="cloned_array";
853 local_symbol.pretty_name=local_symbol.base_name;
854 local_symbol.type = java_reference_type(struct_tag_type);
855 local_symbol.mode=ID_java;
856 symbol_table.add(local_symbol);
857 const auto &local_symexpr=local_symbol.symbol_expr();
859 code_declt declare_cloned(local_symexpr);
861 source_locationt location;
862 location.set_function(local_name);
863 side_effect_exprt java_new_array(
864 ID_java_new_array, java_reference_type(struct_tag_type), location);
865 dereference_exprt old_array(this_symbol.symbol_expr(), struct_tag_type);
866 dereference_exprt new_array(local_symexpr, struct_tag_type);
867 member_exprt old_length(
868 old_array, length_component.get_name(), length_component.type());
869 java_new_array.copy_to_operands(old_length);
870 code_assignt create_blank(local_symexpr, java_new_array);
872 member_exprt old_data(
873 old_array, data_component.get_name(), data_component.type());
874 member_exprt new_data(
875 new_array, data_component.get_name(), data_component.type());
888 const irep_idt index_name=
889 id2string(clone_name)+"::index";
890 auxiliary_symbolt index_symbol;
891 index_symbol.name=index_name;
892 index_symbol.base_name="index";
893 index_symbol.pretty_name=index_symbol.base_name;
894 index_symbol.type = length_component.type();
895 index_symbol.mode=ID_java;
896 symbol_table.add(index_symbol);
897 const auto &index_symexpr=index_symbol.symbol_expr();
899 code_declt declare_index(index_symexpr);
901 side_effect_exprt inc(ID_assign, typet(), location);
902 inc.operands().resize(2);
903 inc.op0()=index_symexpr;
904 inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));
906 dereference_exprt old_cell(
907 plus_exprt(old_data, index_symexpr), old_data.type().subtype());
908 dereference_exprt new_cell(
909 plus_exprt(new_data, index_symexpr), new_data.type().subtype());
911 const code_fort copy_loop(
912 code_assignt(index_symexpr, from_integer(0, index_symexpr.type())),
913 binary_relation_exprt(index_symexpr, ID_lt, old_length),
915 code_assignt(std::move(new_cell), std::move(old_cell)));
917 member_exprt new_base_class(
918 new_array, base_class_component.get_name(), base_class_component.type());
919 address_of_exprt retval(new_base_class);
920 code_returnt return_inst(retval);
922 const code_blockt clone_body(
923 {declare_cloned, create_blank, declare_index, copy_loop, return_inst});
925 symbolt clone_symbol;
926 clone_symbol.name=clone_name;
927 clone_symbol.pretty_name =
928 id2string(struct_tag_type_identifier) + ".clone:()";
929 clone_symbol.base_name="clone";
930 clone_symbol.type=clone_type;
931 clone_symbol.value=clone_body;
932 clone_symbol.mode=ID_java;
933 symbol_table.add(clone_symbol);
937 bool java_bytecode_convert_class(
938 const java_class_loadert::parse_tree_with_overlayst &parse_trees,
939 symbol_tablet &symbol_table,
940 message_handlert &message_handler,
941 size_t max_array_length,
942 method_bytecodet &method_bytecode,
943 java_string_library_preprocesst &string_preprocess,
944 const std::unordered_set<std::string> &no_load_classes)
946 java_bytecode_convert_classt java_bytecode_convert_class(
956 java_bytecode_convert_class(parse_trees);
966 java_bytecode_convert_class.error() << e << messaget::eom;
969 catch(const std::string &e)
971 java_bytecode_convert_class.error() << e << messaget::eom;
989 static void find_and_replace_parameter(
990 java_generic_parametert ¶meter,
991 const std::vector<java_generic_parametert> &replacement_parameters)
994 const std::string ¶meter_full_name =
995 id2string(parameter.type_variable_ref().get_identifier());
996 const std::string ¶meter_name =
997 parameter_full_name.substr(parameter_full_name.rfind("::") + 2);
1000 const auto replacement_parameter_p = std::find_if(
1001 replacement_parameters.begin(),
1002 replacement_parameters.end(),
1003 [¶meter_name](const java_generic_parametert &replacement_param)
1005 const std::string &replacement_parameter_full_name =
1006 id2string(replacement_param.type_variable().get_identifier());
1007 return parameter_name.compare(
1008 replacement_parameter_full_name.substr(
1009 replacement_parameter_full_name.rfind("::") + 2)) == 0;
1013 if(replacement_parameter_p != replacement_parameters.end())
1015 const std::string &replacement_parameter_full_name =
1016 id2string(replacement_parameter_p->type_variable().get_identifier());
1021 parameter_full_name.substr(0, parameter_full_name.rfind("::"))
1023 replacement_parameter_full_name.substr(
1024 0, replacement_parameter_full_name.rfind("::"))) > 0);
1026 parameter.type_variable_ref().set_identifier(
1027 replacement_parameter_full_name);
1038 static void find_and_replace_parameters(
1040 const std::vector<java_generic_parametert> &replacement_parameters)
1042 if(is_java_generic_parameter(type))
1044 find_and_replace_parameter(
1045 to_java_generic_parameter(type), replacement_parameters);
1047 else if(is_java_generic_type(type))
1049 java_generic_typet &generic_type = to_java_generic_type(type);
1050 std::vector<reference_typet> &arguments =
1051 generic_type.generic_type_arguments();
1052 for(auto &argument : arguments)
1054 find_and_replace_parameters(argument, replacement_parameters);
1057 else if(is_java_generic_struct_tag_type(type))
1059 java_generic_struct_tag_typet &generic_base =
1060 to_java_generic_struct_tag_type(type);
1061 std::vector<reference_typet> &gen_types = generic_base.generic_types();
1062 for(auto &gen_type : gen_types)
1064 find_and_replace_parameters(gen_type, replacement_parameters);
1072 void convert_annotations(
1073 const java_bytecode_parse_treet::annotationst &parsed_annotations,
1074 std::vector<java_annotationt> &java_annotations)
1076 for(const auto &annotation : parsed_annotations)
1078 java_annotations.emplace_back(annotation.type);
1079 std::vector<java_annotationt::valuet> &values =
1080 java_annotations.back().get_values();
1082 annotation.element_value_pairs.begin(),
1083 annotation.element_value_pairs.end(),
1084 std::back_inserter(values),
1085 [](const decltype(annotation.element_value_pairs)::value_type &value) {
1086 return java_annotationt::valuet(value.element_name, value.value);
1095 void convert_java_annotations(
1096 const std::vector<java_annotationt> &java_annotations,
1097 java_bytecode_parse_treet::annotationst &annotations)
1099 for(const auto &java_annotation : java_annotations)
1101 annotations.emplace_back(java_bytecode_parse_treet::annotationt());
1102 auto &annotation = annotations.back();
1103 annotation.type = java_annotation.get_type();
1106 java_annotation.get_values().begin(),
1107 java_annotation.get_values().end(),
1108 std::back_inserter(annotation.element_value_pairs),
1109 [](const java_annotationt::valuet &value)
1110 -> java_bytecode_parse_treet::annotationt::element_value_pairt {
1111 return {value.get_name(), value.get_value()};
1122 void mark_java_implicitly_generic_class_type(
1123 const irep_idt &class_name,
1124 symbol_tablet &symbol_table)
1126 const std::string qualified_class_name = "java::" + id2string(class_name);
1127 PRECONDITION(symbol_table.has_symbol(qualified_class_name));
1128 symbolt &class_symbol = symbol_table.get_writeable_ref(qualified_class_name);
1129 java_class_typet &class_type = to_java_class_type(class_symbol.type);
1134 bool no_this_field = std::none_of(
1135 class_type.components().begin(),
1136 class_type.components().end(),
1137 [](const struct_union_typet::componentt &component)
1139 return id2string(component.get_name()).substr(0, 5) == "this$";
1148 std::vector<java_generic_parametert> implicit_generic_type_parameters;
1149 std::string::size_type outer_class_delimiter =
1150 qualified_class_name.rfind("$");
1151 while(outer_class_delimiter != std::string::npos)
1153 std::string outer_class_name =
1154 qualified_class_name.substr(0, outer_class_delimiter);
1155 if(symbol_table.has_symbol(outer_class_name))
1157 const symbolt &outer_class_symbol =
1158 symbol_table.lookup_ref(outer_class_name);
1159 const java_class_typet &outer_class_type =
1160 to_java_class_type(outer_class_symbol.type);
1161 if(is_java_generic_class_type(outer_class_type))
1163 const auto &outer_generic_type_parameters =
1164 to_java_generic_class_type(outer_class_type).generic_types();
1165 implicit_generic_type_parameters.insert(
1166 implicit_generic_type_parameters.begin(),
1167 outer_generic_type_parameters.begin(),
1168 outer_generic_type_parameters.end());
1170 outer_class_delimiter = outer_class_name.rfind("$");
1174 throw missing_outer_class_symbol_exceptiont(
1175 outer_class_name, qualified_class_name);
1181 if(!implicit_generic_type_parameters.empty())
1183 class_symbol.type = java_implicitly_generic_class_typet(
1184 class_type, implicit_generic_type_parameters);
1186 for(auto &field : class_type.components())
1188 find_and_replace_parameters(
1189 field.type(), implicit_generic_type_parameters);
1192 for(auto &base : class_type.bases())
1194 find_and_replace_parameters(
1195 base.type(), implicit_generic_type_parameters);
The type of an expression, extends irept.
java_bytecode_parse_treet::methodt methodt
const std::string & id2string(const irep_idt &d)
java_bytecode_parse_treet::fieldt fieldt
static bool is_overlay_method(const methodt &method)
Check if a method is an overlay method by searching for ID_overlay_method in its list of annotations.
method_bytecodet & method_bytecode
java_bytecode_parse_treet::classt classt
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void set_base_name(const irep_idt &base_name)
void set_name(const irep_idt &name)
std::vector< componentt > componentst
java_string_library_preprocesst & string_preprocess
const java_generic_parametert & to_java_generic_parameter(const typet &type)
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
const componentst & components() const
void set_final(bool is_final)
optionalt< std::string > signature
A struct tag type, i.e., struct_typet with an identifier.
static optionalt< std::string > extract_generic_superclass_reference(const optionalt< std::string > &signature)
Auxiliary function to extract the generic superclass reference from the class signature.
typet & type()
Return the type of the expression.
An exception that is raised for unsupported class signature.
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
bool has_annotation(const irep_idt &annotation_id) const
void set_access(const irep_idt &access)
std::unordered_set< std::string > no_load_classes
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
mstreamt & warning() const
size_t find_closing_delimiter(const std::string &src, size_t open_pos, char open_char, char close_char)
Finds the corresponding closing delimiter to the given opening delimiter.
Expression Initialization.
void set_outer_class(const irep_idt &outer_class)
void set_super_class(const irep_idt &super_class)
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
const basest & bases() const
Get the collection of base classes/structs.
void set_is_inner_class(const bool &is_inner_class)
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
JAVA Bytecode Language Conversion.
nonstd::optional< T > optionalt
API to expression classes.
#define PRECONDITION(CONDITION)
void set_tag(const irep_idt &tag)
size_t find_closing_semi_colon_for_reference_type(const std::string src, size_t starting_point)
Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point.
void add_base(const struct_tag_typet &base)
Add a base class/struct.
java_bytecode_convert_classt(symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &_string_preprocess, const std::unordered_set< std::string > &no_load_classes)
const size_t max_array_length
Class that provides messages with a built-in verbosity 'level'.
bool check_field_exists(const fieldt &field, const irep_idt &qualified_fieldname, const struct_union_typet::componentst &fields) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
static optionalt< std::string > extract_generic_interface_reference(const optionalt< std::string > &signature, const std::string &interface_name)
Auxiliary function to extract the generic interface reference of an interface with the specified name...
Type for a generic symbol, extends struct_tag_typet with a vector of java generic types.
static bool is_ignored_method(const methodt &method)
Check if a method is an ignored method by searching for ID_ignored_method in its list of annotations.
message_handlert & get_message_handler()
void set_is_static_class(const bool &is_static_class)
java_bytecode_parse_treet::annotationt annotationt
void set_pretty_name(const irep_idt &name)
void set_is_anonymous_class(const bool &is_anonymous_class)
static void add_array_types(symbol_tablet &symbol_table)
Register in the symbol_table new symbols for the objects java::array[X] where X is byte,...
void convert(const classt &c, const overlay_classest &overlay_classes)
Convert a class, adding symbols to the symbol table for its members.
void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Add to the symbol table type declaration for a String-like Java class.
symbol_tablet & symbol_table
std::vector< typet > java_generic_type_from_string(const std::string &class_name, const std::string &src)
Converts the content of a generic class type into a vector of Java types, that is each type variable ...
JAVA Bytecode Language Conversion.
void operator()(const java_class_loadert::parse_tree_with_overlayst &parse_trees)
Converts all the class parse trees into a class symbol and adds it to the symbol table.
const generic_typest & generic_types() const
void set(const irep_namet &name, const irep_idt &value)
std::list< std::reference_wrapper< const classt > > overlay_classest