37 new_symbol.
value=expr;
65 if(expr.
id()==ID_dereference ||
66 expr.
id()==ID_side_effect ||
67 expr.
id()==ID_compound_literal ||
71 if(expr.
id()==ID_index)
97 if(expr.
id()==ID_forall || expr.
id()==ID_exists)
110 assert(expr.
id()==ID_and || expr.
id()==ID_or);
115 error() <<
"`" << expr.
id() <<
"' must be Boolean, but got " 125 if(expr.
id()==ID_and)
133 for(exprt::operandst::reverse_iterator
143 error() <<
"`" << expr.
id() <<
"' takes Boolean " 144 <<
"operands only, but got " << op.
pretty() <<
eom;
148 if(expr.
id()==ID_and)
179 if(expr.
id()==ID_and || expr.
id()==ID_or)
188 else if(expr.
id()==ID_if)
204 error() <<
"first argument of `if' must be boolean, but got " 245 assignment_true.rhs()=if_expr.
true_case();
247 convert(assignment_true, tmp_true);
253 convert(assignment_false, tmp_false);
264 convert(code_expression, tmp_true);
270 convert(code_expression, tmp_false);
278 if_expr.
cond(), tmp_true, tmp_false,
279 source_location, dest);
283 else if(expr.
id()==ID_comma)
291 bool last=(it==--expr.
operands().end());
327 else if(expr.
id()==ID_typecast)
332 error() <<
"typecast takes one argument" <<
eom;
344 else if(expr.
id()==ID_side_effect)
349 if(statement==ID_gcc_conditional_expression)
355 else if(statement==ID_statement_expression)
363 else if(statement==ID_assign)
368 if(expr.
op1().
id()==ID_side_effect &&
376 assignment.
lhs()=lhs;
377 assignment.
rhs()=expr.
op1();
388 else if(statement==ID_function_call)
393 function()).get_identifier()==
"__noop")
401 else if(expr.
id()==ID_forall || expr.
id()==ID_exists)
407 if(tmp.instructions.empty())
410 error() <<
"no side-effects in quantified expressions allowed" 416 else if(expr.
id()==ID_address_of)
428 if(expr.
id()==ID_side_effect)
432 else if(expr.
id()==ID_compound_literal)
447 if(expr.
id()==ID_compound_literal)
453 else if(expr.
id()==ID_string_constant)
458 else if(expr.
id()==ID_index)
464 else if(expr.
id()==ID_dereference)
469 else if(expr.
id()==ID_comma)
478 bool last=(it==--expr.
operands().end());
510 error() <<
"conditional_expression takes two operands" <<
eom;
521 if_expr.true_case()=expr.
op0();
522 if_expr.false_case()=expr.
op1();
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
void convert(const codet &code, goto_programt &dest)
converts 'code' and appends the result to 'dest'
symbol_tablet & symbol_table
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, symbol_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
struct goto_convertt::targetst targets
Fresh auxiliary symbol creation.
void convert_assign(const code_assignt &code, goto_programt &dest)
exprt value
Initial value of symbol.
The trinary if-then-else operator.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
side_effect_exprt & to_side_effect_expr(exprt &expr)
destructor_stackt destructor_stack
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
The boolean constant true.
std::string tmp_symbol_prefix
A declaration of a local variable.
void clean_expr_address_of(exprt &expr, goto_programt &dest)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
const source_locationt & find_source_location() const
source_locationt source_location
API to expression classes.
void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest)
#define forall_operands(it, expr)
void clean_expr(exprt &expr, goto_programt &dest, bool result_is_used=true)
The boolean constant false.
std::vector< exprt > operandst
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
static bool needs_cleaning(const exprt &expr)
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
source_locationt & add_source_location()
const source_locationt & source_location() const
exprt::operandst & arguments()
A removal of a local variable.
#define Forall_operands(it, expr)
source_locationt & add_source_location()
Expression to hold a symbol (variable)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
const irep_idt & get_statement() const
bool simplify(exprt &expr, const namespacet &ns)
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest)
if(guard) true_case; else false_case;