cprover
|
#include <expr2c_class.h>
Public Member Functions | |
expr2ct (const namespacet &_ns) | |
virtual | ~expr2ct () |
virtual std::string | convert (const typet &src) |
virtual std::string | convert (const exprt &src) |
void | get_shorthands (const exprt &expr) |
Protected Member Functions | |
virtual std::string | convert_rec (const typet &src, const qualifierst &qualifiers, const std::string &declarator) |
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) |
virtual std::string | convert_code (const codet &src, unsigned indent) |
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) |
virtual std::string | convert_with_precedence (const exprt &src, unsigned &precedence) |
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 (const constant_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) |
virtual std::string | convert_struct (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... | |
Static Protected Member Functions | |
static std::string | indent_str (unsigned indent) |
Protected Attributes | |
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 |
Definition at line 23 of file expr2c_class.h.
|
inlineexplicit |
Definition at line 26 of file expr2c_class.h.
|
inlinevirtual |
Definition at line 27 of file expr2c_class.h.
|
virtual |
Reimplemented in expr2javat.
Definition at line 161 of file expr2c.cpp.
References convert_rec().
Referenced by expr2javat::convert(), convert_allocate(), convert_array(), convert_array_list(), convert_array_member_value(), convert_array_of(), convert_array_type(), convert_byte_extract(), convert_byte_update(), convert_code_asm(), convert_code_assert(), convert_code_assume(), expr2cppt::convert_code_cpp_delete(), convert_code_dead(), convert_code_decl(), convert_code_dowhile(), convert_code_expression(), convert_code_for(), convert_code_free(), convert_code_ifthenelse(), convert_code_lock(), convert_code_return(), convert_code_switch(), convert_code_switch_case(), convert_code_unlock(), convert_code_while(), convert_constant(), expr2cppt::convert_cpp_new(), convert_designated_initializer(), expr2cppt::convert_extractbit(), expr2cppt::convert_extractbits(), convert_Hoare(), convert_index(), convert_index_designator(), convert_initializer_list(), convert_let(), convert_nondet(), convert_object_descriptor(), convert_overflow(), convert_pointer_arithmetic(), convert_pointer_difference(), convert_pointer_object_has_type(), convert_prob_coin(), convert_prob_uniform(), convert_quantifier(), convert_rec(), expr2cppt::convert_rec(), convert_sizeof(), expr2cppt::convert_struct(), convert_struct(), convert_struct_member_value(), convert_symbol(), convert_typecast(), convert_union(), convert_update(), convert_vector(), and convert_with_precedence().
|
virtual |
Reimplemented in expr2javat.
Definition at line 3961 of file expr2c.cpp.
References convert_with_precedence().
|
protected |
Definition at line 1187 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), irept::id(), exprt::op0(), exprt::op1(), exprt::operands(), typet::subtype(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 2182 of file expr2c.cpp.
References char_type(), convert(), namespace_baset::follow(), forall_operands, irept::get_bool(), integer2unsigned(), ns, exprt::operands(), to_integer(), exprt::type(), and wchar_t_type().
Referenced by convert_constant(), and convert_with_precedence().
|
protected |
Definition at line 2288 of file expr2c.cpp.
References convert(), convert_norep(), forall_operands, and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1642 of file expr2c.cpp.
References convert(), convert_norep(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1361 of file expr2c.cpp.
References convert(), convert_norep(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protectedvirtual |
To generate a C-like type declaration of an array.
Includes the size of the array in the []
src | The array type to convert qualifier declarator_str |
Definition at line 732 of file expr2c.cpp.
Referenced by convert_rec().
|
protected |
To generate a C-like type declaration of an array.
Optionally can include or exclude the size of the array in the []
src | The array type to convert qualifier declarator_str |
inc_size_if_possible | Should the generated string include the size of the array (if it is known). |
Definition at line 748 of file expr2c.cpp.
References convert(), convert_rec(), typet::subtype(), and to_array_type().
|
protected |
Definition at line 1040 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), irept::id(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by convert_code_assign(), convert_code_init(), and convert_with_precedence().
|
protected |
Definition at line 1371 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1396 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 3362 of file expr2c.cpp.
Referenced by expr2javat::convert_code(), expr2cppt::convert_code(), convert_code(), convert_code_block(), convert_code_decl_block(), convert_code_dowhile(), convert_code_for(), convert_code_ifthenelse(), convert_code_label(), convert_code_switch(), convert_code_switch_case(), convert_code_while(), convert_Hoare(), convert_statement_expression(), and convert_with_precedence().
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 2889 of file expr2c.cpp.
References convert_code(), convert_code_array_copy(), convert_code_array_replace(), convert_code_array_set(), convert_code_asm(), convert_code_assert(), convert_code_assign(), convert_code_assume(), convert_code_block(), convert_code_break(), convert_code_continue(), convert_code_dead(), convert_code_decl(), convert_code_decl_block(), convert_code_dowhile(), convert_code_expression(), convert_code_fence(), convert_code_for(), convert_code_free(), convert_code_function_call(), convert_code_goto(), convert_code_ifthenelse(), convert_code_init(), convert_code_input(), convert_code_label(), convert_code_lock(), convert_code_output(), convert_code_printf(), convert_code_return(), convert_code_switch(), convert_code_switch_case(), convert_code_unlock(), convert_code_while(), convert_function(), convert_norep(), dstringt::empty(), source_locationt::get_comment(), codet::get_statement(), id2string(), indent_str(), exprt::source_location(), to_code_asm(), to_code_assign(), to_code_block(), to_code_dowhile(), to_code_for(), to_code_function_call(), to_code_ifthenelse(), to_code_label(), to_code_switch_case(), and to_code_while().
|
protected |
Definition at line 3245 of file expr2c.cpp.
References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3267 of file expr2c.cpp.
References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3223 of file expr2c.cpp.
References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 2464 of file expr2c.cpp.
References convert(), forall_operands, code_asmt::get_flavor(), indent_str(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::op3(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3288 of file expr2c.cpp.
References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3021 of file expr2c.cpp.
References convert_binary(), and indent_str().
Referenced by convert_code().
|
protected |
Definition at line 3301 of file expr2c.cpp.
References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 2829 of file expr2c.cpp.
References convert_code(), forall_operands, indent_str(), and to_code().
Referenced by convert_code().
|
protected |
|
protected |
|
protected |
Definition at line 2778 of file expr2c.cpp.
References convert(), convert_norep(), exprt::op0(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 2733 of file expr2c.cpp.
References configt::ansi_c, config, convert(), convert_norep(), convert_rec(), code_typet::get_inlined(), irept::id(), indent_str(), symbolt::is_exported, symbolt::is_extern, symbolt::is_file_local, symbolt::is_static_lifetime, namespacet::lookup(), ns, exprt::op0(), exprt::op1(), exprt::operands(), configt::ansi_ct::os, configt::ansi_ct::OS_WIN, to_code_type(), to_symbol_expr(), symbolt::type, and exprt::type().
Referenced by convert_code().
|
protected |
Definition at line 2852 of file expr2c.cpp.
References convert_code(), forall_operands, and to_code().
Referenced by convert_code().
|
protected |
Definition at line 2568 of file expr2c.cpp.
References code_dowhilet::body(), code_dowhilet::cond(), convert(), convert_code(), convert_norep(), codet::get_statement(), indent_str(), irept::is_nil(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 2867 of file expr2c.cpp.
References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3150 of file expr2c.cpp.
References dstringt::empty(), irept::get_bool(), id2string(), and indent_str().
Referenced by convert_code().
|
protected |
Definition at line 2792 of file expr2c.cpp.
References code_fort::body(), convert(), convert_code(), convert_norep(), codet::get_statement(), indent_str(), irept::is_nil(), exprt::op0(), exprt::op1(), exprt::op2(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3032 of file expr2c.cpp.
References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3080 of file expr2c.cpp.
References code_function_callt::arguments(), convert_norep(), convert_with_precedence(), forall_expr, code_function_callt::function(), indent_str(), irept::is_not_nil(), code_function_callt::lhs(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 2656 of file expr2c.cpp.
References clean_identifier(), irept::get(), and indent_str().
Referenced by convert_code().
|
protected |
Definition at line 2597 of file expr2c.cpp.
References code_ifthenelset::cond(), convert(), convert_code(), convert_norep(), code_ifthenelset::else_case(), indent_str(), irept::is_nil(), exprt::operands(), code_ifthenelset::then_case(), and to_code().
Referenced by convert_code().
|
protected |
Definition at line 3045 of file expr2c.cpp.
References convert_binary(), and indent_str().
Referenced by convert_code().
|
protected |
Definition at line 3180 of file expr2c.cpp.
References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3314 of file expr2c.cpp.
References clean_identifier(), code_labelt::code(), convert_code(), code_labelt::get_label(), and indent_str().
Referenced by convert_code().
|
protected |
Definition at line 3054 of file expr2c.cpp.
References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3202 of file expr2c.cpp.
References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 3128 of file expr2c.cpp.
References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 2634 of file expr2c.cpp.
References convert(), convert_norep(), indent_str(), exprt::op0(), exprt::operands(), and to_code_return().
Referenced by convert_code().
|
protected |
Definition at line 2679 of file expr2c.cpp.
References convert(), convert_code(), convert_norep(), forall_operands, irept::get(), indent_str(), exprt::op0(), exprt::operands(), and to_code().
Referenced by convert_code().
|
protected |
Definition at line 3332 of file expr2c.cpp.
References code_switch_caset::case_op(), code_switch_caset::code(), convert(), convert_code(), codet::get_statement(), indent_str(), and code_switch_caset::is_default().
Referenced by convert_code().
|
protected |
Definition at line 3067 of file expr2c.cpp.
References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 2542 of file expr2c.cpp.
References code_whilet::body(), code_whilet::cond(), convert(), convert_code(), convert_norep(), codet::get_statement(), indent_str(), irept::is_nil(), and exprt::operands().
Referenced by convert_code().
|
protected |
Definition at line 1286 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1310 of file expr2c.cpp.
References convert_with_precedence(), double_type(), float_type(), namespace_baset::follow(), forall_operands, irept::id(), exprt::is_zero(), long_double_type(), ns, exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
|
protected |
Definition at line 1006 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), forall_operands, and exprt::operands().
Referenced by convert_with_precedence().
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 1786 of file expr2c.cpp.
References configt::ansi_c, binary2integer(), build_sizeof_expr(), char_type(), config, convert(), convert_array(), convert_constant_bool(), convert_norep(), convert_with_precedence(), double_type(), irept::find(), float_type(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::get(), constant_exprt::get_value(), has_prefix(), irept::id(), id2string(), integer2string(), integer2ulong(), irept::is_not_nil(), is_signed(), exprt::is_true(), long_double_type(), c_enum_typet::members(), ns, configt::ansi_ct::NULL_is_zero, exprt::op0(), exprt::operands(), signed_int_type(), dstringt::size(), sizeof_nesting, typet::subtype(), fixedbvt::to_ansi_c_string(), ieee_floatt::to_ansi_c_string(), to_c_enum_tag_type(), to_c_enum_type(), to_constant_expr(), exprt::type(), and unsigned_int_type().
Referenced by expr2javat::convert_constant(), expr2cppt::convert_constant(), and convert_with_precedence().
|
protectedvirtual |
To get the C-like representation of a given boolean value.
boolean_value | The value of the constant bool expression |
Definition at line 2017 of file expr2c.cpp.
Referenced by convert_constant().
|
protected |
Definition at line 2350 of file expr2c.cpp.
References convert(), convert_norep(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 3410 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 3425 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), exprt::op0(), exprt::op1(), exprt::op2(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1262 of file expr2c.cpp.
References convert_with_precedence(), forall_operands, and exprt::operands().
Referenced by convert_code(), expr2javat::convert_with_precedence(), expr2cppt::convert_with_precedence(), and convert_with_precedence().
|
protected |
Definition at line 2368 of file expr2c.cpp.
References function_application_exprt::arguments(), convert_with_precedence(), forall_expr, and function_application_exprt::function().
Referenced by convert_with_precedence().
|
protected |
Definition at line 3367 of file expr2c.cpp.
References convert(), convert_code(), convert_norep(), irept::find(), irept::is_nil(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1448 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1556 of file expr2c.cpp.
References convert(), convert_norep(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 2322 of file expr2c.cpp.
References convert(), forall_operands, irept::id(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 942 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), exprt::op0(), exprt::operands(), let_exprt::symbol(), let_exprt::value(), and let_exprt::where().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1245 of file expr2c.cpp.
References irept::get_string().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1566 of file expr2c.cpp.
References struct_union_typet::components(), convert_norep(), convert_with_precedence(), dstringt::empty(), namespace_baset::follow(), irept::get(), struct_union_typet::get_component(), member_exprt::get_component_name(), member_exprt::get_component_number(), irept::get_string(), irept::id(), id2string(), irept::is_nil(), ns, exprt::op0(), exprt::operands(), to_struct_union_type(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1546 of file expr2c.cpp.
References convert_norep(), irept::get_string(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1095 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), forall_operands, irept::id(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1214 of file expr2c.cpp.
References convert(), convert_norep(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1755 of file expr2c.cpp.
Referenced by convert_with_precedence().
|
protected |
Definition at line 1715 of file expr2c.cpp.
References nondet_symbol_exprt::get_identifier(), and id2string().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1662 of file expr2c.cpp.
References lispexprt::expr2string(), irep2lisp(), and MetaString().
Referenced by convert_allocate(), convert_array_list(), convert_array_member_value(), convert_array_of(), convert_binary(), convert_byte_extract(), convert_byte_update(), convert_code(), convert_code_assert(), convert_code_assume(), expr2cppt::convert_code_cpp_delete(), convert_code_dead(), convert_code_decl(), convert_code_dowhile(), convert_code_expression(), convert_code_for(), convert_code_free(), expr2javat::convert_code_function_call(), convert_code_function_call(), convert_code_ifthenelse(), expr2javat::convert_code_java_delete(), convert_code_lock(), convert_code_return(), convert_code_switch(), convert_code_unlock(), convert_code_while(), convert_comma(), convert_cond(), convert_constant(), convert_designated_initializer(), convert_extractbit(), convert_extractbits(), convert_Hoare(), convert_index(), convert_index_designator(), expr2javat::convert_java_instanceof(), convert_let(), convert_member(), convert_member_designator(), convert_multi_ary(), convert_nondet(), convert_object_descriptor(), convert_pointer_arithmetic(), convert_pointer_difference(), convert_pointer_object_has_type(), convert_prob_coin(), convert_prob_uniform(), convert_quantifier(), convert_sizeof(), convert_statement_expression(), expr2javat::convert_struct(), expr2cppt::convert_struct(), convert_struct(), convert_struct_member_value(), convert_trinary(), convert_typecast(), convert_unary(), convert_unary_post(), convert_union(), convert_update(), convert_vector(), convert_with(), and convert_with_precedence().
|
protected |
Definition at line 1762 of file expr2c.cpp.
References convert(), convert_norep(), irept::is_nil(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 2428 of file expr2c.cpp.
References dstringt::c_str(), convert(), convert_with_precedence(), forall_operands, irept::id(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1472 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1509 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1167 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), irept::find(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1731 of file expr2c.cpp.
References irept::get_string().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1739 of file expr2c.cpp.
References irept::get_string().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1723 of file expr2c.cpp.
References irept::get_string().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1235 of file expr2c.cpp.
References convert(), convert_norep(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1252 of file expr2c.cpp.
References convert(), convert_norep(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1747 of file expr2c.cpp.
References irept::get_string().
Referenced by convert_with_precedence().
|
protected |
Definition at line 852 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 166 of file expr2c.cpp.
References configt::ansi_c, c_qualifierst::as_string(), symbolt::base_name, c_type_as_string(), configt::ansi_ct::char_is_unsigned, configt::ansi_ct::char_width, qualifierst::clone(), struct_union_typet::components(), config, convert(), convert_array_type(), convert_struct_type(), configt::ansi_ct::double_width, dstringt::empty(), lispexprt::expr2string(), irept::find(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::get(), fixedbv_typet::get_fraction_bits(), irept::get_string(), struct_union_typet::get_tag(), bitvector_typet::get_width(), code_typet::has_ellipsis(), irept::id(), id2string(), irept::id_string(), configt::ansi_ct::int_width, integer2string(), irep2lisp(), irept::is_nil(), c_qualifierst::is_noreturn, irept::is_not_nil(), is_signed(), configt::ansi_ct::long_double_width, configt::ansi_ct::long_int_width, configt::ansi_ct::long_long_int_width, namespacet::lookup(), c_enum_typet::members(), MetaString(), ns, code_typet::parameters(), c_qualifierst::read(), code_typet::return_type(), configt::ansi_ct::short_int_width, configt::ansi_ct::single_width, vector_typet::size(), sizeof_nesting, string2integer(), typet::subtype(), to_c_bit_field_type(), to_c_enum_tag_type(), to_c_enum_type(), to_code_type(), to_fixedbv_type(), to_floatbv_type(), to_integer(), to_string(), to_struct_tag_type(), to_struct_type(), to_symbol_type(), to_union_tag_type(), to_union_type(), and to_vector_type().
Referenced by convert(), convert_array_type(), convert_code_decl(), expr2javat::convert_rec(), expr2cppt::convert_rec(), and convert_struct_type().
|
protected |
Definition at line 2398 of file expr2c.cpp.
References side_effect_expr_function_callt::arguments(), convert_with_precedence(), forall_expr, and side_effect_expr_function_callt::function().
Referenced by convert_with_precedence().
|
protected |
Definition at line 3442 of file expr2c.cpp.
References convert(), convert_norep(), irept::find(), and exprt::has_operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1224 of file expr2c.cpp.
References convert_code(), convert_norep(), exprt::op0(), exprt::operands(), to_code(), and to_code_block().
Referenced by convert_with_precedence().
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 2026 of file expr2c.cpp.
Referenced by convert_with_precedence().
|
protected |
To generate a C-like string representing a struct.
Can optionally include the padding parameters.
src | The struct declaration expression precedence |
include_padding_components | Should the generated C code include the padding members added to structs for GOTOs benefit |
Definition at line 2040 of file expr2c.cpp.
References struct_union_typet::components(), convert(), convert_norep(), namespace_baset::follow(), irept::id(), ns, exprt::operands(), to_struct_type(), and exprt::type().
|
protected |
Definition at line 1652 of file expr2c.cpp.
References convert(), convert_norep(), irept::get_string(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protectedvirtual |
To generate C-like string for defining the given struct.
src | the struct type being converted |
qualifiers | any qualifiers on the type |
declarator | the declarator on the type |
Definition at line 659 of file expr2c.cpp.
Referenced by convert_rec().
|
protected |
To generate C-like string for declaring (or defining) the given struct.
src | the struct type being converted |
qualifiers | any qualifiers on the type |
declarator | the declarator on the type |
inc_struct_body | when generating the code, should we include a complete definition of the struct |
inc_padding_components | should the padding parameters be included Note this only makes sense if inc_struct_body |
Definition at line 677 of file expr2c.cpp.
References struct_union_typet::components(), convert_rec(), struct_union_typet::get_tag(), id2string(), and to_struct_type().
|
protectedvirtual |
Definition at line 1673 of file expr2c.cpp.
References convert(), irept::get(), get_shorthands(), irept::get_string(), has_prefix(), irept::id(), id2string(), exprt::op0(), exprt::operands(), shorthands, sizeof_nesting, and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 802 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), exprt::op0(), exprt::op1(), exprt::op2(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 768 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), namespace_baset::follow(), from_type(), irept::id(), ns, unary_exprt::op(), exprt::operands(), and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1144 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), has_prefix(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 1426 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 2161 of file expr2c.cpp.
References convert(), convert_norep(), irept::get_string(), exprt::op0(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 962 of file expr2c.cpp.
References convert(), convert_norep(), convert_with_precedence(), forall_operands, exprt::op0(), exprt::op1(), exprt::op2(), and exprt::operands().
Referenced by convert_with_precedence().
|
protected |
Definition at line 2114 of file expr2c.cpp.
References convert(), convert_norep(), namespace_baset::follow(), forall_operands, irept::id(), ns, and exprt::type().
Referenced by convert_with_precedence().
|
protected |
Definition at line 874 of file expr2c.cpp.
References convert_norep(), convert_with_precedence(), dstringt::empty(), namespace_baset::follow(), struct_union_typet::get_component(), struct_union_typet::componentt::get_pretty_name(), id2string(), irept::is_not_nil(), ns, exprt::op0(), exprt::operands(), to_struct_union_type(), and exprt::type().
Referenced by convert_with_precedence().
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 3456 of file expr2c.cpp.
References configt::ansi_c, config, convert(), convert_allocate(), convert_array(), convert_array_list(), convert_array_member_value(), convert_array_of(), convert_binary(), convert_byte_extract(), convert_byte_update(), convert_code(), convert_comma(), convert_complex(), convert_cond(), convert_constant(), convert_designated_initializer(), convert_extractbit(), convert_extractbits(), convert_function(), convert_function_application(), convert_Hoare(), convert_index(), convert_index_designator(), convert_initializer_list(), convert_let(), convert_literal(), convert_member(), convert_member_designator(), convert_multi_ary(), convert_nondet(), convert_nondet_bool(), convert_nondet_symbol(), convert_norep(), convert_object_descriptor(), convert_overflow(), convert_pointer_arithmetic(), convert_pointer_difference(), convert_pointer_object_has_type(), convert_predicate_next_symbol(), convert_predicate_passive_symbol(), convert_predicate_symbol(), convert_prob_coin(), convert_prob_uniform(), convert_quantified_symbol(), convert_quantifier(), convert_side_effect_expr_function_call(), convert_sizeof(), convert_statement_expression(), convert_struct(), convert_struct_member_value(), convert_symbol(), convert_trinary(), convert_typecast(), convert_unary(), convert_unary_post(), convert_union(), convert_update(), convert_vector(), convert_with(), namespace_baset::follow(), irept::get(), irept::get_string(), has_prefix(), irept::id(), id2string(), irept::id_string(), integer2string(), exprt::is_zero(), MetaString(), configt::ansi_ct::mode, ns, exprt::op0(), exprt::op1(), exprt::operands(), pointer_offset_bits(), typet::subtype(), to_code(), to_constant_expr(), to_function_application_expr(), to_index_expr(), to_let_expr(), to_member_expr(), to_nondet_symbol_expr(), to_side_effect_expr_function_call(), to_typecast_expr(), exprt::type(), and configt::ansi_ct::VISUAL_STUDIO.
Referenced by convert(), convert_allocate(), convert_binary(), convert_byte_extract(), convert_byte_update(), convert_code_array_copy(), convert_code_array_replace(), convert_code_array_set(), convert_code_function_call(), convert_code_input(), convert_code_output(), convert_code_printf(), convert_comma(), convert_complex(), convert_cond(), convert_constant(), convert_extractbit(), convert_extractbits(), convert_function(), convert_function_application(), convert_index(), convert_let(), convert_member(), convert_multi_ary(), convert_overflow(), convert_pointer_arithmetic(), convert_pointer_difference(), convert_pointer_object_has_type(), convert_quantifier(), convert_side_effect_expr_function_call(), convert_trinary(), convert_typecast(), convert_unary(), convert_unary_post(), convert_update(), convert_with(), expr2javat::convert_with_precedence(), and expr2cppt::convert_with_precedence().
void expr2ct::get_shorthands | ( | const exprt & | expr | ) |
Definition at line 87 of file expr2c.cpp.
References clean_identifier(), find_symbols(), source_locationt::get_function(), id2string(), id_shorthand(), symbolt::is_parameter, symbolt::location, namespacet::lookup(), ns, ns_collision, shorthands, and UNREACHABLE.
Referenced by convert_symbol().
Definition at line 44 of file expr2c.cpp.
References symbolt::base_name, dstringt::empty(), has_suffix(), id2string(), namespacet::lookup(), ns, pos(), and size_type().
Referenced by get_shorthands().
|
staticprotected |
Definition at line 2459 of file expr2c.cpp.
Referenced by convert_code(), convert_code_array_copy(), convert_code_array_replace(), convert_code_array_set(), convert_code_asm(), convert_code_assert(), convert_code_assign(), convert_code_assume(), convert_code_block(), convert_code_break(), convert_code_continue(), expr2cppt::convert_code_cpp_delete(), convert_code_decl(), convert_code_dowhile(), convert_code_expression(), convert_code_fence(), convert_code_for(), convert_code_free(), expr2javat::convert_code_function_call(), convert_code_function_call(), convert_code_goto(), convert_code_ifthenelse(), convert_code_init(), convert_code_input(), expr2javat::convert_code_java_delete(), convert_code_label(), convert_code_lock(), convert_code_output(), convert_code_printf(), convert_code_return(), convert_code_switch(), convert_code_switch_case(), convert_code_unlock(), and convert_code_while().
|
protected |
Definition at line 35 of file expr2c_class.h.
Referenced by expr2javat::convert(), convert_array(), convert_code_decl(), convert_complex(), convert_constant(), convert_member(), convert_rec(), expr2cppt::convert_rec(), expr2javat::convert_struct(), expr2cppt::convert_struct(), convert_struct(), convert_typecast(), convert_vector(), convert_with(), convert_with_precedence(), get_shorthands(), and id_shorthand().
Definition at line 67 of file expr2c_class.h.
Referenced by get_shorthands().
Definition at line 68 of file expr2c_class.h.
Referenced by convert_symbol(), and get_shorthands().
|
protected |
Definition at line 70 of file expr2c_class.h.
Referenced by convert_constant(), convert_rec(), and convert_symbol().