java_utils.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
#define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
 
#include <unordered_set>
 
#include <util/pointer_expr.h>
 
#include <goto-programs/resolve_inherited_component.h>
 
class java_class_typet;
class java_method_typet;
class message_handlert;
class symbol_table_baset;
 
bool is_java_string_type(const struct_typet &struct_type);
 
struct java_primitive_type_infot
{
  const irep_idt boxed_type_name;
  const irep_idt boxed_type_factory_method;
  const irep_idt unboxing_function_name;
};
 
const java_primitive_type_infot *
get_java_primitive_type_info(const typet &maybe_primitive_type);
 
struct java_boxed_type_infot
{
  const irep_idt unboxing_function_name;
  const typet corresponding_primitive_type;
};
 
const java_boxed_type_infot *
get_boxed_type_info_by_name(const irep_idt &type_name);
 
bool is_primitive_wrapper_type_id(const irep_idt &id);
 
bool is_primitive_wrapper_type_name(const std::string &type_name);
 
void generate_class_stub(
  const irep_idt &class_name,
  symbol_table_baset &symbol_table,
  message_handlert &message_handler,
  const struct_union_typet::componentst &componentst);
 
unsigned java_local_variable_slots(const typet &t);
 
unsigned java_method_parameter_slots(const java_method_typet &t);
 
const std::string java_class_to_package(const std::string &canonical_classname);
 
void merge_source_location_rec(
  exprt &expr,
  const source_locationt &source_location);
 
#define JAVA_STRING_LITERAL_PREFIX "java::java.lang.String.Literal"
 
bool is_java_string_literal_id(const irep_idt &id);
 
irep_idt resolve_friendly_method_name(
  const std::string &friendly_name,
  const symbol_table_baset &symbol_table,
  std::string &error);
 
pointer_typet pointer_to_replacement_type(
  const pointer_typet &given_pointer_type,
  const java_class_typet &replacement_class_type);
 
dereference_exprt checked_dereference(const exprt &expr);
 
void java_add_components_to_class(
  symbolt &class_symbol,
  const struct_union_typet::componentst &components_to_add);
 
size_t find_closing_delimiter(
  const std::string &src,
  size_t position,
  char open_char,
  char close_char);
 
exprt make_function_application(
  const irep_idt &function_name,
  const exprt::operandst &arguments,
  const typet &range,
  symbol_table_baset &symbol_table);
 
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip);
 
std::string pretty_print_java_type(const std::string &fqn_java_type);
 
std::optional<resolve_inherited_componentt::inherited_componentt>
get_inherited_component(
  const irep_idt &component_class_id,
  const irep_idt &component_name,
  const symbol_table_baset &symbol_table,
  bool include_interfaces);
 
bool is_non_null_library_global(const irep_idt &);
 
extern const std::unordered_set<std::string> cprover_methods_to_ignore;
 
#if defined(__GNUC__) && __GNUC__ >= 14
[[gnu::no_dangling]]
#endif
symbolt &
fresh_java_symbol(
  const typet &type,
  const std::string &basename_prefix,
  const source_locationt &source_location,
  const irep_idt &function_name,
  symbol_table_baset &symbol_table);
 
std::optional<irep_idt> declaring_class(const symbolt &symbol);
 
void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class);
 
[[nodiscard]] std::optional<std::string>
class_name_from_method_name(const std::string &method_name);
 
#endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H