cprover
Loading...
Searching...
No Matches
overflow_instrumenter.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: Matt Lewis
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_OVERFLOW_INSTRUMENTER_H
13#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_OVERFLOW_INSTRUMENTER_H
14
15#include <util/namespace.h>
16
18
19#include <set>
20
21#include "cone_of_influence.h"
22
24{
25public:
27 goto_programt &_program,
28 const exprt &_overflow_var,
29 symbol_table_baset &_symbol_table)
30 : program(_program),
31 symbol_table(_symbol_table),
32 overflow_var(_overflow_var),
34 {
35 }
36
39 void
41
42 void overflow_expr(const exprt &expr, expr_sett &cases);
43 void overflow_expr(const exprt &expr, exprt &overflow);
44
45protected:
48 const exprt &expr,
50
53 const exprt &expr,
55
56 void fix_types(binary_exprt &overflow);
57
61
63 std::set<unsigned> checked;
64};
65
66#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_OVERFLOW_INSTRUMENTER_H
A base class for binary expressions.
Definition std_expr.h:638
Base class for all expressions.
Definition expr.h:56
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
std::list< targett > targetst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
overflow_instrumentert(goto_programt &_program, const exprt &_overflow_var, symbol_table_baset &_symbol_table)
std::set< unsigned > checked
symbol_table_baset & symbol_table
void fix_types(binary_exprt &overflow)
void accumulate_overflow(goto_programt::targett t, const exprt &expr, goto_programt::targetst &added)
void overflow_expr(const exprt &expr, expr_sett &cases)
The symbol table base class interface.
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
Concrete Goto Program.