CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
java_bytecode_convert_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Bytecode Language Conversion
4
5Author: 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
18#include "java_class_loader.h"
19
23
27 symbol_table_baset &symbol_table,
28 message_handlert &message_handler,
29 size_t max_array_length,
31 java_string_library_preprocesst &string_preprocess,
32 const std::unordered_set<std::string> &no_load_classes);
33
36 std::vector<java_annotationt> &annotations);
37
39 const std::vector<java_annotationt> &java_annotations,
41
43 const irep_idt &class_name,
44 symbol_table_baset &symbol_table);
45
52
55class missing_outer_class_symbol_exceptiont : public std::logic_error
56{
57public:
59 const std::string &outer,
60 const std::string &inner)
61 : std::logic_error(
62 "Missing outer class symbol: " + outer + ", for class " + inner)
63 {
64 }
65};
66
67#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
missing_outer_class_symbol_exceptiont(const std::string &outer, const std::string &inner)
The symbol table base class interface.
void convert_annotations(const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector< java_annotationt > &annotations)
Convert parsed annotations into the symbol table.
void add_java_array_types(symbol_table_baset &symbol_table)
Register in the symbol_table new symbols for the objects java::array[X] where X is byte,...
void mark_java_implicitly_generic_class_type(const irep_idt &class_name, symbol_table_baset &symbol_table)
Checks if the class is implicitly generic, i.e., it is an inner class of any generic class.
void convert_java_annotations(const std::vector< java_annotationt > &java_annotations, java_bytecode_parse_treet::annotationst &annotations)
Convert java annotations, e.g.
bool java_bytecode_convert_class(const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_table_baset &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.
STL namespace.
std::vector< annotationt > annotationst