dfcc_cfg_info.h File Reference

Class that computes CFG information about the loop structure of a GOTO function for the purpose of dynamic frame conditions checking and loop contract instrumentation. More...

#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/goto_program.h>
#include <goto-instrument/contracts/loop_contract_config.h>
#include <map>
#include <set>
#include <unordered_set>

Include dependency graph for dfcc_cfg_info.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	dfcc_loop_infot
	Describes a single loop for the purpose of DFCC loop contract instrumentation. More...
class	dfcc_cfg_infot
	Computes natural loops, enforces normal form conditions, computes the nesting graph, tags each instruction of the function with the loop ID of the innermost loop and loop instruction type. More...

Detailed Description

Class that computes CFG information about the loop structure of a GOTO function for the purpose of dynamic frame conditions checking and loop contract instrumentation.

Definition in file dfcc_cfg_info.h.