Go to the documentation of this file.
25 if(expr.
id()==ID_symbol)
27 if(expr.
get_bool(ID_C_invalid_object))
32 const irep_idt &failed_symbol = ptr_symbol.
type.
get(ID_C_failed_symbol);
34 if(failed_symbol.
empty())
37 const symbolt *symbol =
nullptr;
53 if(expr.
id()==ID_and || expr.
id()==ID_or)
56 throw expr.
id_string()+
" must be Boolean, but got "+
62 throw expr.
id_string()+
" takes Boolean operands only, but got "+
70 else if(expr.
id()==ID_if)
74 if(!if_expr.cond().is_boolean())
76 std::string msg =
"first argument of if must be boolean, but got " +
77 if_expr.cond().pretty();
83 bool o1 =
has_subexpr(if_expr.true_case(), ID_dereference);
84 bool o2 =
has_subexpr(if_expr.false_case(), ID_dereference);
95 if(expr.
id() == ID_address_of)
109 if(expr.
id()==ID_dereference)
113 else if(expr.
id()==ID_index)
156 const bool checks_only)
171 for(goto_programt::instructionst::iterator
193 for(goto_functionst::function_mapt::iterator
234 for(
auto &arg : function_call.
arguments())
243 if(
r.return_value().is_not_nil())
252 const irep_idt &statement = code.get_statement();
254 if(statement==ID_expression)
256 if(code.operands().size() != 1)
257 throw "expression expects one operand";
261 else if(statement==ID_printf)
263 for(
auto &op : code.operands())
294 goto_program_dereference(
313 goto_program_dereference(ns, new_symbol_table, options, value_sets);
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)
void set_other(codet &c)
Set the statement for OTHER.
code_expressiont & to_code_expression(codet &code)
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
void dereference_expression(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr)
Set the current target to target and remove derefence from expr.
#define Forall_operands(it, expr)
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const code_returnt & get_return() const
Get the return statement for READ.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
typet type
Type of symbol.
void set_return(code_returnt c)
Set the return statement for READ.
Base class for all expressions.
function_mapt function_map
void dereference_expr(exprt &expr, const bool checks_only)
Remove dereference expressions contained in expr.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
const codet & get_other() const
Get the statement for OTHER.
value_set_dereferencet dereference
void get_value_set(const exprt &expr, value_setst::valuest &dest) const override
Gets the value set corresponding to the current target and expression expr.
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
exprt dereference(const exprt &pointer)
Dereference the given pointer-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.
bool get_bool(const irep_namet &name) const
std::list< exprt > valuest
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Wrapper for functions removing dereferences in expressions contained in a goto program.
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets)
Remove dereferences in all expressions contained in the program goto_model.
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
const std::string & id_string() const
bool has_condition() const
Does this instruction have a condition?
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
#define Forall_goto_functions(it, functions)
void clear()
Clear the goto program.
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
A collection of goto functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
goto_functionst goto_functions
GOTO functions.
const irep_idt & get(const irep_namet &name) const
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
void dereference_program(goto_programt &goto_program, bool checks_only=false)
A generic container class for the GOTO intermediate representation of one function.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
instructionst::const_iterator const_targett
virtual void get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr, valuest &dest)=0
goto_programt::const_targett current_target
irep_idt current_function
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
bool is_function_call() const
bool is_boolean() const
Return whether the expression represents a Boolean.
void dereference_rec(exprt &expr)
Turn subexpression of expr of the form &*p into p and use dereference on subexpressions of the form *...
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet symbol_table
Symbol table.
instructionst::iterator targett