cprover
java_utils.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
10 #define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
11 
12 #include "java_types.h"
13 
14 #include <unordered_set>
15 
16 #include <util/message.h>
17 #include <util/std_expr.h>
18 #include <util/symbol_table.h>
19 
21 
22 bool java_is_array_type(const typet &type);
23 
25  const irep_idt &class_name,
26  symbol_table_baset &symbol_table,
27  message_handlert &message_handler,
28  const struct_union_typet::componentst &componentst);
29 
32 unsigned java_local_variable_slots(const typet &t);
33 
37 
38 const std::string java_class_to_package(const std::string &canonical_classname);
39 
50  exprt &expr,
51  const source_locationt &source_location);
52 
53 #define JAVA_STRING_LITERAL_PREFIX "java::java.lang.String.Literal"
54 
57 bool is_java_string_literal_id(const irep_idt &id);
58 
67  const std::string &friendly_name,
68  const symbol_table_baset &symbol_table,
69  std::string &error);
70 
74 dereference_exprt checked_dereference(const exprt &expr, const typet &type);
75 
81  symbolt &class_symbol,
82  const struct_union_typet::componentst &components_to_add);
83 
85  const std::string &src,
86  size_t position,
87  char open_char,
88  char close_char);
89 
90 void declare_function(
91  irep_idt function_name,
92  const typet &type,
93  symbol_table_baset &symbol_table);
94 
96  const irep_idt &function_name,
97  const exprt::operandst &arguments,
98  const typet &type,
99  symbol_table_baset &symbol_table);
100 
102 
103 std::string pretty_print_java_type(const std::string &fqn_java_type);
104 
106  const irep_idt &component_class_id,
107  const irep_idt &component_name,
108  const symbol_tablet &symbol_table,
109  const class_hierarchyt &class_hierarchy,
110  bool include_interfaces);
111 
113 
114 extern const std::unordered_set<std::string> cprover_methods_to_ignore;
115 
116 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
checked_dereference
dereference_exprt checked_dereference(const exprt &expr, const typet &type)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:174
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:42
declare_function
void declare_function(irep_idt function_name, const typet &type, symbol_table_baset &symbol_table)
Declare a function with the given name and type.
Definition: java_utils.cpp:253
java_local_variable_slots
unsigned java_local_variable_slots(const typet &t)
Returns the number of JVM local variables (slots) taken by a local variable that, when translated to ...
Definition: java_utils.cpp:29
get_inherited_component
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:335
typet
The type of an expression, extends irept.
Definition: type.h:27
is_java_string_literal_id
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:111
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:3355
find_closing_delimiter
size_t find_closing_delimiter(const std::string &src, size_t position, char open_char, char close_char)
Finds the corresponding closing delimiter to the given opening delimiter.
Definition: java_utils.cpp:195
exprt
Base class for all expressions.
Definition: expr.h:54
resolve_inherited_componentt::inherited_componentt
Definition: resolve_inherited_component.h:27
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:203
java_method_parameter_slots
unsigned java_method_parameter_slots(const java_method_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call,...
Definition: java_utils.cpp:48
resolve_inherited_component.h
resolve_friendly_method_name
irep_idt resolve_friendly_method_name(const std::string &friendly_name, const symbol_table_baset &symbol_table, std::string &error)
Resolves a user-friendly method name (like packagename.Class.method) into an internal name (like java...
Definition: java_utils.cpp:116
java_add_components_to_class
void java_add_components_to_class(symbolt &class_symbol, const struct_union_typet::componentst &components_to_add)
Add the components in components_to_add to the class denoted by class symbol.
Definition: java_utils.cpp:234
pretty_print_java_type
std::string pretty_print_java_type(const std::string &fqn_java_type)
Strip the package name from a java type, for the type to be pretty printed (java::java....
Definition: java_utils.cpp:308
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
java_is_array_type
bool java_is_array_type(const typet &type)
Definition: java_utils.cpp:22
java_class_to_package
const std::string java_class_to_package(const std::string &canonical_classname)
Definition: java_utils.cpp:58
message_handlert
Definition: message.h:24
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
strip_java_namespace_prefix
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:294
merge_source_location_rec
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
Definition: java_utils.cpp:102
make_function_application
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
Create a function application expression.
Definition: java_utils.cpp:275
source_locationt
Definition: source_location.h:20
symbolt
Symbol table entry.
Definition: symbol.h:27
java_types.h
cprover_methods_to_ignore
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
Definition: java_utils.cpp:421
symbol_table.h
Author: Diffblue Ltd.
message.h
std_expr.h
generate_class_stub
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
Definition: java_utils.cpp:63
java_method_typet
Definition: java_types.h:264
is_non_null_library_global
bool is_non_null_library_global(const irep_idt &)
Check if a symbol is a well-known non-null global.
Definition: java_utils.cpp:410