java_bytecode_convert_class.h File Reference

JAVA Bytecode Language Conversion. More...

#include <unordered_set>
#include <util/symbol_table.h>
#include <util/message.h>
#include "java_bytecode_parse_tree.h"
#include "java_bytecode_language.h"
+ Include dependency graph for java_bytecode_convert_class.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.


class  missing_outer_class_symbol_exceptiont
 An exception that is raised checking whether a class is implicitly generic if a symbol for an outer class is missing. More...


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. More...
void convert_annotations (const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector< java_annotationt > &annotations)
 Convert parsed annotations into the symbol table. More...
void convert_java_annotations (const std::vector< java_annotationt > &java_annotations, java_bytecode_parse_treet::annotationst &annotations)
 Convert java annotations, e.g. More...
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. More...

Detailed Description

JAVA Bytecode Language Conversion.

Definition in file java_bytecode_convert_class.h.

Function Documentation

◆ convert_annotations()

void convert_annotations ( const java_bytecode_parse_treet::annotationst parsed_annotations,
std::vector< java_annotationt > &  java_annotations 

Convert parsed annotations into the symbol table.

parsed_annotationsThe parsed annotations to convert
java_annotationsThe java_annotationt collection to populate

Definition at line 1090 of file java_bytecode_convert_class.cpp.

◆ 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.

as retrieved from the symbol table, back to type annotationt (inverse of convert_annotations())

java_annotationsThe java_annotationt collection to convert
annotationsThe annotationt collection to populate

Definition at line 1113 of file java_bytecode_convert_class.cpp.

◆ 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 at line 957 of file java_bytecode_convert_class.cpp.

◆ 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.

All uses of the implicit generic type parameters within the inner class are updated to point to the type parameters of the corresponding outer classes.

Definition at line 1138 of file java_bytecode_convert_class.cpp.