cprover
|
Stores information about a goto function computed from its CFG, together with a target
iterator into the instructions of the function.
More...
#include <utils.h>
Public Member Functions | |
cfg_infot (const namespacet &_ns, goto_functiont &_goto_function) | |
void | step () |
Steps the target iterator forward. | |
bool | is_not_local_or_dirty_local (irep_idt ident) const |
Returns true iff the given ident is either not a goto_function local or is a local that is dirty. | |
bool | is_maybe_alive (const symbol_exprt &symbol_expr) |
Returns true whenever the given symbol_expr might be alive at the current target instruction. | |
bool | is_local (irep_idt ident) const |
Returns true iff ident is a local (or parameter) of goto_function . | |
const goto_programt::targett & | get_current_target () const |
returns the current target instruction | |
Private Attributes | |
const namespacet & | ns |
goto_functiont & | goto_function |
goto_programt::targett | target |
const dirtyt | dirty_analysis |
const localst | locals |
Stores information about a goto function computed from its CFG, together with a target
iterator into the instructions of the function.
The methods of this class provide information about identifiers at the current target
instruction to allow simplifying assigns clause checking assertions.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
private |
|
private |
|
private |