cprover
java_root_class.cpp File Reference
#include "java_root_class.h"
#include <util/arith_tools.h>
#include <util/symbol.h>
#include "java_types.h"
Include dependency graph for java_root_class.cpp:

Go to the source code of this file.

Functions

void java_root_class (symbolt &class_symbol)
 
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). More...
 

Function Documentation

◆ java_root_class()

◆ java_root_class_init()

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).

Parameters
jlo[out] : object to initialize
root_typetype of the root class
locklock field
class_identifierclass 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().