Go to the documentation of this file.
32 if(expr.
id()==ID_side_effect &&
33 expr.
get(ID_statement)==ID_function_call)
50 if(statement==ID_assign)
54 if(result_is_used && !address_taken &&
needs_cleaning(old_assignment.lhs()))
56 if(!old_assignment.rhs().is_constant())
59 replacement_expr_opt = old_assignment.rhs();
65 code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs));
70 else if(statement==ID_assign_plus ||
71 statement==ID_assign_minus ||
72 statement==ID_assign_mult ||
73 statement==ID_assign_div ||
74 statement==ID_assign_mod ||
75 statement==ID_assign_shl ||
76 statement==ID_assign_ashr ||
77 statement==ID_assign_lshr ||
78 statement==ID_assign_bitand ||
79 statement==ID_assign_bitxor ||
80 statement==ID_assign_bitor)
84 id2string(statement) +
" expects two arguments",
89 if(statement==ID_assign_plus)
91 else if(statement==ID_assign_minus)
93 else if(statement==ID_assign_mult)
95 else if(statement==ID_assign_div)
97 else if(statement==ID_assign_mod)
99 else if(statement==ID_assign_shl)
101 else if(statement==ID_assign_ashr)
103 else if(statement==ID_assign_lshr)
105 else if(statement==ID_assign_bitand)
107 else if(statement==ID_assign_bitxor)
109 else if(statement==ID_assign_bitor)
121 op0_type.
id() != ID_c_enum_tag && op0_type.
id() != ID_c_enum &&
122 op0_type.
id() != ID_c_bool && op0_type.
id() != ID_bool);
131 result_is_used && !address_taken &&
135 replacement_expr_opt = rhs;
144 convert(assignment, dest, mode);
150 if(replacement_expr_opt.has_value())
156 else if(result_is_used)
167 lhs.
id() == ID_typecast,
169 " expression with different operand type expected to have a "
173 id2string(expr.
id()) +
" type mismatch in lhs operand");
191 "preincrement/predecrement must have one operand",
197 statement == ID_preincrement || statement == ID_predecrement,
198 "expects preincrement or predecrement");
203 if(statement==ID_preincrement)
209 const typet &op_type = op.type();
212 op_type.
id() != ID_c_enum_tag && op_type.
id() != ID_c_enum &&
213 op_type.
id() != ID_c_bool && op_type.
id() != ID_bool);
217 if(op_type.
id() == ID_pointer)
220 constant_type = op_type;
228 if(constant_type.
id() == ID_complex)
238 rhs.
type() = op.type();
240 const bool cannot_use_lhs =
248 convert(assignment, dest, mode);
277 "postincrement/postdecrement must have one operand",
283 statement == ID_postincrement || statement == ID_postdecrement,
284 "expects postincrement or postdecrement");
289 if(statement==ID_postincrement)
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)
324 rhs.
type() = op.type();
329 convert(assignment, tmp2, mode);
362 std::string new_base_name =
"return_value";
373 new_symbol_mode = symbol.
mode;
405 if(dest.
id()==
"new_object")
448 tmp.
set(ID_destructor, expr.
find(ID_destructor));
495 "temporary_object takes zero or one operands",
506 convert(assignment, dest, mode);
513 "temporary_object takes zero operands",
515 exprt initializer=
static_cast<const exprt &
>(expr.
find(ID_initializer));
546 "statement_expression takes block as operand",
551 "statement_expression takes non-empty block as operand",
560 expr.
type(),
"statement_expression", dest, source_location, mode);
565 if(last.
get(ID_statement)==ID_expression)
572 else if(last.
get(ID_statement)==ID_assign)
577 code.
operands().push_back(assignment);
590 static_cast<exprt &
>(expr)=tmp_symbol_expr;
606 auto const make_operation = [&statement](
exprt lhs,
exprt rhs) ->
exprt {
608 if(lhs.
type().
id() == ID_unsignedbv)
611 if(rhs.
type().
id() == ID_unsignedbv)
614 if(statement == ID_overflow_plus)
616 std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
621 else if(statement == ID_overflow_minus)
623 std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
631 statement == ID_overflow_mult,
632 "the three overflow operations are add, sub and mul");
633 std::size_t ssize = lhs_ssize + rhs_ssize;
648 auto operation = make_operation(lhs, rhs);
652 operation.add_source_location().
add_pragma(
"disable:signed-overflow-check");
657 if(
result.type().id() == ID_pointer)
667 result_type =
result.type();
677 inner_tc.add_source_location().
add_pragma(
"disable:conversion-check");
680 outer_tc.add_source_location().
add_pragma(
"disable:conversion-check");
685 expr.
swap(overflow_check);
700 if(statement==ID_function_call)
703 else if(statement==ID_assign ||
704 statement==ID_assign_plus ||
705 statement==ID_assign_minus ||
706 statement==ID_assign_mult ||
707 statement==ID_assign_div ||
708 statement==ID_assign_bitor ||
709 statement==ID_assign_bitxor ||
710 statement==ID_assign_bitand ||
711 statement==ID_assign_lshr ||
712 statement==ID_assign_ashr ||
713 statement==ID_assign_shl ||
714 statement==ID_assign_mod)
716 else if(statement==ID_postincrement ||
717 statement==ID_postdecrement)
719 else if(statement==ID_preincrement ||
720 statement==ID_predecrement)
721 remove_pre(expr, dest, result_is_used, address_taken, mode);
722 else if(statement==ID_cpp_new ||
723 statement==ID_cpp_new_array)
725 else if(statement==ID_cpp_delete ||
726 statement==ID_cpp_delete_array)
728 else if(statement==ID_allocate)
730 else if(statement==ID_temporary_object)
732 else if(statement==ID_statement_expression)
734 else if(statement==ID_nondet)
738 else if(statement==ID_skip)
742 else if(statement==ID_throw)
755 statement == ID_overflow_plus || statement == ID_overflow_minus ||
756 statement == ID_overflow_mult)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
#define UNREACHABLE
This should be used to mark dead code.
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
code_expressiont & to_code_expression(codet &code)
const typet & subtype() const
static bool needs_cleaning(const exprt &expr)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
#define Forall_operands(it, expr)
const side_effect_expr_overflowt & to_side_effect_expr_overflow(const exprt &expr)
Cast an exprt to a side_effect_expr_overflowt.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
static void replace_new_object(const exprt &object, exprt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
The type of an expression, extends irept.
Fresh auxiliary symbol creation.
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
typet type
Type of symbol.
Operator to dereference a pointer.
static bool has_function_call(const exprt &expr)
A side_effect_exprt representation of a function call side effect.
std::string tmp_symbol_prefix
const irept & find(const irep_namet &name) const
A codet representing the declaration of a local variable.
void add_pragma(const irep_idt &pragma)
targett add(instructiont &&instruction)
Adds a given instruction at the end.
The plus expression Associativity is not specified.
void remove_function_call(side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Expression to hold a symbol (variable)
bitvector_typet index_type()
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
#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...
void remove_overflow(side_effect_expr_overflowt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
irep_idt mode
Language mode.
mstreamt & result() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
#define forall_operands(it, expr)
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
API to expression classes that are internal to the C frontend.
#define PRECONDITION(CONDITION)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const irep_idt & get_identifier() const
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Fixed-width bit-vector representing a signed or unsigned integer.
Binary multiplication Associativity is not specified.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
Complex constructor from a pair of numbers.
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
void remove_post(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
source_locationt & add_source_location()
nonstd::optional< T > optionalt
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
const irep_idt & get_statement() const
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
std::size_t get_width() const
Deprecated expression utility functions.
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & get(const irep_namet &name) const
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
exprt::operandst & arguments()
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
A generic container class for the GOTO intermediate representation of one function.
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken)
A side_effect_exprt representation of a side effect that throws an exception.
symbol_table_baset & symbol_table
const code_blockt & to_code_block(const codet &code)
void convert_cpp_delete(const codet &code, goto_programt &dest)
const exprt & expression() const
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
codet & find_last_statement()
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
Semantic type conversion.
A codet representing an assignment in the program.
const irep_idt & get_statement() const
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
const source_locationt & source_location() const
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 ...
irep_idt name
The unique identifier.
An expression containing a side effect.
codet representation of an expression statement.
Data structure for representing an arbitrary statement in a program.
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)