CBMC
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
overflow_instrumentert Class Reference

#include <overflow_instrumenter.h>

+ Collaboration diagram for overflow_instrumentert:

Public Member Functions

 overflow_instrumentert (goto_programt &_program, const exprt &_overflow_var, symbol_table_baset &_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 (binary_exprt &overflow)
 

Protected Attributes

goto_programt & program
 
symbol_table_baset & symbol_table
 
const exprt & overflow_var
 
namespacet ns
 
std::set< unsigned > checked
 

Detailed Description

Definition at line 23 of file overflow_instrumenter.h.

Constructor & Destructor Documentation

◆ overflow_instrumentert()

overflow_instrumentert::overflow_instrumentert ( goto_programt &  _program,
const exprt &  _overflow_var,
symbol_table_baset &  _symbol_table 
)
inline

Definition at line 26 of file overflow_instrumenter.h.

Member Function Documentation

◆ accumulate_overflow()

void overflow_instrumentert::accumulate_overflow ( goto_programt::targett  t,
const exprt &  expr,
goto_programt::targetst &  added 
)
protected

Definition at line 272 of file overflow_instrumenter.cpp.

◆ add_overflow_checks() [1/4]

void overflow_instrumentert::add_overflow_checks ( )

Definition at line 26 of file overflow_instrumenter.cpp.

◆ add_overflow_checks() [2/4]

void overflow_instrumentert::add_overflow_checks ( goto_programt::targett  t)

Definition at line 67 of file overflow_instrumenter.cpp.

◆ add_overflow_checks() [3/4]

void overflow_instrumentert::add_overflow_checks ( goto_programt::targett  t,
const exprt &  expr,
goto_programt::targetst &  added 
)
protected

Definition at line 74 of file overflow_instrumenter.cpp.

◆ add_overflow_checks() [4/4]

void overflow_instrumentert::add_overflow_checks ( goto_programt::targett  t,
goto_programt::targetst &  added 
)

Definition at line 41 of file overflow_instrumenter.cpp.

◆ fix_types()

void overflow_instrumentert::fix_types ( binary_exprt &  overflow)
protected

Definition at line 255 of file overflow_instrumenter.cpp.

◆ overflow_expr() [1/2]

void overflow_instrumentert::overflow_expr ( const exprt &  expr,
expr_sett &  cases 
)

Definition at line 88 of file overflow_instrumenter.cpp.

◆ overflow_expr() [2/2]

void overflow_instrumentert::overflow_expr ( const exprt &  expr,
exprt &  overflow 
)

Definition at line 232 of file overflow_instrumenter.cpp.

Member Data Documentation

◆ checked

std::set<unsigned> overflow_instrumentert::checked
protected

Definition at line 63 of file overflow_instrumenter.h.

◆ ns

namespacet overflow_instrumentert::ns
protected

Definition at line 62 of file overflow_instrumenter.h.

◆ overflow_var

const exprt& overflow_instrumentert::overflow_var
protected

Definition at line 60 of file overflow_instrumenter.h.

◆ program

goto_programt& overflow_instrumentert::program
protected

Definition at line 58 of file overflow_instrumenter.h.

◆ symbol_table

symbol_table_baset& overflow_instrumentert::symbol_table
protected

Definition at line 59 of file overflow_instrumenter.h.

The documentation for this class was generated from the following files: