diffblue.github.io/cbmc/class__identifier_8h_source.html

/*******************************************************************\


Module: Extract class identifier


Author: Chris Smowton, [email protected]


\*******************************************************************/


#ifndef CPROVER_GOTO_PROGRAMS_CLASS_IDENTIFIER_H

#define CPROVER_GOTO_PROGRAMS_CLASS_IDENTIFIER_H


class exprt;

class namespacet;

class struct_tag_typet;

class struct_exprt;


#define JAVA_CLASS_IDENTIFIER_FIELD_NAME "@class_identifier"


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);


#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

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

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:91

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