10 #ifndef CPROVER_ANSI_C_EXPR2C_CLASS_H
11 #define CPROVER_ANSI_C_EXPR2C_CLASS_H
16 #include <unordered_map>
17 #include <unordered_set>
55 const std::string &declarator);
59 const std::string &qualifiers_str,
60 const std::string &declarator_str);
64 const std::string &qualifer_str,
65 const std::string &declarator_str,
67 bool inc_padding_components);
72 const std::string &declarator_str);
77 const std::string &declarator_str,
78 bool inc_size_if_possible);
80 static std::string
indent_str(
unsigned indent);
82 std::unordered_map<irep_idt, std::unordered_set<irep_idt>>
ns_collision;
94 unsigned &precedence);
98 unsigned &precedence);
102 const std::string &symbol,
104 bool full_parentheses);
107 const exprt &src,
const std::string &symbol,
108 unsigned precedence,
bool full_parentheses);
111 const exprt &src,
unsigned precedence);
114 const exprt &src,
unsigned precedence);
117 const exprt &src,
unsigned precedence);
126 const std::string &symbol1,
127 const std::string &symbol2,
128 unsigned precedence);
131 const exprt &src,
unsigned &precedence);
135 const std::string &symbol,
136 unsigned precedence);
139 const exprt &src,
unsigned precedence);
150 const exprt &src,
unsigned precedence);
165 const std::string &symbol,
166 unsigned precedence);
169 const exprt &src,
const std::string &symbol,
170 unsigned precedence);
176 unsigned precedence);
180 unsigned precedence);
221 const exprt &src,
unsigned &precedence);
262 unsigned &precedence,
263 bool include_padding_components);
API to expression classes for bitvectors.
Expression classes for byte-level operators.
A base class for binary expressions.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
codet representation of an inline assembler statement.
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
codet representation of a do while statement.
codet representation of a for statement.
codet representation of a function call statement.
codet representation of an if-then-else statement.
codet representation of a label for branch targets.
codet representation of a switch-case, i.e. a case statement within a switch.
codet representing a while statement.
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string convert_nondet(const exprt &src, unsigned &precedence)
std::string convert_literal(const exprt &src)
std::string convert_code_continue(unsigned indent)
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_code_switch_case(const code_switch_caset &src, unsigned indent)
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
std::string convert_comma(const exprt &src, unsigned precedence)
std::string convert_code_assert(const codet &src, unsigned indent)
std::string convert_quantifier(const quantifier_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_union(const exprt &src, unsigned &precedence)
std::string convert_code_expression(const codet &src, unsigned indent)
std::string convert_code_goto(const codet &src, unsigned indent)
std::string convert_code_switch(const codet &src, unsigned indent)
std::string convert_initializer_list(const exprt &src)
std::string convert_quantified_symbol(const exprt &src)
std::string convert_function_application(const function_application_exprt &src)
std::string convert_code_unlock(const codet &src, unsigned indent)
std::string convert_code_decl_block(const codet &src, unsigned indent)
static std::string indent_str(unsigned indent)
std::string convert_byte_update(const byte_update_exprt &, unsigned precedence)
std::string convert_code(const codet &src)
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
std::string convert_let(const let_exprt &, unsigned precedence)
std::string convert_nondet_bool()
std::string convert_norep(const exprt &src, unsigned &precedence)
const expr2c_configurationt & configuration
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
std::string convert_code_output(const codet &src, unsigned indent)
std::string convert_code_while(const code_whilet &src, unsigned indent)
std::string convert_index_designator(const exprt &src)
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
std::string convert_code_block(const code_blockt &src, unsigned indent)
std::string convert_code_asm(const code_asmt &src, unsigned indent)
std::string convert_allocate(const exprt &src, unsigned &precedence)
std::string convert_Hoare(const exprt &src)
std::string convert_sizeof(const exprt &src, unsigned &precedence)
std::string convert_code_lock(const codet &src, unsigned indent)
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
irep_idt id_shorthand(const irep_idt &identifier) const
std::string convert_cond(const exprt &src, unsigned precedence)
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src)
std::string convert_overflow(const exprt &src, unsigned &precedence)
std::string convert_member(const member_exprt &src, unsigned precedence)
void get_shorthands(const exprt &expr)
std::string convert_code_for(const code_fort &src, unsigned indent)
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 sy...
std::string convert_extractbits(const extractbits_exprt &src, unsigned precedence)
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
std::string convert_code_decl(const codet &src, unsigned indent)
std::string convert_trinary(const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
std::string convert_update(const update_exprt &, unsigned precedence)
std::string convert_nondet_symbol(const nondet_symbol_exprt &)
std::string convert_code_printf(const codet &src, unsigned indent)
std::string convert_unary(const unary_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
std::string convert_member_designator(const exprt &src)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
std::string convert_code_label(const code_labelt &src, unsigned indent)
virtual std::string convert_symbol(const exprt &src)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
std::string convert_code_array_copy(const codet &src, unsigned indent)
std::string convert_concatenation(const exprt &src, unsigned &precedence)
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
std::string convert_code_dead(const codet &src, unsigned indent)
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
std::string convert_designated_initializer(const exprt &src)
std::string convert_vector(const exprt &src, unsigned &precedence)
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string convert_array_member_value(const exprt &src, unsigned precedence)
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
std::unordered_map< irep_idt, irep_idt > shorthands
std::string convert_complex(const exprt &src, unsigned precedence)
std::string convert_code_assign(const code_assignt &src, unsigned indent)
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
std::string convert_code_fence(const codet &src, unsigned indent)
virtual std::string convert(const typet &src)
std::string convert_code_return(const codet &src, unsigned indent)
std::string convert_code_break(unsigned indent)
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_with(const exprt &src, unsigned precedence)
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
std::string convert_predicate_passive_symbol(const exprt &src)
std::string convert_array_list(const exprt &src, unsigned &precedence)
std::string convert_array_of(const exprt &src, unsigned precedence)
std::string convert_code_array_replace(const codet &src, unsigned indent)
std::string convert_index(const exprt &src, unsigned precedence)
std::string convert_code_assume(const codet &src, unsigned indent)
std::string convert_code_input(const codet &src, unsigned indent)
std::string convert_extractbit(const extractbit_exprt &, unsigned precedence)
std::string convert_predicate_next_symbol(const exprt &src)
std::string convert_code_array_set(const codet &src, unsigned indent)
std::string convert_function(const exprt &src, const std::string &symbol)
std::string convert_binary(const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
std::string convert_predicate_symbol(const exprt &src)
expr2ct(const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration)
std::string convert_array(const exprt &src)
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Base class for all expressions.
Application of (mathematical) function.
Extract member of struct or union.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a nondeterministic choice.
A base class for quantifier expressions.
A side_effect_exprt representation of a function call side effect.
An expression with three operands.
Semantic type conversion.
The type of an expression, extends irept.
Generic base class for unary expressions.
Operator to update elements in structs and arrays.
API to expression classes for 'mathematical' expressions.
API to expression classes.
Used for configuring the behaviour of expr2c and type2c.
static expr2c_configurationt default_configuration
This prints a human readable C like syntax that closely mirrors the internals of the GOTO program.