cprover
|
#include "java_types.h"
#include <cassert>
#include <cctype>
#include <util/std_types.h>
#include <util/c_types.h>
#include <util/std_expr.h>
#include <util/ieee_float.h>
Go to the source code of this file.
Functions | |
typet | java_int_type () |
typet | java_void_type () |
typet | java_long_type () |
typet | java_short_type () |
typet | java_byte_type () |
typet | java_char_type () |
typet | java_float_type () |
typet | java_double_type () |
typet | java_boolean_type () |
reference_typet | java_reference_type (const typet &subtype) |
reference_typet | java_lang_object_type () |
reference_typet | java_array_type (const char subtype) |
bool | is_reference_type (const char t) |
typet | java_type_from_char (char t) |
typet | java_bytecode_promotion (const typet &type) |
Java does not support byte/short return types. These are always promoted. More... | |
exprt | java_bytecode_promotion (const exprt &expr) |
Java does not support byte/short return types. These are always promoted. More... | |
typet | java_type_from_string (const std::string &src) |
char | java_char_from_type (const typet &type) |
static std::string | slash_to_dot (const std::string &src) |
symbol_typet | java_classname (const std::string &id) |
bool is_reference_type | ( | const char | t | ) |
Definition at line 106 of file java_types.cpp.
reference_typet java_array_type | ( | const char | subtype | ) |
Definition at line 77 of file java_types.cpp.
References id2string(), java_reference_type(), java_type_from_char(), and irept::set().
Referenced by java_bytecode_convert_classt::add_array_types(), java_bytecode_convert_methodt::convert_instructions(), and java_type_from_string().
typet java_boolean_type | ( | ) |
Definition at line 59 of file java_types.cpp.
Referenced by java_bytecode_convert_classt::add_string_type(), java_bytecode_convert_methodt::convert_instructions(), expr2javat::convert_rec(), java_bytecode_promotion(), java_root_class(), java_type_from_char(), and java_type_from_string().
typet java_byte_type | ( | ) |
Definition at line 39 of file java_types.cpp.
Referenced by expr2javat::convert_constant(), java_bytecode_convert_methodt::convert_instructions(), expr2javat::convert_rec(), java_bytecode_promotion(), java_char_from_type(), java_type_from_char(), and java_type_from_string().
Java does not support byte/short return types. These are always promoted.
Definition at line 130 of file java_types.cpp.
References java_boolean_type(), java_byte_type(), java_char_type(), java_int_type(), and java_short_type().
Referenced by java_bytecode_convert_methodt::convert_instructions(), and java_bytecode_promotion().
Java does not support byte/short return types. These are always promoted.
Definition at line 142 of file java_types.cpp.
References java_bytecode_promotion(), and exprt::type().
char java_char_from_type | ( | const typet & | type | ) |
Definition at line 252 of file java_types.cpp.
References bitvector_typet::get_width(), irept::id(), java_byte_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_short_type(), to_floatbv_type(), and to_signedbv_type().
Referenced by java_bytecode_convert_methodt::convert().
typet java_char_type | ( | ) |
Definition at line 44 of file java_types.cpp.
Referenced by string_constraint_generatort::add_axioms_for_java_char_array(), java_bytecode_convert_classt::add_string_type(), expr2javat::convert_constant(), java_bytecode_convert_methodt::convert_instructions(), expr2javat::convert_rec(), java_bytecode_promotion(), java_type_from_char(), java_type_from_string(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), and utf16_to_array().
symbol_typet java_classname | ( | const std::string & | id | ) |
Definition at line 294 of file java_types.cpp.
References java_type_from_string(), irept::set(), slash_to_dot(), and to_symbol_type().
Referenced by java_bytecode_parsert::rconstant_pool().
typet java_double_type | ( | ) |
Definition at line 54 of file java_types.cpp.
References ieee_float_spect::double_precision(), and ieee_float_spect::to_type().
Referenced by expr2javat::convert_rec(), java_char_from_type(), java_type_from_char(), and java_type_from_string().
typet java_float_type | ( | ) |
Definition at line 49 of file java_types.cpp.
References ieee_float_spect::single_precision(), and ieee_float_spect::to_type().
Referenced by expr2javat::convert_rec(), java_char_from_type(), java_type_from_char(), and java_type_from_string().
typet java_int_type | ( | ) |
Definition at line 19 of file java_types.cpp.
Referenced by java_bytecode_convert_classt::add_array_types(), string_constraint_generatort::add_axioms_for_java_char_array(), java_bytecode_convert_classt::add_string_type(), java_object_factoryt::allocate_nondet_length_array(), java_bytecode_convert_methodt::convert_instructions(), expr2javat::convert_rec(), java_object_factoryt::gen_nondet_array_init(), java_bytecode_convert_methodt::get_array_bounds_check(), java_bytecode_promotion(), java_char_from_type(), java_type_from_char(), java_type_from_string(), java_bytecode_parsert::rconstant_pool(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), and utf16_to_array().
reference_typet java_lang_object_type | ( | ) |
Definition at line 72 of file java_types.cpp.
References java_reference_type().
typet java_long_type | ( | ) |
Definition at line 29 of file java_types.cpp.
Referenced by expr2javat::convert_constant(), expr2javat::convert_rec(), java_char_from_type(), java_type_from_char(), java_type_from_string(), and java_bytecode_parsert::rconstant_pool().
reference_typet java_reference_type | ( | const typet & | subtype | ) |
Definition at line 67 of file java_types.cpp.
References reference_type(), and to_reference_type().
Referenced by java_bytecode_convert_classt::add_string_type(), java_bytecode_convert_methodt::convert_instructions(), java_array_type(), java_bytecode_convert_method_lazy(), java_entry_point(), java_lang_object_type(), java_type_from_char(), java_type_from_string(), and to_member().
typet java_short_type | ( | ) |
Definition at line 34 of file java_types.cpp.
Referenced by expr2javat::convert_constant(), java_bytecode_convert_methodt::convert_instructions(), expr2javat::convert_rec(), java_bytecode_promotion(), java_char_from_type(), java_type_from_char(), and java_type_from_string().
typet java_type_from_char | ( | char | t | ) |
Definition at line 111 of file java_types.cpp.
References java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_reference_type(), and java_short_type().
Referenced by java_bytecode_convert_classt::add_array_types(), java_bytecode_convert_methodt::convert_instructions(), java_array_type(), and java_bytecode_convert_methodt::variable().
typet java_type_from_string | ( | const std::string & | src | ) |
Definition at line 152 of file java_types.cpp.
References irept::find(), irept::id(), java_array_type(), java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_reference_type(), java_short_type(), java_type_from_string(), java_void_type(), code_typet::parameters(), code_typet::return_type(), irept::set(), typet::subtype(), and exprt::type().
Referenced by java_bytecode_convert_classt::convert(), java_bytecode_convert_methodt::convert(), java_bytecode_parsert::get_class_refs(), java_build_arguments(), java_bytecode_convert_method_lazy(), java_classname(), java_type_from_string(), java_bytecode_convert_methodt::setup_local_variables(), and java_bytecode_parsert::type_entry().
typet java_void_type | ( | ) |
Definition at line 24 of file java_types.cpp.
Referenced by java_type_from_string().
|
static |
Definition at line 285 of file java_types.cpp.
Referenced by java_classname().