File: dictionary.ads

package info (click to toggle)
spark 2012.0.deb-9
links: PTS, VCS
area: main
in suites: jessie, jessie-kfreebsd
size: 29,260 kB
ctags: 3,098
sloc: ada: 186,243; cpp: 13,497; makefile: 685; yacc: 440; lex: 176; ansic: 119; sh: 16
file content (4636 lines) | stat: -rw-r--r-- 188,299 bytes
parent folder | download | duplicates (2)
-------------------------------------------------------------------------------
-- (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 ContextManager;
with ExaminerConstants;
with E_Strings;
with LexTokenManager;
with SPARK_IO;
with SP_Symbols;

use type ContextManager.UnitDescriptors;
use type ExaminerConstants.RefType;
use type LexTokenManager.Str_Comp_Result;
use type SPARK_IO.File_Status;
use type SP_Symbols.SP_Symbol;

--# inherit CommandLineData,
--#         CommandLineHandler,
--#         ContextManager,
--#         ExaminerConstants,
--#         E_Strings,
--#         FileSystem,
--#         LexTokenManager,
--#         LexTokenStacks,
--#         Maths,
--#         ScreenEcho,
--#         SPARK_IO,
--#         SP_Symbols,
--#         Statistics,
--#         SystemErrors,
--#         XMLReport;

package Dictionary
--# own Dict : Dictionaries;
is

   --------------------------------------------------------------------------------
   --                             TYPE DEFINITIONS                               --
   --------------------------------------------------------------------------------

   type Symbol is private;
   NullSymbol : constant Symbol;

   type Iterator is private;
   NullIterator : constant Iterator;

   type Location is record
      Start_Position : LexTokenManager.Token_Position;
      End_Position   : LexTokenManager.Token_Position;
   end record;

   Null_Location : constant Location :=
     Location'(Start_Position => LexTokenManager.Null_Token_Position,
               End_Position   => LexTokenManager.Null_Token_Position);

   type Scopes is private;
   -- following constant is not valid for use other than as a placeholder for constructing a
   -- an aggregate that needs a Scope in it (e.g. EmptyNumericError in Error_Types)
   NullScope : constant Scopes;

   -- conversion routines to and from scope follow in access function section

   type Contexts is (ProofContext, ProgramContext);

   type Modes is (DefaultMode, InMode, OutMode, InOutMode, InvalidMode);

   type Abstractions is (IsAbstract, IsRefined);

   type PrefixSort is (AType, ABaseType, AnObject);

   type PackageSort is (Public, PrivateChild);

   type RavenscarPragmas is (Priority, InterruptPriority, AttachHandler);
   subtype RavenscarPragmasWithValue is RavenscarPragmas range Priority .. InterruptPriority;

   type Generic_Kind is (Generic_Of_Subprogram, Generic_Of_Package);

   type Generic_Parameter_Kind is (Generic_Type_Parameter, Generic_Object_Parameter);

   type SLI_Type is (
                     SLI_Array_Object,
                     SLI_Array_Type,
                     SLI_Boolean_Object,
                     SLI_Boolean_Type,
                     SLI_Enumeration_Object,
                     SLI_Enumeration_Type,
                     SLI_Floating_Point_Object,
                     SLI_Floating_Point_Type,
                     SLI_Abstract_Type,
                     SLI_Signed_Integer_Object,
                     SLI_Signed_Integer_Type,
                     SLI_Generic_Package_Type,
                     SLI_Package_Type,
                     SLI_Label_On_Loop,
                     SLI_Modular_Integer_Object,
                     SLI_Modular_Integer_Type,
                     SLI_Enumeration_Literal,
                     SLI_Named_Number,
                     SLI_Fixed_Point_Object,
                     SLI_Fixed_Point_Type,
                     SLI_Record_Object,
                     SLI_Record_Type,
                     SLI_String_Object,
                     SLI_String_Type,
                     SLI_Task_Object,
                     SLI_Task_Type,
                     SLI_Generic_Procedure_Type,
                     SLI_Procedure_Type,
                     SLI_Generic_Function_Op,
                     SLI_Function_Op,
                     SLI_Protected_Object,
                     SLI_Protected_Type,
                     SLI_Entry_Family,
                     SLI_Generic_Formal_Parameter,
                     SLI_Unknown_Type);

   -- The generation of replacement rules for composite constants is governed
   -- by an object_assertion annotation.  This can either explicitly request
   -- that a rule be generated, request that NO rule be generated, or can be
   -- left unspecified.  The action of the Examiner for these cases also depends
   -- on the setting of the /rules=XXX command-line switch declared in
   -- commandlinedata.ads
   type Rule_Policies is (Unspecified, Rule_Requested, No_Rule_Requested);

   type Visibility is (Visible, Privat, Local);

   function Is_Null_Symbol (TheSymbol : Symbol) return Boolean;
   --# return TheSymbol = NullSymbol;

   function IsDeclaration (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsEnumerationLiteral (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsArrayIndex (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsSubcomponent (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsTypeMark (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsConstant (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsVariable (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsGlobalVariable (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsQuantifiedVariable (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsImplicitReturnVariable (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsImplicitInStream (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsRulePolicy (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsParameterConstraint (TheSymbol : Symbol) return Boolean;
   --# global in Dict;
   -- A subprgoram parameter constraint is a special symbol associated with unconstrained formal parameters

   function IsSubprogramParameter (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsSubprogram (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsOperator (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsDependency (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsPackage (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsGenericParameterSymbol (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsKnownDiscriminant (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsLoop (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsImplicitProofFunction (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsLoopParameter (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   --------------------------------------------------------------------------------
   -- Null Test and Equality of Symbols                                          --
   --                                                                            --
   -- If you know two Symbols are of the same kind (e.g. both denote a package,  --
   -- a type, and so on), then equality should be tested using the strongly-     --
   -- typed functions below.                                                     --
   --                                                                            --
   -- General equality between two Symbols is available using the predefined     --
   -- "=" operator.                                                              --
   --------------------------------------------------------------------------------

   -- This function replaces the "=" function between 2 symbols but
   -- works only between 2 Enumeration_Literals or Null Symbols. If one of the arguments
   -- is not an Enumeration_Literal, the function terminates the Examiner.
   function Enumeration_Literals_Are_Equal (Left_Symbol, Right_Symbol : Symbol) return Boolean;
   --# global in Dict;
   --# return Left_Symbol = Right_Symbol;

   -- This function replaces the "=" function between 2 symbols but
   -- works only between 2 Record_Components or Null Symbols. If one of the arguments
   -- is not an Record_Component, the function terminates the Examiner.
   function Record_Components_Are_Equal (Left_Symbol, Right_Symbol : Symbol) return Boolean;
   --# global in Dict;
   --# return Left_Symbol = Right_Symbol;

   -- This function replaces the "=" function between 2 symbols but
   -- works only between 2 Types or Null Symbols. If one of the arguments
   -- is not a Type, the function terminates the Examiner.
   function Types_Are_Equal (Left_Symbol, Right_Symbol : Symbol;
                             Full_Range_Subtype        : Boolean) return Boolean;
   --# global in Dict;
   --# return R => (not Full_Range_Subtype -> R = (Left_Symbol = Right_Symbol));

   -- This function replaces the "=" function between 2 symbols but
   -- works only between 2 Variables or Null Symbols. If one of the arguments
   -- is not a Variable, the function terminates the Examiner.
   function Variables_Are_Equal (Left_Symbol, Right_Symbol : Symbol) return Boolean;
   --# global in Dict;
   --# return Left_Symbol = Right_Symbol;

   -- This function replaces the "=" function between 2 symbols but
   -- works only between 2 Implicit_Return_Variables or Null Symbols. If one of the arguments
   -- is not a Implicit_Return_Variable, the function terminates the Examiner.
   function Implicit_Return_Variables_Are_Equal (Left_Symbol, Right_Symbol : Symbol) return Boolean;
   --# global in Dict;
   --# return Left_Symbol = Right_Symbol;

   -- This function replaces the "=" function between 2 symbols but
   -- works only between 2 Subprograms or Null Symbols. If one of the arguments
   -- is not a Subprogram, the function terminates the Examiner.
   function Subprograms_Are_Equal (Left_Symbol, Right_Symbol : Symbol) return Boolean;
   --# global in Dict;
   --# return Left_Symbol = Right_Symbol;

   -- This function replaces the "=" function between 2 symbols but
   -- works only between 2 Packages or Null Symbols. If one of the arguments
   -- is not a Package, the function terminates the Examiner.
   function Packages_Are_Equal (Left_Symbol, Right_Symbol : Symbol) return Boolean;
   --# global in Dict;
   --# return Left_Symbol = Right_Symbol;

   --------------------------------------------------------------------------------
   --                               HOUSEKEEPING                                 --
   --------------------------------------------------------------------------------

   procedure Initialize (Write_To_File : in Boolean);
   --# global in     CommandLineData.Content;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --#           out Dict;
   --# derives Dict,
   --#         SPARK_IO.File_Sys     from CommandLineData.Content,
   --#                                    LexTokenManager.State,
   --#                                    SPARK_IO.File_Sys,
   --#                                    Write_To_File &
   --#         LexTokenManager.State from *,
   --#                                    CommandLineData.Content;

   procedure Set_Current_File_Name (File_Name : in E_Strings.T);
   --# global in     CommandLineData.Content;
   --#        in out Dict;
   --# derives Dict from *,
   --#                   CommandLineData.Content,
   --#                   File_Name;

   function GetOwnVariableOrConstituentMode (Variable : Symbol) return Modes;
   --# global in Dict;

   procedure Write (File_Name : in     E_Strings.T;
                    Status    :    out SPARK_IO.File_Status);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                File_Name,
   --#                                SPARK_IO.File_Sys &
   --#         SPARK_IO.File_Sys,
   --#         Status            from Dict,
   --#                                File_Name,
   --#                                LexTokenManager.State,
   --#                                SPARK_IO.File_Sys;

   procedure Add_Generic_Unit
     (Kind         : in     Generic_Kind;
      Scope        : in     Scopes;
      Comp_Unit    : in     ContextManager.UnitDescriptors;
      Declaration  : in     Location;
      Generic_Unit :    out Symbol);
   --# global in out Dict;
   --# derives Dict,
   --#         Generic_Unit from Comp_Unit,
   --#                           Declaration,
   --#                           Dict,
   --#                           Kind,
   --#                           Scope;

   procedure ReportUsage;
   --# global in     Dict;
   --#        in out Statistics.TableUsage;
   --# derives Statistics.TableUsage from *,
   --#                                    Dict;

   procedure Read_Target_Data_File;
   --# global in     CommandLineData.Content;
   --#        in out Dict;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         LexTokenManager.State,
   --#         SPARK_IO.File_Sys     from *,
   --#                                    CommandLineData.Content,
   --#                                    LexTokenManager.State,
   --#                                    SPARK_IO.File_Sys;

   procedure Output_Target_Data_File (To_File : in SPARK_IO.File_Type);
   --# global in     CommandLineData.Content;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out XMLReport.State;
   --# derives LexTokenManager.State,
   --#         SPARK_IO.File_Sys,
   --#         XMLReport.State       from CommandLineData.Content,
   --#                                    LexTokenManager.State,
   --#                                    SPARK_IO.File_Sys,
   --#                                    To_File,
   --#                                    XMLReport.State;

   --------------------------------------------------------------------------------
   --                                SYMBOLS and ORDERING                        --
   --------------------------------------------------------------------------------

   function Declared_Before (Left, Right : in Symbol) return Boolean;

   --------------------------------------------------------------------------------
   --                              LOOKUP ROUTINES                               --
   --------------------------------------------------------------------------------

   function GlobalScope return Scopes;
   --# global in Dict;

   function Set_Visibility (The_Visibility : Visibility;
                            The_Unit       : Symbol) return Scopes;

   function Get_Visibility (Scope : Scopes) return Visibility;

   function IsLibraryLevel (Scope : Scopes) return Boolean;
   --# global in Dict;

   function IsPredefinedScope (Scope : Scopes) return Boolean;
   --# global in Dict;

   function IsGlobalScope (Scope : Scopes) return Boolean;
   --# global in Dict;

   function GetRegion (Scope : Scopes) return Symbol;

   function IsLocal (Inner, Outer : Scopes) return Boolean;
   --# global in Dict;

   function GetContext (TheSymbol : Symbol) return Contexts;
   --# global in Dict;

   function GetRootPackage (ThePackage : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsPackage (S, Dict));

   function GetLibraryPackage (Scope : Scopes) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsPackage (S, Dict));

   function IsPrivatePackage (ThePackage : Symbol) return Boolean;
   --# global in Dict;

   function GetPackageParent (ThePackage : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsPackage (S, Dict));

   function PackageDeclaresTaggedType (ThePackage : Symbol) return Boolean;
   --# global in Dict;

   function PackageExtendsAnotherPackage (ThePackage : Symbol) return Boolean;
   --# global in Dict;

   function GetPackageThatIsExtended (ThePackage : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsPackage (S, Dict));

   -- Package ownership is a relationship defined as follows:
   -- The owner of a package (if any) is defined to be the
   -- the parent of its closest private ancestor, where the term ancestor is
   -- as defined 10.1.1(11) of the Ada 95 LRM [2], to include the package itself.
   -- As a consequence of this rule only a private package or its private
   -- or public descendents can have an owner.
   -- This definition is given in S.P0468.42.8 section 2.3.3.6 and
   -- a consequntial rule given in the SPARK LRM section 7.1.1.
   function GetPackageOwner (ThePackage : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsPackage (S, Dict));

   function IsProperDescendent (Inner, Outer : Symbol) return Boolean;
   --# global in Dict;

   function IsPrivateDescendent (Inner, Outer : Symbol) return Boolean;
   --# global in Dict;

   function IsDescendentOfPrivateSibling (Candidate, ThePackage : Symbol) return Boolean;
   --# global in Dict;

   function IsDirectlyDefined
     (Name    : LexTokenManager.Lex_String;
      Scope   : Scopes;
      Context : Contexts)
     return    Boolean;
   --# global in Dict;
   --#        in LexTokenManager.State;

   function IsDefined
     (Name              : LexTokenManager.Lex_String;
      Scope             : Scopes;
      Context           : Contexts;
      Full_Package_Name : Boolean)
     return              Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;
   --#        in LexTokenManager.State;

   function UnaryOperatorIsDefined (Name    : SP_Symbols.SP_Symbol;
                                    Operand : Symbol) return Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;

   function Get_Binary_Operator_Type
     (Name  : SP_Symbols.SP_Symbol;
      Left  : Symbol;
      Right : Symbol)
     return  Symbol;
   --# global in CommandLineData.Content;
   --#        in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function UnaryOperatorIsVisible
     (Name    : SP_Symbols.SP_Symbol;
      Operand : Symbol;
      Scope   : Scopes)
     return    Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;

   function BinaryOperatorIsVisible
     (Name  : SP_Symbols.SP_Symbol;
      Left  : Symbol;
      Right : Symbol;
      Scope : Scopes)
     return  Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;

   function AttributeIsVisible
     (Name     : LexTokenManager.Lex_String;
      Prefix   : PrefixSort;
      TypeMark : Symbol;
      Scope    : Scopes)
     return     Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;
   --#        in LexTokenManager.State;

   function Attribute_Is_Visible_But_Obsolete
     (Name     : LexTokenManager.Lex_String;
      Prefix   : PrefixSort;
      TypeMark : Symbol;
      Scope    : Scopes)
     return     Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;
   --#        in LexTokenManager.State;

   function PrefixAllowed (Prefix : Symbol;
                           Scope  : Scopes) return Boolean;
   --# global in Dict;

   function PrefixRequired (Item  : Symbol;
                            Scope : Scopes) return Boolean;
   --# global in Dict;

   function GetPrefix (Item : Symbol) return LexTokenManager.Lex_String;
   --# global in Dict;

   function LookupImmediateScope
     (Name    : LexTokenManager.Lex_String;
      Scope   : Scopes;
      Context : Contexts)
     return    Symbol;
   --# global in Dict;
   --#        in LexTokenManager.State;

   function LookupItem
     (Name              : LexTokenManager.Lex_String;
      Scope             : Scopes;
      Context           : Contexts;
      Full_Package_Name : Boolean)
     return              Symbol;
   --# global in CommandLineData.Content;
   --#        in Dict;
   --#        in LexTokenManager.State;

   function LookupSelectedItem
     (Prefix   : Symbol;
      Selector : LexTokenManager.Lex_String;
      Scope    : Scopes;
      Context  : Contexts)
     return     Symbol;
   --# global in CommandLineData.Content;
   --#        in Dict;
   --#        in LexTokenManager.State;

   function Is_Subprogram (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   -- starting in Scope look for operations inherited as a result of use of
   -- tagged and extended tagged types.  Returns NullSymbol if no match found.
   -- ActualTaggedType is set (on successful return) to the type of the tagged parameter
   -- required in the calling environment.
   procedure SearchForInheritedOperations
     (Name             : in     LexTokenManager.Lex_String;
      Scope            : in     Scopes;
      Prefix           : in     Symbol;
      Context          : in     Contexts;
      OpSym            :    out Symbol;
      ActualTaggedType :    out Symbol);
   --# global in CommandLineData.Content;
   --#        in Dict;
   --#        in LexTokenManager.State;
   --# derives ActualTaggedType,
   --#         OpSym            from CommandLineData.Content,
   --#                               Context,
   --#                               Dict,
   --#                               LexTokenManager.State,
   --#                               Name,
   --#                               Prefix,
   --#                               Scope;
   --# post (Is_Null_Symbol (OpSym) or Is_Subprogram (OpSym, Dict)) and
   --#   (Is_Null_Symbol (ActualTaggedType) or IsTypeMark (ActualTaggedType, Dict));

   function GetSubprogramControllingType (Subprogram : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));
   -- returns null symbol if the subprogram does not have a controlling type (i.e. a parameter of a tagged
   -- type which is declared in the same package as the subprogram)

   function GetOverriddenSubprogram (Subprogram : Symbol) return Symbol;
   --# global in Dict;
   --#        in LexTokenManager.State;

   function IsCallable
     (Subprogram   : Symbol;
      PrefixNeeded : Boolean;
      Scope        : Scopes)
     return         Boolean;
   --# global in Dict;

   function GenerateSimpleName (Item      : Symbol;
                                Separator : String) return E_Strings.T;
   --# global in Dict;
   --#        in LexTokenManager.State;

   function GetAnyPrefixNeeded
     (Sym       : Symbol;
      Scope     : Scopes;
      Separator : String)
     return      E_Strings.T;
   --# global in CommandLineData.Content;
   --#        in Dict;
   --#        in LexTokenManager.State;

   function IsValidGenericTypeAssociation (Formal, Actual : Symbol;
                                           Scope          : Scopes) return Boolean;
   --# global in Dict;

   function Get_Symbol_Compilation_Unit (Item : Symbol) return ContextManager.UnitDescriptors;
   --# global in Dict;

   function Get_Symbol_Location (Item : Symbol) return LexTokenManager.Token_Position;
   --# global in Dict;

   --  This procedure returns RESULT containing the SLI type
   --  associated with the symbol ITEM.
   procedure Get_SLI_Type (Item   : in     Symbol;
                           Result :    out SLI_Type);
   --# global in     CommandLineData.Content;
   --#        in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives Result            from Dict,
   --#                                Item &
   --#         SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Dict,
   --#                                Item,
   --#                                LexTokenManager.State;

   --------------------------------------------------------------------------------
   --                               CONSTRUCTORS                                 --
   --------------------------------------------------------------------------------

   procedure Add_Deferred_Constant
     (Name           : in     LexTokenManager.Lex_String;
      Type_Mark      : in     Symbol;
      Type_Reference : in     Location;
      Comp_Unit      : in     ContextManager.UnitDescriptors;
      Declaration    : in     Location;
      The_Package    : in     Symbol;
      TheConstant    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         TheConstant       from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Name,
   --#                                The_Package,
   --#                                Type_Mark &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                The_Package,
   --#                                Type_Mark,
   --#                                Type_Reference;
   --# post IsConstant (TheConstant, Dict);

   procedure Promote_Deferred_To_Full_Constant
     (Constant_Sym : in Symbol;
      Comp_Unit    : in ContextManager.UnitDescriptors;
      Declaration  : in Location;
      Value        : in LexTokenManager.Lex_String;
      Exp_Node     : in ExaminerConstants.RefType;
      The_Package  : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Comp_Unit,
   --#                   Constant_Sym,
   --#                   Declaration,
   --#                   Exp_Node,
   --#                   The_Package,
   --#                   Value;

   procedure Add_Constant
     (Name              : in     LexTokenManager.Lex_String;
      The_Type          : in     Symbol;
      Static            : in     Boolean;
      Comp_Unit         : in     ContextManager.UnitDescriptors;
      Declaration       : in     Location;
      Value             : in     LexTokenManager.Lex_String;
      Exp_Is_Wellformed : in     Boolean;
      Exp_Node          : in     ExaminerConstants.RefType;
      Constant_Sym      : in out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Constant_Sym,
   --#         Dict              from Comp_Unit,
   --#                                Constant_Sym,
   --#                                Declaration,
   --#                                Dict,
   --#                                Exp_Is_Wellformed,
   --#                                Exp_Node,
   --#                                Name,
   --#                                Static,
   --#                                The_Type,
   --#                                Value &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Constant_Sym,
   --#                                Declaration,
   --#                                Dict,
   --#                                Exp_Is_Wellformed,
   --#                                Exp_Node,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Static,
   --#                                The_Type,
   --#                                Value;
   --# post IsConstant (Constant_Sym, Dict);

   procedure Add_Constant_Declaration
     (Name              : in     LexTokenManager.Lex_String;
      Type_Mark         : in     Symbol;
      Type_Reference    : in     Location;
      Value             : in     LexTokenManager.Lex_String;
      Exp_Is_Wellformed : in     Boolean;
      Exp_Node          : in     ExaminerConstants.RefType;
      Static            : in     Boolean;
      Comp_Unit         : in     ContextManager.UnitDescriptors;
      Declaration       : in     Location;
      Scope             : in     Scopes;
      Context           : in     Contexts;
      TheConstant       :    out Symbol);
   --# global in     CommandLineData.Content;
   --#        in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         TheConstant       from CommandLineData.Content,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                Exp_Is_Wellformed,
   --#                                Exp_Node,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Static,
   --#                                Type_Mark,
   --#                                Value &
   --#         SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                Exp_Is_Wellformed,
   --#                                Exp_Node,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Static,
   --#                                Type_Mark,
   --#                                Type_Reference,
   --#                                Value;
   --# post IsConstant (TheConstant, Dict);

   procedure AddConstantRulePolicy
     (TheConstant   : in     Symbol;
      Comp_Unit     : in     ContextManager.UnitDescriptors;
      Declaration   : in     Location;
      TheScope      : in     Scopes;
      ThePolicy     : in     Rule_Policies;
      TheRulePolicy :    out Symbol);
   --# global in out Dict;
   --# derives Dict,
   --#         TheRulePolicy from Comp_Unit,
   --#                            Declaration,
   --#                            Dict,
   --#                            TheConstant,
   --#                            ThePolicy,
   --#                            TheScope;
   --# post IsRulePolicy (TheRulePolicy, Dict);

   procedure Add_Variable_Declaration
     (Variable_Sym       : in     Symbol;
      The_Type           : in     Symbol;
      Initialized        : in     Boolean;
      Is_Aliased         : in     Boolean;
      Exp_Node           : in     ExaminerConstants.RefType;
      Type_Reference     : in     Location;
      Comp_Unit          : in     ContextManager.UnitDescriptors;
      Declaration        : in     Location;
      Scope              : in     Scopes;
      Declaration_Symbol :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Declaration_Symbol,
   --#         Dict               from Comp_Unit,
   --#                                 Declaration,
   --#                                 Dict,
   --#                                 Exp_Node,
   --#                                 Initialized,
   --#                                 Is_Aliased,
   --#                                 Scope,
   --#                                 The_Type,
   --#                                 Variable_Sym &
   --#         SPARK_IO.File_Sys  from *,
   --#                                 Comp_Unit,
   --#                                 Declaration,
   --#                                 Dict,
   --#                                 Exp_Node,
   --#                                 Initialized,
   --#                                 Is_Aliased,
   --#                                 LexTokenManager.State,
   --#                                 Scope,
   --#                                 The_Type,
   --#                                 Type_Reference,
   --#                                 Variable_Sym;
   --# pre not Is_Null_Symbol (Variable_Sym);
   --# post IsDeclaration (Declaration_Symbol, Dict);

   -- This procedure may also be called to modify an existing
   --  variable.
   procedure Add_Variable
     (Name               : in     LexTokenManager.Lex_String;
      The_Type           : in     Symbol;
      Initialized        : in     Boolean;
      Is_Aliased         : in     Boolean;
      Exp_Node           : in     ExaminerConstants.RefType;
      Type_Reference     : in     Location;
      Comp_Unit          : in     ContextManager.UnitDescriptors;
      Declaration        : in     Location;
      Scope              : in     Scopes;
      Declaration_Symbol :    out Symbol;
      Variable_Symbol    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Declaration_Symbol,
   --#         Dict,
   --#         Variable_Symbol    from Comp_Unit,
   --#                                 Declaration,
   --#                                 Dict,
   --#                                 Exp_Node,
   --#                                 Initialized,
   --#                                 Is_Aliased,
   --#                                 Name,
   --#                                 Scope,
   --#                                 The_Type &
   --#         SPARK_IO.File_Sys  from *,
   --#                                 Comp_Unit,
   --#                                 Declaration,
   --#                                 Dict,
   --#                                 Exp_Node,
   --#                                 Initialized,
   --#                                 Is_Aliased,
   --#                                 LexTokenManager.State,
   --#                                 Name,
   --#                                 Scope,
   --#                                 The_Type,
   --#                                 Type_Reference;
   --# post IsDeclaration (Declaration_Symbol, Dict) and IsVariable (Variable_Symbol, Dict);

   procedure AddVariableAddressClause (Variable : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Variable;
   -- could also be extended to write location to dictionary file as for other reps

   procedure AddVariablePragmaImport (Variable : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Variable;
   -- could also be extended to write location to dictionary file as for other reps

   procedure AddTypeSizeAttribute (TypeMark : in Symbol;
                                   SizeVal  : in LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   SizeVal,
   --#                   TypeMark;

   procedure SetTypeAtomic (TypeMark : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TypeMark;

   procedure AddRecordSubcomponent
     (Prefix       : in     Symbol;
      Component    : in     Symbol;
      Comp_Unit    : in     ContextManager.UnitDescriptors;
      Subcomponent :    out Symbol);
   --# global in out Dict;
   --# derives Dict,
   --#         Subcomponent from Component,
   --#                           Comp_Unit,
   --#                           Dict,
   --#                           Prefix;
   --# post IsSubcomponent (Subcomponent, Dict);

   procedure AddQuantifiedVariable
     (Name          : in     LexTokenManager.Lex_String;
      Comp_Unit     : in     ContextManager.UnitDescriptors;
      Declaration   : in     Location;
      TypeMark      : in     Symbol;
      TheConstraint : in     Symbol;
      Region        : in     Symbol;
      Variable      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         Variable          from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Name,
   --#                                Region,
   --#                                TheConstraint,
   --#                                TypeMark &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Region,
   --#                                TheConstraint,
   --#                                TypeMark;
   --# post IsQuantifiedVariable (Variable, Dict);

   procedure Add_Type_Announcement
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      The_Package : in     Symbol;
      The_Type    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type          from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Name,
   --#                                The_Package &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                The_Package;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Private_Type
     (Name           : in     LexTokenManager.Lex_String;
      Comp_Unit      : in     ContextManager.UnitDescriptors;
      Declaration    : in     Location;
      The_Package    : in     Symbol;
      Is_Limited     : in     Boolean;
      Is_Tagged_Type : in     Boolean;
      Extends        : in     Symbol;
      The_Type       :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type          from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Extends,
   --#                                Is_Limited,
   --#                                Is_Tagged_Type,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                The_Package &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Extends,
   --#                                Is_Limited,
   --#                                Is_Tagged_Type,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                The_Package;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Abstract_Proof_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Scope       : in     Scopes;
      The_Type    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope &
   --#         The_Type          from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Default_Abstract_Proof_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Scope       : in     Scopes;
      The_Type    :    out Symbol);
   --# global in out Dict;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         SPARK_IO.File_Sys     from *,
   --#                                    Comp_Unit,
   --#                                    Declaration,
   --#                                    Dict,
   --#                                    LexTokenManager.State,
   --#                                    Name,
   --#                                    Scope &
   --#         LexTokenManager.State from *,
   --#                                    Name &
   --#         The_Type              from Comp_Unit,
   --#                                    Declaration,
   --#                                    Dict,
   --#                                    LexTokenManager.State,
   --#                                    Name,
   --#                                    Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Enumeration_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Scope       : in     Scopes;
      Context     : in     Contexts;
      The_Type    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope &
   --#         The_Type          from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure AddEnumerationLiteral
     (Name                  : in     LexTokenManager.Lex_String;
      Comp_Unit             : in     ContextManager.UnitDescriptors;
      Declaration           : in     Location;
      Position              : in     LexTokenManager.Lex_String;
      The_Type              : in     Symbol;
      TheEnumerationLiteral :    out Symbol);
   --# global in out Dict;
   --# derives Dict,
   --#         TheEnumerationLiteral from Comp_Unit,
   --#                                    Declaration,
   --#                                    Dict,
   --#                                    Name,
   --#                                    Position,
   --#                                    The_Type;
   --# post IsEnumerationLiteral (TheEnumerationLiteral, Dict);

   procedure Add_Representation_Clause (The_Type : in Symbol;
                                        Clause   : in Location);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Clause,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                The_Type;

   procedure AddEnumerationLiteralRepresentation (Literal : in Symbol;
                                                  Code    : in Integer);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Code,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Literal;

   procedure Add_Integer_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Lower       : in     LexTokenManager.Lex_String;
      Upper       : in     LexTokenManager.Lex_String;
      Scope       : in     Scopes;
      Context     : in     Contexts;
      The_Type    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type          from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Scope,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Predef_Integer_Type
     (Name        : in LexTokenManager.Lex_String;
      Comp_Unit   : in ContextManager.UnitDescriptors;
      Declaration : in Location;
      Lower       : in LexTokenManager.Lex_String;
      Upper       : in LexTokenManager.Lex_String;
      Scope       : in Scopes;
      Context     : in Contexts);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Scope,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;

   procedure Add_Modular_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Modulus     : in     LexTokenManager.Lex_String;
      Scope       : in     Scopes;
      Context     : in     Contexts;
      The_Type    :    out Symbol);
   --# global in out Dict;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type              from Comp_Unit,
   --#                                    Context,
   --#                                    Declaration,
   --#                                    Dict,
   --#                                    LexTokenManager.State,
   --#                                    Modulus,
   --#                                    Name,
   --#                                    Scope &
   --#         LexTokenManager.State from *,
   --#                                    Modulus &
   --#         SPARK_IO.File_Sys     from *,
   --#                                    Comp_Unit,
   --#                                    Context,
   --#                                    Declaration,
   --#                                    Dict,
   --#                                    LexTokenManager.State,
   --#                                    Name,
   --#                                    Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Floating_Point_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Lower       : in     LexTokenManager.Lex_String;
      Upper       : in     LexTokenManager.Lex_String;
      Error_Bound : in     LexTokenManager.Lex_String;
      Scope       : in     Scopes;
      Context     : in     Contexts;
      The_Type    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type          from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                Error_Bound,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Scope,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Predef_Floating_Point_Type
     (Name        : in LexTokenManager.Lex_String;
      Comp_Unit   : in ContextManager.UnitDescriptors;
      Declaration : in Location;
      Lower       : in LexTokenManager.Lex_String;
      Upper       : in LexTokenManager.Lex_String;
      Error_Bound : in LexTokenManager.Lex_String;
      Scope       : in Scopes;
      Context     : in Contexts);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Error_Bound,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Scope,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;

   procedure Add_Protected_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Scope       : in     Scopes;
      Context     : in     Contexts;
      Mode        : in     Modes;
      Constrained : in     Boolean;
      The_Type    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type          from Comp_Unit,
   --#                                Constrained,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Mode,
   --#                                Name,
   --#                                Scope &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Task_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Scope       : in     Scopes;
      Context     : in     Contexts;
      Constrained : in     Boolean;
      The_Type    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type          from Comp_Unit,
   --#                                Constrained,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Task_Or_Protected_Subtype
     (Name        : in     LexTokenManager.Lex_String;
      Parent      : in     Symbol;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Scope       : in     Scopes;
      Context     : in     Contexts;
      The_Subtype :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Scope &
   --#         The_Subtype       from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Scope;
   --# post IsTypeMark (The_Subtype, Dict);

   procedure SetTypeIsWellformed (TypeMark   : in Symbol;
                                  Wellformed : in Boolean);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TypeMark,
   --#                   Wellformed;

   procedure SetBaseType (TypeMark, BaseType : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   BaseType,
   --#                   TypeMark;

   procedure Add_Fixed_Point_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Lower       : in     LexTokenManager.Lex_String;
      Upper       : in     LexTokenManager.Lex_String;
      Error_Bound : in     LexTokenManager.Lex_String;
      Scope       : in     Scopes;
      Context     : in     Contexts;
      The_Type    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type          from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                Error_Bound,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Scope,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure Add_Array_Type
     (Name                     : in     LexTokenManager.Lex_String;
      Comp_Unit                : in     ContextManager.UnitDescriptors;
      Declaration              : in     Location;
      Scope                    : in     Scopes;
      Context                  : in     Contexts;
      Constrained              : in     Boolean;
      Component_Type           : in     Symbol;
      Component_Type_Reference : in     Location;
      The_Type                 :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type          from Component_Type,
   --#                                Comp_Unit,
   --#                                Constrained,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope &
   --#         SPARK_IO.File_Sys from *,
   --#                                Component_Type,
   --#                                Component_Type_Reference,
   --#                                Comp_Unit,
   --#                                Constrained,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure AddArrayIndex
     (TheArrayType  : in     Symbol;
      IndexType     : in     Symbol;
      Comp_Unit     : in     ContextManager.UnitDescriptors;
      Declaration   : in     Location;
      TheArrayIndex :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         TheArrayIndex     from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                IndexType,
   --#                                TheArrayType &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                IndexType,
   --#                                LexTokenManager.State,
   --#                                TheArrayType;
   --# post IsArrayIndex (TheArrayIndex, Dict);

   procedure Add_Record_Type
     (Name           : in     LexTokenManager.Lex_String;
      Is_Tagged_Type : in     Boolean;
      Extends        : in     Symbol;
      Comp_Unit      : in     ContextManager.UnitDescriptors;
      Declaration    : in     Location;
      Scope          : in     Scopes;
      Context        : in     Contexts;
      The_Type       :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Type          from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                Extends,
   --#                                Is_Tagged_Type,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure AddRecordComponent
     (Name                   : in LexTokenManager.Lex_String;
      Comp_Unit              : in ContextManager.UnitDescriptors;
      Declaration            : in Location;
      TheRecordType          : in Symbol;
      TheComponentType       : in Symbol;
      InheritedField         : in Boolean;
      ComponentTypeReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                InheritedField,
   --#                                Name,
   --#                                TheComponentType,
   --#                                TheRecordType &
   --#         SPARK_IO.File_Sys from *,
   --#                                ComponentTypeReference,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                InheritedField,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                TheComponentType,
   --#                                TheRecordType;

   -- Generic types

   procedure Add_Generic_Type
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Scope       : in     Scopes;
      The_Type    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope &
   --#         The_Type          from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope;
   --# post IsTypeMark (The_Type, Dict);

   procedure Set_Generic_Private_Type (The_Type   : in Symbol;
                                       Is_Limited : in Boolean);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Is_Limited,
   --#                   The_Type;

   procedure Set_Generic_Discrete_Type (The_Type : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   The_Type;

   procedure Set_Generic_Integer_Type (The_Type : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   The_Type;

   procedure Set_Generic_Modular_Type (The_Type : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   The_Type;

   procedure Set_Generic_Floating_Point_Type (The_Type : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   The_Type;

   procedure Set_Generic_Fixed_Point_Type (The_Type : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   The_Type;

   procedure Set_Generic_Array_Type (The_Type : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   The_Type;

   procedure Add_Generic_Object
     (Name           : in     LexTokenManager.Lex_String;
      Comp_Unit      : in     ContextManager.UnitDescriptors;
      Declaration    : in     Location;
      Scope          : in     Scopes;
      The_Type       : in     Symbol;
      The_Object_Sym :    out Symbol);
   --# global in out Dict;
   --# derives Dict,
   --#         The_Object_Sym from Comp_Unit,
   --#                             Declaration,
   --#                             Dict,
   --#                             Name,
   --#                             Scope,
   --#                             The_Type;
   --# post IsConstant (The_Object_Sym, Dict);

   procedure AddRecordComponentRepresentation
     (Component        : in Symbol;
      Clause           : in Location;
      RelativeAddress  : in Natural;
      FirstBitPosition : in Natural;
      LastBitPosition  : in Natural);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Clause,
   --#                                Component,
   --#                                Dict,
   --#                                FirstBitPosition,
   --#                                LastBitPosition,
   --#                                LexTokenManager.State,
   --#                                RelativeAddress;

   procedure AddAlignmentClause (TheType : in Symbol;
                                 Clause  : in Location);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Clause,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                TheType;

   procedure AddLoop
     (Scope         : in     Scopes;
      Comp_Unit     : in     ContextManager.UnitDescriptors;
      LoopStatement : in     Location;
      TheLoop       :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                LoopStatement,
   --#                                Scope &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                LoopStatement,
   --#                                Scope &
   --#         TheLoop           from Comp_Unit,
   --#                                Dict,
   --#                                LoopStatement;

   procedure AddLoopName (Name    : in LexTokenManager.Lex_String;
                          TheLoop : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Name,
   --#                   TheLoop;

   procedure AddLoopParameter
     (TheLoop       : in Symbol;
      Comp_Unit     : in ContextManager.UnitDescriptors;
      Declaration   : in Location;
      Name          : in LexTokenManager.Lex_String;
      TypeMark      : in Symbol;
      StaticRange   : in Boolean;
      IsReverse     : in Boolean;
      TypeReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                IsReverse,
   --#                                Name,
   --#                                StaticRange,
   --#                                TheLoop,
   --#                                TypeMark &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                IsReverse,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                StaticRange,
   --#                                TheLoop,
   --#                                TypeMark,
   --#                                TypeReference;

   procedure MarkLoopHasExits (TheLoop : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheLoop;

   -- This is used by the VCG to store a Cells.Cell representing the exit expression of
   -- a for loop. Used by DAG.BuildGraph to build the default loop invariant.
   procedure SetLoopExitExpn (ForLoop : in Symbol;
                              Expn    : in Natural);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Expn,
   --#                   ForLoop;

   -- This is used by the VCG to store a Cells.Cell representing the entry expression of
   -- a for loop. Used by DAG.BuildGraph to build the default loop invariant.
   procedure SetLoopEntryExpn (ForLoop : in Symbol;
                               Expn    : in Natural);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Expn,
   --#                   ForLoop;

   -- Following is used by VCG in for loop modelling to create a variable uniquely associated
   -- with an original variable and a loop.  The original variable is used in the exit expression
   -- of a for loop and the new one is used to store the value on entry to the loop so as to
   -- freeze the loop bounds as required by Ada semantics.
   procedure IdempotentCreateLoopOnEntryVariable
     (OriginalVariable : in     Symbol;
      TheLoop          : in     Symbol;
      OnEntryVariable  :    out Symbol);
   --# global in out Dict;
   --# derives Dict,
   --#         OnEntryVariable from Dict,
   --#                              OriginalVariable,
   --#                              TheLoop;

   -- Provides access to variable created by previous call.
   function GetLoopOnEntryVariable (OriginalVariable : Symbol;
                                    TheLoop          : Symbol) return Symbol;
   --# global in Dict;

   procedure Add_Full_Range_Subtype
     (Name             : in     LexTokenManager.Lex_String;
      Parent           : in     Symbol;
      Parent_Reference : in     Location;
      Comp_Unit        : in     ContextManager.UnitDescriptors;
      Declaration      : in     Location;
      Scope            : in     Scopes;
      Context          : in     Contexts;
      The_Subtype      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Subtype       from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Scope &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Parent_Reference,
   --#                                Scope;
   --# post IsTypeMark (The_Subtype, Dict);

   procedure Add_Enumeration_Subtype
     (Name             : in     LexTokenManager.Lex_String;
      Static           : in     Boolean;
      Parent           : in     Symbol;
      Parent_Reference : in     Location;
      Lower            : in     LexTokenManager.Lex_String;
      Upper            : in     LexTokenManager.Lex_String;
      Comp_Unit        : in     ContextManager.UnitDescriptors;
      Declaration      : in     Location;
      Scope            : in     Scopes;
      Context          : in     Contexts;
      The_Subtype      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Subtype       from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Parent,
   --#                                Scope,
   --#                                Static,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Parent_Reference,
   --#                                Scope;
   --# post IsTypeMark (The_Subtype, Dict);

   procedure Add_Integer_Subtype
     (Name             : in     LexTokenManager.Lex_String;
      Static           : in     Boolean;
      Parent           : in     Symbol;
      Parent_Reference : in     Location;
      Lower            : in     LexTokenManager.Lex_String;
      Upper            : in     LexTokenManager.Lex_String;
      Comp_Unit        : in     ContextManager.UnitDescriptors;
      Declaration      : in     Location;
      Scope            : in     Scopes;
      Context          : in     Contexts;
      The_Subtype      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Subtype       from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Parent,
   --#                                Scope,
   --#                                Static,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Parent_Reference,
   --#                                Scope;
   --# post IsTypeMark (The_Subtype, Dict);

   procedure Add_Modular_Subtype
     (Name             : in     LexTokenManager.Lex_String;
      Parent           : in     Symbol;
      Parent_Reference : in     Location;
      Lower            : in     LexTokenManager.Lex_String;
      Upper            : in     LexTokenManager.Lex_String;
      Comp_Unit        : in     ContextManager.UnitDescriptors;
      Declaration      : in     Location;
      Scope            : in     Scopes;
      Context          : in     Contexts;
      The_Subtype      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Subtype       from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Parent,
   --#                                Scope,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Parent_Reference,
   --#                                Scope;
   --# post IsTypeMark (The_Subtype, Dict);

   procedure Add_Floating_Point_Subtype
     (Name             : in     LexTokenManager.Lex_String;
      Static           : in     Boolean;
      Parent           : in     Symbol;
      Parent_Reference : in     Location;
      Lower            : in     LexTokenManager.Lex_String;
      Upper            : in     LexTokenManager.Lex_String;
      Error_Bound      : in     LexTokenManager.Lex_String;
      Comp_Unit        : in     ContextManager.UnitDescriptors;
      Declaration      : in     Location;
      Scope            : in     Scopes;
      Context          : in     Contexts;
      The_Subtype      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Subtype       from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                Error_Bound,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Parent,
   --#                                Scope,
   --#                                Static,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Parent_Reference,
   --#                                Scope;
   --# post IsTypeMark (The_Subtype, Dict);

   procedure Add_Fixed_Point_Subtype
     (Name             : in     LexTokenManager.Lex_String;
      Static           : in     Boolean;
      Parent           : in     Symbol;
      Parent_Reference : in     Location;
      Lower            : in     LexTokenManager.Lex_String;
      Upper            : in     LexTokenManager.Lex_String;
      Error_Bound      : in     LexTokenManager.Lex_String;
      Comp_Unit        : in     ContextManager.UnitDescriptors;
      Declaration      : in     Location;
      Scope            : in     Scopes;
      Context          : in     Contexts;
      The_Subtype      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Subtype       from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                Error_Bound,
   --#                                LexTokenManager.State,
   --#                                Lower,
   --#                                Name,
   --#                                Parent,
   --#                                Scope,
   --#                                Static,
   --#                                Upper &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Parent_Reference,
   --#                                Scope;
   --# post IsTypeMark (The_Subtype, Dict);

   -- Adds an array subtype that has a (possibly static) constraint. For example -
   -- addition of a constrained subtype of an unconstrained array type
   procedure Add_Array_Subtype
     (Name             : in     LexTokenManager.Lex_String;
      Parent           : in     Symbol;
      Parent_Reference : in     Location;
      Comp_Unit        : in     ContextManager.UnitDescriptors;
      Declaration      : in     Location;
      Scope            : in     Scopes;
      Context          : in     Contexts;
      Static           : in     Boolean;
      The_Subtype      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         The_Subtype       from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Scope,
   --#                                Static &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Parent,
   --#                                Parent_Reference,
   --#                                Scope;
   --# post IsTypeMark (The_Subtype, Dict);

   procedure AddAssertStatement (Statement : in Location);
   --# global in     Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Dict,
   --#                                Statement;

   procedure AddCheckStatement (Statement : in Location);
   --# global in     Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Dict,
   --#                                Statement;

   procedure AddPrecondition
     (Abstraction  : in Abstractions;
      Subprogram   : in Symbol;
      Predicate    : in ExaminerConstants.RefType;
      Precondition : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Abstraction,
   --#                                Predicate,
   --#                                Subprogram &
   --#         SPARK_IO.File_Sys from *,
   --#                                Abstraction,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Precondition,
   --#                                Predicate,
   --#                                Subprogram;

   procedure AddPostcondition
     (Abstraction   : in Abstractions;
      Subprogram    : in Symbol;
      Predicate     : in ExaminerConstants.RefType;
      Postcondition : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Abstraction,
   --#                                Predicate,
   --#                                Subprogram &
   --#         SPARK_IO.File_Sys from *,
   --#                                Abstraction,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Postcondition,
   --#                                Predicate,
   --#                                Subprogram;

   procedure AddSubprogram
     (Name          : in     LexTokenManager.Lex_String;
      Comp_Unit     : in     ContextManager.UnitDescriptors;
      Specification : in     Location;
      Scope         : in     Scopes;
      Context       : in     Contexts;
      Subprogram    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         Subprogram        from Comp_Unit,
   --#                                Context,
   --#                                Dict,
   --#                                Name,
   --#                                Scope,
   --#                                Specification &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Specification;
   --# post IsSubprogram (Subprogram, Dict);

   function ActualOfGenericFormalType (TheGenericFormalSym : Symbol;
                                       ActualSubprogramSym : Symbol) return Symbol;
   --# global in Dict;
   --# return S => IsTypeMark (S, Dict);
   -- returns the symbol that is the generic actual that matches the given generic formal for a
   -- given instantiation

   function ActualOfGenericFormalObject (TheGenericFormalSym : Symbol;
                                         ActualSubprogramSym : Symbol) return Symbol;
   --# global in Dict;
   --# return S => IsConstant (S, Dict);
   -- returns the symbol that is the generic actual that matches the given generic formal for a
   -- given instantiation

   function ActualOfGenericParameter (TheParameter        : Symbol;
                                      ActualSubprogramSym : Symbol) return Symbol;
   --# global in Dict;
   --# return S => IsSubprogramParameter (S, Dict);
   -- returns the symbol of the actual parameter that has the same posiiton number in the instantiated
   -- subprogram as the parameter symbol  has in the generic from which it comes

   function ActualOfParameterConstraint (TheParameter        : Symbol;
                                         ActualSubprogramSym : Symbol) return Symbol;
   --# global in Dict;
   --# return S => IsParameterConstraint (S, Dict);

   procedure AddSubprogramInstantiation
     (Name          : in     LexTokenManager.Lex_String;
      Comp_Unit     : in     ContextManager.UnitDescriptors;
      Declaration   : in     Location;
      TheGeneric    : in     Symbol;
      Specification : in     Location;
      Scope         : in     Scopes;
      Context       : in     Contexts;
      Subprogram    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         Subprogram        from Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                Name,
   --#                                Scope,
   --#                                Specification,
   --#                                TheGeneric &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Context,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Specification,
   --#                                TheGeneric;
   --# post IsSubprogram (Subprogram, Dict);

   function IsInstantiation (PackageOrSubProgram : Symbol) return Boolean;
   --# global in Dict;

   function GetGenericOfInstantiation (PackageOrSubProgram : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsSubprogram (S, Dict));

   -- Copies the parameters and return types from Generic to Instantiation substituting
   -- actual types as it goes (using generic association linked list of Instantiation)
   procedure InstantiateSubprogramParameters
     (ActualSubprogramSym : in Symbol;
      Comp_Unit           : in ContextManager.UnitDescriptors;
      Declaration         : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                ActualSubprogramSym,
   --#                                Comp_Unit,
   --#                                Declaration &
   --#         SPARK_IO.File_Sys from *,
   --#                                ActualSubprogramSym,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State;

   procedure SetSubprogramSignatureNotWellformed (Abstraction : in Abstractions;
                                                  Subprogram  : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Abstraction,
   --#                   Subprogram;

   procedure SetSubprogramIsEntry (Subprogram : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Subprogram;

   procedure Set_Package_Generic_Unit (Pack_Sym     : in Symbol;
                                       Generic_Unit : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Generic_Unit,
   --#                   Pack_Sym;

   procedure Set_Subprogram_Generic_Unit (Subprogram   : in Symbol;
                                          Generic_Unit : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Generic_Unit,
   --#                   Subprogram;

   procedure Set_Generic_Unit_Owning_Package (Generic_Unit : in Symbol;
                                              Pack_Sym     : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Generic_Unit,
   --#                   Pack_Sym;

   procedure Set_Generic_Unit_Owning_Subprogram (Generic_Unit : in Symbol;
                                                 Subprogram   : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Generic_Unit,
   --#                   Subprogram;

   -- Call this to record the fact that a procedure or task has an explicit
   -- derives annotation.
   procedure SetHasDerivesAnnotation (Task_Or_Proc : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Task_Or_Proc;

   procedure SetSubprogramEntryBarrier (Subprogram, TheBarrier : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Subprogram,
   --#                   TheBarrier;

   procedure SetIsInterruptHandler (Subprogram : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Subprogram;

   procedure SetHasDelayProperty (TheProcedure : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheProcedure;

   procedure SetUsesUnprotectedVariables (Sym : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Sym;

   procedure SetUnprotectedReference (Variable : in Symbol;
                                      ByThread : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ByThread,
   --#                   Variable;

   procedure SetSuspendsReference (Variable : in Symbol;
                                   ByThread : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ByThread,
   --#                   Variable;

   procedure SetVirtualElementSeenByOwner (TheVariable : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheVariable;

   procedure SetPriorityProperty (OwnVariable : in Symbol;
                                  TheValue    : in LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   OwnVariable,
   --#                   TheValue;

   procedure SetIntegrityProperty (OwnVariable : in Symbol;
                                   TheValue    : in LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   OwnVariable,
   --#                   TheValue;

   procedure SetIsSuspendable (Variable : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Variable;

   procedure SetHasInterruptProperty (Variable : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Variable;

   procedure MarkAccountsForDelay (TheProcedure : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheProcedure;

   procedure MarkAccountsForSuspendsListItem (TheTaskOrProc : in Symbol;
                                              ThePOorSO     : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ThePOorSO,
   --#                   TheTaskOrProc;

   procedure MarkAccountsForSuspendsListItems (TheTaskOrProc       : in Symbol;
                                               TheItemsInProcedure : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheItemsInProcedure,
   --#                   TheTaskOrProc;

   procedure SetProtectedTypeElementsHidden (TheProtectedType : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheProtectedType;

   procedure SetProtectedTypeEntry (TheProtectedType, TheEntry : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheEntry,
   --#                   TheProtectedType;

   procedure SetTypeHasPragma (TheProtectedOrTaskType : in Symbol;
                               ThePragma              : in RavenscarPragmas);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ThePragma,
   --#                   TheProtectedOrTaskType;

   procedure SetTypePragmaValue
     (TheProtectedOrTaskType : in Symbol;
      ThePragma              : in RavenscarPragmasWithValue;
      TheValue               : in LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ThePragma,
   --#                   TheProtectedOrTaskType,
   --#                   TheValue;

   procedure SetMainProgramPriority (TheValue : in LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheValue;

   procedure AddReturnType
     (TheFunction   : in Symbol;
      TypeMark      : in Symbol;
      Comp_Unit     : in ContextManager.UnitDescriptors;
      TypeReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                TheFunction,
   --#                                TypeMark,
   --#                                TypeReference &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                TheFunction,
   --#                                TypeMark,
   --#                                TypeReference;

   procedure AddImplicitReturnVariable
     (Abstraction : in     Abstractions;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Name        : in     LexTokenManager.Lex_String;
      TheFunction : in     Symbol;
      Variable    :    out Symbol);
   --# global in out Dict;
   --# derives Dict,
   --#         Variable from Abstraction,
   --#                       Comp_Unit,
   --#                       Declaration,
   --#                       Dict,
   --#                       Name,
   --#                       TheFunction;
   --# post IsImplicitReturnVariable (Variable, Dict);

   procedure AddSubprogramParameter
     (Name          : in LexTokenManager.Lex_String;
      Subprogram    : in Symbol;
      TypeMark      : in Symbol;
      TypeReference : in Location;
      Mode          : in Modes;
      Comp_Unit     : in ContextManager.UnitDescriptors;
      Specification : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                Mode,
   --#                                Name,
   --#                                Specification,
   --#                                Subprogram,
   --#                                TypeMark &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Mode,
   --#                                Name,
   --#                                Specification,
   --#                                Subprogram,
   --#                                TypeMark,
   --#                                TypeReference;

   procedure Add_Generic_Formal_Parameter
     (Comp_Unit    : in ContextManager.UnitDescriptors;
      Declaration  : in Location;
      Generic_Unit : in Symbol;
      The_Type     : in Symbol;
      The_Object   : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Comp_Unit,
   --#                   Declaration,
   --#                   Generic_Unit,
   --#                   The_Object,
   --#                   The_Type;

   procedure AddGenericTypeAssociation
     (SubprogramOrPackage : in Symbol;
      Comp_Unit           : in ContextManager.UnitDescriptors;
      Declaration         : in Location;
      FormalSym           : in Symbol;
      ActualSym           : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ActualSym,
   --#                   Comp_Unit,
   --#                   Declaration,
   --#                   FormalSym,
   --#                   SubprogramOrPackage;

   procedure AddGenericObjectAssociation
     (SubprogramOrPackage : in Symbol;
      Comp_Unit           : in ContextManager.UnitDescriptors;
      Declaration         : in Location;
      FormalSym           : in Symbol;
      ActualSym           : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ActualSym,
   --#                   Comp_Unit,
   --#                   Declaration,
   --#                   FormalSym,
   --#                   SubprogramOrPackage;

   procedure AddKnownDiscriminant
     (Name                : in LexTokenManager.Lex_String;
      Comp_Unit           : in ContextManager.UnitDescriptors;
      Declaration         : in Location;
      ProtectedOrTaskType : in Symbol;
      TypeMark            : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Comp_Unit,
   --#                   Declaration,
   --#                   Name,
   --#                   ProtectedOrTaskType,
   --#                   TypeMark;

   procedure SetDiscriminantSetsPriority (TheDiscriminant : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheDiscriminant;

   procedure AddDiscriminantConstraintStaticValue
     (ProtectedOrTaskSubtype : in Symbol;
      Comp_Unit              : in ContextManager.UnitDescriptors;
      Declaration            : in Location;
      TheValue               : in LexTokenManager.Lex_String);

   --# global in out Dict;
   --# derives Dict from *,
   --#                   Comp_Unit,
   --#                   Declaration,
   --#                   ProtectedOrTaskSubtype,
   --#                   TheValue;

   procedure AddDiscriminantConstraintAccessedObject
     (ProtectedOrTaskSubtype : in Symbol;
      Comp_Unit              : in ContextManager.UnitDescriptors;
      Declaration            : in Location;
      TheObject              : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Comp_Unit,
   --#                   Declaration,
   --#                   ProtectedOrTaskSubtype,
   --#                   TheObject;

   procedure SetSubtypePriority (ProtectedOrTaskSubtype : in Symbol;
                                 ThePriority            : in LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ProtectedOrTaskSubtype,
   --#                   ThePriority;

   procedure AddBody
     (CompilationUnit : in Symbol;
      Comp_Unit       : in ContextManager.UnitDescriptors;
      TheBody         : in Location;
      Hidden          : in Boolean);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                CompilationUnit,
   --#                                Comp_Unit,
   --#                                Hidden,
   --#                                TheBody &
   --#         SPARK_IO.File_Sys from *,
   --#                                CompilationUnit,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                Hidden,
   --#                                LexTokenManager.State,
   --#                                TheBody;

   procedure AddBodyStub (CompilationUnit : in Symbol;
                          Comp_Unit       : in ContextManager.UnitDescriptors;
                          BodyStub        : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                BodyStub,
   --#                                CompilationUnit,
   --#                                Comp_Unit &
   --#         SPARK_IO.File_Sys from *,
   --#                                BodyStub,
   --#                                CompilationUnit,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State;

   procedure AddMainProgram (Subprogram : in Symbol;
                             Annotation : in Location);
   --# global in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Subprogram &
   --#         SPARK_IO.File_Sys from *,
   --#                                Annotation,
   --#                                Dict,
   --#                                Subprogram;

   procedure AddDependencyRelation (Abstraction        : in Abstractions;
                                    TheProcedure       : in Symbol;
                                    DependencyRelation : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Abstraction,
   --#                                TheProcedure &
   --#         SPARK_IO.File_Sys from *,
   --#                                Abstraction,
   --#                                DependencyRelation,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                TheProcedure;

   procedure RenameSubprogram
     (Subprogram          : in Symbol;
      SubprogramReference : in Location;
      Comp_Unit           : in ContextManager.UnitDescriptors;
      Declaration         : in Location;
      Scope               : in Scopes);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Scope,
   --#                                Subprogram &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Scope,
   --#                                Subprogram,
   --#                                SubprogramReference;

   procedure RenameUnaryOperator
     (Name        : in     SP_Symbols.SP_Symbol;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Operand     : in     Symbol;
      Scope       : in     Scopes;
      Op_Sym      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         Op_Sym            from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Name,
   --#                                Operand,
   --#                                Scope &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Operand,
   --#                                Scope;
   --# post IsOperator (Op_Sym, Dict);

   procedure RenameBinaryOperator
     (Name        : in     SP_Symbols.SP_Symbol;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      Left        : in     Symbol;
      Right       : in     Symbol;
      Scope       : in     Scopes;
      Op_Sym      :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         Op_Sym            from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Left,
   --#                                Name,
   --#                                Right,
   --#                                Scope &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Left,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Right,
   --#                                Scope;
   --# post IsOperator (Op_Sym, Dict);

   procedure AddGlobalAnnotation
     (Abstraction : in Abstractions;
      Subprogram  : in Symbol;
      Comp_Unit   : in ContextManager.UnitDescriptors;
      Annotation  : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Abstraction,
   --#                                Annotation,
   --#                                Comp_Unit,
   --#                                Subprogram &
   --#         SPARK_IO.File_Sys from *,
   --#                                Abstraction,
   --#                                Annotation,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Subprogram;

   procedure AddGlobalVariable
     (Abstraction         : in     Abstractions;
      Subprogram          : in     Symbol;
      Variable            : in     Symbol;
      Mode                : in     Modes;
      PrefixNeeded        : in     Boolean;
      Comp_Unit           : in     ContextManager.UnitDescriptors;
      VariableReference   : in     Location;
      Global_Variable_Sym :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         Global_Variable_Sym from Abstraction,
   --#                                  Comp_Unit,
   --#                                  Dict,
   --#                                  Mode,
   --#                                  PrefixNeeded,
   --#                                  Subprogram,
   --#                                  Variable,
   --#                                  VariableReference &
   --#         SPARK_IO.File_Sys   from *,
   --#                                  Abstraction,
   --#                                  Comp_Unit,
   --#                                  Dict,
   --#                                  LexTokenManager.State,
   --#                                  Mode,
   --#                                  PrefixNeeded,
   --#                                  Subprogram,
   --#                                  Variable,
   --#                                  VariableReference;
   --# post IsGlobalVariable (Global_Variable_Sym, Dict);

   procedure AddExport
     (Abstraction     : in Abstractions;
      TheProcedure    : in Symbol;
      TheExport       : in Symbol;
      ExportReference : in Location;
      Annotation      : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Abstraction,
   --#                                TheExport,
   --#                                TheProcedure &
   --#         SPARK_IO.File_Sys from *,
   --#                                Abstraction,
   --#                                Annotation,
   --#                                Dict,
   --#                                ExportReference,
   --#                                LexTokenManager.State,
   --#                                TheExport,
   --#                                TheProcedure;

   procedure AddDependency
     (Abstraction     : in Abstractions;
      Comp_Unit       : in ContextManager.UnitDescriptors;
      TheProcedure    : in Symbol;
      TheExport       : in Symbol;
      TheImport       : in Symbol;
      ImportReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Abstraction,
   --#                                Comp_Unit,
   --#                                ImportReference,
   --#                                TheExport,
   --#                                TheImport,
   --#                                TheProcedure &
   --#         SPARK_IO.File_Sys from *,
   --#                                Abstraction,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                ImportReference,
   --#                                LexTokenManager.State,
   --#                                TheExport,
   --#                                TheImport,
   --#                                TheProcedure;

   procedure AddVirtualElement
     (ToProtectedType   : in Symbol;
      Comp_Unit         : in ContextManager.UnitDescriptors;
      Declaration       : in Location;
      TheVirtualElement : in Symbol;
      TheOwner          : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Comp_Unit,
   --#                   Declaration,
   --#                   TheOwner,
   --#                   TheVirtualElement,
   --#                   ToProtectedType;

   procedure AddPOorSOToSuspendsList
     (TheTaskOrProc : in Symbol;
      Comp_Unit     : in ContextManager.UnitDescriptors;
      Declaration   : in Location;
      ThePOorSO     : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Comp_Unit,
   --#                   Declaration,
   --#                   ThePOorSO,
   --#                   TheTaskOrProc;

   procedure AddInterruptStreamMapping
     (Subject             : in Symbol;
      Comp_Unit           : in ContextManager.UnitDescriptors;
      Declaration         : in Location;
      TheInterruptHandler : in LexTokenManager.Lex_String;
      TheInterruptStream  : in LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Comp_Unit,
   --#                   Declaration,
   --#                   Subject,
   --#                   TheInterruptHandler,
   --#                   TheInterruptStream;

   procedure CopyDependencyList
     (Abstraction  : in Abstractions;
      TheProcedure : in Symbol;
      FromExport   : in Symbol;
      ToExport     : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Abstraction,
   --#                   FromExport,
   --#                   TheProcedure,
   --#                   ToExport;

   procedure ForceImport
     (Abstraction     : in Abstractions;
      TheProcedure    : in Symbol;
      TheImport       : in Symbol;
      ImportReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Abstraction,
   --#                                TheImport,
   --#                                TheProcedure &
   --#         SPARK_IO.File_Sys from *,
   --#                                Abstraction,
   --#                                Dict,
   --#                                ImportReference,
   --#                                LexTokenManager.State,
   --#                                TheImport,
   --#                                TheProcedure;

   procedure Add_Package
     (Name          : in     LexTokenManager.Lex_String;
      Comp_Unit     : in     ContextManager.UnitDescriptors;
      Specification : in     Location;
      Scope         : in     Scopes;
      ThePackage    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Specification &
   --#         ThePackage        from Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Specification;
   --# post IsPackage (ThePackage, Dict);

   procedure AddChildPackage
     (TheParent     : in     Symbol;
      Sort          : in     PackageSort;
      Name          : in     LexTokenManager.Lex_String;
      Comp_Unit     : in     ContextManager.UnitDescriptors;
      Specification : in     Location;
      Scope         : in     Scopes;
      ThePackage    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Sort,
   --#                                Specification,
   --#                                TheParent &
   --#         ThePackage        from Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Sort,
   --#                                Specification,
   --#                                TheParent;
   --# post IsPackage (ThePackage, Dict);

   procedure AddPrivatePackage
     (Name          : in     LexTokenManager.Lex_String;
      Comp_Unit     : in     ContextManager.UnitDescriptors;
      Specification : in     Location;
      Scope         : in     Scopes;
      ThePackage    :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Specification &
   --#         ThePackage        from Comp_Unit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Scope,
   --#                                Specification;
   --# post IsPackage (ThePackage, Dict);

   procedure AddPrivatePart (ThePackage  : in Symbol;
                             PrivatePart : in Location;
                             Hidden      : in Boolean);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Dict,
   --#                                Hidden,
   --#                                LexTokenManager.State,
   --#                                PrivatePart,
   --#                                ThePackage;

   procedure AddOwnAnnotation (ThePackage : in Symbol;
                               Annotation : in Location);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Annotation,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                ThePackage;

   procedure Add_Own_Variable
     (Name                : in     LexTokenManager.Lex_String;
      The_Package         : in     Symbol;
      Mode                : in     Modes;
      Is_Protected        : in     Boolean;
      Is_Interrupt_Stream : in     Boolean;
      Comp_Unit           : in     ContextManager.UnitDescriptors;
      Declaration         : in     Location;
      Var_Symbol          :    out Symbol);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict,
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Is_Interrupt_Stream,
   --#                                Is_Protected,
   --#                                LexTokenManager.State,
   --#                                Mode,
   --#                                Name,
   --#                                The_Package &
   --#         Var_Symbol        from Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Is_Interrupt_Stream,
   --#                                Is_Protected,
   --#                                LexTokenManager.State,
   --#                                Mode,
   --#                                Name,
   --#                                The_Package;
   --# post IsVariable (Var_Symbol, Dict);

   procedure AddOwnVariableType (OwnVariable   : in Symbol;
                                 TypeMark      : in Symbol;
                                 TypeReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                OwnVariable,
   --#                                TypeMark &
   --#         SPARK_IO.File_Sys from *,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                OwnVariable,
   --#                                TypeMark,
   --#                                TypeReference;

   procedure AddOwnTask
     (Name        : in     LexTokenManager.Lex_String;
      Comp_Unit   : in     ContextManager.UnitDescriptors;
      Declaration : in     Location;
      TypeMark    : in     Symbol;
      ThePackage  : in     Symbol;
      TaskSym     :    out Symbol);
   --# global in out Dict;
   --# derives Dict,
   --#         TaskSym from Comp_Unit,
   --#                      Declaration,
   --#                      Dict,
   --#                      Name,
   --#                      ThePackage,
   --#                      TypeMark;
   --# post IsVariable (TaskSym, Dict);

   procedure AddRefinementDefinition (ThePackage : in Symbol;
                                      Annotation : in Location);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Annotation,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                ThePackage;

   procedure AddConstituent
     (Name                 : in LexTokenManager.Lex_String;
      Subject              : in Symbol;
      Mode                 : in Modes;
      SubjectReference     : in Location;
      Comp_Unit            : in ContextManager.UnitDescriptors;
      ConstituentReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                ConstituentReference,
   --#                                Mode,
   --#                                Name,
   --#                                Subject &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                ConstituentReference,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Name,
   --#                                Subject,
   --#                                SubjectReference;

   procedure AddConstituentSym
     (ConstituentVariable  : in Symbol;
      Subject              : in Symbol;
      Comp_Unit            : in ContextManager.UnitDescriptors;
      ConstituentReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                ConstituentReference,
   --#                                ConstituentVariable,
   --#                                Subject &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                ConstituentReference,
   --#                                ConstituentVariable,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Subject;

   procedure AddEmbeddedConstituent
     (PackageName          : in LexTokenManager.Lex_String;
      VariableName         : in LexTokenManager.Lex_String;
      Subject              : in Symbol;
      Mode                 : in Modes;
      SubjectReference     : in Location;
      Comp_Unit            : in ContextManager.UnitDescriptors;
      ConstituentReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                ConstituentReference,
   --#                                LexTokenManager.State,
   --#                                Mode,
   --#                                PackageName,
   --#                                Subject,
   --#                                VariableName &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                ConstituentReference,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                PackageName,
   --#                                Subject,
   --#                                SubjectReference,
   --#                                VariableName;

   procedure AddChildConstituent
     (Variable             : in Symbol;
      Subject              : in Symbol;
      Mode                 : in Modes;
      SubjectReference     : in Location;
      Comp_Unit            : in ContextManager.UnitDescriptors;
      ConstituentReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                ConstituentReference,
   --#                                Mode,
   --#                                Subject,
   --#                                Variable &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                ConstituentReference,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Subject,
   --#                                SubjectReference,
   --#                                Variable;

   procedure AddInitializationSpecification (ThePackage : in Symbol;
                                             Annotation : in Location);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Annotation,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                ThePackage;

   procedure AddInitializedOwnVariable (Variable          : in Symbol;
                                        VariableReference : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Variable &
   --#         SPARK_IO.File_Sys from *,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Variable,
   --#                                VariableReference;

   procedure AddPackageInitialization (ThePackage     : in Symbol;
                                       Initialization : in Location;
                                       Hidden         : in Boolean);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Dict,
   --#                                Hidden,
   --#                                Initialization,
   --#                                LexTokenManager.State,
   --#                                ThePackage;

   procedure AddWithReference
     (The_Visibility    : in     Visibility;
      The_Unit          : in     Symbol;
      The_Withed_Symbol : in     Symbol;
      Explicit          : in     Boolean;
      Comp_Unit         : in     ContextManager.UnitDescriptors;
      Declaration       : in     Location;
      Already_Present   :    out Boolean);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Already_Present   from Dict,
   --#                                Explicit,
   --#                                The_Unit,
   --#                                The_Visibility,
   --#                                The_Withed_Symbol &
   --#         Dict              from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Explicit,
   --#                                The_Unit,
   --#                                The_Visibility,
   --#                                The_Withed_Symbol &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Explicit,
   --#                                LexTokenManager.State,
   --#                                The_Unit,
   --#                                The_Visibility,
   --#                                The_Withed_Symbol;

   procedure AddUseTypeReference
     (The_Visibility : in Visibility;
      The_Unit       : in Symbol;
      TheType        : in Symbol;
      Comp_Unit      : in ContextManager.UnitDescriptors;
      Declaration    : in Location);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Dict              from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                TheType,
   --#                                The_Unit,
   --#                                The_Visibility &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                TheType,
   --#                                The_Unit,
   --#                                The_Visibility;

   procedure AddInheritsReference
     (The_Unit             : in     Symbol;
      The_Inherited_Symbol : in     Symbol;
      Explicit             : in     Boolean;
      Comp_Unit            : in     ContextManager.UnitDescriptors;
      Declaration          : in     Location;
      Already_Present      :    out Boolean);
   --# global in     LexTokenManager.State;
   --#        in out Dict;
   --#        in out SPARK_IO.File_Sys;
   --# derives Already_Present   from Dict,
   --#                                Explicit,
   --#                                The_Inherited_Symbol,
   --#                                The_Unit &
   --#         Dict              from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Explicit,
   --#                                The_Inherited_Symbol,
   --#                                The_Unit &
   --#         SPARK_IO.File_Sys from *,
   --#                                Comp_Unit,
   --#                                Declaration,
   --#                                Dict,
   --#                                Explicit,
   --#                                LexTokenManager.State,
   --#                                The_Inherited_Symbol,
   --#                                The_Unit;

   procedure SetPackageElaborateBodyFound (ThePackage : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ThePackage;

   procedure SetPackageAsExtendingAnother (ThePackage          : in Symbol;
                                           ThePackageItExtends : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   ThePackage,
   --#                   ThePackageItExtends;

   procedure AddWriteReference (Variable, CompilationUnit : in Symbol;
                                Reference                 : in Location);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CompilationUnit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Reference,
   --#                                Variable;

   procedure AddReadReference (Object, CompilationUnit : in Symbol;
                               Reference               : in Location);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CompilationUnit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Object,
   --#                                Reference;

   procedure AddSubprogramCall (Subprogram, CompilationUnit : in Symbol;
                                Call                        : in Location);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Call,
   --#                                CompilationUnit,
   --#                                Dict,
   --#                                LexTokenManager.State,
   --#                                Subprogram;

   procedure AddOtherReference (Item, CompilationUnit : in Symbol;
                                Reference             : in Location);
   --# global in     Dict;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CompilationUnit,
   --#                                Dict,
   --#                                Item,
   --#                                LexTokenManager.State,
   --#                                Reference;

   procedure AddUsesUncheckedConversion (TheUnit : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheUnit;

   procedure AddAssignsFromExternal (TheUnit : in Symbol);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   TheUnit;

   --------------------------------------------------------------------------------
   --                             ACCESS FUNCTIONS                               --
   --------------------------------------------------------------------------------

   function SymbolRef (Item : Symbol) return ExaminerConstants.RefType;

   function ConvertSymbolRef (Ref : ExaminerConstants.RefType) return Symbol;

   function GetSimpleName (Item : Symbol) return LexTokenManager.Lex_String;
   --# global in Dict;

   function GetType (TheSymbol : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function Get_Unconstrained_Array_Index (TheSymbol : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsParameterConstraint (S, Dict));

   -- There is no need for a GetUnaryOperatorType function since the result type
   -- of every SPARK unary operator is the same as the operand type

   function GetAccess (TheProtectedType : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetScalarAttributeType (Name     : LexTokenManager.Lex_String;
                                    TypeMark : Symbol) return Symbol;
   --# global in Dict;
   --#        in LexTokenManager.State;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetArrayAttributeType
     (Name      : LexTokenManager.Lex_String;
      TypeMark  : Symbol;
      Dimension : Positive)
     return      Symbol;
   --# global in Dict;
   --#        in LexTokenManager.State;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetScalarAttributeValue
     (Base     : Boolean;
      Name     : LexTokenManager.Lex_String;
      TypeMark : Symbol)
     return     LexTokenManager.Lex_String;
   --# global in Dict;
   --#        in LexTokenManager.State;

   function GetArrayAttributeValue
     (Name      : LexTokenManager.Lex_String;
      TypeMark  : Symbol;
      Dimension : Positive)
     return      LexTokenManager.Lex_String;
   --# global in Dict;
   --#        in LexTokenManager.State;

   function GetEnumerationLiteral (EnumerationType : Symbol;
                                   Position        : LexTokenManager.Lex_String) return Symbol;
   --# global in Dict;
   --#        in LexTokenManager.State;

   function GetPositionNumber (Literal : Symbol) return LexTokenManager.Lex_String;
   --# global in Dict;

   function GetRecordType (Component : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   -- Predefined types -------------------------------------------------------------

   function GetUnknownTypeMark return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetUniversalIntegerType return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetUniversalRealType return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetUniversalFixedType return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function IsUniversalFixedType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function GetPredefinedBooleanType return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function IsPredefinedBooleanType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   -- The NullVariable is an out stream used as a data sink for null derives etc.
   function GetNullVariable return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsVariable (S, Dict));

   function Is_Null_Variable (TheVariable : Symbol) return Boolean;
   --# global in Dict;

   -- ThePartition is a subprogram symbol (predefined when Ravenscar profile is selected)
   -- that is used as place with which to associate the partition annotation.
   function GetThePartition return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsSubprogram (S, Dict));

   function GetFalse return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsEnumerationLiteral (S, Dict));

   function GetTrue return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsEnumerationLiteral (S, Dict));

   function GetPredefinedIntegerType return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetPredefinedLongIntegerType return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetPredefinedCharacterType return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetPredefinedStringType return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetPredefinedNaturalSubtype return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetPredefinedPositiveSubtype return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetPredefinedTimeType return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function IsPredefinedTimeSpanType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   -- Note: following function is to with getting the true base type
   --       of a type which is derived (from say root_integer).
   --       Use GetRootType to get the "first named subtype" of a subtype
   function GetBaseType (TypeMark : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetRootOfExtendedType (TypeMark : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));
   -- Applies to types extended from tagged types.  Gives the immediately

   -- Returns the type at the root of the "Parent" relation between
   -- subtypes and types.
   --
   -- For signed integer and floating point (sub)types,
   -- the root type is the first subtype of the
   -- anonymous type chosen by the compiler when a signed integer
   -- or floating point type is declared.  For example:
   --  type T is range 1 .. 10;
   --  subtype S is T range 2 .. 8;
   -- then
   --  GetRootType (T) = T -- identity
   --  GetRootType (S) = T
   --
   -- For array and record subtypes:
   --  type A is array (...) of ... ; -- full type declaration
   --  subtype A2 is A;
   -- then
   --  GetRootType (A) = A -- identity
   --  GetRootType (A2) = A
   function GetRootType (TypeMark : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   -- Returns the number of Dimensions of the given array
   -- type or subtype. GetRootType (see above) is
   -- used to step over any subtypes until the full
   -- parent type is found.
   function GetNumberOfDimensions (TypeMark : Symbol) return Positive;
   --# global in Dict;

   -- Returns the index type of the given Dimension for the given array
   -- type or subtype.  In the case of a full-range array subtype, the index
   -- type is obtained from the first constrained subtype.
   function GetArrayIndex (TypeMark  : Symbol;
                           Dimension : Positive) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetArrayComponent (TypeMark : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetNumberOfNonExtendedComponents (TheRecordType : Symbol) return Natural;
   --# global in Dict;
   -- Returns the number of record components in a record but does nor traverse a group of
   -- records modelling an extended tagged record.  The count includes the Inherit field of
   -- an extended record.

   function GetNumberOfActualComponents (TheRecordType : Symbol) return Natural;
   --# global in Dict;
   -- As above but ignore Inherit fields of extended tagged records

   function GetNumberOfComponents (TheRecordType : Symbol) return Natural;
   --# global in Dict;
   -- if the type is extended we get all the fields whether locally declared
   -- or inherited

   function GetNonExtendedRecordComponent (TheRecordType : Symbol;
                                           Number        : Positive) return Symbol;
   --# global in Dict;
   -- Returns field N of a single record (i.e ignores structured composition of records used to
   -- model tagged extended records.  If record is an extension, it cann return the "Inherit" field

   function GetRecordComponent (TheRecordType : Symbol;
                                Number        : Positive) return Symbol;
   --# global in Dict;
   -- Works for extended records as well as non-extended ones; does not ever return Inherit fields

   function GetInheritDepth (FieldName  : LexTokenManager.Lex_String;
                             RecordType : Symbol) return Natural;
   --# global in Dict;
   --#        in LexTokenManager.State;
   -- Assuming we have used LookUpSelectedItem and established that there is a field
   -- called FieldName in record RecordType we can use this function to find out
   -- how far FieldName is down a chain of inherit-from-root-type pointers.  So if
   -- R.F directly exists we return 0, and if R.F actually represents R.Inherit.F then we get
   -- 1 and so on

   function RecordComponentIsInherited (TheComponent : Symbol) return Boolean;
   --# global in Dict;
   -- returns true for extended types where a field is inherited rather than
   -- explicitly declared

   function GetVariableExpNode (Variable : Symbol) return ExaminerConstants.RefType;
   --# global in Dict;

   function GetConstantExpNode (TheConstant : Symbol) return ExaminerConstants.RefType;
   --# global in Dict;

   function ConstantExpIsWellformed (TheConstant : Symbol) return Boolean;
   --# global in Dict;

   function Get_Value (The_Constant : Symbol) return LexTokenManager.Lex_String;
   --# global in Dict;

   function GetConstantRulePolicy (TheConstant : Symbol;
                                   TheScope    : Scopes) return Rule_Policies;
   --# global in Dict;

   function IsConstantRulePolicyPresent (TheConstant : Symbol;
                                         TheScope    : Scopes) return Boolean;
   --# global in Dict;

   function TypeIsWellformed (TheType : Symbol) return Boolean;
   --# global in Dict;

   function GetPredefinedPackageStandard return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsPackage (S, Dict));

   function IsPredefinedPackageStandard (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function GetPredefinedPackageASCII return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsPackage (S, Dict));

   function GetOwner (Variable : Symbol) return Symbol;
   --# global in Dict;

   function LastMostEnclosingLoop (CompilationUnit : Symbol) return Symbol;
   --# global in Dict;

   function GetLoop (CompilationUnit : Symbol;
                     Number          : Positive) return Symbol;
   --# global in Dict;

   function GetLoopParameter (TheLoop : Symbol) return Symbol;
   --# global in Dict;

   -- Returns a Cells.Cell previously planted by the VCG and representing
   -- the exit expression of a for loop
   function GetLoopExitExpn (TheLoop : Symbol) return Natural;
   --# global in Dict;

   -- Returns a Cells.Cell previously planted by the VCG and representing
   -- the entry expression of a for loop
   function GetLoopEntryExpn (TheLoop : Symbol) return Natural;
   --# global in Dict;

   function GetLoopHasExits (TheLoop : Symbol) return Boolean;
   --# global in Dict;

   function LoopParameterHasStaticRange (TheLoopParameter : Symbol) return Boolean;
   --# global in Dict;

   function LoopParameterMovesInReverse (TheLoopParameter : Symbol) return Boolean;
   --# global in Dict;

   function GetScope (Item : Symbol) return Scopes;
   --# global in Dict;

   function GetEnclosingScope (Scope : Scopes) return Scopes;
   --# global in Dict;

   function GetEnclosingPackage (Scope : Scopes) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsPackage (S, Dict));

   function GetEnclosingProtectedRegion (Scope : Scopes) return Symbol;
   --# global in Dict;

   function IsOrIsInProtectedScope (Scope : Scopes) return Boolean;
   --# global in Dict;

   function SubprogramSignatureIsWellformed (Abstraction : Abstractions;
                                             Subprogram  : Symbol) return Boolean;
   --# global in Dict;

   function HasPrecondition (Abstraction : Abstractions;
                             Subprogram  : Symbol) return Boolean;
   --# global in Dict;
   -- NOTE: a task type is allowed but always returns False since tasks don't have preconditions

   function GetPrecondition (Abstraction : Abstractions;
                             Subprogram  : Symbol) return ExaminerConstants.RefType;
   --# global in Dict;
   -- NOTE: a task type is allowed but always returns 0 since tasks don't have preconditions

   function HasPostcondition (Abstraction : Abstractions;
                              Subprogram  : Symbol) return Boolean;
   --# global in Dict;

   function GetPostcondition (Abstraction : Abstractions;
                              Subprogram  : Symbol) return ExaminerConstants.RefType;
   --# global in Dict;

   function HasImplicitReturnVariable (Abstraction : Abstractions;
                                       TheFunction : Symbol) return Boolean;
   --# global in Dict;

   function GetImplicitReturnVariable (Abstraction : Abstractions;
                                       TheFunction : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsImplicitReturnVariable (S, Dict));

   function GetAdaFunction (ProofFunction : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsSubprogram (S, Dict));

   function GetImplicitProofFunction (Abstraction : Abstractions;
                                      TheFunction : Symbol) return Symbol;
   --# global in Dict;

   function GetSubprogramParameterNumber (Parameter : Symbol) return Positive;
   --# global in Dict;

   function GetSubprogramParameterMode (Parameter : Symbol) return Modes;
   --# global in Dict;

   function GetSubprogramParameterConstraint (Parameter : Symbol;
                                              Dimension : Positive) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsParameterConstraint (S, Dict));
   -- Returns the symbol for x__index_subtype__n where x is the paraeter and n the dimension number. This is
   -- a symbol with discriminant ParameterConstraintSymbol and which is used to pass information about
   -- unconstrained parameters between the wffs and the VCG.  Pseudo annotation describes normal behaviour; an
   -- illegal SPARK program might result in calls being made which violate the "precondition", in which case
   -- the unknown type mark is returned.

   function GetSubprogramParameterConstraintDimension (TheConstraint : Symbol) return Positive;
   --# global in Dict;

   function GetParameterAssociatedWithParameterConstraint (TheConstraint : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsSubprogramParameter (S, Dict));

   function GetNumberOfSubprogramParameters (Subprogram : Symbol) return Natural;
   --# global in Dict;

   function GetSubprogramParameter (Subprogram : Symbol;
                                    Number     : Positive) return Symbol;
   --# global in Dict;

   function GetNumberOfGlobalVariables (Abstraction : Abstractions;
                                        Subprogram  : Symbol) return Natural;
   --# global in Dict;

   function GetGlobalMode
     (Abstraction : Abstractions;
      Subprogram  : Symbol;
      Variable    : Symbol)
     return        Modes;
   --# global in Dict;

   function GetOwnVariableMode (Variable : Symbol) return Modes;
   --# global in Dict;

   function GetOwnVariableProtected (Variable : Symbol) return Boolean;
   --# global in Dict;

   function GetOwnVariableIsInterruptStream (Variable : Symbol) return Boolean;
   --# global in Dict;

   function GetOwnVariableTypeHere (OwnVariable : in Symbol;
                                    Scope       : in Scopes) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsTypeMark (S, Dict));

   function GetConstituentMode (Variable : Symbol) return Modes;
   --# global in Dict;

   function IsOwnVariableOrConstituentWithMode (Variable : Symbol) return Boolean;
   --# global in Dict;

   function GetProtectedTypeOwnVariable (TheProtectedType : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsVariable (S, Dict));
   --  return "the implicitly-declared abstract own variable that belongs to the PT"

   function IsUnmodedProtectedOwnVariable (Sym : Symbol) return Boolean;
   --# global in Dict;

   function GetProtectedImplicitInStream (TheProtectedOwnVar : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsImplicitInStream (S, Dict));
   -- Failure to observe precondtion will result in a null symbol being returned or dict crash.

   function GetProtectedTypeHasEntry (TheProtectedType : Symbol) return Boolean;
   --# global in Dict;

   function GetTypeHasPragma (TheProtectedOrTaskType : in Symbol;
                              ThePragma              : in RavenscarPragmas) return Boolean;
   --# global in Dict;

   function GetTypePragmaValue
     (TheProtectedOrTaskType : in Symbol;
      ThePragma              : in RavenscarPragmasWithValue)
     return                   LexTokenManager.Lex_String;
   --# global in Dict;

   function GetTypePriority (TheProtectedOrTaskType : in Symbol) return LexTokenManager.Lex_String;
   --# global in Dict;

   function GetPriorityProperty (OwnVariable : in Symbol) return LexTokenManager.Lex_String;
   --# global in Dict;

   -- If IsOwnVariable (S), then returns the Integrity of that
   -- own var (which could be of a library package, nested package,
   -- or private child package.) Otherwise, returns Null_String.
   function GetIntegrityProperty (S : in Symbol) return LexTokenManager.Lex_String;
   --# global in Dict;

   -- Implements information flow policy checking based on the Integrity
   -- property of the given import and export symbol.  CommandLineData is
   -- used to determine which info flow policy (if any) if being checked.
   function RelationViolatesInfoFlowPolicy (TheExport : in Symbol;
                                            TheImport : in Symbol) return Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;
   --#        in LexTokenManager.State;

   function GetIsSuspendable (Variable : in Symbol) return Boolean;
   --# global in Dict;

   function GetHasInterruptProperty (Variable : in Symbol) return Boolean;
   --# global in Dict;

   function GetVirtualElementOwner (Variable : in Symbol) return Symbol;
   --# global in Dict;

   function IsVirtualElement (Variable : in Symbol) return Boolean;
   --# global in Dict;

   function IsVirtualElementForType (TheVariable      : in Symbol;
                                     TheProtectedType : in Symbol) return Boolean;
   --# global in Dict;

   function VirtualElementSeenByOwner (Variable : in Symbol) return Boolean;
   --# global in Dict;

   function GetMainProgram return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsSubprogram (S, Dict));

   function GetMainProgramPriority return  LexTokenManager.Lex_String;
   --# global in Dict;

   function GetAbstraction (Subprogram : Symbol;
                            Scope      : Scopes) return Abstractions;
   --# global in Dict;

   function GetConstraintAbstraction (Subprogram : Symbol;
                                      Scope      : Scopes) return Abstractions;
   --# global in Dict;
   -- Similar above but selects which subprgoram constraint to use.  May return different
   -- result to GetAbstraction because a subprogram may have only one flow annotation
   -- but have two proof contexts (if private type refinement is involved).

   procedure AdjustTypeUpperBound (TypeMark : Symbol;
                                   NewBound : LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   NewBound,
   --#                   TypeMark;

   procedure AdjustTypeLowerBound (TypeMark : Symbol;
                                   NewBound : LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   NewBound,
   --#                   TypeMark;

   procedure AdjustTypeErrorBound (TypeMark : Symbol;
                                   NewBound : LexTokenManager.Lex_String);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   NewBound,
   --#                   TypeMark;

   -- **********************************************************************
   -- NB: the three above operations are not intended for general use,
   --     and are present for the benefit of the ConfigFile package.
   -- **********************************************************************

   --------------------------------------------------------------------------------
   --                              QUERY FUNCTIONS                               --
   --------------------------------------------------------------------------------

   function IsObject (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function Is_Declared (Item : Symbol) return Boolean;
   --# global in Dict;

   function Is_Constant (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function Is_Variable (TheSymbol : Symbol) return Boolean;
   --# global in Dict;
   -- Note, returns false for a record subcomponent

   function IsVariableOrSubcomponent (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function GetFirstRecordSubcomponent (TheSymbol : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsSubcomponent (S, Dict));

   function GetNextRecordSubcomponent (TheSubcomponent : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsSubcomponent (S, Dict));

   function VariableIsInitialized (Variable : Symbol) return Boolean;
   --# global in Dict;

   function VariableHasAddressClause (Variable : Symbol) return Boolean;
   --# global in Dict;

   function VariableHasPragmaImport (Variable : Symbol) return Boolean;
   --# global in Dict;

   function TypeSizeAttribute (TypeMark : Symbol) return LexTokenManager.Lex_String;
   --# global in Dict;

   function VariableIsAliased (Variable : Symbol) return Boolean;
   --# global in Dict;

   procedure SetVariableMarkedValid (Variable : in Symbol;
                                     Val      : in Boolean);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Val,
   --#                   Variable;

   function VariableIsMarkedValid (TheVariable : Symbol) return Boolean;
   --# global in Dict;

   procedure SetSubcomponentMarkedValid (Subcomponent : in Symbol;
                                         Val          : in Boolean);
   --# global in out Dict;
   --# derives Dict from *,
   --#                   Subcomponent,
   --#                   Val;

   function SubcomponentIsMarkedValid (TheSubcomponent : Symbol) return Boolean;
   --# global in Dict;

   function VariableOrSubcomponentIsMarkedValid (TheSym : Symbol) return Boolean;
   --# global in Dict;

   function IsAtomic (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsPragmaAtomic (TheSymbol : Symbol) return Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;

   function IsDeferredConstant (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function ConstantIsDeferredHere (TheConstant : Symbol;
                                    Scope       : Scopes) return Boolean;
   --# global in Dict;

   function IsUnknownTypeMark (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsUniversalIntegerType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsUniversalRealType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   -- True iff IsTypeMark (TheSymbol) and ISN'T UnknownType and
   -- ISN'T a subtype
   function IsType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsSubtype (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsTaskType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsProtectedType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsProtectedTypeMark (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsProtectedFunction (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function CompatibleTypes
     (Scope : Scopes;
      Left  : Symbol;
      Right : Symbol)
     return  Boolean;
   --# global in Dict;

   function IsScalarTypeMark (TheSymbol : Symbol;
                              Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsDiscreteTypeMark (TheSymbol : Symbol;
                                Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsIntegerTypeMark (TheSymbol : Symbol;
                               Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsModularTypeMark (TheSymbol : Symbol;
                               Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsRealTypeMark (TheSymbol : Symbol;
                            Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsFixedPointTypeMark (TheSymbol : Symbol;
                                  Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsFloatingPointTypeMark (TheSymbol : Symbol;
                                     Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsArrayTypeMark (TheSymbol : Symbol;
                             Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsRecordTypeMark (TheSymbol : Symbol;
                              Scope     : Scopes) return Boolean;
   --# global in Dict;

   function TypeIsBoolean (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsCharacter (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsEnumeration (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsInteger (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsModular (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsDiscrete (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsFixedPoint (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsFloatingPoint (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsReal (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsNumeric (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsScalar (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsRecord (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsAbstractProof (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsArray (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsAnnounced (TheType : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsPrivate (TheType : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsTagged (TheType : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsExtendedTagged (TheType : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsTask (TheType : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsAccess (TheType : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsGeneric (TheType : Symbol) return Boolean;
   --# global in Dict;

   function ExtendedTaggedHasPrivateAncestors (TheType : Symbol;
                                               Scope   : Scopes) return Boolean;
   --# global in Dict;

   function IsAnExtensionOf (RootType, ExtendedType : Symbol) return Boolean;
   --# global in Dict;

   function NoFieldsBelowThisRecord (RecordSym : Symbol) return Boolean;
   --# global in Dict;
   -- Returns true for an extended record if all its inherited records are null
   -- extensions or null records

   function RecordHasSomeFields (RecordSym : Symbol) return Boolean;
   --# global in Dict;
   -- return true if a record either has soem fields itself or it inherits some from an
   -- ancestor type

   function ContainsFloat (TypeMark : Symbol) return Boolean;
   --# global in Dict;

   function GetEnclosingCompilationUnit (Scope : Scopes) return Symbol;
   --# global in Dict;

   function LoopHasName (TheLoop : Symbol) return Boolean;
   --# global in Dict;
   --#        in LexTokenManager.State;

   function GetLoopNumber (TheLoop : Symbol) return Positive;
   --# global in Dict;

   function IsPrivateTypeMark (TheSymbol : Symbol;
                               Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsPrivateType (TheSymbol : Symbol;
                           Scope     : Scopes) return Boolean;
   --# global in Dict;

   -- Returns True iff the given Type is INCOMPLETE
   -- the point of view of the given Scope.
   function TypeIsIncompleteHere (TypeMark : Symbol;
                                  Scope    : Scopes) return Boolean;
   --# global in Dict;

   function IsLimitedPrivateType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function TypeIsLimited (TypeMark : Symbol;
                           Scope    : Scopes) return Boolean;
   --# global in Dict;

   function TypeIsOwnAbstractHere (TypeMark : in Symbol;
                                   Scope    : in Scopes) return Boolean;
   --# global in Dict;

   function IsStatic (Item  : Symbol;
                      Scope : Scopes) return Boolean;
   --# global in Dict;

   function IsScalarType (TheSymbol : Symbol;
                          Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsNumericType (TheSymbol : Symbol;
                           Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsIntegerType (TheSymbol : Symbol;
                           Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsModularType (TheSymbol : Symbol;
                           Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsFixedPointType (TheSymbol : Symbol;
                              Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsFloatingPointType (TheSymbol : Symbol;
                                 Scope     : Scopes) return Boolean;
   --# global in Dict;

   function Is_Constrained_Array_Type_Mark (TheSymbol : Symbol;
                                            Scope     : Scopes) return Boolean;
   --# global in Dict;

   function Is_Unconstrained_Array_Type_Mark (TheSymbol : Symbol;
                                              Scope     : Scopes) return Boolean;
   --# global in Dict;

   function IsUnconstrainedArrayType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsUnconstrainedTaskType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsUnconstrainedProtectedType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsRecordComponent (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function GetEnclosingObject (Object : Symbol) return Symbol;
   --# global in Dict;

   function GetMostEnclosingObject (Object : Symbol) return Symbol;
   --# global in Dict;

   function DefinedInPackageStandard (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsPredefined (TheSymbol : Symbol) return Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;
   -- Returns true if the scope of the symbol is the visible scope of any of the
   -- following predefined packages:
   -- STANDARD
   -- ASCII
   -- Ada                           -- Ada95
   -- Ada.Characters                -- Ada95
   -- Ada.Characters.Latin_1        -- Ada95
   -- Ada.Real_Time                 -- Ravenscar
   -- Ada.Synchronous_Task_Control, -- Ravenscar
   -- Ada.Interrupts                -- Ravenscar

   function IsPredefinedIntegerType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsPredefinedFloatType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsPredefinedCharacterType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsPredefinedStringType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsPredefinedTimeType (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsPredefinedSuspensionObjectType (TheSymbol : Symbol) return Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;

   function IsPredefinedSuspendUntilTrueOperation (TheProcedure : Symbol) return Boolean;
   --# global in Dict;

   function IsPredefinedRealTimeClockOperation (TheProcedure : Symbol) return Boolean;
   --# global in Dict;

   function IsCompilationUnit (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function Is_Withed (The_Withed_Symbol : Symbol;
                       Scope             : Scopes) return Boolean;
   --# global in Dict;

   function Is_Withed_Locally (The_Withed_Symbol : Symbol;
                               Scope             : Scopes) return Boolean;
   --# global in Dict;

   function IsUsedLocally (TheType : Symbol;
                           Scope   : Scopes) return Boolean;
   --# global in Dict;

   function IsInherited (ThePackage, CompilationUnit : Symbol) return Boolean;
   --# global in Dict;

   function Is_Generic_Subprogram (The_Symbol : Symbol) return Boolean;
   --# global in Dict;

   function IsFunction (TheSymbol : Symbol) return Boolean;
   --# global in Dict;
   --# return S => (S -> Is_Subprogram (TheSymbol, Dict));

   function IsEntry (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function GetSubprogramEntryBarrier (Subprogram : Symbol) return Symbol;
   --# global in Dict;
   -- return Entries Booelan variable barrier symbol if there is one, else null sym

   function IsInterruptHandler (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsAnUncheckedConversion (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function UsesUncheckedConversion (TheUnit : Symbol) return Boolean;
   --# global in Dict;

   function AssignsFromExternal (TheUnit : Symbol) return Boolean;
   --# global in Dict;

   function IsProcedure (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsProofConstant (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsAdaFunction (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsProofFunction (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function Is_Renamed (Subprogram : Symbol;
                        Scope      : Scopes) return Boolean;
   --# global in Dict;

   function SetsPriority (TheDiscriminant : Symbol) return Boolean;
   --# global in Dict;

   function IsFormalParameter (Subprogram, Parameter : Symbol) return Boolean;
   --# global in Dict;

   function IsGenericFormalParameter (TheGeneric, Parameter : Symbol) return Boolean;
   --# global in Dict;

   function HasBody (CompilationUnit : Symbol) return Boolean;
   --# global in Dict;

   function HasBodyStub (CompilationUnit : Symbol) return Boolean;
   --# global in Dict;

   function Is_Global_Variable
     (Abstraction : Abstractions;
      Subprogram  : Symbol;
      Variable    : Symbol)
     return        Boolean;
   --# global in Dict;

   function IsImportExport
     (Abstraction  : Abstractions;
      TheProcedure : Symbol;
      Variable     : Symbol)
     return         Boolean;
   --# global in Dict;

   function IsExport
     (Abstraction  : Abstractions;
      TheProcedure : Symbol;
      Variable     : Symbol)
     return         Boolean;
   --# global in Dict;

   function IsImport
     (Abstraction  : Abstractions;
      TheProcedure : Symbol;
      Variable     : Symbol)
     return         Boolean;
   --# global in Dict;

   function IsArrayAttribute (Name     : LexTokenManager.Lex_String;
                              TypeMark : Symbol) return Boolean;
   --# global in Dict;
   --#        in LexTokenManager.State;

   function IsEmbeddedPackage (TheSymbol : Symbol) return Boolean;
   --# global in Dict;

   function IsOwnVariable (Variable : Symbol) return Boolean;
   --# global in Dict;

   function IsOwnTask (Variable : Symbol) return Boolean;
   --# global in Dict;

   function IsRefinedOwnVariable (Variable : Symbol) return Boolean;
   --# global in Dict;

   function OwnVariableHasType (OwnVariable : Symbol;
                                Scope       : Scopes) return Boolean;
   --# global in Dict;

   function OwnVariableIsAnnounced (Variable : Symbol) return Boolean;
   --# global in Dict;

   function OwnVariableIsInitialized (Variable : Symbol) return Boolean;
   --# global in Dict;

   function OwnVariableHasConstituents (Variable : Symbol) return Boolean;
   --# global in Dict;

   function IsConcreteOwnVariable (Variable : Symbol) return Boolean;
   --# global in Dict;

   function IsRefinement (Subject, Constituent : Symbol) return Boolean;
   --# global in Dict;

   function IsRefinementConstituent (ThePackage, Variable : Symbol) return Boolean;
   --# global in Dict;

   function IsConstituent (Variable : Symbol) return Boolean;
   --# global in Dict;

   function GetSubject (Constituent : Symbol) return Symbol;
   --# global in Dict;
   --# return S => (Is_Null_Symbol (S) or IsVariable (S, Dict));

   function HasDelayProperty (TheProcedure : Symbol) return Boolean;
   --# global in Dict;

   function DelayPropertyIsAccountedFor (TheProcedure : Symbol) return Boolean;
   --# global in Dict;

   function HasValidPriorityProperty (OwnVariable : Symbol) return Boolean;
   --# global in Dict;

   function IsThread (Sym : in Symbol) return Boolean;
   --# global in Dict;

   function UsesUnprotectedVariables (Sym : in Symbol) return Boolean;
   --# global in Dict;

   function GetUnprotectedReference (Variable : in Symbol) return Symbol;
   --# global in Dict;

   function GetSuspendsReference (Variable : in Symbol) return Symbol;
   --# global in Dict;

   function SuspendsOn (TheTaskOrProc : Symbol;
                        ThePOorSO     : Symbol) return Boolean;
   --# global in Dict;

   function SuspendsListItemIsAccountedFor (TheTaskOrProc : Symbol;
                                            ThePOorSO     : Symbol) return Boolean;
   --# global in Dict;

   function SuspendsListIsPropagated (FromProcedure : Symbol;
                                      ToTaskOrProc  : Symbol) return Boolean;
   --# global in Dict;

   function SubprogramMayBlock (Subprogram : Symbol) return Boolean;
   --# global in Dict;

   function BodyIsHidden (Sym : Symbol) return Boolean;
   --# global in Dict;

   -- Returns true to indicate that a procedure or task has an explicit
   -- derives annotation (rather than a synthesised one).
   function GetHasDerivesAnnotation (Task_Or_Proc : Symbol) return Boolean;
   --# global in Dict;

   function IsMainProgram (Subprogram : Symbol) return Boolean;
   --# global in Dict;

   function IsThePartition (Subprogram : Symbol) return Boolean;
   --# global in Dict;

   -- Returns True iff Sym is a program unit as defined by
   -- Ada95 LRM Annex N.31.  Used to check the legality of
   -- adddress representation clauses.  This definition also
   -- seems to be consistent with that given in Ada83 LRM 13.1(4).
   function IsProgramUnit (Sym : Symbol) return Boolean;
   --# global in Dict;

   function MainProgramExists return Boolean;
   --# global in Dict;

   function MainProgramPrioritySupplied return Boolean;
   --# global in Dict;

   function PackageRequiresBody (ThePackage : Symbol) return Boolean;
   --# global in CommandLineData.Content;
   --#        in Dict;

   function GetInterruptStreamVariable (ProtectedObject  : in Symbol;
                                        InterruptHandler : in Symbol) return Symbol;
   --# global in CommandLineData.Content;
   --#        in Dict;
   --#        in LexTokenManager.State;

   --------------------------------------------------------------------------------
   --                                 ITERATORS                                  --
   --------------------------------------------------------------------------------

   function CurrentSymbol (CurrentIterator : Iterator) return Symbol;
   --# global in Dict;

   function NextSymbol (Previous : Iterator) return Iterator;
   --# global in Dict;

   function IsNullIterator (Current : Iterator) return Boolean;

   function First_Deferred_Constant (The_Package : Symbol) return Iterator;
   --# global in Dict;

   function FirstArrayIndex (TypeMark : Symbol) return Iterator;
   --# global in Dict;

   function First_Undeclared_Type (The_Package : Symbol) return Iterator;
   --# global in Dict;

   function First_Private_Type (The_Package : Symbol) return Iterator;
   --# global in Dict;

   function FirstEnumerationLiteral (EnumerationType : Symbol) return Iterator;
   --# global in Dict;

   function FirstRecordComponent (TheRecordType : Symbol) return Iterator;
   --# global in Dict;
   -- N.B. This iterator works over a single record; if you want to iterate
   --      over a group of records modelling extension of tagged types then
   --      use the following function instead.

   function FirstExtendedRecordComponent (TheRecordType : Symbol) return Iterator;
   --# global in Dict;

   function First_Visible_Subprogram (The_Package_Or_Type : Symbol) return Iterator;
   --# global in Dict;

   function First_Private_Subprogram (The_Package : Symbol) return Iterator;
   --# global in Dict;

   function First_Visible_Task_Type (The_Package : Symbol) return Iterator;
   --# global in Dict;

   function First_Private_Task_Type (The_Package : Symbol) return Iterator;
   --# global in Dict;

   function FirstOwnTask (ThePackage : Symbol) return Iterator;
   --# global in Dict;

   function First_Visible_Protected_Type (The_Package : Symbol) return Iterator;
   --# global in Dict;

   function First_Private_Protected_Type (The_Package : Symbol) return Iterator;
   --# global in Dict;

   function FirstSubprogramParameter (Subprogram : Symbol) return Iterator;
   --# global in Dict;

   function FirstGenericFormalParameter (TheGeneric : Symbol) return Iterator;
   --# global in Dict;

   function GetNumberOfGenericFormalParameters (TheGeneric : Symbol) return Natural;
   --# global in Dict;

   function GetGenericFormalParameterKind (TheGenericFormalParameter : Symbol) return Generic_Parameter_Kind;
   --# global in Dict;

   function FirstKnownDiscriminant (ProtectedOrTaskType : Symbol) return Iterator;
   --# global in Dict;

   function FirstGlobalVariable (Abstraction : Abstractions;
                                 Subprogram  : Symbol) return Iterator;
   --# global in Dict;

   function First_Local_Variable (Subprogram : Symbol) return Iterator;
   --# global in Dict;

   function First_Initialized_Variable (Subprogram : Symbol) return Iterator;
   --# global in Dict;

   function FirstProtectedElement (The_Protected_Type : Symbol) return Iterator;
   --# global in Dict;

   function FirstImportExport (Abstraction  : Abstractions;
                               TheProcedure : Symbol) return Iterator;
   --# global in Dict;

   function FirstExport (Abstraction  : Abstractions;
                         TheProcedure : Symbol) return Iterator;
   --# global in Dict;

   function FirstImport (Abstraction  : Abstractions;
                         TheProcedure : Symbol) return Iterator;
   --# global in Dict;

   function FirstDependency
     (Abstraction  : Abstractions;
      TheProcedure : Symbol;
      TheExport    : Symbol)
     return         Iterator;
   --# global in Dict;

   function FirstSuspendsListItem (TheTaskOrProc : Symbol) return Iterator;
   --# global in Dict;

   function FirstVirtualElement (TheProtectedType : Symbol) return Iterator;
   --# global in Dict;

   function FirstOwnedPackage (ThePackage : Symbol) return Iterator;
   --# global in Dict;

   function First_Embedded_Package (Compilation_Unit : Symbol) return Iterator;
   --# global in Dict;

   function FirstOwnVariable (ThePackage : Symbol) return Iterator;
   --# global in Dict;

   function FirstInitializedOwnVariable (ThePackage : Symbol) return Iterator;
   --# global in Dict;

   function FirstConstituent (Subject : Symbol) return Iterator;
   --# global in Dict;

   function FirstInheritsClause (Sym : Symbol) return Iterator;
   --# global in Dict;

   function FirstInterruptStreamMapping (Sym : Symbol) return Iterator;
   --# global in Dict;

   function FirstLoopOnEntryVar (TheLoop : Symbol) return Iterator;
   --# global in Dict;
   -- returns first variable used in exit expression of for loop

   function GetInterruptStreamMappingHandler (TheMapping : in Symbol) return LexTokenManager.Lex_String;

   function GetInterruptStreamMappingStream (TheMapping : in Symbol) return LexTokenManager.Lex_String;

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

private
   --  We allocate SymbolTableSize entries for user-defined Symbols,
   --  plus sentinel value 0 for NullSymbol
   type Symbol is range 0 .. Natural'Last;
   --# assert Symbol'Base is Integer;

   NullSymbol : constant Symbol := Symbol'First;

   type IteratorDiscriminant is (
                                 NullSymIterator,
                                 DeclarativeItemIterator,
                                 DeferredConstantIterator,
                                 ArrayIndexIterator,
                                 LoopIterator,
                                 UndeclaredTypeIterator,
                                 PrivateTypeIterator,
                                 EnumerationLiteralIterator,
                                 RecordComponentIterator,
                                 ExtendedRecordComponentIterator,
                                 LibraryUnitIterator,
                                 WithedPackageIterator,
                                 InheritedPackageIterator,
                                 VisibleSubprogramIterator,
                                 PrivateSubprogramIterator,
                                 TaskTypeIterator,
                                 OwnTaskIterator,
                                 ProtectedTypeIterator,
                                 SubprogramParameterIterator,
                                 GenericFormalParameterIterator,
                                 KnownDiscriminantIterator,
                                 DiscriminantConstraintIterator,
                                 ImplicitProofFunctionParameterIterator,
                                 ImplicitProofFunctionGlobalIterator,
                                 GlobalVariableIterator,
                                 LocalVariableIterator,
                                 InitializedVariableIterator,
                                 ImportExportIterator,
                                 ExportIterator,
                                 ImportIterator,
                                 DependencyIterator,
                                 InterruptStreamMappingIterator,
                                 SuspendsListItemIterator,
                                 VirtualElementIterator,
                                 OwnedPackageIterator,
                                 ProtectedElementIterator,
                                 LoopOnEntryVarIterator,
                                 EmbeddedPackageIterator,
                                 -- see Dictionary.CurrentSymbol before adding to this list, position matters
                                 OwnVariableIterator,
                                 InitializedOwnVariableIterator,
                                 AbstractOwnVariableIterator,
                                 -- see Dictionary.CurrentSymbol before adding to this list, position matters
                                 ConstituentIterator);

   type Iterator is record
      Discriminant : IteratorDiscriminant;
      Abstraction  : Abstractions;
      Current      : Symbol;
      Context      : Symbol;
   end record;

   NullIterator : constant Iterator := Iterator'(NullSymIterator, IsAbstract, NullSymbol, NullSymbol);

   --  If you change this, please also change
   --  Cells.Utility.Create_Scope_Cell and
   --  Cells.Utility.Scope_Cell_Get_Scope.
   type Scopes is record
      The_Visibility : Visibility;
      The_Unit       : Symbol;
   end record;

   NullScope : constant Scopes := Scopes'(The_Visibility => Visible,
                                          The_Unit       => NullSymbol);
end Dictionary;