Go to the documentation of this file.
67 if(t->has_condition())
70 checked.insert(t->location_number);
105 if(expr.
id()==ID_typecast)
109 if(typecast_expr.op().id() == ID_constant)
112 const typet &old_type = typecast_expr.op().type();
116 if(type.
id()==ID_signedbv)
118 if(old_type.
id()==ID_signedbv)
121 if(new_width >= old_width)
137 else if(old_type.
id()==ID_unsignedbv)
140 if(new_width >= old_width + 1)
152 else if(type.
id()==ID_unsignedbv)
154 if(old_type.
id()==ID_signedbv)
159 if(new_width < old_width - 1)
168 else if(old_type.
id()==ID_unsignedbv)
171 if(new_width>=old_width)
184 else if(expr.
id()==ID_div)
189 if(type.
id()==ID_signedbv)
195 cases.insert(
and_exprt(int_min_eq, minus_one_eq));
198 else if(expr.
id()==ID_unary_minus)
200 if(type.
id()==ID_signedbv)
209 else if(expr.
id()==ID_plus ||
210 expr.
id()==ID_minus ||
220 for(std::size_t i=1; i<expr.
operands().size(); i++)
240 cases.insert(overflow);
246 cases.insert(overflow);
259 for(expr_sett::iterator it=cases.begin();
299 assignment->swap(*t);
301 added.push_back(assignment);
#define Forall_goto_program_instructions(it, program)
A base class for multi-ary expressions Associativity is not specified.
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.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
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)
void compute_location_numbers(unsigned &nr)
Compute location numbers.
void fix_types(binary_exprt &overflow)
const std::string & id_string() const
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.
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.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
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
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.