12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_OVERFLOW_INSTRUMENTER_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_OVERFLOW_INSTRUMENTER_H 29 const exprt &_overflow_var,
64 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_OVERFLOW_INSTRUMENTER_H
overflow_instrumentert(goto_programt &_program, const exprt &_overflow_var, symbol_tablet &_symbol_table)
void add_overflow_checks()
std::unordered_set< exprt, irep_hash > expr_sett
API to expression classes.
std::list< targett > targetst
void overflow_expr(const exprt &expr, expr_sett &cases)
void accumulate_overflow(goto_programt::targett t, const exprt &expr, goto_programt::targetst &added)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void fix_types(exprt &overflow)
Base class for all expressions.
symbol_tablet & symbol_table
const exprt & overflow_var
instructionst::iterator targett