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