CBMC
|
Classes providing CFG-based information about symbols to guide simplifications in function and loop assigns clause checking. More...
#include <ansi-c/goto-conversion/goto_convert_class.h>
#include <util/byte_operators.h>
#include <util/expr_cast.h>
#include <util/find_symbols.h>
#include <util/message.h>
#include <goto-programs/goto_model.h>
#include <analyses/dirty.h>
#include <analyses/locals.h>
#include <goto-instrument/havoc_utils.h>
#include <goto-instrument/loop_utils.h>
#include <set>
#include <vector>
Go to the source code of this file.
Classes | |
class | cfg_infot |
Stores information about a goto function computed from its CFG. More... | |
class | function_cfg_infot |
class | loop_cfg_infot |
class | goto_program_cfg_infot |
For a goto program. More... | |
Classes providing CFG-based information about symbols to guide simplifications in function and loop assigns clause checking.
Definition in file cfg_info.h.