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'
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, extends irept.
Definition: type.h:27
Symbol table entry.
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically,...
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
std::vector< componentt > componentst
Definition: std_types.h:203
const componentst & components() const
Definition: std_types.h:205
Symbol table entry.
Definition: symbol.h:27
A constant literal expression.
Definition: std_expr.h:4384
Structure type, corresponds to C style structs.
Definition: std_types.h:276
String type.
Definition: std_types.h:1662
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:215
typet type
Type of symbol.
Definition: symbol.h:31
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
Return the sequence number of the component with given name.
Definition: std_types.cpp:35
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Struct constructor from list of elements.
Definition: std_expr.h:1920