Go to the documentation of this file.
68 if(t->has_condition())
71 checked.insert(t->location_number);
106 if(expr.
id()==ID_typecast)
110 if(typecast_expr.op().id() == ID_constant)
113 const typet &old_type = typecast_expr.op().type();
117 if(type.
id()==ID_signedbv)
119 if(old_type.
id()==ID_signedbv)
122 if(new_width >= old_width)
138 else if(old_type.
id()==ID_unsignedbv)
141 if(new_width >= old_width + 1)
153 else if(type.
id()==ID_unsignedbv)
155 if(old_type.
id()==ID_signedbv)
160 if(new_width < old_width - 1)
169 else if(old_type.
id()==ID_unsignedbv)
172 if(new_width>=old_width)
185 else if(expr.
id()==ID_div)
190 if(type.
id()==ID_signedbv)
196 cases.insert(
and_exprt(int_min_eq, minus_one_eq));
199 else if(expr.
id()==ID_unary_minus)
201 if(type.
id()==ID_signedbv)
210 else if(expr.
id()==ID_plus ||
211 expr.
id()==ID_minus ||
216 for(std::size_t i = 1; i < expr.
operands().size(); i++)
234 cases.insert(overflow);
247 for(expr_sett::iterator it=cases.begin();
287 assignment->swap(*t);
289 added.push_back(assignment);
#define Forall_goto_program_instructions(it, program)
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
The type of an expression, extends irept.
Base class for all expressions.
A base class for binary expressions.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::list< targett > targetst
typet & type()
Return the type of the expression.
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
void accumulate_overflow(goto_programt::targett t, const exprt &expr, goto_programt::targetst &added)
#define forall_operands(it, expr)
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
void compute_location_numbers(unsigned &nr)
Compute location numbers.
void fix_types(binary_exprt &overflow)
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
std::unordered_set< exprt, irep_hash > expr_sett
const irep_idt & id() const
The Boolean constant false.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
typet join_types(const typet &t1, const typet &t2)
Return the smallest type that both t1 and t2 can be cast to without losing information.
std::size_t get_width() const
const exprt & overflow_var
instructionst instructions
The list of instructions in the goto program.
std::set< unsigned > checked
const code_assignt & to_code_assign(const codet &code)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
A base class for relations, i.e., binary predicates whose two operands have the same type.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Semantic type conversion.
A codet representing an assignment in the program.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
API to expression classes.
void overflow_expr(const exprt &expr, expr_sett &cases)
void add_overflow_checks()
instructionst::iterator targett
API to expression classes for bitvectors.