10 #ifndef CPROVER_ANSI_C_EXPR2C_CLASS_H
11 #define CPROVER_ANSI_C_EXPR2C_CLASS_H
16 #include <unordered_map>
17 #include <unordered_set>
54 const std::string &declarator);
58 const std::string &qualifiers_str,
59 const std::string &declarator_str);
63 const std::string &qualifer_str,
64 const std::string &declarator_str,
66 bool inc_padding_components);
71 const std::string &declarator_str);
76 const std::string &declarator_str,
77 bool inc_size_if_possible);
81 std::unordered_map<irep_idt, std::unordered_set<irep_idt>>
ns_collision;
93 unsigned &precedence);
97 unsigned &precedence);
101 const std::string &symbol,
103 bool full_parentheses);
106 const exprt &src,
const std::string &symbol,
107 unsigned precedence,
bool full_parentheses);
110 const exprt &src,
unsigned precedence);
113 const exprt &src,
unsigned precedence);
116 const exprt &src,
unsigned precedence);
125 const std::string &symbol1,
126 const std::string &symbol2,
127 unsigned precedence);
139 const exprt &src,
unsigned &precedence);
143 const std::string &symbol,
144 unsigned precedence);
147 const exprt &src,
unsigned precedence);
158 const exprt &src,
unsigned precedence);
173 const std::string &symbol,
174 unsigned precedence);
177 const exprt &src,
const std::string &symbol,
178 unsigned precedence);
187 unsigned precedence);
191 unsigned precedence);
232 const exprt &src,
unsigned &precedence);
273 unsigned &precedence,
274 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.
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_nondet(const exprt &src, unsigned &precedence)
std::string convert_literal(const exprt &src)
std::string convert_code_continue(unsigned indent)
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
virtual std::string convert_symbol(const exprt &src)
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)
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_struct(const exprt &src, unsigned &precedence, bool include_padding_components)
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)
virtual std::string convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str)
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)
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
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)
std::string convert_extractbits(const extractbits_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)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
virtual std::string convert(const exprt &src)
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_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
static std::string indent_str(unsigned indent)
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
std::string convert_code_label(const code_labelt &src, unsigned indent)
std::string convert_code_array_copy(const codet &src, unsigned indent)
std::string convert_concatenation(const exprt &src, unsigned &precedence)
virtual std::string convert_constant_bool(bool boolean_value)
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...
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)
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_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible)
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)
virtual std::string convert_code(const codet &src, unsigned indent)
std::string convert_predicate_next_symbol(const exprt &src)
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
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)
std::string convert_predicate_symbol(const exprt &src)
expr2ct(const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration)
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)
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.