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 
21 void java_root_class(symbolt &class_symbol)
22 {
23  struct_typet &struct_type=to_struct_type(class_symbol.type);
24  struct_typet::componentst &components=struct_type.components();
25 
26  {
27  // the class identifier is used for stuff such as 'instanceof'
28  struct_typet::componentt component;
29  component.set_name("@class_identifier");
30  component.set_pretty_name("@class_identifier");
31  component.type()=string_typet();
32 
33  // add at the beginning
34  components.insert(components.begin(), component);
35  }
36 }
37 
44  struct_exprt &jlo,
45  const struct_typet &root_type,
46  const irep_idt &class_identifier)
47 {
48  jlo.operands().resize(root_type.components().size());
49 
50  const std::size_t clsid_nb=root_type.component_number("@class_identifier");
51  const typet &clsid_type=root_type.components()[clsid_nb].type();
52  constant_exprt clsid(class_identifier, clsid_type);
53  jlo.operands()[clsid_nb]=clsid;
54 
55  // Check if the 'cproverMonitorCount' component exists and initialize it.
56  // This field is only present when the java core models are embedded. It is
57  // used to implement a critical section, which is necessary to support
58  // concurrency.
59  if(root_type.has_component("cproverMonitorCount"))
60  {
61  const std::size_t count_nb =
62  root_type.component_number("cproverMonitorCount");
63  const typet &count_type = root_type.components()[count_nb].type();
64  jlo.operands()[count_nb] = from_integer(0, count_type);
65  }
66 }
The type of an expression.
Definition: type.h:22
Symbol table entry.
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically, we add a new component, &#39;@class_identifier&#39;.
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:4422
Structure type.
Definition: std_types.h:297
TO_BE_DOCUMENTED.
Definition: std_types.h:1578
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:255
typet type
Type of symbol.
Definition: symbol.h:34
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
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