10 #ifndef CPROVER_ANSI_C_EXPR2C_CLASS_H 11 #define CPROVER_ANSI_C_EXPR2C_CLASS_H 14 #include <unordered_map> 15 #include <unordered_set> 40 const std::string &declarator);
44 const std::string &qualifiers_str,
45 const std::string &declarator_str);
49 const std::string &qualifer_str,
50 const std::string &declarator_str,
52 bool inc_padding_components);
57 const std::string &declarator_str);
62 const std::string &declarator_str,
63 bool inc_size_if_possible);
65 static std::string
indent_str(
unsigned indent);
68 std::unordered_set<irep_idt, irep_id_hash>,
70 std::unordered_map<irep_idt, irep_idt, irep_id_hash>
shorthands;
81 unsigned &precedence);
85 unsigned &precedence);
88 const exprt &src,
const std::string &symbol,
89 unsigned precedence,
bool full_parentheses);
92 const exprt &src,
unsigned precedence);
95 const exprt &src,
unsigned precedence);
98 const exprt &src,
unsigned precedence);
104 const exprt &src,
unsigned precedence);
109 const exprt &src,
const std::string &symbol1,
110 const std::string &symbol2,
unsigned precedence);
113 const exprt &src,
unsigned &precedence);
116 const exprt &src,
const std::string &symbol,
117 unsigned precedence);
120 const exprt &src,
unsigned precedence);
123 const exprt &src,
unsigned precedence);
132 const exprt &src,
unsigned precedence);
136 unsigned precedence);
140 unsigned precedence);
144 unsigned precedence);
148 unsigned precedence);
151 const exprt &src,
const std::string &symbol,
152 unsigned precedence);
155 const exprt &src,
const std::string &symbol,
156 unsigned precedence);
159 const exprt &src,
const std::string &symbol,
160 unsigned precedence);
164 unsigned precedence);
168 unsigned precedence);
211 const exprt &src,
unsigned &precedence);
254 unsigned &precedence,
255 bool include_padding_components);
258 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H std::string convert_statement_expression(const exprt &src, unsigned &precendence)
The type of an expression.
std::string convert_code_assume(const codet &src, unsigned indent)
std::string convert_complex(const exprt &src, unsigned precedence)
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.
void get_shorthands(const exprt &expr)
application of (mathematical) function
std::string convert_code_expression(const codet &src, unsigned indent)
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
std::string convert_code_continue(const codet &src, unsigned indent)
std::string convert_code_fence(const codet &src, unsigned indent)
std::string convert_Hoare(const exprt &src)
std::string convert_union(const exprt &src, unsigned &precedence)
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
std::string convert_overflow(const exprt &src, unsigned &precedence)
std::string convert_code_block(const code_blockt &src, unsigned indent)
std::string convert_code(const codet &src)
std::string convert_array_of(const exprt &src, unsigned precedence)
std::string convert_code_unlock(const codet &src, unsigned indent)
virtual std::string convert_symbol(const exprt &src, unsigned &precedence)
A constant literal expression.
std::string convert_code_break(const codet &src, unsigned indent)
std::string convert_code_decl(const codet &src, unsigned indent)
std::string convert_code_return(const codet &src, unsigned indent)
std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence)
std::unordered_map< irep_idt, irep_idt, irep_id_hash > shorthands
virtual std::string convert(const typet &src)
expr2ct(const namespacet &_ns)
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
std::string convert_malloc(const exprt &src, unsigned &precedence)
irep_idt id_shorthand(const irep_idt &identifier) const
std::string convert_sizeof(const exprt &src, unsigned &precedence)
std::string convert_code_printf(const codet &src, unsigned indent)
Extract member of struct or union.
std::string convert_binary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence)
std::string convert_code_free(const codet &src, unsigned indent)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
std::string convert_unary(const exprt &src, const std::string &symbol, unsigned precedence)
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
std::string convert_literal(const exprt &src, unsigned &precedence)
std::string convert_code_assign(const code_assignt &src, unsigned indent)
std::string convert_code_label(const code_labelt &src, unsigned indent)
std::unordered_map< irep_idt, std::unordered_set< irep_idt, irep_id_hash >, irep_id_hash > ns_collision
std::string convert_byte_update(const exprt &src, unsigned precedence)
std::string convert_pointer_object_has_type(const exprt &src, unsigned precedence)
std::string convert_nondet_bool(const exprt &src, unsigned &precedence)
std::string convert_code_input(const codet &src, unsigned indent)
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
std::string convert_index_designator(const exprt &src)
std::string convert_code_array_set(const codet &src, unsigned indent)
std::string convert_member(const member_exprt &src, unsigned precedence)
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
std::string convert_trinary(const exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
API to expression classes.
std::string convert_code_asm(const code_asmt &src, unsigned indent)
std::string convert_initializer_list(const exprt &src, unsigned &precedence)
std::string convert_code_dead(const codet &src, unsigned indent)
A label for branch targets.
std::string convert_code_lock(const codet &src, unsigned indent)
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_list(const exprt &src, unsigned &precedence)
std::string convert_with(const exprt &src, unsigned precedence)
A `while' instruction.
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
std::string convert_extractbits(const exprt &src, unsigned precedence)
std::string convert_extractbit(const exprt &src, unsigned precedence)
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence)
std::string convert_vector(const exprt &src, unsigned &precedence)
std::string convert_concatenation(const exprt &src, unsigned &precedence)
std::string convert_predicate_symbol(const exprt &src, unsigned &precedence)
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
std::string convert_nondet(const exprt &src, unsigned &precedence)
std::string convert_norep(const exprt &src, unsigned &precedence)
std::string convert_code_assert(const codet &src, unsigned indent)
std::string convert_index(const exprt &src, unsigned precedence)
std::string convert_array_member_value(const exprt &src, unsigned precedence)
A function call side effect.
std::string convert_byte_extract(const exprt &src, unsigned precedence)
std::string convert_member_designator(const exprt &src)
std::string convert_nondet_symbol(const exprt &src, unsigned &precedence)
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
std::string convert_quantified_symbol(const exprt &src, unsigned &precedence)
std::string convert_code_array_copy(const codet &src, unsigned indent)
Base class for all expressions.
std::string convert_update(const exprt &src, unsigned precedence)
std::string convert_cond(const exprt &src, unsigned precedence)
std::string convert_code_for(const code_fort &src, unsigned indent)
A `do while' instruction.
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
An inline assembler statement.
std::string convert_code_decl_block(const codet &src, unsigned indent)
std::string convert_code_array_replace(const codet &src, unsigned indent)
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
std::string convert_array(const exprt &src, unsigned &precedence)
std::string convert_designated_initializer(const exprt &src, unsigned &precedence)
std::string convert_code_goto(const codet &src, unsigned indent)
A statement in a programming language.
std::string convert_comma(const exprt &src, unsigned precedence)
std::string convert_code_while(const code_whilet &src, unsigned indent)
std::string convert_code_output(const codet &src, unsigned indent)
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
std::string convert_code_init(const codet &src, unsigned indent)
std::string convert_quantifier(const exprt &src, const std::string &symbol, unsigned precedence)
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
std::string convert_code_switch(const codet &src, unsigned indent)
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
static std::string indent_str(unsigned indent)
std::string convert_function_application(const function_application_exprt &src, unsigned &precedence)
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)