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/symbol_table.h>
16 #include <util/namespace.h>
17 
19 
20 #include <set>
21 
22 #include "cone_of_influence.h"
23 
25 {
26  public:
28  const exprt &_overflow_var,
29  symbol_tablet &_symbol_table) :
30  program(_program),
31  symbol_table(_symbol_table),
32  overflow_var(_overflow_var),
34  {
35  }
36 
37  void add_overflow_checks();
42 
43  void overflow_expr(const exprt &expr, expr_sett &cases);
44  void overflow_expr(const exprt &expr, exprt &overflow);
45 
46  protected:
49 
52 
53  void fix_types(binary_exprt &overflow);
54 
58 
60  std::set<unsigned> checked;
61 };
62 
63 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_OVERFLOW_INSTRUMENTER_H
A base class for binary expressions.
Definition: std_expr.h:550
Base class for all expressions.
Definition: expr.h:54
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:592
std::list< targett > targetst
Definition: goto_program.h:594
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_tablet &_symbol_table)
std::set< unsigned > checked
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.
Definition: symbol_table.h:14
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
Concrete Goto Program.
Author: Diffblue Ltd.