Add can_load_class helper

load_class() has side effects and cannot be used
for checking whether a class could be loaded.
can_load_class() only affects the jar_pool.

Author: peterschrammel

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -103,6 +103,17 @@ static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
     .has_value();
 }
 
+bool java_class_loadert::can_load_class(const irep_idt &class_name)
+{
+  for(const auto &cp_entry : classpath_entries)
+  {
+    auto parse_tree = load_class(class_name, cp_entry);
+    if(parse_tree.has_value())
+      return true;
+  }
+  return false;
+}
+
 /// Check through all the places class parse trees can appear and returns the
 /// first implementation it finds plus any overlay class implementations.
 /// Uses \p class_loader_limit to limit the class files that it might (directly

jbmc/src/java_bytecode/java_class_loader.h

@@ -43,6 +43,10 @@ class java_class_loadert : public java_class_loader_baset
 
   parse_tree_with_overlayst &operator()(const irep_idt &class_name);
 
+  /// Checks whether \p class_name is parseable from the classpath,
+  /// ignoring class loading limits.
+  bool can_load_class(const irep_idt &class_name);
+
   parse_tree_with_overlayst &get_parse_tree(
     java_class_loader_limitt &class_loader_limit,
     const irep_idt &class_name);