cprover
|
#include <expr2c_class.h>
Public Member Functions | |
expr2ct (const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration) | |
virtual | ~expr2ct () |
virtual std::string | convert (const typet &src) |
virtual std::string | convert (const exprt &src) |
void | get_shorthands (const exprt &expr) |
std::string | convert_with_identifier (const typet &src, const std::string &identifier) |
Build a declaration string, which requires converting both a type and putting an identifier in the syntactically correct position. | |
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. | |
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. | |
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. | |
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. | |
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 binary_exprt &, 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_array_of (const exprt &src, unsigned precedence) |
std::string | convert_trinary (const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence) |
std::string | convert_rox (const shift_exprt &src, unsigned precedence) |
Conversion function from rol/ror expressions to C code strings Note that this constructs a complex expression to do bit twiddling since rol/ror operations are not native to ANSI-C. | |
std::string | convert_overflow (const exprt &src, unsigned &precedence) |
std::string | convert_quantifier (const quantifier_exprt &, const std::string &symbol, unsigned precedence) |
std::string | convert_with (const exprt &src, unsigned precedence) |
std::string | convert_update (const update_exprt &, 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 byte_extract_exprt &, unsigned precedence) |
std::string | convert_byte_update (const byte_update_exprt &, unsigned precedence) |
std::string | convert_extractbit (const extractbit_exprt &, unsigned precedence) |
std::string | convert_extractbits (const extractbits_exprt &src, unsigned precedence) |
std::string | convert_unary (const unary_exprt &, const std::string &symbol, unsigned precedence) |
std::string | convert_unary_post (const exprt &src, const std::string &symbol, unsigned precedence) |
optionalt< std::string > | convert_function (const exprt &src) |
Returns a string if src is a function with a known conversion, else returns nullopt. | |
std::string | convert_function (const exprt &src, const std::string &symbol) |
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_frontend_assign (const code_frontend_assignt &, 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 (unsigned indent) |
std::string | convert_code_switch (const codet &src, unsigned indent) |
std::string | convert_code_continue (unsigned indent) |
std::string | convert_code_frontend_decl (const codet &, 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) |
std::string | convert_side_effect_expr_function_call (const side_effect_expr_function_callt &src) |
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) |
std::string | convert_predicate_symbol (const exprt &src) |
std::string | convert_predicate_next_symbol (const exprt &src) |
std::string | convert_predicate_passive_symbol (const exprt &src) |
std::string | convert_nondet_symbol (const nondet_symbol_exprt &) |
std::string | convert_quantified_symbol (const exprt &src) |
std::string | convert_nondet_bool () |
std::string | convert_object_descriptor (const exprt &src, unsigned &precedence) |
std::string | convert_literal (const exprt &src) |
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. | |
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) |
std::string | convert_array_list (const exprt &src, unsigned &precedence) |
std::string | convert_initializer_list (const exprt &src) |
std::string | convert_designated_initializer (const exprt &src) |
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. | |
std::string | convert_conditional_target_group (const exprt &src) |
std::string | convert_bitreverse (const bitreverse_exprt &src) |
Static Protected Member Functions | |
static std::string | indent_str (unsigned indent) |
Protected Attributes | |
const namespacet & | ns |
const expr2c_configurationt & | configuration |
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 29 of file expr2c_class.h.
|
inlineexplicit |
Definition at line 32 of file expr2c_class.h.
|
inlinevirtual |
Definition at line 39 of file expr2c_class.h.
|
virtual |
Reimplemented in expr2javat.
Definition at line 3993 of file expr2c.cpp.
|
virtual |
Reimplemented in expr2javat.
Definition at line 214 of file expr2c.cpp.
Definition at line 1147 of file expr2c.cpp.
|
protected |
Definition at line 2155 of file expr2c.cpp.
Definition at line 2256 of file expr2c.cpp.
|
protected |
Definition at line 1598 of file expr2c.cpp.
Definition at line 1321 of file expr2c.cpp.
|
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 |
qualifiers | Any qualifiers on the type |
declarator_str | Previously computed string denoting the array symbol |
Definition at line 715 of file expr2c.cpp.
|
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 |
qualifiers | Any qualifiers on the type |
declarator_str | Previously computed string denoting the array symbol |
inc_size_if_possible | Should the generated string include the size of the array (if it is known). |
Definition at line 732 of file expr2c.cpp.
|
protected |
Definition at line 1026 of file expr2c.cpp.
|
protected |
Definition at line 3504 of file expr2c.cpp.
|
protected |
Definition at line 1331 of file expr2c.cpp.
|
protected |
Definition at line 1357 of file expr2c.cpp.
|
protected |
Definition at line 3393 of file expr2c.cpp.
Reimplemented in expr2javat, and expr2cppt.
Definition at line 2931 of file expr2c.cpp.
Definition at line 3275 of file expr2c.cpp.
Definition at line 3297 of file expr2c.cpp.
Definition at line 3253 of file expr2c.cpp.
Definition at line 2512 of file expr2c.cpp.
Definition at line 3318 of file expr2c.cpp.
Definition at line 3331 of file expr2c.cpp.
|
protected |
Definition at line 2871 of file expr2c.cpp.
|
protected |
Definition at line 2715 of file expr2c.cpp.
|
protected |
Definition at line 2767 of file expr2c.cpp.
Definition at line 2820 of file expr2c.cpp.
Definition at line 2894 of file expr2c.cpp.
|
protected |
Definition at line 2616 of file expr2c.cpp.
Definition at line 2909 of file expr2c.cpp.
Definition at line 3180 of file expr2c.cpp.
Definition at line 2834 of file expr2c.cpp.
|
protected |
Definition at line 3076 of file expr2c.cpp.
Definition at line 2777 of file expr2c.cpp.
|
protected |
Definition at line 3110 of file expr2c.cpp.
Definition at line 2703 of file expr2c.cpp.
|
protected |
Definition at line 2645 of file expr2c.cpp.
Definition at line 3210 of file expr2c.cpp.
|
protected |
Definition at line 3345 of file expr2c.cpp.
Definition at line 3084 of file expr2c.cpp.
Definition at line 3232 of file expr2c.cpp.
Definition at line 3158 of file expr2c.cpp.
Definition at line 2682 of file expr2c.cpp.
Definition at line 2724 of file expr2c.cpp.
|
protected |
Definition at line 3363 of file expr2c.cpp.
Definition at line 3097 of file expr2c.cpp.
|
protected |
Definition at line 2590 of file expr2c.cpp.
Definition at line 1247 of file expr2c.cpp.
Definition at line 1271 of file expr2c.cpp.
Definition at line 992 of file expr2c.cpp.
|
protected |
Definition at line 3479 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2javat, and expr2cppt.
Definition at line 1731 of file expr2c.cpp.
|
protectedvirtual |
To get the C-like representation of a given boolean value.
boolean_value | The value of the constant bool expression |
Definition at line 1992 of file expr2c.cpp.
|
protected |
Definition at line 2376 of file expr2c.cpp.
|
protected |
Definition at line 3442 of file expr2c.cpp.
|
protected |
Definition at line 3453 of file expr2c.cpp.
Returns a string if src
is a function with a known conversion, else returns nullopt.
Definition at line 3939 of file expr2c.cpp.
|
protected |
Definition at line 1226 of file expr2c.cpp.
|
protected |
Definition at line 2419 of file expr2c.cpp.
|
protected |
Definition at line 3398 of file expr2c.cpp.
Definition at line 1404 of file expr2c.cpp.
|
protected |
Definition at line 1514 of file expr2c.cpp.
|
protected |
Definition at line 2290 of file expr2c.cpp.
Definition at line 927 of file expr2c.cpp.
|
protected |
Definition at line 1210 of file expr2c.cpp.
|
protected |
Definition at line 1524 of file expr2c.cpp.
|
protected |
Definition at line 1504 of file expr2c.cpp.
|
protected |
Definition at line 1078 of file expr2c.cpp.
Definition at line 1175 of file expr2c.cpp.
|
protected |
Definition at line 1702 of file expr2c.cpp.
|
protected |
Definition at line 1672 of file expr2c.cpp.
Definition at line 1618 of file expr2c.cpp.
|
protected |
Definition at line 1707 of file expr2c.cpp.
Definition at line 2476 of file expr2c.cpp.
|
protected |
Definition at line 1428 of file expr2c.cpp.
|
protected |
Definition at line 1465 of file expr2c.cpp.
|
protected |
Definition at line 1684 of file expr2c.cpp.
|
protected |
Definition at line 1690 of file expr2c.cpp.
|
protected |
Definition at line 1678 of file expr2c.cpp.
Definition at line 1200 of file expr2c.cpp.
Definition at line 1215 of file expr2c.cpp.
|
protected |
Definition at line 1696 of file expr2c.cpp.
|
protected |
Definition at line 835 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2javat, and expr2cppt.
Definition at line 219 of file expr2c.cpp.
|
protected |
Conversion function from rol/ror expressions to C code strings Note that this constructs a complex expression to do bit twiddling since rol/ror operations are not native to ANSI-C.
The complex expression is then recursively converted.
src | is an exprt that must be either an rol or ror |
precedence | precedence for bracketing |
Definition at line 2316 of file expr2c.cpp.
|
protected |
Definition at line 2447 of file expr2c.cpp.
Definition at line 3465 of file expr2c.cpp.
|
protected |
Definition at line 1185 of file expr2c.cpp.
Reimplemented in expr2javat, and expr2cppt.
Definition at line 2000 of file expr2c.cpp.
|
protected |
To generate a C-like string representing a struct.
Can optionally include the padding parameters.
src | The struct declaration expression | |
[out] | precedence | Precedence of the top level operator in the resulting string, used to decide about adding parentheses |
include_padding_components | Should the generated C code include the padding members added to structs for GOTOs benefit |
Definition at line 2016 of file expr2c.cpp.
|
protected |
Definition at line 1608 of file expr2c.cpp.
|
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 661 of file expr2c.cpp.
|
protectedvirtual |
To generate C-like string for defining the given struct.
src | the struct type being converted |
qualifiers_str | any qualifiers on the type |
declarator_str | the declarator on the type |
Definition at line 638 of file expr2c.cpp.
|
protectedvirtual |
Definition at line 1629 of file expr2c.cpp.
|
protected |
Definition at line 788 of file expr2c.cpp.
|
protected |
Definition at line 754 of file expr2c.cpp.
|
protected |
Definition at line 1127 of file expr2c.cpp.
|
protected |
Definition at line 1382 of file expr2c.cpp.
Definition at line 2136 of file expr2c.cpp.
|
protected |
Definition at line 954 of file expr2c.cpp.
Definition at line 2089 of file expr2c.cpp.
Definition at line 858 of file expr2c.cpp.
std::string expr2ct::convert_with_identifier | ( | const typet & | src, |
const std::string & | identifier | ||
) |
Build a declaration string, which requires converting both a type and putting an identifier in the syntactically correct position.
src | the type to convert |
identifier | the identifier to use as the type |
Definition at line 4004 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2javat, and expr2cppt.
Definition at line 3520 of file expr2c.cpp.
Definition at line 117 of file expr2c.cpp.
Definition at line 76 of file expr2c.cpp.
|
staticprotected |
Definition at line 2507 of file expr2c.cpp.
|
protected |
Definition at line 51 of file expr2c_class.h.
|
protected |
Definition at line 50 of file expr2c_class.h.
Definition at line 83 of file expr2c_class.h.
Definition at line 84 of file expr2c_class.h.
|
protected |
Definition at line 86 of file expr2c_class.h.