CBMC
cfg_info.h File Reference

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>
+ Include dependency graph for cfg_info.h:
+ This graph shows which files directly or indirectly include this file:

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...
 

Detailed Description

Classes providing CFG-based information about symbols to guide simplifications in function and loop assigns clause checking.

Definition in file cfg_info.h.