34 init_overflow->make_assignment();
70 checked.insert(t->location_number);
105 if(expr.
id()==ID_typecast)
107 if(expr.
op0().
id()==ID_constant)
113 std::size_t new_width=expr.
type().
get_int(ID_width);
114 std::size_t old_width=old_type.
get_int(ID_width);
116 if(type.
id()==ID_signedbv)
118 if(old_type.
id()==ID_signedbv)
121 if(new_width >= old_width)
135 else if(old_type.
id()==ID_unsignedbv)
138 if(new_width >= old_width + 1)
149 else if(type.
id()==ID_unsignedbv)
151 if(old_type.
id()==ID_signedbv)
157 if(new_width < old_width - 1)
165 else if(old_type.
id()==ID_unsignedbv)
168 if(new_width>=old_width)
180 else if(expr.
id()==ID_div)
183 if(type.
id()==ID_signedbv)
189 cases.insert(
and_exprt(int_min_eq, minus_one_eq));
192 else if(expr.
id()==ID_unary_minus)
194 if(type.
id()==ID_signedbv)
203 else if(expr.
id()==ID_plus ||
204 expr.
id()==ID_minus ||
214 for(std::size_t i=1; i<expr.
operands().size(); i++)
228 overflow.operands().resize(2);
234 cases.insert(overflow);
240 cases.insert(overflow);
253 for(expr_sett::iterator it=cases.begin();
290 goto_programt::instructiont a(
ASSIGN);
294 assignment->swap(*t);
296 added.push_back(assignment);
The type of an expression.
const typet & follow(const typet &src) const
A generic base class for relations, i.e., binary predicates.
instructionst instructions
The list of instructions in the goto program.
void add_overflow_checks()
signed int get_int(const irep_namet &name) const
void compute_location_numbers(unsigned &nr)
Compute location numbers.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
std::unordered_set< exprt, irep_hash > expr_sett
constant_exprt smallest_expr() const
API to expression classes.
std::list< targett > targetst
#define forall_operands(it, expr)
targett insert_after(const_targett target)
Insertion after the given target.
void overflow_expr(const exprt &expr, expr_sett &cases)
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.
void accumulate_overflow(goto_programt::targett t, const exprt &expr, goto_programt::targetst &added)
The boolean constant false.
targett insert_before(const_targett target)
Insertion before the given target.
void fix_types(exprt &overflow)
Base class for all expressions.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
const std::string & id_string() const
#define Forall_goto_program_instructions(it, program)
const exprt & overflow_var
instructionst::iterator targett