cprover
java_root_class.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_root_class.h"
10 
11 #include <util/symbol.h>
12 #include <util/std_types.h>
13 
14 #include "java_types.h"
15 
16 /*******************************************************************
17 
18  Function: java_root_class
19 
20  Inputs:
21 
22  Outputs:
23 
24  Purpose:
25 
26 \*******************************************************************/
27 
28 void java_root_class(symbolt &class_symbol)
29 {
30  struct_typet &struct_type=to_struct_type(class_symbol.type);
31  struct_typet::componentst &components=struct_type.components();
32 
33  {
34  // for monitorenter/monitorexit
35  struct_typet::componentt component;
36  component.set_name("@lock");
37  component.set_pretty_name("@lock");
38  component.type()=java_boolean_type();
39 
40  // add at the beginning
41  components.insert(components.begin(), component);
42  }
43 
44  {
45  // the class identifier is used for stuff such as 'instanceof'
46  struct_typet::componentt component;
47  component.set_name("@class_identifier");
48  component.set_pretty_name("@class_identifier");
49  component.type()=string_typet();
50 
51  // add at the beginning
52  components.insert(components.begin(), component);
53  }
54 }
Symbol table entry.
void java_root_class(symbolt &class_symbol)
typet java_boolean_type()
Definition: java_types.cpp:59
void set_name(const irep_idt &name)
Definition: std_types.h:184
std::vector< componentt > componentst
Definition: std_types.h:240
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
Structure type.
Definition: std_types.h:296
TO_BE_DOCUMENTED.
Definition: std_types.h:1490
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:214