CBMC
class_identifier.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Extract class identifier
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_CLASS_IDENTIFIER_H
13 #define CPROVER_GOTO_PROGRAMS_CLASS_IDENTIFIER_H
14 
15 class exprt;
16 class namespacet;
17 class struct_tag_typet;
18 class struct_exprt;
19 
20 #define JAVA_CLASS_IDENTIFIER_FIELD_NAME "@class_identifier"
21 
22 exprt get_class_identifier_field(
23  const exprt &this_expr,
24  const struct_tag_typet &suggested_type,
25  const namespacet &ns);
26 
27 void set_class_identifier(
28  struct_exprt &expr,
29  const namespacet &ns,
30  const struct_tag_typet &class_type);
31 
32 #endif
set_class_identifier
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.
Definition: class_identifier.cpp:83
get_class_identifier_field
exprt get_class_identifier_field(const exprt &this_expr, const struct_tag_typet &suggested_type, const namespacet &ns)
Definition: class_identifier.cpp:57
exprt
Base class for all expressions.
Definition: expr.h:56
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1877
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493