-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================

with Clists;
with CommandLineData;
with DAG_IO;
with Debug;
with Declarations;
with E_Strings.Not_SPARK;
with LexTokenManager;
with Pairs;
with Structures;
with SystemErrors;

package body Graph
--# own Table is Assertion_Locn,
--#              Column,
--#              In_Degree,
--#              Nmbr_Of_Stmts,
--#              Out_Degree,
--#              Proof_Context,
--#              Refinement_Post_Check,
--#              Refinement_Pre_Check,
--#              Row,
--#              Subclass_Post_Check,
--#              Subclass_Pre_Check,
--#              Text_Line_Nmbr;
-- If more refinement constituents are added here, then
-- the initialization code in the package body elaboration part
-- AND in procedure Reinitialize_Graph will need to be updated.
is
   type Vector_Of_Cells is array (Matrix_Index) of Cells.Cell;
   type Proof_Context_Array is array (Matrix_Index) of Proof_Context_Type;
   type Vector_Of_Integers is array (Matrix_Index) of Integer;
   type Vector_Of_Degrees is array (Matrix_Index) of Natural;

   Row                   : Vector_Of_Cells;
   Column                : Vector_Of_Cells;
   In_Degree             : Vector_Of_Degrees;
   Out_Degree            : Vector_Of_Degrees;
   Nmbr_Of_Stmts         : Matrix_Index;
   Assertion_Locn        : Vector_Of_Cells;
   Proof_Context         : Proof_Context_Array;
   Text_Line_Nmbr        : Vector_Of_Integers;
   Refinement_Pre_Check  : Cells.Cell;
   Refinement_Post_Check : Cells.Cell;
   Subclass_Pre_Check    : Cells.Cell;
   Subclass_Post_Check   : Cells.Cell;

   --------------------------------------------------------------------------
   procedure Inc_Nmbr_Of_Stmts
   --# global in out Nmbr_Of_Stmts;
   --# derives Nmbr_Of_Stmts from *;
   is
   begin
      if Nmbr_Of_Stmts = ExaminerConstants.VCGMatrixOrder then
         SystemErrors.Fatal_Error (Sys_Err => SystemErrors.VCG_Graph_Size_Exceeded,
                                   Msg     => "");
      end if;
      Nmbr_Of_Stmts := Nmbr_Of_Stmts + 1;
   end Inc_Nmbr_Of_Stmts;

   --------------------------------------------------------------------------

   procedure Set_Nmbr_Of_Stmts (N : in Matrix_Index)
   --# global out Nmbr_Of_Stmts;
   --# derives Nmbr_Of_Stmts from N;
   is
   begin
      Nmbr_Of_Stmts := N;
   end Set_Nmbr_Of_Stmts;

   --------------------------------------------------------------------------

   function Get_Nmbr_Of_Stmts return Matrix_Index
   --# global in Nmbr_Of_Stmts;
   is
   begin
      return Nmbr_Of_Stmts;
   end Get_Nmbr_Of_Stmts;

   --------------------------------------------------------------------------

   procedure Set_Proof_Context (X : in Proof_Context_Type)
   --# global in     Nmbr_Of_Stmts;
   --#        in out Proof_Context;
   --# derives Proof_Context from *,
   --#                            Nmbr_Of_Stmts,
   --#                            X;
   is
   begin
      Proof_Context (Nmbr_Of_Stmts) := X;
   end Set_Proof_Context;

   --------------------------------------------------------------------------

   procedure Set_First_Proof_Context (X : in Proof_Context_Type)
   --# global in out Proof_Context;
   --# derives Proof_Context from *,
   --#                            X;
   is
   begin
      Proof_Context (1) := X;
   end Set_First_Proof_Context;

   --------------------------------------------------------------------------

   procedure Set_Assertion_Locn (X : in Cells.Cell)
   --# global in     Nmbr_Of_Stmts;
   --#        in out Assertion_Locn;
   --# derives Assertion_Locn from *,
   --#                             Nmbr_Of_Stmts,
   --#                             X;
   is
   begin
      Assertion_Locn (Nmbr_Of_Stmts) := X;
   end Set_Assertion_Locn;

   --------------------------------------------------------------------------

   procedure Set_First_Assertion_Locn (X : in Cells.Cell)
   --# global in out Assertion_Locn;
   --# derives Assertion_Locn from *,
   --#                             X;
   is
   begin
      Assertion_Locn (1) := X;
   end Set_First_Assertion_Locn;

   --------------------------------------------------------------------------

   function Get_Assertion_Locn return  Cells.Cell
   --# global in Assertion_Locn;
   --#        in Nmbr_Of_Stmts;
   is
   begin
      return Assertion_Locn (Nmbr_Of_Stmts);
   end Get_Assertion_Locn;

   --------------------------------------------------------------------------

   function Get_Preceding_Assertion_Locn return  Cells.Cell
   --# global in Assertion_Locn;
   --#        in Nmbr_Of_Stmts;
   --  pre     Nmbr_Of_Stmts > 1;
   is
   begin
      return Assertion_Locn (Nmbr_Of_Stmts - 1);
   end Get_Preceding_Assertion_Locn;

   --------------------------------------------------------------------------

   procedure Set_Text_Line_Nmbr (X : in Integer)
   --# global in     Nmbr_Of_Stmts;
   --#        in out Text_Line_Nmbr;
   --# derives Text_Line_Nmbr from *,
   --#                             Nmbr_Of_Stmts,
   --#                             X;
   is
   begin
      Text_Line_Nmbr (Nmbr_Of_Stmts) := X;
   end Set_Text_Line_Nmbr;

   -----------------------------------------------------------------------

   procedure Insert_Text_Line_Nmbr (Index : in Matrix_Index;
                                    X     : in Integer)
   --# global in out Text_Line_Nmbr;
   --# derives Text_Line_Nmbr from *,
   --#                             Index,
   --#                             X;
   is
   begin
      Text_Line_Nmbr (Index) := X;
   end Insert_Text_Line_Nmbr;

   -----------------------------------------------------------------------

   procedure Set_Refinement_Pre_Check (X : in Cells.Cell)
   --# global out Refinement_Pre_Check;
   --# derives Refinement_Pre_Check from X;
   is
   begin
      Refinement_Pre_Check := X;
   end Set_Refinement_Pre_Check;

   --------------------------------------------------------------------------

   procedure Set_Refinement_Post_Check (X : in Cells.Cell)
   --# global out Refinement_Post_Check;
   --# derives Refinement_Post_Check from X;
   is
   begin
      Refinement_Post_Check := X;
   end Set_Refinement_Post_Check;

   --------------------------------------------------------------------------

   procedure Set_Subclass_Pre_Check (X : in Cells.Cell)
   --# global out Subclass_Pre_Check;
   --# derives Subclass_Pre_Check from X;
   is
   begin
      Subclass_Pre_Check := X;
   end Set_Subclass_Pre_Check;

   --------------------------------------------------------------------------

   procedure Set_Subclass_Post_Check (X : in Cells.Cell)
   --# global out Subclass_Post_Check;
   --# derives Subclass_Post_Check from X;
   is
   begin
      Subclass_Post_Check := X;
   end Set_Subclass_Post_Check;

   --------------------------------------------------------------------------

   procedure Reinitialize_Graph
   --# global out Assertion_Locn;
   --#        out Column;
   --#        out In_Degree;
   --#        out Nmbr_Of_Stmts;
   --#        out Out_Degree;
   --#        out Proof_Context;
   --#        out Refinement_Post_Check;
   --#        out Refinement_Pre_Check;
   --#        out Row;
   --#        out Subclass_Post_Check;
   --#        out Subclass_Pre_Check;
   --#        out Text_Line_Nmbr;
   --# derives Assertion_Locn,
   --#         Column,
   --#         In_Degree,
   --#         Nmbr_Of_Stmts,
   --#         Out_Degree,
   --#         Proof_Context,
   --#         Refinement_Post_Check,
   --#         Refinement_Pre_Check,
   --#         Row,
   --#         Subclass_Post_Check,
   --#         Subclass_Pre_Check,
   --#         Text_Line_Nmbr        from ;
   is
   begin
      -- If this procedure changes, then the package
      -- elaboration code at the end of this compilation
      -- unit will also need to be updated.

      --# accept F, 23, Row, "Initialization is total" &
      --#        F, 23, Column, "Initialization is total" &
      --#        F, 23, In_Degree, "Initialization is total" &
      --#        F, 23, Out_Degree, "Initialization is total" &
      --#        F, 23, Proof_Context, "Initialization is total" &
      --#        F, 23, Text_Line_Nmbr, "Initialization is total" &
      --#        F, 23, Assertion_Locn, "Initialization is total";
      for I in Matrix_Index loop
         Row (I)            := Cells.Null_Cell;
         Column (I)         := Cells.Null_Cell;
         In_Degree (I)      := 0;
         Out_Degree (I)     := 0;
         Proof_Context (I)  := Unspecified;
         Text_Line_Nmbr (I) := 0;
         Assertion_Locn (I) := Cells.Null_Cell;
      end loop;
      --# end accept;
      Nmbr_Of_Stmts         := 1;
      Refinement_Pre_Check  := Cells.Null_Cell;
      Refinement_Post_Check := Cells.Null_Cell;
      Subclass_Pre_Check    := Cells.Null_Cell;
      Subclass_Post_Check   := Cells.Null_Cell;
      --# accept F, 602, Row, Row, "Initialization is total" &
      --#        F, 602, Column, Column, "Initialization is total" &
      --#        F, 602, In_Degree, In_Degree, "Initialization is total" &
      --#        F, 602, Out_Degree, Out_Degree, "Initialization is total" &
      --#        F, 602, Proof_Context, Proof_Context, "Initialization is total" &
      --#        F, 602, Text_Line_Nmbr, Text_Line_Nmbr, "Initialization is total" &
      --#        F, 602, Assertion_Locn, Assertion_Locn, "Initialization is total";
   end Reinitialize_Graph;

   --------------------------------------------------------------------------

   procedure Create_Coeff (Heap : in out Cells.Heap_Record;
                           I, J : in     Matrix_Index;
                           K    : in     Labels.Label)
   --# global in out Column;
   --#        in out In_Degree;
   --#        in out Out_Degree;
   --#        in out Row;
   --#        in out Statistics.TableUsage;
   --# derives Column                from *,
   --#                                    Heap,
   --#                                    J &
   --#         Heap                  from *,
   --#                                    Column,
   --#                                    I,
   --#                                    J,
   --#                                    K,
   --#                                    Row &
   --#         In_Degree             from *,
   --#                                    J &
   --#         Out_Degree            from *,
   --#                                    I &
   --#         Row                   from *,
   --#                                    Heap,
   --#                                    I &
   --#         Statistics.TableUsage from *,
   --#                                    Heap;
   -- creates coefficient A(I, J), with value K;
   is
      -- 2 New_Element Cells used to reduce heap coupling in flow relations
      New_Row_Element, New_Col_Element : Cells.Cell;
   begin
      -- Create both new cells first
      Cells.Create_Cell (Heap, New_Row_Element);
      Cells.Create_Cell (Heap, New_Col_Element);

      -- Set row pointer;
      Cells.Set_Natural_Value (Heap, New_Row_Element, J);
      Cells.Set_B_Ptr (Heap, New_Row_Element, Labels.LabelHead (K));
      Cells.Set_A_Ptr (Heap, New_Row_Element, Row (I));
      Row (I)        := New_Row_Element;
      Out_Degree (I) := Out_Degree (I) + 1;

      -- Set column pointer;
      Cells.Set_Natural_Value (Heap, New_Col_Element, I);
      Cells.Set_B_Ptr (Heap, New_Col_Element, Labels.LabelHead (K));
      Cells.Set_A_Ptr (Heap, New_Col_Element, Column (J));
      Column (J)    := New_Col_Element;
      In_Degree (J) := In_Degree (J) + 1;
   end Create_Coeff;

   --------------------------------------------------------------------------

   function Coefficient (Heap : Cells.Heap_Record;
                         I, J : Matrix_Index) return Labels.Label
   --# global in Row;
   is
      Elem, Coeff_Cell : Cells.Cell;
   begin
      Coeff_Cell := Cells.Null_Cell;

      -- Pick out the head of the coefficient list for Row I
      Elem := Row (I);
      loop
         exit when Cells.Is_Null_Cell (Elem);

         -- Search the coeff list until a coefficient for column J
         -- is found
         if Cells.Get_Natural_Value (Heap, Elem) = J then
            -- Got it!  Return the Label associated with this coefficient
            Coeff_Cell := Cells.Get_B_Ptr (Heap, Elem);
            exit;
         end if;
         Elem := Cells.Get_A_Ptr (Heap, Elem);
      end loop;
      return Labels.CellToLabel (Coeff_Cell);
   end Coefficient;

   --------------------------------------------------------------------------

   procedure Dump_Graph_Dot
     (Heap                    : in out Cells.Heap_Record;
      Output_File_Name        : in     E_Strings.T;
      Output_File_Name_Suffix : in     Natural;
      Scope                   : in     Dictionary.Scopes;
      Print_Edges_As          : in     DOT_Dump_Kind)
   --# global in Assertion_Locn;
   --#        in Column;
   --#        in In_Degree;
   --#        in Nmbr_Of_Stmts;
   --#        in Out_Degree;
   --#        in Proof_Context;
   --#        in Row;
   --# derives Heap from * &
   --#         null from Assertion_Locn,
   --#                   Column,
   --#                   In_Degree,
   --#                   Nmbr_Of_Stmts,
   --#                   Output_File_Name,
   --#                   Output_File_Name_Suffix,
   --#                   Out_Degree,
   --#                   Print_Edges_As,
   --#                   Proof_Context,
   --#                   Row,
   --#                   Scope;
   is
      --# hide Dump_Graph_Dot;
      Arc          : Cells.Cell;
      Arc_Found    : Boolean;
      Arc_Label    : Labels.Label;
      Current_Pair : Pairs.Pair;
      Output_File  : SPARK_IO.File_Type;
      OK           : SPARK_IO.File_Status;

      procedure Form_And_Open_Output_File is
         -- Chop of the .vcg extension
         FN : constant String :=
           E_Strings.Not_SPARK.Get_String
           (E_Str => E_Strings.Section
              (E_Str     => Output_File_Name,
               Start_Pos => 1,
               Length    => E_Strings.Get_Length (E_Str => Output_File_Name) - 4));
         -- Form the suffix string and chop off the leading space
         Suffix         : constant String := Natural'Image (Output_File_Name_Suffix);
         Chopped_Suffix : constant String := String (Suffix (2 .. Suffix'Last));

         DOT_Name : constant String := FN & "_" & Chopped_Suffix & ".dot";
      begin
         SPARK_IO.Create
           (File         => Output_File,
            Name_Length  => DOT_Name'Length,
            Name_Of_File => DOT_Name,
            Form_Of_File => "",
            Status       => OK);
      end Form_And_Open_Output_File;

      procedure Print_Logical_Expn_DOT (Root : in Cells.Cell) is
         Sub_Expn_List : Cells.Cell;
         List_Member   : Cells.Cell;
      begin
         Clists.CreateList (Heap, Sub_Expn_List);
         DAG_IO.Partition (Root, Sub_Expn_List, Heap);

         List_Member := Clists.FirstCell (Heap, Sub_Expn_List);

         DAG_IO.PrintDag (Heap, Output_File, Cells.Get_B_Ptr (Heap, List_Member), Scope, DAG_IO.No_Wrap);
         List_Member := Clists.NextCell (Heap, List_Member);
         loop
            exit when Cells.Is_Null_Cell (List_Member);
            SPARK_IO.Put_String (File => Output_File,
                                 Item => " and\l",
                                 Stop => 0);
            DAG_IO.PrintDag (Heap, Output_File, Cells.Get_B_Ptr (Heap, List_Member), Scope, DAG_IO.No_Wrap);
            List_Member := Clists.NextCell (Heap, List_Member);
         end loop;
         SPARK_IO.Put_String (File => Output_File,
                              Item => "\l",
                              Stop => 0);

         Clists.DisposeOfList (Heap, Sub_Expn_List);
      end Print_Logical_Expn_DOT;

      procedure Print_PTC is
         Predicate : Cells.Cell;
      begin
         SPARK_IO.Put_String (File => Output_File,
                              Item => "taillabel=""",
                              Stop => 0);
         if Pairs.IsTrue (Heap, Current_Pair) then
            SPARK_IO.Put_String (File => Output_File,
                                 Item => "true",
                                 Stop => 0);
         else
            Predicate := Cells.Get_B_Ptr (Heap, Pairs.PairHead (Current_Pair));
            Print_Logical_Expn_DOT (Root => Predicate);
         end if;
         SPARK_IO.Put_String (File => Output_File,
                              Item => """",
                              Stop => 0);
      end Print_PTC;

      procedure Print_Action is
         Suppress_Wrap : Boolean := False;

         Action   : Cells.Cell;
         Mod_Cell : Cells.Cell;
      begin
         SPARK_IO.Put_String (File => Output_File,
                              Item => "headlabel=""",
                              Stop => 0);

         if Pairs.IsUnitAction (Heap, Current_Pair) then
            SPARK_IO.Put_String (File => Output_File,
                                 Item => "null",
                                 Stop => 0);
         else
            Action   := Cells.Get_C_Ptr (Heap, Pairs.PairHead (Current_Pair));
            Mod_Cell := Clists.FirstCell (Heap, Action);

            DAG_IO.Print_Cell_Contents
              (Heap          => Heap,
               Output_File   => Output_File,
               Cell_Name     => Mod_Cell,
               Suppress_Wrap => Suppress_Wrap,
               Scope         => Scope,
               Wrap_Limit    => DAG_IO.No_Wrap,
               Escape_DOT    => False);
            SPARK_IO.Put_String (File => Output_File,
                                 Item => " := ",
                                 Stop => 0);
            DAG_IO.PrintDag (Heap, Output_File, Cells.Get_B_Ptr (Heap, Mod_Cell), Scope, DAG_IO.No_Wrap);
            Mod_Cell := Clists.NextCell (Heap, Mod_Cell);

            loop
               exit when Cells.Is_Null_Cell (Mod_Cell);

               SPARK_IO.Put_String (File => Output_File,
                                    Item => " &\n",
                                    Stop => 0);
               DAG_IO.Print_Cell_Contents
                 (Heap          => Heap,
                  Output_File   => Output_File,
                  Cell_Name     => Mod_Cell,
                  Suppress_Wrap => Suppress_Wrap,
                  Scope         => Scope,
                  Wrap_Limit    => DAG_IO.No_Wrap,
                  Escape_DOT    => False);
               SPARK_IO.Put_String (File => Output_File,
                                    Item => " := ",
                                    Stop => 0);
               DAG_IO.PrintDag (Heap, Output_File, Cells.Get_B_Ptr (Heap, Mod_Cell), Scope, DAG_IO.No_Wrap);
               Mod_Cell := Clists.NextCell (Heap, Mod_Cell);
            end loop;

         end if;
         SPARK_IO.Put_String (File => Output_File,
                              Item => """",
                              Stop => 0);
      end Print_Action;

      procedure Print_VC is
         Hypotheses  : Cells.Cell;
         Conclusions : Cells.Cell;
      begin
         SPARK_IO.Put_String (File => Output_File,
                              Item => "label=""",
                              Stop => 0);
         if Pairs.IsTrue (Heap, Current_Pair) then
            SPARK_IO.Put_String (File => Output_File,
                                 Item => "true",
                                 Stop => 0);
         else
            Hypotheses := Cells.Get_B_Ptr (Heap, Pairs.PairHead (Current_Pair));
            Print_Logical_Expn_DOT (Root => Hypotheses);

            SPARK_IO.Put_String (File => Output_File,
                                 Item => "\l->\l",
                                 Stop => 0);

            Conclusions := Cells.Get_C_Ptr (Heap, Pairs.PairHead (Current_Pair));
            Print_Logical_Expn_DOT (Root => Conclusions);
         end if;

         SPARK_IO.Put_String (File => Output_File,
                              Item => """",
                              Stop => 0);
      end Print_VC;

      procedure Print_Node_Detail (I : in Matrix_Index) is
      begin
         SPARK_IO.Put_Integer (File  => Output_File,
                               Item  => I,
                               Width => 0,
                               Base  => 10);

         case Proof_Context (I) is
            when Precondition | Assertion | Default_Assertion | Postcondition =>

               -- Make cut-point nodes filled in 50% gray, so they are easy to see
               SPARK_IO.Put_String (File => Output_File,
                                    Item => " [style=filled,color=gray50,",
                                    Stop => 0);
            when others =>
               SPARK_IO.Put_String (File => Output_File,
                                    Item => " [",
                                    Stop => 0);
         end case;
         SPARK_IO.Put_String (File => Output_File,
                              Item => "label=""",
                              Stop => 0);

         -- Write label as node number and node type...
         SPARK_IO.Put_String
           (File => Output_File,
            Item => Matrix_Index'Image (I) & ' ' & Proof_Context_Type'Image (Proof_Context (I)),
            Stop => 0);

         -- ...and source line if present
         if Text_Line_Nmbr (I) /= 0 then
            SPARK_IO.Put_String (File => Output_File,
                                 Item => " line ",
                                 Stop => 0);
            SPARK_IO.Put_Integer (File  => Output_File,
                                  Item  => Text_Line_Nmbr (I),
                                  Width => 0,
                                  Base  => 10);
         end if;

         SPARK_IO.Put_String (File => Output_File,
                              Item => "\n",
                              Stop => 0);
         Print_Logical_Expn_DOT (Root => Assertion_Locn (I));
         SPARK_IO.Put_String (File => Output_File,
                              Item => """];",
                              Stop => 0);
      end Print_Node_Detail;

   begin
      Form_And_Open_Output_File;

      if OK = SPARK_IO.Ok then
         SPARK_IO.Put_String (File => Output_File,
                              Item => "digraph ",
                              Stop => 0);
         E_Strings.Put_String
           (File  => Output_File,
            E_Str => E_Strings.Lower_Case
              (E_Str => LexTokenManager.Lex_String_To_String (Lex_Str => Dictionary.GetSimpleName (Dictionary.GetRegion (Scope)))));
         SPARK_IO.Put_Line (File => Output_File,
                            Item => " {",
                            Stop => 0);
         SPARK_IO.Put_Line (File => Output_File,
                            Item => "ranksep=""1.0 equally"";",
                            Stop => 0);
         SPARK_IO.Put_Line (File => Output_File,
                            Item => "nodesep=1.0;",
                            Stop => 0);
         SPARK_IO.Put_Line (File => Output_File,
                            Item => "node [shape=box,fontname=helvetica];",
                            Stop => 0);
         SPARK_IO.Put_Line (File => Output_File,
                            Item => "edge [labelfontname=helvetica,labelfontsize=10];",
                            Stop => 0);

         -- Nodes
         for I in Matrix_Index range 1 .. Nmbr_Of_Stmts loop
            if In_Degree (I) = 0 and Out_Degree (I) = 0 then
               null; -- node not connected, so skip
            else
               if I = 1 then -- Precondition
                  SPARK_IO.Put_String (File => Output_File,
                                       Item => "{ rank = source; ",
                                       Stop => 0);
                  Print_Node_Detail (I => I);
                  SPARK_IO.Put_String (File => Output_File,
                                       Item => " }",
                                       Stop => 0);
               elsif I = Nmbr_Of_Stmts then -- Postcondition
                  SPARK_IO.Put_String (File => Output_File,
                                       Item => "{ rank = sink; ",
                                       Stop => 0);
                  Print_Node_Detail (I => I);
                  SPARK_IO.Put_String (File => Output_File,
                                       Item => " }",
                                       Stop => 0);
               else
                  Print_Node_Detail (I => I);
               end if;
               SPARK_IO.New_Line (File    => Output_File,
                                  Spacing => 1);
            end if;
         end loop;

         -- Edges
         -- For all statements except the precondition
         for Node in Matrix_Index range 2 .. Nmbr_Of_Stmts loop
            -- If that node has predecessors
            if In_Degree (Node) > 0 then

               -- Then search the coefficients in the Matrix for all
               -- Predecessors whose Successor is Node.
               for Predec in Matrix_Index range 1 .. Nmbr_Of_Stmts - 1 loop
                  Arc_Found := False;
                  Arc       := Column (Node);
                  while (not Arc_Found) and (not Cells.Is_Null_Cell (Arc)) loop
                     if Cells.Get_Natural_Value (Heap, Arc) = Predec then
                        Arc_Found := True;
                     else
                        Arc := Cells.Get_A_Ptr (Heap, Arc);
                     end if;
                  end loop;

                  if Arc_Found then
                     -- Found an arc from Statement Predec to Statement Node

                     Arc_Label := Labels.CellToLabel (Cells.Get_B_Ptr (Heap, Arc));

                     Current_Pair := Labels.FirstPair (Heap, Arc_Label);
                     loop
                        exit when Pairs.IsNullPair (Current_Pair);

                        SPARK_IO.Put_Integer (File  => Output_File,
                                              Item  => Predec,
                                              Width => 0,
                                              Base  => 10);
                        SPARK_IO.Put_String (File => Output_File,
                                             Item => " -> ",
                                             Stop => 0);
                        SPARK_IO.Put_Integer (File  => Output_File,
                                              Item  => Node,
                                              Width => 0,
                                              Base  => 10);

                        SPARK_IO.Put_String (File => Output_File,
                                             Item => "[style=",
                                             Stop => 0);

                        case Proof_Context (Node) is
                           when Check_Statement | Run_Time_Check | Precon_Check =>

                              SPARK_IO.Put_String (File => Output_File,
                                                   Item => "dashed",
                                                   Stop => 0);

                           when Assertion | Default_Assertion | Postcondition =>
                              SPARK_IO.Put_String (File => Output_File,
                                                   Item => "bold,headport=n,tailport=s",
                                                   Stop => 0);

                              -- Increase weight for forward edges terminating
                              -- at an assertion of postcondition.
                              if Node > Predec then
                                 SPARK_IO.Put_String (File => Output_File,
                                                      Item => ",weight=8.0",
                                                      Stop => 0);
                              end if;

                           when others =>
                              SPARK_IO.Put_String (File => Output_File,
                                                   Item => "solid",
                                                   Stop => 0);
                        end case;

                        case Print_Edges_As is
                           when PFs =>
                              SPARK_IO.Put_String (File => Output_File,
                                                   Item => ",",
                                                   Stop => 0);
                              Print_PTC;
                              SPARK_IO.Put_String (File => Output_File,
                                                   Item => ",",
                                                   Stop => 0);
                              Print_Action;
                           when VCs =>
                              SPARK_IO.Put_String (File => Output_File,
                                                   Item => ",",
                                                   Stop => 0);
                              Print_VC;
                        end case;

                        SPARK_IO.Put_String (File => Output_File,
                                             Item => "];",
                                             Stop => 0);

                        SPARK_IO.New_Line (File    => Output_File,
                                           Spacing => 1);

                        Current_Pair := Labels.NextPair (Heap, Current_Pair);
                     end loop;

                  end if;
               end loop;
            end if;
         end loop;

         SPARK_IO.Put_Line (File => Output_File,
                            Item => "}",
                            Stop => 0);
      end if;

   end Dump_Graph_Dot;

   ----------------------------------------------------------------------

   procedure Gen_VCs
     (Heap             : in out Cells.Heap_Record;
      Output_File      : in     SPARK_IO.File_Type;
      Output_File_Name : in     E_Strings.T;
      Scope            : in     Dictionary.Scopes;
      Gen_VC_Failure   :    out Boolean)
   --# global in     Assertion_Locn;
   --#        in     CommandLineData.Content;
   --#        in     Nmbr_Of_Stmts;
   --#        in     Proof_Context;
   --#        in out Column;
   --#        in out In_Degree;
   --#        in out Out_Degree;
   --#        in out Row;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Statistics.TableUsage;
   --# derives Column,
   --#         Gen_VC_Failure,
   --#         In_Degree,
   --#         Out_Degree,
   --#         Row                   from Column,
   --#                                    CommandLineData.Content,
   --#                                    Heap,
   --#                                    In_Degree,
   --#                                    Nmbr_Of_Stmts,
   --#                                    Out_Degree,
   --#                                    Proof_Context,
   --#                                    Row &
   --#         Heap,
   --#         Statistics.TableUsage from *,
   --#                                    Assertion_Locn,
   --#                                    Column,
   --#                                    CommandLineData.Content,
   --#                                    Heap,
   --#                                    In_Degree,
   --#                                    Nmbr_Of_Stmts,
   --#                                    Out_Degree,
   --#                                    Proof_Context,
   --#                                    Row &
   --#         SPARK_IO.File_Sys     from *,
   --#                                    Column,
   --#                                    CommandLineData.Content,
   --#                                    Heap,
   --#                                    In_Degree,
   --#                                    Nmbr_Of_Stmts,
   --#                                    Output_File,
   --#                                    Out_Degree,
   --#                                    Proof_Context,
   --#                                    Row &
   --#         null                  from Output_File_Name,
   --#                                    Scope;
   is
      Arc_Label                                                          : Labels.Label;
      Assertion_Copy, Conjunction, Current_Predicate, Matrix_Element, WP : Cells.Cell;
      Current_Pair                                                       : Pairs.Pair;
      Failure                                                            : Boolean;
      Initial_Node                                                       : Matrix_Index;
      Graph_Suffix                                                       : Natural;

      function Is_Check_Statement (X : Proof_Context_Type) return Boolean is
      begin
         return X = Check_Statement or else X = Run_Time_Check or else X = Precon_Check;
      end Is_Check_Statement;

      function Is_Assert_Statement (X : Proof_Context_Type) return Boolean is
      begin
         return X = Assertion or else X = Default_Assertion;
      end Is_Assert_Statement;

      -- deletes pointers to A(I, J);
      procedure Delete_Coeff (Heap : in out Cells.Heap_Record;
                              I, J : in     Matrix_Index)
      --# global in out Column;
      --#        in out In_Degree;
      --#        in out Out_Degree;
      --#        in out Row;
      --# derives Column,
      --#         Row        from *,
      --#                         Heap,
      --#                         I,
      --#                         J &
      --#         Heap       from *,
      --#                         Column,
      --#                         I,
      --#                         J,
      --#                         Row &
      --#         In_Degree  from *,
      --#                         J &
      --#         Out_Degree from *,
      --#                         I;
      is
         L1, M1, L2, M2 : Cells.Cell;
      begin
         -- Delete row pointer;
         L1 := Row (I);
         if Cells.Get_Natural_Value (Heap, L1) = J then
            Row (I) := Cells.Get_A_Ptr (Heap, L1);
         else
            loop
               M1 := L1;
               L1 := Cells.Get_A_Ptr (Heap, L1);
               exit when Cells.Get_Natural_Value (Heap, L1) = J;
            end loop;
            Cells.Set_A_Ptr (Heap, M1, Cells.Get_A_Ptr (Heap, L1));
         end if;
         Out_Degree (I) := Out_Degree (I) - 1;

         -- delete column pointer;
         L2 := Column (J);
         if Cells.Get_Natural_Value (Heap, L2) = I then
            Column (J) := Cells.Get_A_Ptr (Heap, L2);
         else
            loop
               M2 := L2;
               L2 := Cells.Get_A_Ptr (Heap, L2);
               exit when Cells.Get_Natural_Value (Heap, L2) = I;
            end loop;
            Cells.Set_A_Ptr (Heap, M2, Cells.Get_A_Ptr (Heap, L2));
         end if;
         Cells.Dispose_Of_Cell (Heap, L1);
         Cells.Dispose_Of_Cell (Heap, L2);
         In_Degree (J) := In_Degree (J) - 1;

         --# accept F, 601, Column, Row, "False coupling OK";
      end Delete_Coeff;

      -----------------------------------------------------------------
      -- Partially eliminate statement K of program,
      -- where K denotes a Check statement
      --
      -- For each sequence of paths I -> K -> J, replace
      -- this with I -> J with a Label formed from the
      -- Product of LabelIK and LabelKJ BUT
      -- leave paths I -> K remaining in place.
      --
      -- Repeat until all successors of K
      -- have been considered, at which point K will have
      -- no remaining successors.
      -----------------------------------------------------------------
      procedure Partial_Eliminate (K : in Matrix_Index)
      --# global in     Nmbr_Of_Stmts;
      --#        in     Proof_Context;
      --#        in out Column;
      --#        in out Heap;
      --#        in out In_Degree;
      --#        in out Out_Degree;
      --#        in out Row;
      --#        in out Statistics.TableUsage;
      --# derives Column,
      --#         Heap,
      --#         In_Degree,
      --#         Out_Degree,
      --#         Row,
      --#         Statistics.TableUsage from *,
      --#                                    Column,
      --#                                    Heap,
      --#                                    K,
      --#                                    Nmbr_Of_Stmts,
      --#                                    Row &
      --#         null                  from Proof_Context;
      is
         P1, P2, Product : Labels.Label;
      begin
         SystemErrors.RT_Assert
           (C       => Is_Check_Statement (X => Proof_Context (K)),
            Sys_Err => SystemErrors.Precondition_Failure,
            Msg     => "Trying to Partial_Eliminate a node which isn't a Check");

         -- For all statements J except the Precondition...
         for J in Matrix_Index range 2 .. Nmbr_Of_Stmts loop

            -- If J is a successor or K
            if not Labels.IsNull (Coefficient (Heap => Heap,
                                               I    => K,
                                               J    => J)) then

               -- For all statements I except the Postcondition
               for I in Matrix_Index range 1 .. Nmbr_Of_Stmts - 1 loop

                  -- If I is a predecessor of K
                  if not Labels.IsNull (Coefficient (Heap => Heap,
                                                     I    => I,
                                                     J    => K)) then

                     -- I is a predecessor of K;

                     -- form product, taking deep copies of the Labels
                     -- on the paths from I to K and K to J first:
                     Labels.CopyLabel (Heap, Coefficient (Heap => Heap,
                                                          I    => I,
                                                          J    => K), P1);
                     Labels.CopyLabel (Heap, Coefficient (Heap => Heap,
                                                          I    => K,
                                                          J    => J), P2);
                     Labels.MultiplyLabels (Heap, P1, P2, Product);

                     -- Check to see of an existing path from
                     -- I to J already exists.
                     if Labels.IsNull (Coefficient (Heap => Heap,
                                                    I    => I,
                                                    J    => J)) then
                        -- no existing path, so just add a new path from
                        -- I to J with Label Product
                        Create_Coeff (Heap => Heap,
                                      I    => I,
                                      J    => J,
                                      K    => Product);
                     else
                        -- Existing path from I to J, so add Product to its
                        -- Label
                        Labels.AddLabels (Heap, Coefficient (Heap => Heap,
                                                             I    => I,
                                                             J    => J), Product);
                     end if;

                  end if;
               end loop;

               -- Once we've dealt with all the predecessors I that form
               -- paths from I to J via K for a specific Label from K to J,
               -- we can delete the Label from K to J, before going
               -- on to consider the next successor J.
               Delete_Coeff (Heap => Heap,
                             I    => K,
                             J    => J);

               -- NOTE that we DON'T delete the original Labels I -> K here,
               -- since these forms the VCs for "all paths reaching a check"
               -- that we need. This is why this is _partial_ eliminate of
               -- statement K
            end if;
         end loop;

         SystemErrors.RT_Assert
           (C       => Out_Degree (K) = 0,
            Sys_Err => SystemErrors.Postcondition_Failure,
            Msg     => "Out_Degree of node is not zero after Partial_Eliminate");
      end Partial_Eliminate;

      --------------------------------------------------------------------------
      -- Eliminate statement K of program.
      --
      -- For each sequence of paths I -> K -> J, replace
      -- this with I -> J with a Label formed from the
      -- Product of LabelIK and LabelKJ.
      --
      -- Repeat until all predecessors and successors of K
      -- have been considered, at which point K will have
      -- no reamaining predecessors and successors, effectively
      -- removing it from the BPG.
      --------------------------------------------------------------------------
      procedure Eliminate (Heap : in out Cells.Heap_Record;
                           K    : in     Matrix_Index)
      --# global in     Nmbr_Of_Stmts;
      --#        in     Proof_Context;
      --#        in out Column;
      --#        in out In_Degree;
      --#        in out Out_Degree;
      --#        in out Row;
      --#        in out Statistics.TableUsage;
      --# derives Column,
      --#         Heap,
      --#         In_Degree,
      --#         Out_Degree,
      --#         Row,
      --#         Statistics.TableUsage from *,
      --#                                    Column,
      --#                                    Heap,
      --#                                    In_Degree,
      --#                                    K,
      --#                                    Nmbr_Of_Stmts,
      --#                                    Out_Degree,
      --#                                    Row &
      --#         null                  from Proof_Context;
      is
         P1, P2, Product : Labels.Label;
      begin
         SystemErrors.RT_Assert
           (C       => Proof_Context (K) = Unspecified,
            Sys_Err => SystemErrors.Precondition_Failure,
            Msg     => "Trying to eliminate a node which isn't UNSPECIFIED");

         -- For each statement
         for I in Matrix_Index range 1 .. Nmbr_Of_Stmts - 1 loop

            if not Labels.IsNull (Coefficient (Heap => Heap,
                                               I    => I,
                                               J    => K)) then
               -- I is a predecessor of K, since the Label connecting I to K is not null

               for J in Matrix_Index range 2 .. Nmbr_Of_Stmts loop

                  if not Labels.IsNull (Coefficient (Heap => Heap,
                                                     I    => K,
                                                     J    => J)) then
                     -- J is a successor of K, since the Label connecting K to J is not null

                     -- We've found two nodes I and J such that I is a predecessor
                     -- of K and J is a successor of K in the BPG. Graphically, we've
                     -- found a sequence such as:
                     --    I -> K -> J
                     -- in the BPG.

                     if Out_Degree (K) = 1 then
                        -- J is last successor, so take a shallow
                        -- copy of its content into P1
                        P1 := Coefficient (Heap => Heap,
                                           I    => I,
                                           J    => K);
                     else
                        -- Not the last successor, so take a deep
                        -- copy into P1
                        Labels.CopyLabel (Heap, Coefficient (Heap => Heap,
                                                             I    => I,
                                                             J    => K), P1);
                     end if;

                     if In_Degree (K) = 1 then
                        -- I is the last predecessor, so take a shallow
                        -- copy of its content into P2
                        P2 := Coefficient (Heap => Heap,
                                           I    => K,
                                           J    => J);

                        -- If I is the final predecessor, then we won't
                        -- be needed the information regarding successor J again,
                        -- so that Coeff can now be deleted from the BPG
                        Delete_Coeff (Heap => Heap,
                                      I    => K,
                                      J    => J);
                     else
                        -- Not the last predecessor, so take a deep copy into P2
                        Labels.CopyLabel (Heap, Coefficient (Heap => Heap,
                                                             I    => K,
                                                             J    => J), P2);
                     end if;

                     -- Form the Product of P1 and P2
                     Labels.MultiplyLabels (Heap, P1, P2, Product);

                     -- Check to see of an existing path from
                     -- I to J already exists.
                     if Labels.IsNull (Coefficient (Heap => Heap,
                                                    I    => I,
                                                    J    => J)) then
                        -- no existing path, so just add a new path from
                        -- I to J with Label Product
                        Create_Coeff (Heap => Heap,
                                      I    => I,
                                      J    => J,
                                      K    => Product);
                     else
                        -- Existing path from I to J, so add Product to its
                        -- Label
                        Labels.AddLabels (Heap, Coefficient (Heap => Heap,
                                                             I    => I,
                                                             J    => J), Product);
                     end if;
                  end if;
               end loop;

               -- Finally, having created or augmented a Label for the path from I to J,
               -- the path from I to K can be deleted.
               Delete_Coeff (Heap => Heap,
                             I    => I,
                             J    => K);
            end if;
         end loop;

         -- After elimination, statement K should have both
         -- In_Degree and Out_Degree set to 0 - i.e. no predecessors
         -- and no successors
         SystemErrors.RT_Assert
           (C       => In_Degree (K) = 0,
            Sys_Err => SystemErrors.Postcondition_Failure,
            Msg     => "In_Degree of node is not zero after Eliminate");
         SystemErrors.RT_Assert
           (C       => Out_Degree (K) = 0,
            Sys_Err => SystemErrors.Postcondition_Failure,
            Msg     => "Out_Degree of node is not zero after Eliminate");
      end Eliminate;

   begin -- Gen_VCs
      Failure      := False;
      Graph_Suffix := 1;

      for K in Matrix_Index range 2 .. Nmbr_Of_Stmts - 1 loop

         -- HTML Directives
         --! <NameFormat> <Name>
         --! <ErrorFormat> <"!!! "><Error>

         --! <Name> program-has-a-cyclic-path-without-an-assertion
         --! <Error> Program has a cyclic path without an assertion.
         --! SPARK generates VCs for paths between cutpoints in the code; these must
         --! be chosen by the developer in such a way that every loop traverses at
         --! least one cutpoint. If the SPARK
         --! Examiner detects a loop which is not broken by a cutpoint,
         --! it cannot generate verification
         --! conditions for the subprogram in which the loop is located,
         --! and instead, issues this
         --! warning. This can only be corrected by formulating a suitable
         --! loop-invariant assertion for
         --! the loop and including it as an assertion in the SPARK text
         --! at the appropriate point.

         if not Labels.IsNull (Coefficient (Heap => Heap,
                                            I    => K,
                                            J    => K)) then
            SPARK_IO.New_Line (File    => Output_File,
                               Spacing => 1);
            SPARK_IO.Put_Line (File => Output_File,
                               Item => "!!! Program has a cyclic path without an assertion.",
                               Stop => 0);
            Failure := True;
            exit;
         end if;

         if Is_Check_Statement (X => Proof_Context (K)) then
            -- Explicit Check, Runtime Check, or Precondition Check
            Partial_Eliminate (K => K);
         elsif not Is_Assert_Statement (X => Proof_Context (K)) then
            -- Not a Check nor an Assert of any kind.
            -- Can't be Precondition or PostCondition since K cannot
            -- denote these given range of the enclosing loop, so must be
            -- Unspecified
            Eliminate (Heap => Heap,
                       K    => K);
         end if;

         --# accept F, 41, "Stable expression expected here";
         if CommandLineData.Content.Debug.VCG_All then
            Dump_Graph_Dot
              (Heap                    => Heap,
               Output_File_Name        => Output_File_Name,
               Output_File_Name_Suffix => Graph_Suffix,
               Scope                   => Scope,
               Print_Edges_As          => PFs);
         end if;
         --# end accept;
         Graph_Suffix := Graph_Suffix + 1;

      end loop;

      -- We now have a BPG with all UNSPECIFIED nodes removed - leaving only
      -- explicit assertions, the pre-condition, the post-condition and checks.
      -- Each arc is labelled with its path-traveral condition and action like
      -- a path-function.

      if not Failure then
         -- To generate verification conditions, we do one final application
         -- of the assignment axiom to generate the VC, which is essentially
         --   (Precondition and PTC) -> Postcondition (Action)
         for K in Matrix_Index range 2 .. Nmbr_Of_Stmts loop

            if In_Degree (K) > 0 then
               Matrix_Element := Column (K);
               while not Cells.Is_Null_Cell (Matrix_Element) loop
                  Initial_Node := Cells.Get_Natural_Value (Heap, Matrix_Element);
                  Arc_Label    := Labels.CellToLabel (Cells.Get_B_Ptr (Heap, Matrix_Element));
                  Current_Pair := Labels.FirstPair (Heap, Arc_Label);
                  while not Pairs.IsNullPair (Current_Pair) loop
                     -- replace path traversal condition p of a pair (p, R) by the
                     -- predicate a /\ p, where a is the assertion at the beginning
                     -- of the path represented by (p, R);
                     Structures.CopyStructure (Heap, Assertion_Locn (Initial_Node), Assertion_Copy);
                     if Pairs.IsTrue (Heap, Current_Pair) then
                        Cells.Set_B_Ptr (Heap, Pairs.PairHead (Current_Pair), Assertion_Copy);
                     else
                        Current_Predicate := Cells.Get_B_Ptr (Heap, Pairs.PairHead (Current_Pair));
                        Pairs.FormConjunction (Heap, Assertion_Copy, Current_Predicate, Conjunction);
                        Cells.Set_B_Ptr (Heap, Pairs.PairHead (Current_Pair), Conjunction);
                     end if;

                     -- replace action part R of a pair (p, R) by weakest pre-
                     -- condition WP = q!R, where q is the assertion at the end of the
                     -- path represented by (p, R);
                     Structures.CopyStructure (Heap, Assertion_Locn (K), Assertion_Copy);

                     if Pairs.IsUnitAction (Heap, Current_Pair) then
                        Cells.Set_C_Ptr (Heap, Pairs.PairHead (Current_Pair), Assertion_Copy);
                     else
                        Pairs.CombinePredicateWithAction
                          (Heap        => Heap,
                           Action_R    => Cells.Get_C_Ptr (Heap, Pairs.PairHead (Current_Pair)),
                           Predicate_q => Assertion_Copy,
                           Result      => WP);

                        Cells.Set_C_Ptr (Heap, Pairs.PairHead (Current_Pair), WP);
                     end if;
                     Current_Pair := Labels.NextPair (Heap, Current_Pair);
                  end loop;
                  Matrix_Element := Cells.Get_A_Ptr (Heap, Matrix_Element);
               end loop;
            end if;
         end loop;

         -- Finally, if requested, print out the BPG with VCs on each arc.
         if CommandLineData.Content.Debug.VCG_All then
            Dump_Graph_Dot
              (Heap                    => Heap,
               Output_File_Name        => Output_File_Name,
               Output_File_Name_Suffix => Graph_Suffix,
               Scope                   => Scope,
               Print_Edges_As          => VCs);
         end if;

      end if;
      Gen_VC_Failure := Failure;
   end Gen_VCs;

   ------------------------------------------------------------------------

   procedure Print_VCs_Or_DPCs
     (Heap        : in out Cells.Heap_Record;
      Output_File : in     SPARK_IO.File_Type;
      Scope       : in     Dictionary.Scopes;
      Kind        : in     Valid_Dump_Kind)
   --# global in     Column;
   --#        in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     In_Degree;
   --#        in     Nmbr_Of_Stmts;
   --#        in     Proof_Context;
   --#        in     Refinement_Post_Check;
   --#        in     Refinement_Pre_Check;
   --#        in     Subclass_Post_Check;
   --#        in     Subclass_Pre_Check;
   --#        in     Text_Line_Nmbr;
   --#        in out Declarations.State;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Statistics.TableUsage;
   --# derives Declarations.State,
   --#         Heap,
   --#         LexTokenManager.State,
   --#         Statistics.TableUsage from *,
   --#                                    Column,
   --#                                    Declarations.State,
   --#                                    Dictionary.Dict,
   --#                                    Heap,
   --#                                    In_Degree,
   --#                                    Kind,
   --#                                    LexTokenManager.State,
   --#                                    Nmbr_Of_Stmts,
   --#                                    Proof_Context,
   --#                                    Refinement_Post_Check,
   --#                                    Refinement_Pre_Check,
   --#                                    Subclass_Post_Check,
   --#                                    Subclass_Pre_Check &
   --#         SPARK_IO.File_Sys     from *,
   --#                                    Column,
   --#                                    CommandLineData.Content,
   --#                                    Declarations.State,
   --#                                    Dictionary.Dict,
   --#                                    Heap,
   --#                                    In_Degree,
   --#                                    Kind,
   --#                                    LexTokenManager.State,
   --#                                    Nmbr_Of_Stmts,
   --#                                    Output_File,
   --#                                    Proof_Context,
   --#                                    Refinement_Post_Check,
   --#                                    Refinement_Pre_Check,
   --#                                    Scope,
   --#                                    Subclass_Post_Check,
   --#                                    Subclass_Pre_Check,
   --#                                    Text_Line_Nmbr;
   is
      Arc             : Cells.Cell;
      Arc_Label       : Labels.Label;
      Current_Pair    : Pairs.Pair;
      VC_Counter      : Natural;
      Arc_Found       : Boolean;
      Lex_String      : LexTokenManager.Lex_String;
      Sub_Prog_String : E_Strings.T;

      --------------------------------------------------------------
      procedure Print_Subprog_Prefix
      --# global in     Dictionary.Dict;
      --#        in     Output_File;
      --#        in     Scope;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Dictionary.Dict,
      --#                                Output_File,
      --#                                Scope;
      is
      begin
         if Dictionary.IsFunction (Dictionary.GetRegion (Scope)) then
            SPARK_IO.Put_String (File => Output_File,
                                 Item => "function_",
                                 Stop => 0);
         elsif Dictionary.IsProcedure (Dictionary.GetRegion (Scope)) then
            SPARK_IO.Put_String (File => Output_File,
                                 Item => "procedure_",
                                 Stop => 0);
         elsif Dictionary.IsTaskType (Dictionary.GetRegion (Scope)) then
            SPARK_IO.Put_String (File => Output_File,
                                 Item => "task_type_",
                                 Stop => 0);
         end if;
      end Print_Subprog_Prefix;

      -------------------------------------------------------------

      procedure Print_Refinement_Checks (Heap    : in out Cells.Heap_Record;
                                         Counter : in     Natural)
      --# global in     CommandLineData.Content;
      --#        in     Dictionary.Dict;
      --#        in     Output_File;
      --#        in     Refinement_Post_Check;
      --#        in     Refinement_Pre_Check;
      --#        in     Scope;
      --#        in     Subclass_Post_Check;
      --#        in     Subclass_Pre_Check;
      --#        in     Sub_Prog_String;
      --#        in out Declarations.State;
      --#        in out LexTokenManager.State;
      --#        in out SPARK_IO.File_Sys;
      --#        in out Statistics.TableUsage;
      --# derives Declarations.State,
      --#         Heap,
      --#         Statistics.TableUsage from *,
      --#                                    Counter,
      --#                                    Declarations.State,
      --#                                    Dictionary.Dict,
      --#                                    Heap,
      --#                                    LexTokenManager.State,
      --#                                    Refinement_Post_Check,
      --#                                    Refinement_Pre_Check,
      --#                                    Subclass_Post_Check,
      --#                                    Subclass_Pre_Check &
      --#         LexTokenManager.State from *,
      --#                                    Counter,
      --#                                    Refinement_Post_Check,
      --#                                    Refinement_Pre_Check,
      --#                                    Subclass_Post_Check,
      --#                                    Subclass_Pre_Check &
      --#         SPARK_IO.File_Sys     from *,
      --#                                    CommandLineData.Content,
      --#                                    Counter,
      --#                                    Declarations.State,
      --#                                    Dictionary.Dict,
      --#                                    Heap,
      --#                                    LexTokenManager.State,
      --#                                    Output_File,
      --#                                    Refinement_Post_Check,
      --#                                    Refinement_Pre_Check,
      --#                                    Scope,
      --#                                    Subclass_Post_Check,
      --#                                    Subclass_Pre_Check,
      --#                                    Sub_Prog_String;
      is
         Counter_Local : Natural;
         Lex_String    : LexTokenManager.Lex_String;
      begin
         Counter_Local := Counter;
         if not (Cells.Is_Null_Cell (Refinement_Pre_Check) and then Cells.Is_Null_Cell (Refinement_Post_Check)) then
            -- refinement VCs are needed
            SPARK_IO.Put_Line (File => Output_File,
                               Item => "For checks of refinement integrity: ",
                               Stop => 0);
            SPARK_IO.New_Line (File    => Output_File,
                               Spacing => 1);

            -- mark VC with unique hash code
            --            IO_Routines.HashVCFormula (Heap,
            --                                       Output_File,
            --                                       Pairs.CellToPair (Refinement_Pre_Check),
            --                                       Scope);

            Print_Subprog_Prefix;
            E_Strings.Put_String (File  => Output_File,
                                  E_Str => Sub_Prog_String);
            SPARK_IO.Put_Char (File => Output_File,
                               Item => '_');
            LexTokenManager.Insert_Nat (N       => Counter_Local,
                                        Lex_Str => Lex_String);
            E_Strings.Put_String (File  => Output_File,
                                  E_Str => LexTokenManager.Lex_String_To_String (Lex_Str => Lex_String));
            SPARK_IO.Put_Line (File => Output_File,
                               Item => ".",
                               Stop => 0);

            DAG_IO.PrintVCFormula (Heap, Output_File, Pairs.CellToPair (Refinement_Pre_Check), Scope, DAG_IO.Default_Wrap_Limit);
            Declarations.FindVCFormulaDeclarations (Heap, Pairs.CellToPair (Refinement_Pre_Check), True);

            SPARK_IO.New_Line (File    => Output_File,
                               Spacing => 1);

            if not (Cells.Is_Null_Cell (Refinement_Post_Check)) then
               Counter_Local := Counter_Local + 1;

               -- mark VC with unique hash code
               --               IO_Routines.HashVCFormula (Heap,
               --                                          Output_File,
               --                                          Pairs.CellToPair (Refinement_Post_Check),
               --                                          Scope);

               Print_Subprog_Prefix;
               E_Strings.Put_String (File  => Output_File,
                                     E_Str => Sub_Prog_String);
               SPARK_IO.Put_Char (File => Output_File,
                                  Item => '_');
               LexTokenManager.Insert_Nat (N       => Counter_Local,
                                           Lex_Str => Lex_String);
               E_Strings.Put_String (File  => Output_File,
                                     E_Str => LexTokenManager.Lex_String_To_String (Lex_Str => Lex_String));
               SPARK_IO.Put_Line (File => Output_File,
                                  Item => ".",
                                  Stop => 0);

               DAG_IO.PrintVCFormula
                 (Heap,
                  Output_File,
                  Pairs.CellToPair (Refinement_Post_Check),
                  Scope,
                  DAG_IO.Default_Wrap_Limit);
               Declarations.FindVCFormulaDeclarations (Heap, Pairs.CellToPair (Refinement_Post_Check), True);

               SPARK_IO.New_Line (File    => Output_File,
                                  Spacing => 1);
               Counter_Local := Counter_Local + 1; -- for the benefit of subclass check that follows
            end if;
         end if;

         -- do subclass refinements checksre if needed
         if not (Cells.Is_Null_Cell (Subclass_Pre_Check) and then Cells.Is_Null_Cell (Subclass_Post_Check)) then
            SPARK_IO.Put_Line (File => Output_File,
                               Item => "For checks of subclass inheritance integrity: ",
                               Stop => 0);
            SPARK_IO.New_Line (File    => Output_File,
                               Spacing => 1);

            -- mark VC with unique hash code
            --            IO_Routines.HashVCFormula (Heap,
            --                                       Output_File,
            --                                       Pairs.CellToPair (Subclass_Pre_Check),
            --                                       Scope);

            Print_Subprog_Prefix;
            E_Strings.Put_String (File  => Output_File,
                                  E_Str => Sub_Prog_String);
            SPARK_IO.Put_Char (File => Output_File,
                               Item => '_');
            LexTokenManager.Insert_Nat (N       => Counter_Local,
                                        Lex_Str => Lex_String);
            E_Strings.Put_String (File  => Output_File,
                                  E_Str => LexTokenManager.Lex_String_To_String (Lex_Str => Lex_String));
            SPARK_IO.Put_Line (File => Output_File,
                               Item => ".",
                               Stop => 0);

            DAG_IO.PrintVCFormula (Heap, Output_File, Pairs.CellToPair (Subclass_Pre_Check), Scope, DAG_IO.Default_Wrap_Limit);
            Declarations.FindVCFormulaDeclarations (Heap, Pairs.CellToPair (Subclass_Pre_Check), True);

            SPARK_IO.New_Line (File    => Output_File,
                               Spacing => 1);

            if not Cells.Is_Null_Cell (Subclass_Post_Check) then
               -- mark VC with unique hash code
               --               IO_Routines.HashVCFormula (Heap,
               --                                          Output_File,
               --                                          Pairs.CellToPair (Subclass_Post_Check),
               --                                          Scope);

               Counter_Local := Counter_Local + 1;
               Print_Subprog_Prefix;
               E_Strings.Put_String (File  => Output_File,
                                     E_Str => Sub_Prog_String);
               SPARK_IO.Put_Char (File => Output_File,
                                  Item => '_');
               LexTokenManager.Insert_Nat (N       => Counter_Local,
                                           Lex_Str => Lex_String);
               E_Strings.Put_String (File  => Output_File,
                                     E_Str => LexTokenManager.Lex_String_To_String (Lex_Str => Lex_String));
               SPARK_IO.Put_Line (File => Output_File,
                                  Item => ".",
                                  Stop => 0);

               DAG_IO.PrintVCFormula (Heap, Output_File, Pairs.CellToPair (Subclass_Post_Check), Scope, DAG_IO.Default_Wrap_Limit);
               Declarations.FindVCFormulaDeclarations (Heap, Pairs.CellToPair (Subclass_Post_Check), True);

               SPARK_IO.New_Line (File    => Output_File,
                                  Spacing => 1);
            end if;
         end if;
      end Print_Refinement_Checks;

      -------------------------------------------------------------

   begin -- Print_VCs_Or_DPCs
      Sub_Prog_String :=
        E_Strings.Lower_Case
        (E_Str => LexTokenManager.Lex_String_To_String (Lex_Str => Dictionary.GetSimpleName (Dictionary.GetRegion (Scope))));
      SPARK_IO.New_Line (File    => Output_File,
                         Spacing => 2);
      VC_Counter := 0;
      for Node in Matrix_Index range 2 .. Nmbr_Of_Stmts loop

         if In_Degree (Node) > 0 then

            for Predec in Matrix_Index range 1 .. Nmbr_Of_Stmts - 1 loop
               Arc_Found := False;
               Arc       := Column (Node);
               while (not Arc_Found) and (not Cells.Is_Null_Cell (Arc)) loop
                  if Cells.Get_Natural_Value (Heap, Arc) = Predec then
                     Arc_Found := True;
                  else
                     Arc := Cells.Get_A_Ptr (Heap, Arc);
                  end if;
               end loop;
               if Arc_Found then
                  SPARK_IO.Put_String (File => Output_File,
                                       Item => "For path(s) from ",
                                       Stop => 0);
                  if Predec = 1 then
                     SPARK_IO.Put_String (File => Output_File,
                                          Item => "start",
                                          Stop => 0);
                  else
                     if Proof_Context (Predec) = Assertion then
                        SPARK_IO.Put_String (File => Output_File,
                                             Item => "assertion of line ",
                                             Stop => 0);
                     elsif Proof_Context (Predec) = Default_Assertion then
                        SPARK_IO.Put_String (File => Output_File,
                                             Item => "default assertion of line ",
                                             Stop => 0);
                     else -- error case, above two cover all legal cases
                        SPARK_IO.Put_String (File => Output_File,
                                             Item => "!!!unknown assertion of line ",
                                             Stop => 0);
                     end if;
                     SPARK_IO.Put_Integer (File  => Output_File,
                                           Item  => Text_Line_Nmbr (Predec),
                                           Width => 1,
                                           Base  => 10);
                  end if;
                  SPARK_IO.Put_String (File => Output_File,
                                       Item => " to ",
                                       Stop => 0);

                  --# accept F, 41, "Stable expression here OK";
                  case Proof_Context (Node) is
                     when Assertion =>
                        SPARK_IO.Put_String (File => Output_File,
                                             Item => "assertion of line ",
                                             Stop => 0);
                        SPARK_IO.Put_Integer (File  => Output_File,
                                              Item  => Text_Line_Nmbr (Node),
                                              Width => 1,
                                              Base  => 10);

                     when Default_Assertion =>
                        SPARK_IO.Put_String (File => Output_File,
                                             Item => "default assertion of line ",
                                             Stop => 0);
                        SPARK_IO.Put_Integer (File  => Output_File,
                                              Item  => Text_Line_Nmbr (Node),
                                              Width => 1,
                                              Base  => 10);

                     when Check_Statement =>
                        SPARK_IO.Put_String (File => Output_File,
                                             Item => "check associated with statement of line ",
                                             Stop => 0);
                        SPARK_IO.Put_Integer (File  => Output_File,
                                              Item  => Text_Line_Nmbr (Node),
                                              Width => 1,
                                              Base  => 10);

                     when Run_Time_Check =>
                        SPARK_IO.Put_String
                          (File => Output_File,
                           Item => "run-time check associated with statement of line ",
                           Stop => 0);
                        SPARK_IO.Put_Integer (File  => Output_File,
                                              Item  => Text_Line_Nmbr (Node),
                                              Width => 1,
                                              Base  => 10);

                     when Precon_Check =>
                        SPARK_IO.Put_String
                          (File => Output_File,
                           Item => "precondition check associated with statement of line ",
                           Stop => 0);
                        SPARK_IO.Put_Integer (File  => Output_File,
                                              Item  => Text_Line_Nmbr (Node),
                                              Width => 1,
                                              Base  => 10);

                     when Postcondition =>
                        SPARK_IO.Put_String (File => Output_File,
                                             Item => "finish",
                                             Stop => 0);

                     when Precondition | Unspecified =>
                        null;
                  end case;
                  --# end accept;

                  SPARK_IO.Put_Line (File => Output_File,
                                     Item => ":",
                                     Stop => 0);
                  SPARK_IO.New_Line (File    => Output_File,
                                     Spacing => 1);
                  Arc_Label    := Labels.CellToLabel (Cells.Get_B_Ptr (Heap, Arc));
                  Current_Pair := Labels.FirstPair (Heap, Arc_Label);

                  while not Pairs.IsNullPair (Current_Pair) loop
                     --                     IO_Routines.HashVCFormula (Heap,
                     --                                                Output_File,
                     --                                                Current_Pair,
                     --                                                Scope);
                     Print_Subprog_Prefix;
                     E_Strings.Put_String (File  => Output_File,
                                           E_Str => Sub_Prog_String);
                     SPARK_IO.Put_Char (File => Output_File,
                                        Item => '_');
                     VC_Counter := VC_Counter + 1;
                     LexTokenManager.Insert_Nat (N       => VC_Counter,
                                                 Lex_Str => Lex_String);
                     E_Strings.Put_String
                       (File  => Output_File,
                        E_Str => LexTokenManager.Lex_String_To_String (Lex_Str => Lex_String));
                     SPARK_IO.Put_Line (File => Output_File,
                                        Item => ".",
                                        Stop => 0);

                     --# accept F, 41, "Stable expression here expected and OK";
                     case Kind is
                        when VCs =>
                           DAG_IO.PrintVCFormula (Heap, Output_File, Current_Pair, Scope, DAG_IO.Default_Wrap_Limit);
                        when DPCs =>
                           case Proof_Context (Node) is

                              when Assertion | Default_Assertion | Postcondition =>

                                 DAG_IO.PrintDPC (Heap, Output_File, Current_Pair, Scope, DAG_IO.Default_Wrap_Limit);
                              when others =>
                                 SPARK_IO.Put_Line
                                   (File => Output_File,
                                    Item => "*** true .          /* DPC not required for intermediate check */",
                                    Stop => 0);
                                 SPARK_IO.New_Line (File    => Output_File,
                                                    Spacing => 1);
                           end case;
                     end case;
                     --# end accept;

                     -- Find the FDL declarations needed. If we're printing DPCs, then DON'T
                     -- ignore trivially True VCs, since we _will_ produce the hypotheses
                     -- list for these, so we do need FDL declarations for any entities therein.
                     Declarations.FindVCFormulaDeclarations
                       (Heap                   => Heap,
                        PredicatePair          => Current_Pair,
                        IgnoreTriviallyTrueVCs => (Kind = VCs));

                     Current_Pair := Labels.NextPair (Heap, Current_Pair);
                     SPARK_IO.New_Line (File    => Output_File,
                                        Spacing => 1);
                  end loop;
               end if;
            end loop;
         end if;
      end loop;

      case Kind is
         when VCs =>
            Print_Refinement_Checks (Heap    => Heap,
                                     Counter => VC_Counter + 1);
         when DPCs =>
            null;
      end case;

   end Print_VCs_Or_DPCs;

   procedure Dump_Graph_Table (Heap           : in out Cells.Heap_Record;
                               Scope          : in     Dictionary.Scopes;
                               Print_Edges_As : in     DOT_Dump_Kind)
   --# global in Assertion_Locn;
   --#        in Column;
   --#        in In_Degree;
   --#        in Nmbr_Of_Stmts;
   --#        in Out_Degree;
   --#        in Proof_Context;
   --#        in Refinement_Post_Check;
   --#        in Refinement_Pre_Check;
   --#        in Row;
   --#        in Subclass_Post_Check;
   --#        in Subclass_Pre_Check;
   --#        in Text_Line_Nmbr;
   --# derives Heap from * &
   --#         null from Assertion_Locn,
   --#                   Column,
   --#                   In_Degree,
   --#                   Nmbr_Of_Stmts,
   --#                   Out_Degree,
   --#                   Print_Edges_As,
   --#                   Proof_Context,
   --#                   Refinement_Post_Check,
   --#                   Refinement_Pre_Check,
   --#                   Row,
   --#                   Scope,
   --#                   Subclass_Post_Check,
   --#                   Subclass_Pre_Check,
   --#                   Text_Line_Nmbr;
   is
      --# hide Dump_Graph_Table;
      Arc          : Cells.Cell;
      Arc_Label    : Labels.Label;
      Current_Pair : Pairs.Pair;
      VC_Counter   : Natural;
      Arc_Found    : Boolean;
   begin
      Debug.PrintInt ("Number of Statements is: ", Integer (Nmbr_Of_Stmts));
      for I in Matrix_Index range 1 .. Nmbr_Of_Stmts loop
         if In_Degree (I) = 0 and Out_Degree (I) = 0 then
            Debug.PrintMsg ("Statement" & Integer'Image (I) & " not connected", True);
         else
            Debug.PrintInt ("Statement", I);
            Debug.PrintMsg ("   Proof Context    = " & Proof_Context_Type'Image (Proof_Context (I)), True);
            Debug.PrintInt ("   Text Line Number =", Text_Line_Nmbr (I));
            Debug.PrintInt ("   In Degree        =", Integer (In_Degree (I)));
            Debug.PrintInt ("   Out Degree       =", Integer (Out_Degree (I)));
            Debug.PrintDAG ("   Assertion Locn   = ", Assertion_Locn (I), Heap, Scope);
         end if;
      end loop;

      -- Now Dump each arc represented by each coefficient in the Matrix itself
      -- Basically the same algorithm as Print_VCs above.

      VC_Counter := 0;
      -- For all statements except the precondition
      for Node in Matrix_Index range 2 .. Nmbr_Of_Stmts loop
         -- If that node has predecessors
         if In_Degree (Node) > 0 then

            -- Then search the coefficients in the Matrix for all
            -- Predecessors whose Successor is Node.
            for Predec in Matrix_Index range 1 .. Nmbr_Of_Stmts - 1 loop
               Arc_Found := False;
               Arc       := Column (Node);
               while (not Arc_Found) and (not Cells.Is_Null_Cell (Arc)) loop
                  if Cells.Get_Natural_Value (Heap, Arc) = Predec then
                     Arc_Found := True;
                  else
                     Arc := Cells.Get_A_Ptr (Heap, Arc);
                  end if;
               end loop;

               if Arc_Found then
                  -- Found an arc from Statement Predec to Statement Node
                  Debug.PrintMsg ("Found an arc from Stm" & Integer'Image (Predec) & " to Stm" & Integer'Image (Node), True);

                  -- Fetch the Label associated with that arc
                  Arc_Label := Labels.CellToLabel (Cells.Get_B_Ptr (Heap, Arc));

                  case Print_Edges_As is
                     when PFs =>
                        DAG_IO.PrintLabel (Heap, SPARK_IO.Standard_Output, Arc_Label, Scope, DAG_IO.Default_Wrap_Limit);
                     when VCs =>
                        -- Fetch the first Pair attached to that Label
                        Current_Pair := Labels.FirstPair (Heap, Arc_Label);
                        while not Pairs.IsNullPair (Current_Pair) loop
                           VC_Counter := VC_Counter + 1;
                           Debug.PrintInt ("Pair", VC_Counter);
                           DAG_IO.PrintVCFormula (Heap, SPARK_IO.Standard_Output, Current_Pair, Scope, DAG_IO.Default_Wrap_Limit);
                           Current_Pair := Labels.NextPair (Heap, Current_Pair);
                        end loop;
                  end case;
               end if;
            end loop;
         end if;
      end loop;

   end Dump_Graph_Table;

begin

   -- This code matches that in Reinitialize_Graph

   --# accept F, 23, Row, "Initialization is total" &
   --#        F, 23, Column, "Initialization is total" &
   --#        F, 23, In_Degree, "Initialization is total" &
   --#        F, 23, Out_Degree, "Initialization is total" &
   --#        F, 23, Proof_Context, "Initialization is total" &
   --#        F, 23, Text_Line_Nmbr, "Initialization is total" &
   --#        F, 23, Assertion_Locn, "Initialization is total";
   for I in Matrix_Index loop
      Row (I)            := Cells.Null_Cell;
      Column (I)         := Cells.Null_Cell;
      In_Degree (I)      := 0;
      Out_Degree (I)     := 0;
      Proof_Context (I)  := Unspecified;
      Text_Line_Nmbr (I) := 0;
      Assertion_Locn (I) := Cells.Null_Cell;
   end loop;
   Nmbr_Of_Stmts         := 1;
   Refinement_Pre_Check  := Cells.Null_Cell;
   Refinement_Post_Check := Cells.Null_Cell;
   Subclass_Pre_Check    := Cells.Null_Cell;
   Subclass_Post_Check   := Cells.Null_Cell;

   --# accept F, 602, Row, Row, "Initialization is total" &
   --#        F, 602, Column, Column, "Initialization is total" &
   --#        F, 602, In_Degree, In_Degree, "Initialization is total" &
   --#        F, 602, Out_Degree, Out_Degree, "Initialization is total" &
   --#        F, 602, Proof_Context, Proof_Context, "Initialization is total" &
   --#        F, 602, Text_Line_Nmbr, Text_Line_Nmbr, "Initialization is total" &
   --#        F, 602, Assertion_Locn, Assertion_Locn, "Initialization is total";
end Graph;