10#ifndef CPROVER_ANSI_C_EXPR2C_CLASS_H
11#define CPROVER_ANSI_C_EXPR2C_CLASS_H
16#include <unordered_map>
17#include <unordered_set>
56 const std::string &declarator);
60 const std::string &qualifiers_str,
61 const std::string &declarator_str);
65 const std::string &qualifer_str,
66 const std::string &declarator_str,
68 bool inc_padding_components);
73 const std::string &declarator_str);
78 const std::string &declarator_str,
79 bool inc_size_if_possible);
81 static std::string
indent_str(
unsigned indent);
83 std::unordered_map<irep_idt, std::unordered_set<irep_idt>>
ns_collision;
95 unsigned &precedence);
99 unsigned &precedence);
103 const std::string &symbol,
105 bool full_parentheses);
108 const exprt &src,
const std::string &symbol,
109 unsigned precedence,
bool full_parentheses);
112 const exprt &src,
unsigned precedence);
115 const exprt &src,
unsigned precedence);
118 const exprt &src,
unsigned precedence);
127 const std::string &symbol1,
128 const std::string &symbol2,
129 unsigned precedence);
141 const exprt &src,
unsigned &precedence);
145 const std::string &symbol,
146 unsigned precedence);
149 const exprt &src,
unsigned precedence);
160 const exprt &src,
unsigned precedence);
175 const std::string &symbol,
176 unsigned precedence);
179 const exprt &src,
const std::string &symbol,
180 unsigned precedence);
189 unsigned precedence);
193 unsigned precedence);
235 const exprt &src,
unsigned &precedence);
276 unsigned &precedence,
277 bool include_padding_components);
API to expression classes for bitvectors.
Expression classes for byte-level operators.
A base class for binary expressions.
Reverse the order of bits in a bit-vector.
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 sequential composition of program statements.
codet representation of a do while statement.
codet representation of a for statement.
A codet representing an assignment in the program.
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_code_frontend_decl(const codet &, unsigned indent)
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)
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_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)
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 ex...
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_function_call(const code_function_callt &src, unsigned indent)
std::string convert_code_fence(const codet &src, unsigned indent)
std::string convert_bitreverse(const bitreverse_exprt &src)
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_code_frontend_assign(const code_frontend_assignt &, unsigned indent)
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_conditional_target_group(const exprt &src)
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_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 base class for shift and rotate operators.
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.
nonstd::optional< T > optionalt
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.