cprover
|
#include <expr2java.h>
Public Member Functions | |
expr2javat (const namespacet &_ns) | |
virtual std::string | convert (const typet &src) override |
virtual std::string | convert (const exprt &src) override |
![]() | |
expr2ct (const namespacet &_ns) | |
virtual | ~expr2ct () |
void | get_shorthands (const exprt &expr) |
Protected Member Functions | |
virtual std::string | convert_with_precedence (const exprt &src, unsigned &precedence) override |
std::string | convert_java_this (const exprt &src, unsigned precedence) |
std::string | convert_java_instanceof (const exprt &src, unsigned precedence) |
std::string | convert_java_new (const exprt &src, unsigned precedence) |
std::string | convert_code_java_delete (const exprt &src, unsigned precedence) |
virtual std::string | convert_struct (const exprt &src, unsigned &precedence) override |
virtual std::string | convert_code (const codet &src, unsigned indent) override |
virtual std::string | convert_constant (const constant_exprt &src, unsigned &precedence) override |
std::string | convert_code_function_call (const code_function_callt &src, unsigned indent) |
virtual std::string | convert_rec (const typet &src, const qualifierst &qualifiers, const std::string &declarator) override |
![]() | |
virtual std::string | convert_struct_type (const typet &src, const std::string &qualifiers_str, const std::string &declarator_str) |
To generate C-like string for defining the given struct. More... | |
std::string | convert_struct_type (const typet &src, const std::string &qualifer_str, const std::string &declarator_str, bool inc_struct_body, bool inc_padding_components) |
To generate C-like string for declaring (or defining) the given struct. More... | |
virtual std::string | convert_array_type (const typet &src, const qualifierst &qualifiers, const std::string &declarator_str) |
To generate a C-like type declaration of an array. More... | |
std::string | convert_array_type (const typet &src, const qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible) |
To generate a C-like type declaration of an array. More... | |
irep_idt | id_shorthand (const irep_idt &identifier) const |
std::string | convert_typecast (const typecast_exprt &src, unsigned &precedence) |
std::string | convert_pointer_arithmetic (const exprt &src, unsigned &precedence) |
std::string | convert_pointer_difference (const exprt &src, unsigned &precedence) |
std::string | convert_binary (const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses) |
std::string | convert_multi_ary (const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses) |
std::string | convert_cond (const exprt &src, unsigned precedence) |
std::string | convert_struct_member_value (const exprt &src, unsigned precedence) |
std::string | convert_array_member_value (const exprt &src, unsigned precedence) |
std::string | convert_member (const member_exprt &src, unsigned precedence) |
std::string | convert_pointer_object_has_type (const exprt &src, unsigned precedence) |
std::string | convert_array_of (const exprt &src, unsigned precedence) |
std::string | convert_trinary (const exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence) |
std::string | convert_overflow (const exprt &src, unsigned &precedence) |
std::string | convert_quantifier (const exprt &src, const std::string &symbol, unsigned precedence) |
std::string | convert_with (const exprt &src, unsigned precedence) |
std::string | convert_update (const exprt &src, unsigned precedence) |
std::string | convert_member_designator (const exprt &src) |
std::string | convert_index_designator (const exprt &src) |
std::string | convert_index (const exprt &src, unsigned precedence) |
std::string | convert_byte_extract (const exprt &src, unsigned precedence) |
std::string | convert_byte_update (const exprt &src, unsigned precedence) |
std::string | convert_extractbit (const exprt &src, unsigned precedence) |
std::string | convert_extractbits (const exprt &src, unsigned precedence) |
std::string | convert_unary (const exprt &src, const std::string &symbol, unsigned precedence) |
std::string | convert_unary_post (const exprt &src, const std::string &symbol, unsigned precedence) |
std::string | convert_function (const exprt &src, const std::string &symbol, unsigned precedence) |
std::string | convert_complex (const exprt &src, unsigned precedence) |
std::string | convert_comma (const exprt &src, unsigned precedence) |
std::string | convert_Hoare (const exprt &src) |
std::string | convert_code (const codet &src) |
std::string | convert_code_label (const code_labelt &src, unsigned indent) |
std::string | convert_code_switch_case (const code_switch_caset &src, unsigned indent) |
std::string | convert_code_asm (const code_asmt &src, unsigned indent) |
std::string | convert_code_assign (const code_assignt &src, unsigned indent) |
std::string | convert_code_free (const codet &src, unsigned indent) |
std::string | convert_code_init (const codet &src, unsigned indent) |
std::string | convert_code_ifthenelse (const code_ifthenelset &src, unsigned indent) |
std::string | convert_code_for (const code_fort &src, unsigned indent) |
std::string | convert_code_while (const code_whilet &src, unsigned indent) |
std::string | convert_code_dowhile (const code_dowhilet &src, unsigned indent) |
std::string | convert_code_block (const code_blockt &src, unsigned indent) |
std::string | convert_code_expression (const codet &src, unsigned indent) |
std::string | convert_code_return (const codet &src, unsigned indent) |
std::string | convert_code_goto (const codet &src, unsigned indent) |
std::string | convert_code_assume (const codet &src, unsigned indent) |
std::string | convert_code_assert (const codet &src, unsigned indent) |
std::string | convert_code_break (const codet &src, unsigned indent) |
std::string | convert_code_switch (const codet &src, unsigned indent) |
std::string | convert_code_continue (const codet &src, unsigned indent) |
std::string | convert_code_decl (const codet &src, unsigned indent) |
std::string | convert_code_decl_block (const codet &src, unsigned indent) |
std::string | convert_code_dead (const codet &src, unsigned indent) |
std::string | convert_code_function_call (const code_function_callt &src, unsigned indent) |
std::string | convert_code_lock (const codet &src, unsigned indent) |
std::string | convert_code_unlock (const codet &src, unsigned indent) |
std::string | convert_code_printf (const codet &src, unsigned indent) |
std::string | convert_code_fence (const codet &src, unsigned indent) |
std::string | convert_code_input (const codet &src, unsigned indent) |
std::string | convert_code_output (const codet &src, unsigned indent) |
std::string | convert_code_array_set (const codet &src, unsigned indent) |
std::string | convert_code_array_copy (const codet &src, unsigned indent) |
std::string | convert_code_array_replace (const codet &src, unsigned indent) |
std::string | convert_function_application (const function_application_exprt &src, unsigned &precedence) |
std::string | convert_side_effect_expr_function_call (const side_effect_expr_function_callt &src, unsigned &precedence) |
std::string | convert_allocate (const exprt &src, unsigned &precedence) |
std::string | convert_nondet (const exprt &src, unsigned &precedence) |
std::string | convert_prob_coin (const exprt &src, unsigned &precedence) |
std::string | convert_prob_uniform (const exprt &src, unsigned &precedence) |
std::string | convert_statement_expression (const exprt &src, unsigned &precendence) |
virtual std::string | convert_symbol (const exprt &src, unsigned &precedence) |
std::string | convert_predicate_symbol (const exprt &src, unsigned &precedence) |
std::string | convert_predicate_next_symbol (const exprt &src, unsigned &precedence) |
std::string | convert_predicate_passive_symbol (const exprt &src, unsigned &precedence) |
std::string | convert_nondet_symbol (const nondet_symbol_exprt &, unsigned &precedence) |
std::string | convert_quantified_symbol (const exprt &src, unsigned &precedence) |
std::string | convert_nondet_bool (const exprt &src, unsigned &precedence) |
std::string | convert_object_descriptor (const exprt &src, unsigned &precedence) |
std::string | convert_literal (const exprt &src, unsigned &precedence) |
virtual std::string | convert_constant_bool (bool boolean_value) |
To get the C-like representation of a given boolean value. More... | |
std::string | convert_norep (const exprt &src, unsigned &precedence) |
std::string | convert_union (const exprt &src, unsigned &precedence) |
std::string | convert_vector (const exprt &src, unsigned &precedence) |
std::string | convert_array (const exprt &src, unsigned &precedence) |
std::string | convert_array_list (const exprt &src, unsigned &precedence) |
std::string | convert_initializer_list (const exprt &src, unsigned &precedence) |
std::string | convert_designated_initializer (const exprt &src, unsigned &precedence) |
std::string | convert_concatenation (const exprt &src, unsigned &precedence) |
std::string | convert_sizeof (const exprt &src, unsigned &precedence) |
std::string | convert_let (const let_exprt &, unsigned precedence) |
std::string | convert_struct (const exprt &src, unsigned &precedence, bool include_padding_components) |
To generate a C-like string representing a struct. More... | |
Protected Attributes | |
const std::size_t | char_representation_length =8 |
![]() | |
const namespacet & | ns |
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > | ns_collision |
std::unordered_map< irep_idt, irep_idt > | shorthands |
unsigned | sizeof_nesting |
Additional Inherited Members | |
![]() | |
static std::string | indent_str (unsigned indent) |
Definition at line 19 of file expr2java.h.
|
inlineexplicit |
Definition at line 22 of file expr2java.h.
|
overridevirtual |
Reimplemented from expr2ct.
Definition at line 28 of file expr2java.cpp.
References convert_rec(), and expr2ct::ns.
Referenced by convert_code_java_delete(), convert_java_instanceof(), convert_java_new(), convert_rec(), convert_struct(), and convert_with_precedence().
|
overridevirtual |
Reimplemented from expr2ct.
Definition at line 33 of file expr2java.cpp.
References expr2ct::convert().
|
overrideprotectedvirtual |
Reimplemented from expr2ct.
Definition at line 439 of file expr2java.cpp.
References expr2ct::convert_code(), convert_code_function_call(), convert_java_new(), irept::get(), and to_code_function_call().
|
protected |
Definition at line 38 of file expr2java.cpp.
References code_function_callt::arguments(), expr2ct::convert_norep(), convert_with_precedence(), forall_expr, code_function_callt::function(), code_typet::has_this(), expr2ct::indent_str(), irept::is_not_nil(), code_function_callt::lhs(), exprt::operands(), to_code_type(), and exprt::type().
Referenced by convert_code().
|
protected |
Definition at line 373 of file expr2java.cpp.
References convert(), expr2ct::convert_norep(), expr2ct::indent_str(), exprt::op0(), and exprt::operands().
|
overrideprotectedvirtual |
Reimplemented from expr2ct.
Definition at line 172 of file expr2java.cpp.
References char_representation_length, expr2ct::convert_constant(), floating_point_to_java_string(), irept::id(), integer2string(), ieee_floatt::is_double(), exprt::is_false(), exprt::is_true(), exprt::is_zero(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_long_type(), java_short_type(), to_constant_expr(), ieee_floatt::to_double(), ieee_floatt::to_float(), to_integer(), exprt::type(), UNREACHABLE, and utf16_little_endian_to_java().
Referenced by convert_with_precedence().
|
protected |
Definition at line 334 of file expr2java.cpp.
References convert(), expr2ct::convert_norep(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 347 of file expr2java.cpp.
References convert(), irept::find(), irept::get(), typet::subtype(), and exprt::type().
Referenced by convert_code(), and convert_with_precedence().
|
protected |
Definition at line 327 of file expr2java.cpp.
Referenced by convert_with_precedence().
|
overrideprotectedvirtual |
Reimplemented from expr2ct.
Definition at line 252 of file expr2java.cpp.
References qualifierst::as_string(), qualifierst::clone(), convert(), expr2ct::convert_rec(), code_typet::has_ellipsis(), irept::id(), java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_short_type(), code_typet::parameters(), qualifierst::read(), code_typet::return_type(), and to_code_type().
Referenced by convert().
|
overrideprotectedvirtual |
Reimplemented from expr2ct.
Definition at line 108 of file expr2java.cpp.
References struct_union_typet::components(), convert(), expr2ct::convert_norep(), namespace_baset::follow(), irept::id(), expr2ct::ns, exprt::operands(), to_struct_type(), and exprt::type().
|
overrideprotectedvirtual |
Reimplemented from expr2ct.
Definition at line 392 of file expr2java.cpp.
References code_landingpadt::catch_expr(), convert(), convert_constant(), expr2ct::convert_function(), convert_java_instanceof(), convert_java_new(), convert_java_this(), expr2ct::convert_with_precedence(), irept::get(), codet::get_statement(), irept::get_string(), irept::id(), id2string(), MetaString(), to_code(), to_code_landingpad(), to_constant_expr(), and exprt::type().
Referenced by convert_code_function_call().
|
protected |
Definition at line 49 of file expr2java.h.
Referenced by convert_constant().