9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H 10 #define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H 12 #include <unordered_set> 51 #define JAVA_STRING_LITERAL_PREFIX "java::java.lang.String.Literal" 65 const std::string &friendly_name,
83 const std::string &src,
109 bool include_interfaces);
115 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H The type of an expression.
bool is_java_string_literal_id(const irep_idt &id)
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
const std::string java_class_to_package(const std::string &canonical_classname)
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
std::vector< componentt > componentst
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.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
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.lang.Integer -> Integer).
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted), leaving the driver program to stub them if it wishes.
Operator to dereference a pointer.
API to expression classes.
Given a class and a component (either field or method), find the closest parent that defines that com...
unsigned java_method_parameter_slots(const code_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call...
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
bool is_non_null_library_global(const irep_idt &)
Check if a symbol is a well-known non-null global.
std::vector< exprt > operandst
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.
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const irep_idt &user_class_id, 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.
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 ...
bool java_is_array_type(const typet &type)
Base class for all expressions.
The symbol table base class interface.
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.
dereference_exprt checked_dereference(const exprt &expr, const typet &type)
Dereference an expression and flag it for a null-pointer check.
goto_programt coverage_criteriont message_handlert & message_handler
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...
void declare_function(irep_idt function_name, const typet &type, symbol_table_baset &symbol_table)
Declare a function with the given name and type.