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 c_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 c_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 c_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_binding (const binding_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 binary_exprt &, 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) |
std::optional< 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. | |
virtual std::string | convert_annotated_pointer_constant (const annotated_pointer_constant_exprt &src, unsigned &precedence) |
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) |
std::string | convert_r_or_w_ok (const r_or_w_ok_exprt &src) |
std::string | convert_prophecy_r_or_w_ok (const prophecy_r_or_w_ok_exprt &src) |
std::string | convert_pointer_in_range (const pointer_in_range_exprt &src) |
std::string | convert_prophecy_pointer_in_range (const prophecy_pointer_in_range_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 34 of file expr2c_class.h.
|
inlineexplicit |
Definition at line 37 of file expr2c_class.h.
|
inlinevirtual |
Definition at line 44 of file expr2c_class.h.
|
virtual |
Reimplemented in expr2javat.
Definition at line 4166 of file expr2c.cpp.
|
virtual |
Reimplemented in expr2javat.
Definition at line 213 of file expr2c.cpp.
|
protected |
Definition at line 1154 of file expr2c.cpp.
|
protectedvirtual |
Definition at line 2046 of file expr2c.cpp.
|
protected |
Definition at line 2222 of file expr2c.cpp.
|
protected |
Definition at line 2325 of file expr2c.cpp.
|
protected |
Definition at line 1608 of file expr2c.cpp.
|
protected |
Definition at line 1328 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 726 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 743 of file expr2c.cpp.
|
protected |
Definition at line 1034 of file expr2c.cpp.
|
protected |
Definition at line 846 of file expr2c.cpp.
|
protected |
Definition at line 3582 of file expr2c.cpp.
|
protected |
Definition at line 1338 of file expr2c.cpp.
|
protected |
Definition at line 1364 of file expr2c.cpp.
|
protected |
Definition at line 3462 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 3000 of file expr2c.cpp.
|
protected |
Definition at line 3344 of file expr2c.cpp.
|
protected |
Definition at line 3366 of file expr2c.cpp.
|
protected |
Definition at line 3322 of file expr2c.cpp.
|
protected |
Definition at line 2581 of file expr2c.cpp.
|
protected |
Definition at line 3387 of file expr2c.cpp.
|
protected |
Definition at line 3400 of file expr2c.cpp.
|
protected |
Definition at line 2940 of file expr2c.cpp.
|
protected |
Definition at line 2784 of file expr2c.cpp.
|
protected |
Definition at line 2836 of file expr2c.cpp.
|
protected |
Definition at line 2889 of file expr2c.cpp.
|
protected |
Definition at line 2963 of file expr2c.cpp.
|
protected |
Definition at line 2685 of file expr2c.cpp.
|
protected |
Definition at line 2978 of file expr2c.cpp.
|
protected |
Definition at line 3249 of file expr2c.cpp.
|
protected |
Definition at line 2903 of file expr2c.cpp.
|
protected |
Definition at line 3145 of file expr2c.cpp.
|
protected |
Definition at line 2846 of file expr2c.cpp.
|
protected |
Definition at line 3179 of file expr2c.cpp.
|
protected |
Definition at line 2772 of file expr2c.cpp.
|
protected |
Definition at line 2714 of file expr2c.cpp.
|
protected |
Definition at line 3279 of file expr2c.cpp.
|
protected |
Definition at line 3414 of file expr2c.cpp.
|
protected |
Definition at line 3153 of file expr2c.cpp.
|
protected |
Definition at line 3301 of file expr2c.cpp.
|
protected |
Definition at line 3227 of file expr2c.cpp.
|
protected |
Definition at line 2751 of file expr2c.cpp.
|
protected |
Definition at line 2793 of file expr2c.cpp.
|
protected |
Definition at line 3432 of file expr2c.cpp.
|
protected |
Definition at line 3166 of file expr2c.cpp.
|
protected |
Definition at line 2659 of file expr2c.cpp.
|
protected |
Definition at line 1254 of file expr2c.cpp.
|
protected |
Definition at line 1278 of file expr2c.cpp.
|
protected |
|
protected |
Definition at line 1000 of file expr2c.cpp.
|
protected |
Definition at line 3557 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 1784 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 2059 of file expr2c.cpp.
|
protected |
Definition at line 2445 of file expr2c.cpp.
|
protected |
Definition at line 3511 of file expr2c.cpp.
|
protected |
Definition at line 3522 of file expr2c.cpp.
|
protected |
Returns a string if src
is a function with a known conversion, else returns nullopt.
Definition at line 4109 of file expr2c.cpp.
|
protected |
Definition at line 1233 of file expr2c.cpp.
|
protected |
Definition at line 2488 of file expr2c.cpp.
|
protected |
Definition at line 3467 of file expr2c.cpp.
|
protected |
Definition at line 1411 of file expr2c.cpp.
|
protected |
Definition at line 1516 of file expr2c.cpp.
|
protected |
Definition at line 2359 of file expr2c.cpp.
|
protected |
Definition at line 935 of file expr2c.cpp.
|
protected |
Definition at line 1217 of file expr2c.cpp.
|
protected |
Definition at line 1526 of file expr2c.cpp.
|
protected |
Definition at line 1506 of file expr2c.cpp.
|
protected |
Definition at line 1086 of file expr2c.cpp.
|
protected |
Definition at line 1182 of file expr2c.cpp.
|
protected |
Definition at line 1709 of file expr2c.cpp.
|
protected |
Definition at line 1679 of file expr2c.cpp.
|
protected |
Definition at line 1628 of file expr2c.cpp.
|
protected |
Definition at line 1714 of file expr2c.cpp.
|
protected |
Definition at line 2545 of file expr2c.cpp.
|
protected |
Definition at line 1430 of file expr2c.cpp.
|
protected |
Definition at line 1467 of file expr2c.cpp.
|
protected |
Definition at line 3636 of file expr2c.cpp.
|
protected |
Definition at line 1691 of file expr2c.cpp.
|
protected |
Definition at line 1697 of file expr2c.cpp.
|
protected |
Definition at line 1685 of file expr2c.cpp.
|
protected |
Definition at line 1207 of file expr2c.cpp.
|
protected |
Definition at line 1222 of file expr2c.cpp.
|
protected |
Definition at line 3654 of file expr2c.cpp.
|
protected |
Definition at line 3617 of file expr2c.cpp.
|
protected |
Definition at line 1703 of file expr2c.cpp.
|
protected |
Definition at line 3598 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 218 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 2385 of file expr2c.cpp.
|
protected |
Definition at line 2516 of file expr2c.cpp.
|
protected |
Definition at line 3543 of file expr2c.cpp.
|
protected |
Definition at line 1192 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 2067 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 2083 of file expr2c.cpp.
|
protected |
Definition at line 1618 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 673 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 650 of file expr2c.cpp.
|
protectedvirtual |
Definition at line 1639 of file expr2c.cpp.
|
protected |
Definition at line 799 of file expr2c.cpp.
|
protected |
Definition at line 765 of file expr2c.cpp.
|
protected |
Definition at line 1134 of file expr2c.cpp.
|
protected |
Definition at line 1389 of file expr2c.cpp.
|
protected |
Definition at line 2203 of file expr2c.cpp.
|
protected |
Definition at line 962 of file expr2c.cpp.
|
protected |
Definition at line 2156 of file expr2c.cpp.
|
protected |
Definition at line 869 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 4177 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2cppt, and expr2javat.
Definition at line 3674 of file expr2c.cpp.
void expr2ct::get_shorthands | ( | const exprt & | expr | ) |
Definition at line 116 of file expr2c.cpp.
Definition at line 75 of file expr2c.cpp.
|
staticprotected |
Definition at line 2576 of file expr2c.cpp.
|
protected |
Definition at line 56 of file expr2c_class.h.
|
protected |
Definition at line 55 of file expr2c_class.h.
Definition at line 88 of file expr2c_class.h.
Definition at line 89 of file expr2c_class.h.
|
protected |
Definition at line 91 of file expr2c_class.h.