CBMC
|
#include "ci_lazy_methods.h"
#include <util/expr_iterator.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/suffix.h>
#include <util/symbol_table.h>
#include <goto-programs/resolve_inherited_component.h>
#include "java_bytecode_language.h"
#include "java_class_loader.h"
#include "java_entry_point.h"
#include "remove_exceptions.h"
Go to the source code of this file.
Functions | |
static bool | references_class_model (const exprt &expr) |
Checks if an expression refers to any class literals (e.g. More... | |
|
static |
Checks if an expression refers to any class literals (e.g.
MyType.class) These are expressed as ldc instructions in Java bytecode, and as symbols of the form MyType@class_model
in GOTO programs.
expr | expression to check |
Definition at line 66 of file ci_lazy_methods.cpp.