Merge pull request #2829 from thk123/allow-extra-entry-points

Allow extra entry points loads to be specified [TG-4620]

Author: Thomas Kiley

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -123,6 +123,9 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     extra_entry_points.end(),
     std::back_inserter(extra_methods),
     build_load_method_by_regex);
+  const auto &new_points = build_extra_entry_points(cmd);
+  extra_methods.insert(
+    extra_methods.end(), new_points.begin(), new_points.end());
 
   if(cmd.isset("java-cp-include-files"))
   {
@@ -1207,3 +1210,13 @@ bool java_bytecode_languaget::to_expr(
 java_bytecode_languaget::~java_bytecode_languaget()
 {
 }
+
+/// This method should be overloaded to provide alternative approaches for
+/// specifying extra entry points. To provide a regex entry point, the command
+/// line option `--lazy-methods-extra-entry-point` can be used directly.
+std::vector<load_extra_methodst>
+java_bytecode_languaget::build_extra_entry_points(
+  const cmdlinet &command_line) const
+{
+  return {};
+}

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -199,6 +199,8 @@ class java_bytecode_languaget:public languaget
   std::vector<irep_idt> java_load_classes;
 
 private:
+  virtual std::vector<load_extra_methodst>
+  build_extra_entry_points(const cmdlinet &command_line) const;
   const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
 
   /// Maps synthetic method names on to the particular type of synthetic method

jbmc/src/java_bytecode/java_types.h

@@ -453,31 +453,33 @@ class java_generic_typet:public reference_typet
   }
 };
 
+template <>
+inline bool can_cast_type<java_generic_typet>(const typet &type)
+{
+  return is_reference(type) && type.get_bool(ID_C_java_generic_type);
+}
+
 /// \param type: the type to check
 /// \return true if type is java type containing with generics, e.g., List<T>
 inline bool is_java_generic_type(const typet &type)
 {
-  return type.get_bool(ID_C_java_generic_type);
+  return can_cast_type<java_generic_typet>(type);
 }
 
 /// \param type: source type
 /// \return cast of type into java type with generics
 inline const java_generic_typet &to_java_generic_type(
   const typet &type)
 {
-  PRECONDITION(
-    type.id()==ID_pointer &&
-    is_java_generic_type(type));
+  PRECONDITION(can_cast_type<java_generic_typet>(type));
   return static_cast<const java_generic_typet &>(type);
 }
 
 /// \param type: source type
 /// \return cast of type into java type with generics
 inline java_generic_typet &to_java_generic_type(typet &type)
 {
-  PRECONDITION(
-    type.id()==ID_pointer &&
-    is_java_generic_type(type));
+  PRECONDITION(can_cast_type<java_generic_typet>(type));
   return static_cast<java_generic_typet &>(type);
 }