35 new_symbol.
value=expr;
41 result.add_source_location()=source_location;
50 convert(code_assign, dest, mode);
64 if(expr.
id()==ID_dereference ||
65 expr.
id()==ID_side_effect ||
66 expr.
id()==ID_compound_literal ||
70 if(expr.
id()==ID_index)
96 if(expr.
id()==ID_forall || expr.
id()==ID_exists)
110 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies);
116 "' must be Boolean, but got ",
120 if(
auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
122 expr =
if_exprt{std::move(implies->lhs()),
123 std::move(implies->rhs()),
134 if(expr.
id()==ID_and)
142 for(exprt::operandst::reverse_iterator
151 "boolean operators must have only boolean operands",
154 if(expr.
id()==ID_and)
160 if(expr.
id() == ID_or)
189 if(expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies)
198 else if(expr.
id()==ID_if)
213 "condition for an 'if' must be boolean",
254 convert(assignment_true, tmp_true, mode);
260 convert(assignment_false, tmp_false, mode);
274 convert(code_expression, tmp_true, mode);
283 convert(code_expression, tmp_false, mode);
291 if_expr.
cond(), tmp_true, tmp_false, source_location, dest, mode);
295 else if(expr.
id()==ID_comma)
303 bool last=(it==--expr.
operands().end());
339 else if(expr.
id()==ID_typecast)
351 else if(expr.
id()==ID_side_effect)
356 if(statement==ID_gcc_conditional_expression)
362 else if(statement==ID_statement_expression)
370 else if(statement==ID_assign)
375 "side-effect assignment expressions must have two operands");
380 side_effect_assign.rhs().id() == ID_side_effect &&
384 clean_expr(side_effect_assign.lhs(), dest, mode);
385 exprt lhs = side_effect_assign.lhs();
399 assignment.
lhs()=lhs;
400 assignment.
rhs() = side_effect_assign.rhs();
405 expr = must_use_rhs ? side_effect_assign.rhs() : lhs;
412 else if(expr.
id()==ID_forall || expr.
id()==ID_exists)
416 "the front-end should check quantified expressions for side-effects");
418 else if(expr.
id()==ID_address_of)
430 if(expr.
id()==ID_side_effect)
435 else if(expr.
id()==ID_compound_literal)
439 expr.
operands().size() == 1,
"ID_compound_literal has a single operand");
452 if(expr.
id()==ID_compound_literal)
455 expr.
operands().size() == 1,
"ID_compound_literal has a single operand");
459 else if(expr.
id()==ID_string_constant)
464 else if(expr.
id()==ID_index)
470 else if(expr.
id()==ID_dereference)
475 else if(expr.
id()==ID_comma)
484 bool last=(it==--expr.
operands().end());
504 else if(expr.
id() == ID_side_effect)
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
Operator to return the address of an object.
A codet representing an assignment in the program.
A codet representing the removal of a local variable going out of scope.
A codet representing the declaration of a local variable.
codet representation of an expression statement.
Operator to dereference a pointer.
void add(const codet &destructor)
Adds a destructor to the current stack, attaching itself to the current node.
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).
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
The Boolean constant false.
void remove_function_call(side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
symbol_table_baset & symbol_table
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
std::string tmp_symbol_prefix
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken)
struct goto_convertt::targetst targets
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
static bool needs_cleaning(const exprt &expr)
void clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest, const irep_idt &mode)
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
A generic container class for the GOTO intermediate representation of one function.
The trinary if-then-else operator.
const irep_idt & id() const
mstreamt & result() const
const irep_idt & get_statement() const
Expression to hold a symbol (variable)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
exprt value
Initial value of symbol.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
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.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(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(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
side_effect_exprt & to_side_effect_expr(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)
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
destructor_treet destructor_stack