CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Private Types | Private Member Functions | Static Private Member Functions | Private Attributes | List of all members
java_bytecode_convert_classt Class Reference
+ Collaboration diagram for java_bytecode_convert_classt:
[フレーム]
[legend]

Public Types

typedef java_bytecode_parse_treet::classt  classt
 
typedef java_bytecode_parse_treet::fieldt  fieldt
 
typedef java_bytecode_parse_treet::methodt  methodt
 
typedef java_bytecode_parse_treet::annotationt  annotationt
 

Public Member Functions

  java_bytecode_convert_classt (symbol_table_baset &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &_string_preprocess, const std::unordered_set< std::string > &no_load_classes)
 
void  operator() (const java_class_loadert::parse_tree_with_overlayst &parse_trees)
  Converts all the class parse trees into a class symbol and adds it to the symbol table.
 

Private Types

typedef std::list< std::reference_wrapper< const classt > >  overlay_classest
 

Private Member Functions

void  convert (const classt &c, const overlay_classest &overlay_classes)
  Convert a class, adding symbols to the symbol table for its members.
 
void  convert (symbolt &class_symbol, const fieldt &f)
  Convert a field, adding a symbol to teh symbol table for it.
 
bool  check_field_exists (const fieldt &field, const irep_idt &qualified_fieldname, const struct_union_typet::componentst &fields) const
 

Static Private Member Functions

static bool  is_overlay_method (const methodt &method)
  Check if a method is an overlay method by searching for ID_overlay_method in its list of annotations.
 
static bool  is_ignored_method (const irep_idt &class_name, const methodt &method)
  Check if a method is an ignored method, by one of two mechanisms:
 

Private Attributes

messaget  log
 
symbol_table_baset &  symbol_table
 
const size_t  max_array_length
 
method_bytecodet &  method_bytecode
 
java_string_library_preprocesst &  string_preprocess
 
std::unordered_set< std::string >  no_load_classes
 

Detailed Description

Definition at line 33 of file java_bytecode_convert_class.cpp.

Member Typedef Documentation

◆  annotationt

typedef java_bytecode_parse_treet::annotationt java_bytecode_convert_classt::annotationt

Definition at line 107 of file java_bytecode_convert_class.cpp.

◆  classt

typedef java_bytecode_parse_treet::classt java_bytecode_convert_classt::classt

Definition at line 104 of file java_bytecode_convert_class.cpp.

◆  fieldt

typedef java_bytecode_parse_treet::fieldt java_bytecode_convert_classt::fieldt

Definition at line 105 of file java_bytecode_convert_class.cpp.

◆  methodt

typedef java_bytecode_parse_treet::methodt java_bytecode_convert_classt::methodt

Definition at line 106 of file java_bytecode_convert_class.cpp.

◆  overlay_classest

typedef std::list<std::reference_wrapper<const classt> > java_bytecode_convert_classt::overlay_classest
private

Definition at line 117 of file java_bytecode_convert_class.cpp.

Constructor & Destructor Documentation

◆  java_bytecode_convert_classt()

java_bytecode_convert_classt::java_bytecode_convert_classt ( symbol_table_baset &  _symbol_table,
message_handlert &  _message_handler,
size_t  _max_array_length,
method_bytecodet &  method_bytecode,
java_string_library_preprocesst &  _string_preprocess,
const std::unordered_set< std::string > &  no_load_classes 
)
inline

Definition at line 36 of file java_bytecode_convert_class.cpp.

Member Function Documentation

◆  check_field_exists()

bool java_bytecode_convert_classt::check_field_exists ( const fieldt &  field,
const irep_idt &  qualified_fieldname,
const struct_union_typet::componentst &  fields 
) const
private

Definition at line 621 of file java_bytecode_convert_class.cpp.

◆  convert() [1/2]

void java_bytecode_convert_classt::convert ( const classt &  c,
const overlay_classest &  overlay_classes 
)
private

Convert a class, adding symbols to the symbol table for its members.

Parameters
c Bytecode of the class to convert
overlay_classes Bytecode of any overlays for the class to convert

Definition at line 270 of file java_bytecode_convert_class.cpp.

◆  convert() [2/2]

void java_bytecode_convert_classt::convert ( symbolt &  class_symbol,
const fieldt &  f 
)
private

Convert a field, adding a symbol to teh symbol table for it.

Parameters
class_symbol The already added symbol for the containing class
f The bytecode for the field to convert

this is for a free type variable, e.g., a field of the form T f;

this is for a field that holds a generic type, either with instantiated or with free type variables, e.g., List<T> l; or List<Integer> l;

Definition at line 642 of file java_bytecode_convert_class.cpp.

◆  is_ignored_method()

static bool java_bytecode_convert_classt::is_ignored_method ( const irep_idt &  class_name,
const methodt &  method 
)
inlinestaticprivate

Check if a method is an ignored method, by one of two mechanisms:

  1. If the class under consideration is org.cprover.CProver, and the method is listed as ignored.
  2. If it has the annotation@IgnoredMethodImplementation. This kind of ignord method is intended for use in overlay classes, in particular for methods which must exist in the overlay class so that it will compile, e.g. default constructors, but which we do not want to overlay the corresponding method in the underlying class. It is an error if a method in an overlay class has the same signature as a method in the underlying class and it isn't marked as an overlay method or an ignored method.
Parameters
class_name class the method is declared on
method a methodt object from a java bytecode parse tree
Returns
true if the method is an ignored method, else false

Definition at line 161 of file java_bytecode_convert_class.cpp.

◆  is_overlay_method()

static bool java_bytecode_convert_classt::is_overlay_method ( const methodt &  method )
inlinestaticprivate

Check if a method is an overlay method by searching for ID_overlay_method in its list of annotations.

An overlay method is a method with the annotation @OverlayMethodImplementation. They should only appear in overlay classes. They will be loaded by JBMC instead of the method with the same signature in the underlying class. It is an error if there is no method with the same signature in the underlying class. It is an error if a method in an overlay class has the same signature as a method in the underlying class and it isn't marked as an overlay method or an ignored method.

Parameters
method a methodt object from a java bytecode parse tree
Returns
true if the method is an overlay method, else false

Definition at line 136 of file java_bytecode_convert_class.cpp.

◆  operator()()

void java_bytecode_convert_classt::operator() ( const java_class_loadert::parse_tree_with_overlayst &  parse_trees )
inline

Converts all the class parse trees into a class symbol and adds it to the symbol table.

Parameters
parse_trees The parse trees found for the class to be converted.
Remarks
Allows multiple definitions of the same class to appear on the classpath, so long as all but the first definition are marked with the attribute \@java::org.cprover.OverlayClassImplementation. Overlay class definitions can contain methods with the same signature as methods in the original class, so long as these are marked with the attribute \@java::org.cprover.OverlayMethodImplementation; such overlay methods are replaced in the original file with the version found in the last overlay on the classpath. Later definitions can also contain new supporting methods and fields that are merged in. This will allow insertion of Java methods into library classes to handle, for example, modelling dependency injection.

Definition at line 67 of file java_bytecode_convert_class.cpp.

Member Data Documentation

◆  log

messaget java_bytecode_convert_classt::log
private

Definition at line 110 of file java_bytecode_convert_class.cpp.

◆  max_array_length

const size_t java_bytecode_convert_classt::max_array_length
private

Definition at line 112 of file java_bytecode_convert_class.cpp.

◆  method_bytecode

method_bytecodet& java_bytecode_convert_classt::method_bytecode
private

Definition at line 113 of file java_bytecode_convert_class.cpp.

◆  no_load_classes

std::unordered_set<std::string> java_bytecode_convert_classt::no_load_classes
private

Definition at line 176 of file java_bytecode_convert_class.cpp.

◆  string_preprocess

java_string_library_preprocesst& java_bytecode_convert_classt::string_preprocess
private

Definition at line 114 of file java_bytecode_convert_class.cpp.

◆  symbol_table

symbol_table_baset& java_bytecode_convert_classt::symbol_table
private

Definition at line 111 of file java_bytecode_convert_class.cpp.

The documentation for this class was generated from the following file:

AltStyle によって変換されたページ (->オリジナル) /