CBMC
java_class_loader.cpp File Reference
#include "java_class_loader.h"
#include <stack>
#include <util/message.h>
#include <util/suffix.h>
#include "java_class_loader_limit.h"
+ Include dependency graph for java_class_loader.cpp:

Go to the source code of this file.

Functions

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

Function Documentation

◆ is_overlay_class()

static bool is_overlay_class ( const java_bytecode_parse_treet::classt c)
static

Check if class is an overlay class by searching for ID_overlay_class in its list of annotations.

An overlay class is a class with the annotation @OverlayClassImplementation. They serve the following purpose. When the JVM searches the classpath for a particular class, it uses the first match, and ignores any later matches. JBMC, however, will take account of later matches as long as they are overlay classes. The first match is then referred to as the underlying class. The overlay classes can change the methods of the underlying class in the following ways: adding a field (by having a new field), adding a method (by having a new method) or changing the definition of a method. 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
ca classt object from a java bytecode parse tree
Returns
true if parsed class is an overlay class, else false

Definition at line 100 of file java_class_loader.cpp.