CBMC
ci_lazy_methods.cpp File Reference
+ Include dependency graph for ci_lazy_methods.cpp:

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

Function Documentation

◆ references_class_model()

static bool references_class_model ( const exprt expr)
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.

Parameters
exprexpression to check
Returns
true if the expression or any of its subexpressions refer to a class

Definition at line 66 of file ci_lazy_methods.cpp.