Go to the documentation of this file.
22 debug() <<
"Classpath:";
25 debug() <<
"\n " << entry.path;
29 std::stack<irep_idt> queue;
32 queue.push(
"java.lang.Object");
34 queue.push(
"java.lang.String");
36 queue.push(
"java.lang.Class");
39 queue.push(
"java.lang.Throwable");
40 queue.push(class_name);
57 debug() <<
"Reading class " << c <<
eom;
64 for(
const irep_idt &class_ref : parse_tree.class_refs)
65 queue.push(class_ref);
110 auto parse_tree =
load_class(class_name, cp_entry);
111 if(parse_tree.has_value())
140 debug() <<
"not loading " << class_name <<
" because of limit" <<
eom;
141 parse_trees.emplace_back(class_name);
148 auto parse_tree =
load_class(class_name, cp_entry);
149 if(parse_tree.has_value())
150 parse_trees.emplace_back(std::move(*parse_tree));
153 auto parse_tree_it = parse_trees.begin();
156 while(parse_tree_it != parse_trees.end())
159 if(parse_tree_it->loading_successful)
167 debug() <<
"Skipping class " << class_name
168 <<
" marked with OverlayClassImplementation but found before"
169 " original definition"
172 auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
174 parse_trees.erase(unloaded_or_overlay_out_of_order_it);
177 while(parse_tree_it != parse_trees.end())
182 debug() <<
"Skipping duplicate definition of class " << class_name
183 <<
" not marked with OverlayClassImplementation" <<
eom;
184 auto duplicate_non_overlay_it = parse_tree_it;
186 parse_trees.erase(duplicate_non_overlay_it);
191 if(!parse_trees.empty())
195 debug() <<
"failed to load class " << class_name <<
eom;
196 parse_trees.emplace_back(class_name);
203 const std::string &jar_path)
206 if(!classes.has_value())
212 for(
const auto &c : *classes)
223 std::vector<std::string> filenames;
226 filenames =
jar_pool(jar_path).filenames();
228 catch(
const std::runtime_error &)
230 error() <<
"failed to open JAR file '" << jar_path <<
"'" <<
eom;
233 debug() <<
"Adding JAR file '" << jar_path <<
"'" <<
eom;
237 std::vector<irep_idt> classes;
238 for(
auto &file_name : filenames)
242 debug() <<
"Found class file " << file_name <<
" in JAR '" << jar_path
245 classes.push_back(class_name);
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.
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 ...
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
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.
get_extra_class_refs_functiont get_extra_class_refs
std::vector< irep_idt > load_entire_jar(const std::string &jar_path)
Load all class files from a .jar file.
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
optionalt< std::vector< irep_idt > > read_jar_file(const std::string &jar_path)
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::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
An entry in the classpath.
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.
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
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< classpath_entryt > classpath_entries
List of entries in the classpath.
#define PRECONDITION(CONDITION)
optionalt< java_bytecode_parse_treet > load_class(const irep_idt &class_name, const classpath_entryt &)
attempt to load a class from a classpath_entry
bool can_load_class(const irep_idt &class_name)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
nonstd::optional< T > optionalt
Class representing a filter for class file loading.
parse_tree_with_overridest_mapt class_map
Map from class names to the bytecode parse trees.
message_handlert & get_message_handler()
parse_tree_with_overlayst & operator()(const irep_idt &class_name)