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 
12 #include <util/arith_tools.h>
13 #include <util/symbol.h>
14 
15 #include "java_types.h"
16 
22 void java_root_class(symbolt &class_symbol)
23 {
24  struct_typet &struct_type=to_struct_type(class_symbol.type);
25  struct_typet::componentst &components=struct_type.components();
26 
27  {
28  // the class identifier is used for stuff such as 'instanceof'
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 =
52  const typet &clsid_type=root_type.components()[clsid_nb].type();
53  constant_exprt clsid(class_identifier, clsid_type);
54  jlo.operands()[clsid_nb]=clsid;
55 
56  // Check if the 'cproverMonitorCount' component exists and initialize it.
57  // This field is only present when the java core models are embedded. It is
58  // used to implement a critical section, which is necessary to support
59  // concurrency.
60  if(root_type.has_component("cproverMonitorCount"))
61  {
62  const std::size_t count_nb =
63  root_type.component_number("cproverMonitorCount");
64  const typet &count_type = root_type.components()[count_nb].type();
65  jlo.operands()[count_nb] = from_integer(0, count_type);
66  }
67 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_root_class_init
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).
Definition: java_root_class.cpp:43
java_root_class.h
JAVA_CLASS_IDENTIFIER_FIELD_NAME
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
Definition: class_identifier.h:20
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
typet
The type of an expression, extends irept.
Definition: type.h:29
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
struct_union_typet::component_number
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:36
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
symbol.h
Symbol table entry.
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:152
struct_union_typet::componentt
Definition: std_types.h:64
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
string_typet
String type.
Definition: std_types.h:1655
class_identifier.h
Extract class identifier.
java_root_class
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically,...
Definition: java_root_class.cpp:22
exprt::operands
operandst & operands()
Definition: expr.h:95
java_types.h
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906