cprover
|
#include <overflow_instrumenter.h>
Public Member Functions | |
overflow_instrumentert (goto_programt &_program, const exprt &_overflow_var, symbol_tablet &_symbol_table) | |
void | add_overflow_checks () |
void | add_overflow_checks (goto_programt::targett t) |
void | add_overflow_checks (goto_programt::targett t, goto_programt::targetst &added) |
void | overflow_expr (const exprt &expr, expr_sett &cases) |
void | overflow_expr (const exprt &expr, exprt &overflow) |
Protected Member Functions | |
void | add_overflow_checks (goto_programt::targett t, const exprt &expr, goto_programt::targetst &added) |
void | accumulate_overflow (goto_programt::targett t, const exprt &expr, goto_programt::targetst &added) |
void | fix_types (exprt &overflow) |
Protected Attributes | |
goto_programt & | program |
symbol_tablet & | symbol_table |
const exprt & | overflow_var |
namespacet | ns |
std::set< int > | checked |
Definition at line 25 of file overflow_instrumenter.h.
|
inline |
Definition at line 28 of file overflow_instrumenter.h.
|
protected |
Definition at line 285 of file overflow_instrumenter.cpp.
References ASSIGN, goto_programt::instructiont::code, goto_programt::insert_after(), overflow_var, program, and goto_programt::instructiont::swap().
Referenced by add_overflow_checks().
void overflow_instrumentert::add_overflow_checks | ( | ) |
Definition at line 30 of file overflow_instrumenter.cpp.
References checked, goto_programt::compute_location_numbers(), Forall_goto_program_instructions, goto_programt::insert_before(), goto_programt::instructions, overflow_var, and program.
Referenced by add_overflow_checks(), acceleration_utilst::ensure_no_overflows(), and acceleratet::make_overflow_loc().
void overflow_instrumentert::add_overflow_checks | ( | goto_programt::targett | t | ) |
Definition at line 73 of file overflow_instrumenter.cpp.
References add_overflow_checks().
void overflow_instrumentert::add_overflow_checks | ( | goto_programt::targett | t, |
goto_programt::targetst & | added | ||
) |
Definition at line 46 of file overflow_instrumenter.cpp.
References add_overflow_checks(), checked, code_assignt::lhs(), overflow_var, code_assignt::rhs(), and to_code_assign().
|
protected |
Definition at line 80 of file overflow_instrumenter.cpp.
References accumulate_overflow(), and overflow_expr().
|
protected |
Definition at line 268 of file overflow_instrumenter.cpp.
References join_types(), exprt::op0(), exprt::op1(), and exprt::type().
Referenced by overflow_expr().
Definition at line 94 of file overflow_instrumenter.cpp.
References fix_types(), namespace_baset::follow(), forall_operands, from_integer(), irept::get_int(), irept::id(), irept::id_string(), ns, exprt::op0(), exprt::op1(), exprt::operands(), power(), signedbv_typet::smallest_expr(), to_signedbv_type(), and exprt::type().
Referenced by add_overflow_checks(), polynomial_acceleratort::assert_for_values(), and overflow_expr().
Definition at line 245 of file overflow_instrumenter.cpp.
References overflow_expr().
|
protected |
Definition at line 61 of file overflow_instrumenter.h.
Referenced by add_overflow_checks().
|
protected |
Definition at line 60 of file overflow_instrumenter.h.
Referenced by overflow_expr().
|
protected |
Definition at line 58 of file overflow_instrumenter.h.
Referenced by accumulate_overflow(), and add_overflow_checks().
|
protected |
Definition at line 56 of file overflow_instrumenter.h.
Referenced by accumulate_overflow(), and add_overflow_checks().
|
protected |
Definition at line 57 of file overflow_instrumenter.h.