CBMC
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_program.h>
#include "dfcc_loop_contract_mode.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.