cprover
|
#include <util/std_expr.h>
Go to the source code of this file.
Functions | |
void | java_root_class (class symbolt &class_symbol) |
void | java_root_class_init (struct_exprt &jlo, const struct_typet &root_type, bool lock, const irep_idt &class_identifier) |
Adds members for an object of the root class (usually java.lang.Object). More... | |
void java_root_class | ( | class symbolt & | class_symbol | ) |
Definition at line 28 of file java_root_class.cpp.
References struct_union_typet::components(), java_boolean_type(), struct_union_typet::componentt::set_name(), struct_union_typet::componentt::set_pretty_name(), to_struct_type(), symbolt::type, and exprt::type().
Referenced by generate_class_stub().
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).
jlo | [out] : object to initialize |
root_type | type of the root class |
lock | lock field |
class_identifier | class identifier field, generally begins with "java::" prefix. |
Definition at line 62 of file java_root_class.cpp.
References struct_union_typet::component_number(), struct_union_typet::components(), from_integer(), and exprt::operands().
Referenced by java_string_library_preprocesst::code_assign_components_to_java_string(), get_or_create_string_literal_symbol(), and initialize_nondet_string_struct().