Go to the documentation of this file.
39 const exprt &
function,
47 new_function=
function;
57 if(new_function.id()==ID_symbol &&
60 new_arguments.clear();
68 if(new_function.id()==ID_if)
71 new_lhs,
to_if_expr(new_function), new_arguments, dest, mode);
73 else if(new_function.id()==ID_symbol)
78 else if(new_function.id() == ID_null_object)
81 else if(new_function.id()==ID_dereference ||
82 new_function.id()==
"virtual_function")
90 "unexpected function argument",
92 function.find_source_location());
140 v->source_location=
function.cond().source_location();
162 const exprt &
function,
172 t->source_location=
function.source_location();
173 t->code.
swap(function_call);
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.
#define Forall_expr(it, expr)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
The trinary if-then-else operator.
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
Base class for all expressions.
targett add_instruction()
Adds an instruction at the end.
codet representation of a function call statement.
#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...
virtual void do_function_call_other(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
add function calls to function queue for later processing
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::vector< exprt > operandst
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
virtual void do_function_call_if(const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
A generic container class for the GOTO intermediate representation of one function.
source_locationt & add_source_location()
instructionst::iterator targett