27 if(expr.
id()==ID_symbol)
29 if(expr.
get_bool(ID_C_invalid_object))
34 const irep_idt &failed_symbol = ptr_symbol.
type.
get(ID_C_failed_symbol);
36 if(failed_symbol.
empty())
39 const symbolt *symbol =
nullptr;
55 if(expr.
id()==ID_and || expr.
id()==ID_or)
58 throw expr.
id_string()+
" must be Boolean, but got "+
64 throw expr.
id_string()+
" takes Boolean operands only, but got "+
72 else if(expr.
id()==ID_if)
76 if(!if_expr.cond().is_boolean())
78 std::string msg =
"first argument of if must be boolean, but got " +
79 if_expr.cond().pretty();
85 bool o1 =
has_subexpr(if_expr.true_case(), ID_dereference);
86 bool o2 =
has_subexpr(if_expr.false_case(), ID_dereference);
97 if(expr.
id() == ID_address_of)
111 if(expr.
id()==ID_dereference)
115 else if(expr.
id()==ID_index)
147 const bool checks_only)
162 for(goto_programt::instructionst::iterator
184 for(goto_functionst::function_mapt::iterator
212 if(
as_const(i).call_lhs().is_not_nil())
227 const irep_idt &statement = code.get_statement();
229 if(statement==ID_expression)
231 if(code.operands().size() != 1)
232 throw "expression expects one operand";
236 else if(statement==ID_printf)
238 for(
auto &op : code.operands())
270 ns, goto_model.
symbol_table, options, value_sets, message_handler);
289 ns, new_symbol_table, options, value_sets, message_handler);
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_boolean() const
Return whether the expression represents a Boolean.
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Wrapper for functions removing dereferences in expressions contained in a goto program.
void dereference_program(goto_programt &goto_program, bool checks_only=false)
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
void dereference_expr(exprt &expr, const bool checks_only)
Remove dereference expressions contained in expr.
value_set_dereferencet dereference
std::vector< exprt > get_value_set(const exprt &expr) const override
Gets the value set corresponding to the current target and expression expr.
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
void dereference_rec(exprt &expr)
Turn subexpression of expr of the form &*p into p and use dereference on subexpressions of the form *...
goto_programt::const_targett current_target
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.
irep_idt current_function
This class represents an instruction in the GOTO intermediate representation.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
bool is_set_return_value() const
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
bool has_condition() const
Does this instruction have a condition?
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
exprt & condition_nonconst()
Get the condition of gotos, assume, assert.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
bool is_function_call() const
void set_other(goto_instruction_codet &c)
Set the statement for OTHER.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
instructionst::const_iterator const_targett
bool get_bool(const irep_idt &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & get(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
typet type
Type of symbol.
static exprt conditional_cast(const exprt &expr, const typet &type)
exprt dereference(const exprt &pointer, bool display_points_to_sets=false)
Dereference the given pointer-expression.
virtual std::vector< exprt > get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr)=0
#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.
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in all expressions contained in the program goto_model.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
code_expressiont & to_code_expression(codet &code)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.