cprover
overflow_instrumenter.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: 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/std_expr.h>
16 #include <util/symbol_table.h>
17 #include <util/namespace.h>
18 
20 
21 #include <set>
22 
23 #include "cone_of_influence.h"
24 
26 {
27  public:
29  const exprt &_overflow_var,
30  symbol_tablet &_symbol_table) :
31  program(_program),
32  symbol_table(_symbol_table),
33  overflow_var(_overflow_var),
35  {
36  }
37 
38  void add_overflow_checks();
43 
44  void overflow_expr(const exprt &expr, expr_sett &cases);
45  void overflow_expr(const exprt &expr, exprt &overflow);
46 
47  protected:
50 
53 
54  void fix_types(binary_exprt &overflow);
55 
59 
61  std::set<unsigned> checked;
62 };
63 
64 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_OVERFLOW_INSTRUMENTER_H
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
overflow_instrumentert::ns
namespacet ns
Definition: overflow_instrumenter.h:60
overflow_instrumentert::overflow_instrumentert
overflow_instrumentert(goto_programt &_program, const exprt &_overflow_var, symbol_tablet &_symbol_table)
Definition: overflow_instrumenter.h:28
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
namespace.h
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:581
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
overflow_instrumentert::accumulate_overflow
void accumulate_overflow(goto_programt::targett t, const exprt &expr, goto_programt::targetst &added)
Definition: overflow_instrumenter.cpp:291
overflow_instrumentert::fix_types
void fix_types(binary_exprt &overflow)
Definition: overflow_instrumenter.cpp:274
overflow_instrumentert::symbol_table
symbol_tablet & symbol_table
Definition: overflow_instrumenter.h:57
expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: cone_of_influence.h:21
overflow_instrumentert
Definition: overflow_instrumenter.h:26
goto_program.h
Concrete Goto Program.
overflow_instrumentert::overflow_var
const exprt & overflow_var
Definition: overflow_instrumenter.h:58
overflow_instrumentert::checked
std::set< unsigned > checked
Definition: overflow_instrumenter.h:61
cone_of_influence.h
Loop Acceleration.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
symbol_table.h
Author: Diffblue Ltd.
overflow_instrumentert::program
goto_programt & program
Definition: overflow_instrumenter.h:56
std_expr.h
API to expression classes.
overflow_instrumentert::overflow_expr
void overflow_expr(const exprt &expr, expr_sett &cases)
Definition: overflow_instrumenter.cpp:94
overflow_instrumentert::add_overflow_checks
void add_overflow_checks()
Definition: overflow_instrumenter.cpp:30
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579