CBMC
|
#include <accelerator.h>
Public Member Functions | |
path_acceleratort (patht &_path, goto_programt &pure, goto_programt &overflow, std::set< exprt > &changed, std::set< exprt > &dirty) | |
path_acceleratort () | |
path_acceleratort (const path_acceleratort &that) | |
void | clear () |
Public Attributes | |
patht | path |
goto_programt | pure_accelerator |
goto_programt | overflow_path |
std::set< exprt > | changed_vars |
std::set< exprt > | dirty_vars |
Definition at line 26 of file accelerator.h.
|
inline |
Definition at line 29 of file accelerator.h.
|
inline |
Definition at line 42 of file accelerator.h.
|
inline |
Definition at line 44 of file accelerator.h.
|
inline |
Definition at line 53 of file accelerator.h.
std::set<exprt> path_acceleratort::changed_vars |
Definition at line 65 of file accelerator.h.
std::set<exprt> path_acceleratort::dirty_vars |
Definition at line 66 of file accelerator.h.
goto_programt path_acceleratort::overflow_path |
Definition at line 64 of file accelerator.h.
patht path_acceleratort::path |
Definition at line 62 of file accelerator.h.
goto_programt path_acceleratort::pure_accelerator |
Definition at line 63 of file accelerator.h.