CBMC
|
Extract class identifier. More...
Go to the source code of this file.
Macros | |
#define | JAVA_CLASS_IDENTIFIER_FIELD_NAME "@class_identifier" |
Functions | |
exprt | get_class_identifier_field (const exprt &this_expr, const struct_tag_typet &suggested_type, const namespacet &ns) |
void | set_class_identifier (struct_exprt &expr, const namespacet &ns, const struct_tag_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.h.
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME "@class_identifier" |
Definition at line 20 of file class_identifier.h.
exprt get_class_identifier_field | ( | const exprt & | this_expr_in, |
const struct_tag_typet & | suggested_type, | ||
const namespacet & | ns | ||
) |
Definition at line 57 of file class_identifier.cpp.
void set_class_identifier | ( | struct_exprt & | expr, |
const namespacet & | ns, | ||
const struct_tag_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.