34 init_overflow->make_assignment();
70 checked.insert(t->location_number);
105 if(expr.
id()==ID_typecast)
107 if(expr.
op0().
id()==ID_constant)
114 const std::size_t old_width = old_type.
get_size_t(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();
294 assignment->
swap(*t);
296 added.push_back(assignment);
The type of an expression, extends irept.
Semantic type conversion.
A base class for relations, i.e., binary predicates.
std::list< targett > targetst
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
void add_overflow_checks()
typet & type()
Return the type of the expression.
std::set< unsigned > checked
This class represents an instruction in the GOTO intermediate representation.
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
instructionst::iterator targett
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
#define forall_operands(it, expr)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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.
void fix_types(exprt &overflow)
Base class for all expressions.
void swap(instructiont &instruction)
Swap two instructions.
const std::string & id_string() const
#define Forall_goto_program_instructions(it, program)
const exprt & overflow_var
std::size_t get_size_t(const irep_namet &name) const
A codet representing an assignment in the program.