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/arith_tools.h>
12 #include <util/symbol.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 }
55 
63  struct_exprt &jlo,
64  const struct_typet &root_type,
65  const bool lock,
66  const irep_idt &class_identifier)
67 {
68  jlo.operands().resize(root_type.components().size());
69 
70  const std::size_t clsid_nb=root_type.component_number("@class_identifier");
71  const typet &clsid_type=root_type.components()[clsid_nb].type();
72  constant_exprt clsid(class_identifier, clsid_type);
73  jlo.operands()[clsid_nb]=clsid;
74 
75  const std::size_t lock_nb=root_type.component_number("@lock");
76  const typet &lock_type=root_type.components()[lock_nb].type();
77  jlo.operands()[lock_nb]=from_integer(lock, lock_type);
78 }
The type of an expression.
Definition: type.h:22
Symbol table entry.
void java_root_class(symbolt &class_symbol)
typet java_boolean_type()
Definition: java_types.cpp:72
void set_name(const irep_idt &name)
Definition: std_types.h:187
std::vector< componentt > componentst
Definition: std_types.h:243
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
A constant literal expression.
Definition: std_expr.h:4424
Structure type.
Definition: std_types.h:297
TO_BE_DOCUMENTED.
Definition: std_types.h:1569
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const bool lock, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
typet type
Type of symbol.
Definition: symbol.h:34
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:217
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1815