cprover
|
Extract class identifier. More...
#include "class_identifier.h"
#include <util/std_expr.h>
#include <util/c_types.h>
#include <util/namespace.h>
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... | |
Extract class identifier.
Definition in file class_identifier.cpp.
|
static |
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().
exprt get_class_identifier_field | ( | const exprt & | this_expr_in, |
const symbol_typet & | suggested_type, | ||
const namespacet & | ns | ||
) |
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().
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.
@class_identifier
member expr | An expression that represents a struct |
ns | The namespace used to resolve symbol references in the type of the struct |
class_type | A 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(), initialize_nondet_string_fields(), java_static_lifetime_init(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), and set_class_identifier().