cbmc/dfcc__loop__nesting__graph_8h_source.html

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


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;

};

struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget> {…};


typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;


dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program);


#endif

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

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

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

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

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
A graph node that stores information about a natural loop.
Definition dfcc_loop_nesting_graph.h:27

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

goto_programt::instructiont::target_less_than
A total order over targett and const_targett.
Definition goto_program.h:392