cprover
class_identifier.cpp File Reference

Extract class identifier. More...

#include "class_identifier.h"
#include <util/std_expr.h>
#include <util/c_types.h>
#include <util/namespace.h>
Include dependency graph for class_identifier.cpp:

Go to the source code of this file.

Functions

static exprt build_class_identifier (const exprt &src, const namespacet &ns)
 
exprt get_class_identifier_field (const exprt &this_expr_in, const symbol_typet &suggested_type, const namespacet &ns)
 
void set_class_identifier (struct_exprt &expr, const namespacet &ns, const symbol_typet &class_type)
 If expr has its components filled in then sets the @class_identifier member of the struct. More...
 

Detailed Description

Extract class identifier.

Definition in file class_identifier.cpp.

Function Documentation

◆ build_class_identifier()

static exprt build_class_identifier ( const exprt src,
const namespacet ns 
)
static
parameters: Struct expression
Returns
Member expression giving the clsid field of the input, or its parent, grandparent, etc.

Definition at line 21 of file class_identifier.cpp.

References struct_union_typet::components(), namespace_baset::follow(), irept::swap(), to_struct_type(), and exprt::type().

Referenced by get_class_identifier_field().

◆ get_class_identifier_field()

exprt get_class_identifier_field ( const exprt this_expr_in,
const symbol_typet suggested_type,
const namespacet ns 
)
parameters: Pointer expression of any pointer type, including void*,
and a recommended access type if the pointer is void-typed.
Returns
Member expression to access a class identifier, as above.

Definition at line 56 of file class_identifier.cpp.

References build_class_identifier(), irept::id(), pointer_type(), typet::subtype(), and exprt::type().

Referenced by remove_instanceoft::lower_instanceof(), and remove_virtual_functionst::remove_virtual_function().

◆ set_class_identifier()

void set_class_identifier ( struct_exprt expr,
const namespacet ns,
const symbol_typet class_type 
)

If expr has its components filled in then sets the @class_identifier member of the struct.

Remarks
Follows through base class members until it gets to the object type that contains the @class_identifier member
Parameters
exprAn expression that represents a struct
nsThe namespace used to resolve symbol referencess in the type of the struct
class_typeA symbol whose identifier is the name of the class

Definition at line 83 of file class_identifier.cpp.

References struct_union_typet::components(), namespace_baset::follow(), symbol_typet::get_identifier(), irept::id(), INVARIANT, exprt::op0(), exprt::operands(), PRECONDITION, set_class_identifier(), to_struct_expr(), to_struct_type(), and exprt::type().

Referenced by java_object_factoryt::gen_nondet_struct_init(), java_static_lifetime_init(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), and set_class_identifier().