|
CBMC
|
#include <accelerator.h>
Collaboration diagram for path_acceleratort: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.