Packages/c/cbmc-doc-6.9.0-1.fc45.x86_64.rpm

/*******************************************************************\


Module: Dynamic frame condition checking


Author: Qinheping Hu, qinhh@amazon.com


Author: Remi Delmas, delmasrd@amazon.com


Date: March 2023


\*******************************************************************/


#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_NESTING_GRAPH_H

#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_NESTING_GRAPH_H


#include <util/graph.h>


#include <analyses/loop_analysis.h>


class messaget;


struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>

{

public:

  dfcc_loop_nesting_graph_nodet(

    const goto_programt::targett &head,

    const goto_programt::targett &latch,

    const loop_templatet<

      goto_programt::targett,

      goto_programt::target_less_than> &instructions);


  goto_programt::targett head;


  goto_programt::targett latch;


  loop_templatet<goto_programt::targett, goto_programt::target_less_than>

    instructions;

};


typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;


dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program);


#endif

goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:72

goto_programt::targett
instructionst::iterator targett
Definition goto_program.h:613

goto_programt::target_less_than
instructiont::target_less_than target_less_than
Definition goto_program.h:618

graph_nodet
This class represents a node in a directed graph.
Definition graph.h:35

grapht
A generic directed graph with a parametric node type.
Definition graph.h:167

loop_templatet
A loop, specified as a set of instructions.
Definition loop_analysis.h:24

messaget
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154

build_loop_nesting_graph
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program)
Builds a graph instance describing the nesting structure of natural loops in the given goto_program.
Definition dfcc_loop_nesting_graph.cpp:27

dfcc_loop_nesting_grapht
grapht< dfcc_loop_nesting_graph_nodet > dfcc_loop_nesting_grapht
Definition dfcc_loop_nesting_graph.h:47

graph.h
A Template Class for Graphs.

loop_analysis.h
Data structure representing a loop in a GOTO program and an interface shared by all analyses that fin...

dfcc_loop_nesting_graph_nodet::instructions
loop_templatet< goto_programt::targett, goto_programt::target_less_than > instructions
Set of loop instructions.
Definition dfcc_loop_nesting_graph.h:44

dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet
dfcc_loop_nesting_graph_nodet(const goto_programt::targett &head, const goto_programt::targett &latch, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &instructions)
Definition dfcc_loop_nesting_graph.cpp:17

dfcc_loop_nesting_graph_nodet::head
goto_programt::targett head
Loop head instruction.
Definition dfcc_loop_nesting_graph.h:37

dfcc_loop_nesting_graph_nodet::latch
goto_programt::targett latch
Loop latch instruction.
Definition dfcc_loop_nesting_graph.h:40