23 log.debug() <<
"Classpath:";
26 log.debug() <<
"\n " << entry.path;
30 std::stack<irep_idt> queue;
33 queue.push(
"java.lang.Object");
35 queue.push(
"java.lang.String");
37 queue.push(
"java.lang.Class");
40 queue.push(
"java.lang.Throwable");
41 queue.push(class_name);
114 if(parse_tree.has_value())
147 log.debug() <<
"not loading " << class_name <<
" because of limit"
157 if(parse_tree.has_value())
175 log.debug() <<
"Skipping class " << class_name
176 <<
" marked with OverlayClassImplementation but found before"
177 " original definition"
190 log.debug() <<
"Skipping duplicate definition of class " << class_name
191 <<
" not marked with OverlayClassImplementation"
224 operator()(
c, message_handler);
237 std::vector<std::string> filenames;
242 catch(
const std::runtime_error &)
244 log.error() <<
"failed to open JAR file '" <<
jar_path <<
"'"
253 for(
auto &file_name : filenames)
257 log.debug() <<
"Found class file " << file_name <<
" in JAR '" <<
jar_path
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
jar_poolt jar_pool
a cache for jar_filet, by path name
std::optional< java_bytecode_parse_treet > load_class(const irep_idt &class_name, const classpath_entryt &, message_handlert &)
attempt to load a class from a classpath_entry
static std::string class_name_to_jar_file(const irep_idt &)
Convert a class name to a file name, does the inverse of file_to_class_name.
std::list< classpath_entryt > classpath_entries
List of entries in the classpath.
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
Class representing a filter for class file loading.
std::string java_cp_include_files
Either a regular expression matching files that will be allowed to be loaded or a string of the form ...
std::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
parse_tree_with_overridest_mapt class_map
Map from class names to the bytecode parse trees.
std::vector< irep_idt > load_entire_jar(const std::string &jar_path, message_handlert &)
Load all class files from a .jar file.
bool can_load_class(const irep_idt &class_name, message_handlert &)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
parse_tree_with_overlayst & operator()(const irep_idt &class_name, message_handlert &)
parse_tree_with_overlayst & get_parse_tree(java_class_loader_limitt &class_loader_limit, const irep_idt &class_name, message_handlert &)
Check through all the places class parse trees can appear and returns the first implementation it fin...
get_extra_class_refs_functiont get_extra_class_refs
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
std::optional< std::vector< irep_idt > > read_jar_file(const std::string &jar_path, message_handlert &)
Class that provides messages with a built-in verbosity 'level'.
static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
Check if class is an overlay class by searching for ID_overlay_class in its list of annotations.
#define PRECONDITION(CONDITION)
static std::optional< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
An entry in the classpath.
bool has_suffix(const std::string &s, const std::string &suffix)