22 std::stack<irep_idt> queue;
25 queue.push(
"java.lang.Object");
27 queue.push(
"java.lang.String");
29 queue.push(
"java.lang.Class");
32 queue.push(
"java.lang.Throwable");
33 queue.push(class_name);
50 debug() <<
"Reading class " << c <<
eom;
57 for(
const irep_idt &class_ref : parse_tree.class_refs)
58 queue.push(class_ref);
122 debug() <<
"not loading " << class_name <<
" because of limit" <<
eom;
123 parse_trees.emplace_back(class_name);
130 auto parse_tree =
load_class(class_name, cp_entry);
131 if(parse_tree.has_value())
132 parse_trees.emplace_back(std::move(*parse_tree));
135 auto parse_tree_it = parse_trees.begin();
138 while(parse_tree_it != parse_trees.end())
141 if(parse_tree_it->loading_successful)
150 <<
"Skipping class " << class_name
151 <<
" marked with OverlayClassImplementation but found before" 152 " original definition" 155 auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
157 parse_trees.erase(unloaded_or_overlay_out_of_order_it);
160 while(parse_tree_it != parse_trees.end())
166 <<
"Skipping duplicate definition of class " << class_name
167 <<
" not marked with OverlayClassImplementation" <<
eom;
168 auto duplicate_non_overlay_it = parse_tree_it;
170 parse_trees.erase(duplicate_non_overlay_it);
175 if(!parse_trees.empty())
179 warning() <<
"failed to load class `" << class_name <<
'\'' <<
eom;
180 parse_trees.emplace_back(class_name);
187 const std::string &jar_path)
190 if(!classes.has_value())
196 for(
const auto &c : *classes)
207 std::vector<std::string> filenames;
210 filenames =
jar_pool(jar_path).filenames();
212 catch(
const std::runtime_error &)
214 error() <<
"failed to open JAR file `" << jar_path <<
"'" <<
eom;
217 debug() <<
"Adding JAR file `" << jar_path <<
"'" <<
eom;
221 std::vector<irep_idt> classes;
222 for(
auto &file_name : filenames)
227 <<
"Found class file " << file_name <<
" in JAR `" << jar_path <<
"'" 230 classes.push_back(class_name);
std::list< classpath_entryt > classpath_entries
List of entries in the classpath.
optionalt< java_bytecode_parse_treet > load_class(const irep_idt &class_name, const classpath_entryt &)
attempt to load a class from a classpath_entry
std::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
parse_tree_with_overlayst & get_parse_tree(java_class_loader_limitt &class_loader_limit, const irep_idt &class_name)
Check through all the places class parse trees can appear and returns the first implementation it fin...
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
mstreamt & warning() const
optionalt< std::vector< irep_idt > > read_jar_file(const std::string &jar_path)
nonstd::optional< T > optionalt
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
#define PRECONDITION(CONDITION)
An entry in the classpath.
jar_poolt jar_pool
a cache for jar_filet, by path name
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Class representing a filter for class file loading.
message_handlert & get_message_handler()
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...
get_extra_class_refs_functiont get_extra_class_refs
bool load_class_file(const std::string &class_file_name)
Use the class load limiter to decide whether a class file should be loaded or not.
parse_tree_with_overlayst & operator()(const irep_idt &class_name)
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.
bool has_suffix(const std::string &s, const std::string &suffix)
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 > load_entire_jar(const std::string &jar_path)
Load all class files from a .jar file.
parse_tree_with_overridest_mapt class_map
Map from class names to the bytecode parse trees.