35 std::optional<exprt> replacement_expr_opt;
39 if(statement == ID_assign)
48 if(!old_assignment.rhs().is_constant())
51 old_assignment.rhs(),
"assign", side_effects.
side_effects, mode));
54 replacement_expr_opt =
60 code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs));
66 statement == ID_assign_plus || statement == ID_assign_minus ||
67 statement == ID_assign_mult || statement == ID_assign_div ||
68 statement == ID_assign_mod || statement == ID_assign_shl ||
69 statement == ID_assign_ashr || statement == ID_assign_lshr ||
70 statement == ID_assign_bitand || statement == ID_assign_bitxor ||
71 statement == ID_assign_bitor)
75 id2string(statement) +
" expects two arguments",
80 if(statement == ID_assign_plus)
82 else if(statement == ID_assign_minus)
84 else if(statement == ID_assign_mult)
86 else if(statement == ID_assign_div)
88 else if(statement == ID_assign_mod)
90 else if(statement == ID_assign_shl)
92 else if(statement == ID_assign_ashr)
94 else if(statement == ID_assign_lshr)
96 else if(statement == ID_assign_bitand)
98 else if(statement == ID_assign_bitxor)
100 else if(statement == ID_assign_bitor)
112 op0_type.
id() != ID_c_enum_tag && op0_type.
id() != ID_c_enum &&
113 op0_type.
id() != ID_c_bool && op0_type.
id() != ID_bool);
124 replacement_expr_opt =
139 if(replacement_expr_opt.has_value())
162 lhs.
id() == ID_typecast,
164 " expression with different operand type expected to have a "
168 id2string(expr.
id()) +
" type mismatch in lhs operand");
187 "preincrement/predecrement must have one operand",
193 statement == ID_preincrement || statement == ID_predecrement,
194 "expects preincrement or predecrement");
197 const typet &op_type = op.type();
200 op_type.
id() != ID_c_enum_tag && op_type.
id() != ID_c_enum &&
201 op_type.
id() != ID_c_bool && op_type.
id() != ID_bool);
205 if(op_type.
id() == ID_pointer)
208 constant_type = op_type;
216 if(constant_type.
id() == ID_complex)
226 op, statement == ID_preincrement ? ID_plus : ID_minus, std::move(constant)};
232 if(op.id() == ID_typecast)
242 const bool cannot_use_lhs =
285 "postincrement/postdecrement must have one operand",
291 statement == ID_postincrement || statement == ID_postdecrement,
292 "expects postincrement or postdecrement");
295 const typet &op_type = op.type();
298 op_type.
id() != ID_c_enum_tag && op_type.
id() != ID_c_enum &&
299 op_type.
id() != ID_c_bool && op_type.
id() != ID_bool);
303 if(op_type.
id() == ID_pointer)
306 constant_type = op_type;
314 if(constant_type.
id() == ID_complex)
325 statement == ID_postincrement ? ID_plus : ID_minus,
326 std::move(constant)};
332 convert(assignment, tmp2, mode);
341 std::string suffix =
"post";
342 if(
auto sym_expr = expr_try_dynamic_cast<symbol_exprt>(tmp))
378 std::string new_base_name =
"return_value";
387 new_base_name +=
'_';
389 new_symbol_mode = symbol.
mode;
421 if(dest.
id() ==
"new_object")
468 tmp.
set(ID_destructor, expr.
find(ID_destructor));
522 "temporary_object takes zero or one operands",
544 "temporary_object takes zero operands",
546 exprt initializer =
static_cast<const exprt &
>(expr.
find(ID_initializer));
582 "statement_expression takes block as operand",
587 "statement_expression takes non-empty block as operand",
597 "statement_expression",
605 if(last.
get(ID_statement) == ID_expression)
612 else if(last.
get(ID_statement) == ID_assign)
617 code.
operands().push_back(assignment);
626 static_cast<exprt &
>(expr) = tmp_symbol_expr;
645 if(
result.type().id() != ID_pointer)
660 expr.
swap(overflow_check);
668 irep_idt arithmetic_operation = statement == ID_overflow_plus ? ID_plus
669 : statement == ID_overflow_minus ? ID_minus
670 : statement == ID_overflow_mult ? ID_mult
675 arithmetic_operation,
682 overflow_with_result,
694 member_exprt{overflow_with_result, result_comps[0]}, arith_type),
700 member_exprt overflow_check{overflow_with_result, result_comps[1]};
703 expr.
swap(overflow_check);
720 if(statement == ID_function_call)
726 statement == ID_assign || statement == ID_assign_plus ||
727 statement == ID_assign_minus || statement == ID_assign_mult ||
728 statement == ID_assign_div || statement == ID_assign_bitor ||
729 statement == ID_assign_bitxor || statement == ID_assign_bitand ||
730 statement == ID_assign_lshr || statement == ID_assign_ashr ||
731 statement == ID_assign_shl || statement == ID_assign_mod)
735 else if(statement == ID_postincrement || statement == ID_postdecrement)
739 else if(statement == ID_preincrement || statement == ID_predecrement)
743 else if(statement == ID_cpp_new || statement == ID_cpp_new_array)
747 else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array)
751 else if(statement == ID_allocate)
755 else if(statement == ID_temporary_object)
759 else if(statement == ID_statement_expression)
763 else if(statement == ID_nondet)
768 else if(statement == ID_skip)
773 else if(statement == ID_throw)
789 statement == ID_overflow_plus || statement == ID_overflow_minus ||
790 statement == ID_overflow_mult)
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
API to expression classes for bitvectors.
API to expression classes that are internal to the C frontend.
const side_effect_expr_overflowt & to_side_effect_expr_overflow(const exprt &expr)
Cast an exprt to a side_effect_expr_overflowt.
bitvector_typet c_index_type()
A base class for binary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A goto_instruction_codet representing an assignment in the program.
codet & find_last_statement()
codet representation of an expression statement.
const exprt & expression() const
A codet representing the declaration of a local variable.
goto_instruction_codet representation of a function call statement.
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
Complex constructor from a pair of numbers.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
symbol_table_baset & symbol_table
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_pre(side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)
clean_expr_resultt remove_post(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
std::string tmp_symbol_prefix
void convert_frontend_decl(const code_frontend_declt &, goto_programt &, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
clean_expr_resultt remove_assignment(side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)
void convert_cpp_delete(const codet &code, goto_programt &dest)
clean_expr_resultt remove_malloc(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt remove_side_effect(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used, bool address_taken)
irep_idt make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
clean_expr_resultt remove_cpp_new(side_effect_exprt &expr, bool result_is_used)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
clean_expr_resultt remove_temporary_object(side_effect_exprt &expr)
clean_expr_resultt remove_function_call(side_effect_expr_function_callt &expr, const irep_idt &mode, bool result_is_used)
static void replace_new_object(const exprt &object, exprt &dest)
clean_expr_resultt remove_cpp_delete(side_effect_exprt &expr)
clean_expr_resultt remove_statement_expression(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
clean_expr_resultt remove_overflow(side_effect_expr_overflowt &expr, bool result_is_used, const irep_idt &mode)
static bool assignment_lhs_needs_temporary(const exprt &lhs)
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
Extract member of struct or union.
mstreamt & result() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
const typet & base_type() const
The type of the data what we point to.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
A side_effect_exprt representation of a side effect that throws an exception.
An expression containing a side effect.
const irep_idt & get_statement() const
const componentst & components() const
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt mode
Language mode.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
#define Forall_operands(it, expr)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
const code_assignt & to_code_assign(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
code_expressiont & to_code_expression(codet &code)
const code_blockt & to_code_block(const codet &code)
const codet & to_code(const exprt &expr)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.