cprover
java_bytecode_convert_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Bytecode Language Conversion
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
14 
15 #include <unordered_set>
16 #include <util/symbol_table.h>
17 #include <util/message.h>
18 
20 #include "java_bytecode_language.h"
21 
25  symbol_tablet &symbol_table,
26  message_handlert &message_handler,
27  size_t max_array_length,
29  java_string_library_preprocesst &string_preprocess,
30  const std::unordered_set<std::string> &no_load_classes);
31 
33  const java_bytecode_parse_treet::annotationst &parsed_annotations,
34  std::vector<java_annotationt> &annotations);
35 
37  const std::vector<java_annotationt> &java_annotations,
39 
41  const irep_idt &class_name,
42  symbol_tablet &symbol_table);
43 
49 void add_java_array_types(symbol_tablet &symbol_table);
50 
53 class missing_outer_class_symbol_exceptiont : public std::logic_error
54 {
55 public:
57  const std::string &outer,
58  const std::string &inner)
59  : std::logic_error(
60  "Missing outer class symbol: " + outer + ", for class " + inner)
61  {
62  }
63 };
64 
65 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
method_bytecodet
Definition: ci_lazy_methods.h:34
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
java_bytecode_language.h
add_java_array_types
void add_java_array_types(symbol_tablet &symbol_table)
Register in the symbol_table new symbols for the objects java::array[X] where X is byte,...
Definition: java_bytecode_convert_class.cpp:791
java_bytecode_convert_class
bool java_bytecode_convert_class(const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, method_bytecodet &, java_string_library_preprocesst &string_preprocess, const std::unordered_set< std::string > &no_load_classes)
See class java_bytecode_convert_classt.
Definition: java_bytecode_convert_class.cpp:999
convert_java_annotations
void convert_java_annotations(const std::vector< java_annotationt > &java_annotations, java_bytecode_parse_treet::annotationst &annotations)
Convert java annotations, e.g.
Definition: java_bytecode_convert_class.cpp:1157
java_bytecode_parse_treet::annotationst
std::vector< annotationt > annotationst
Definition: java_bytecode_parse_tree.h:50
missing_outer_class_symbol_exceptiont
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
Definition: java_bytecode_convert_class.h:54
java_class_loadert::parse_tree_with_overlayst
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
Definition: java_class_loader.h:30
convert_annotations
void convert_annotations(const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector< java_annotationt > &annotations)
Convert parsed annotations into the symbol table.
Definition: java_bytecode_convert_class.cpp:1134
java_bytecode_parse_tree.h
message_handlert
Definition: message.h:28
mark_java_implicitly_generic_class_type
void mark_java_implicitly_generic_class_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Checks if the class is implicitly generic, i.e., it is an inner class of any generic class.
Definition: java_bytecode_convert_class.cpp:1182
java_string_library_preprocesst
Definition: java_string_library_preprocess.h:36
symbol_table.h
Author: Diffblue Ltd.
missing_outer_class_symbol_exceptiont::missing_outer_class_symbol_exceptiont
missing_outer_class_symbol_exceptiont(const std::string &outer, const std::string &inner)
Definition: java_bytecode_convert_class.h:56
message.h