Index: sem_spark.adb
===================================================================
--- sem_spark.adb	(revision 0)
+++ sem_spark.adb	(revision 0)
@@ -0,0 +1,6188 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                            S E M _ S P A R K                             --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--          Copyright (C) 2017, Free Software Foundation, Inc.              --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT 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 GNAT; see file COPYING3.  If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license.          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+with Atree;    use Atree;
+with Einfo;    use Einfo;
+with Errout;   use Errout;
+with Namet;    use Namet;
+with Nlists;   use Nlists;
+with Opt;      use Opt;
+with Osint;    use Osint;
+with Sem_Prag; use Sem_Prag;
+with Sem_Util; use Sem_Util;
+with Sem_Aux;  use Sem_Aux;
+with Sinfo;    use Sinfo;
+with Snames;   use Snames;
+with Treepr;   use Treepr;
+
+with Ada.Unchecked_Deallocation;
+with GNAT.Dynamic_HTables; use GNAT.Dynamic_HTables;
+
+package body Sem_SPARK is
+
+   -------------------------------------------------
+   -- Handling of Permissions Associated to Paths --
+   -------------------------------------------------
+
+   package Permissions is
+      Elaboration_Context_Max : constant := 1009;
+      --  The hash range
+
+      type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
+
+      function Elaboration_Context_Hash
+        (Key : Entity_Id) return Elaboration_Context_Index;
+      --  Function to hash any node of the AST
+
+      type Perm_Kind is (No_Access, Read_Only, Read_Write, Write_Only);
+      --  Permission type associated with paths
+
+      subtype Read_Perm is Perm_Kind range Read_Only .. Read_Write;
+      subtype Write_Perm is Perm_Kind range Read_Write .. Write_Only;
+
+      type Perm_Tree_Wrapper;
+
+      type Perm_Tree_Access is access Perm_Tree_Wrapper;
+      --  A tree of permissions is defined, where the root is a whole object
+      --  and tree branches follow access paths in memory. As Perm_Tree is a
+      --  discriminated record, a wrapper type is used for the access type
+      --  designating a subtree, to make it unconstrained so that it can be
+      --  updated.
+
+      --  Nodes in the permission tree are of different kinds
+
+      type Path_Kind is
+        (Entire_Object,    --  Scalar object, or folded object of any type
+         Reference,        --  Unfolded object of access type
+         Array_Component,  --  Unfolded object of array type
+         Record_Component  --  Unfolded object of record type
+        );
+
+      package Perm_Tree_Maps is new Simple_HTable
+        (Header_Num => Elaboration_Context_Index,
+         Key        => Node_Id,
+         Element    => Perm_Tree_Access,
+         No_Element => null,
+         Hash       => Elaboration_Context_Hash,
+         Equal      => "=");
+      --  The instantation of a hash table, with keys being nodes and values
+      --  being pointers to trees. This is used to reference easily all
+      --  extensions of a Record_Component node (that can have name x, y, ...).
+
+      --  The definition of permission trees. This is a tree, which has a
+      --  permission at each node, and depending on the type of the node,
+      --  can have zero, one, or more children pointed to by an access to tree.
+      type Perm_Tree (Kind : Path_Kind := Entire_Object) is record
+         Permission : Perm_Kind;
+         --  Permission at this level in the path
+
+         Is_Node_Deep : Boolean;
+         --  Whether this node is of a deep type, to be used when moving the
+         --  path.
+
+         case Kind is
+
+            --  An entire object is either a leaf (an object which cannot be
+            --  extended further in a path) or a subtree in folded form (which
+            --  could later be unfolded further in another kind of node). The
+            --  field Children_Permission specifies a permission for every
+            --  extension of that node if that permission is different from
+            --  the node's permission.
+
+            when Entire_Object    =>
+               Children_Permission : Perm_Kind;
+
+            --  Unfolded path of access type. The permission of the object
+            --  pointed to is given in Get_All.
+
+            when Reference        =>
+               Get_All : Perm_Tree_Access;
+
+            --  Unfolded path of array type. The permission of the elements is
+            --  given in Get_Elem.
+
+            when Array_Component  =>
+               Get_Elem : Perm_Tree_Access;
+
+            --  Unfolded path of record type. The permission of the regular
+            --  components is given in Component. The permission of unknown
+            --  components (for objects of tagged type) is given in
+            --  Other_Components.
+
+            when Record_Component =>
+               Component : Perm_Tree_Maps.Instance;
+               Other_Components : Perm_Tree_Access;
+         end case;
+      end record;
+
+      type Perm_Tree_Wrapper is record
+         Tree : Perm_Tree;
+      end record;
+      --  We use this wrapper in order to have unconstrained discriminants
+
+      type Perm_Env is new Perm_Tree_Maps.Instance;
+      --  The definition of a permission environment for the analysis. This
+      --  is just a hash table of permission trees, each of them rooted with
+      --  an Identifier/Expanded_Name.
+
+      type Perm_Env_Access is access Perm_Env;
+      --  Access to permission environments
+
+      package Env_Maps is new Simple_HTable
+        (Header_Num => Elaboration_Context_Index,
+         Key        => Entity_Id,
+         Element    => Perm_Env_Access,
+         No_Element => null,
+         Hash       => Elaboration_Context_Hash,
+         Equal      => "=");
+      --  The instantiation of a hash table whose elements are permission
+      --  environments. This hash table is used to save the environments at
+      --  the entry of each loop, with the key being the loop label.
+
+      type Env_Backups is new Env_Maps.Instance;
+      --  The type defining the hash table saving the environments at the entry
+      --  of each loop.
+
+      package Boolean_Variables_Maps is new Simple_HTable
+        (Header_Num => Elaboration_Context_Index,
+         Key        => Entity_Id,
+         Element    => Boolean,
+         No_Element => False,
+         Hash       => Elaboration_Context_Hash,
+         Equal      => "=");
+      --  These maps allow tracking the variables that have been declared but
+      --  never used anywhere in the source code. Especially, we do not raise
+      --  an error if the variable stays write-only and is declared at package
+      --  level, because there is no risk that the variable has been moved,
+      --  because it has never been used.
+
+      type Initialization_Map is new Boolean_Variables_Maps.Instance;
+
+      --------------------
+      -- Simple Getters --
+      --------------------
+
+      --  Simple getters to avoid having .all.Tree.Field everywhere. Of course,
+      --  that's only for the top access, as otherwise this reverses the order
+      --  in accesses visually.
+
+      function Children_Permission (T : Perm_Tree_Access) return Perm_Kind;
+      function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance;
+      function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access;
+      function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access;
+      function Is_Node_Deep (T : Perm_Tree_Access) return Boolean;
+      function Kind (T : Perm_Tree_Access) return Path_Kind;
+      function Other_Components (T : Perm_Tree_Access) return Perm_Tree_Access;
+      function Permission (T : Perm_Tree_Access) return Perm_Kind;
+
+      -----------------------
+      -- Memory Management --
+      -----------------------
+
+      procedure Copy_Env
+        (From : Perm_Env;
+         To : in out Perm_Env);
+      --  Procedure to copy a permission environment
+
+      procedure Copy_Init_Map
+        (From : Initialization_Map;
+         To : in out Initialization_Map);
+      --  Procedure to copy an initialization map
+
+      procedure Copy_Tree
+        (From : Perm_Tree_Access;
+         To : Perm_Tree_Access);
+      --  Procedure to copy a permission tree
+
+      procedure Free_Env
+        (PE : in out Perm_Env);
+      --  Procedure to free a permission environment
+
+      procedure Free_Perm_Tree
+        (PT : in out Perm_Tree_Access);
+      --  Procedure to free a permission tree
+
+      --------------------
+      -- Error Messages --
+      --------------------
+
+      procedure Perm_Mismatch
+        (Exp_Perm, Act_Perm : Perm_Kind;
+         N                   : Node_Id);
+      --  Issues a continuation error message about a mismatch between a
+      --  desired permission Exp_Perm and a permission obtained Act_Perm. N
+      --  is the node on which the error is reported.
+
+   end Permissions;
+
+   package body Permissions is
+
+      -------------------------
+      -- Children_Permission --
+      -------------------------
+
+      function Children_Permission
+        (T : Perm_Tree_Access)
+          return Perm_Kind
+      is
+      begin
+         return T.all.Tree.Children_Permission;
+      end Children_Permission;
+
+      ---------------
+      -- Component --
+      ---------------
+
+      function Component
+        (T : Perm_Tree_Access)
+          return Perm_Tree_Maps.Instance
+      is
+      begin
+         return T.all.Tree.Component;
+      end Component;
+
+      --------------
+      -- Copy_Env --
+      --------------
+
+      procedure Copy_Env
+        (From : Perm_Env;
+         To : in out Perm_Env)
+      is
+         Comp_From : Perm_Tree_Access;
+         Key_From : Perm_Tree_Maps.Key_Option;
+         Son : Perm_Tree_Access;
+
+      begin
+         Reset (To);
+         Key_From := Get_First_Key (From);
+         while Key_From.Present loop
+            Comp_From := Get (From, Key_From.K);
+            pragma Assert (Comp_From /= null);
+
+            Son := new Perm_Tree_Wrapper;
+            Copy_Tree (Comp_From, Son);
+
+            Set (To, Key_From.K, Son);
+            Key_From := Get_Next_Key (From);
+         end loop;
+      end Copy_Env;
+
+      -------------------
+      -- Copy_Init_Map --
+      -------------------
+
+      procedure Copy_Init_Map
+        (From : Initialization_Map;
+         To : in out Initialization_Map)
+      is
+         Comp_From : Boolean;
+         Key_From : Boolean_Variables_Maps.Key_Option;
+
+      begin
+         Reset (To);
+         Key_From := Get_First_Key (From);
+         while Key_From.Present loop
+            Comp_From := Get (From, Key_From.K);
+            Set (To, Key_From.K, Comp_From);
+            Key_From := Get_Next_Key (From);
+         end loop;
+      end Copy_Init_Map;
+
+      ---------------
+      -- Copy_Tree --
+      ---------------
+
+      procedure Copy_Tree
+        (From : Perm_Tree_Access;
+         To : Perm_Tree_Access)
+      is
+      begin
+         To.all := From.all;
+
+         case Kind (From) is
+            when Entire_Object =>
+               null;
+
+            when Reference =>
+               To.all.Tree.Get_All := new Perm_Tree_Wrapper;
+
+               Copy_Tree (Get_All (From), Get_All (To));
+
+            when Array_Component =>
+               To.all.Tree.Get_Elem := new Perm_Tree_Wrapper;
+
+               Copy_Tree (Get_Elem (From), Get_Elem (To));
+
+            when Record_Component =>
+               declare
+                  Comp_From : Perm_Tree_Access;
+                  Key_From : Perm_Tree_Maps.Key_Option;
+                  Son : Perm_Tree_Access;
+                  Hash_Table : Perm_Tree_Maps.Instance;
+               begin
+               --  We put a new hash table, so that it gets dealiased from the
+               --  Component (From) hash table.
+                  To.all.Tree.Component := Hash_Table;
+
+                  To.all.Tree.Other_Components :=
+                    new Perm_Tree_Wrapper'(Other_Components (From).all);
+
+                  Copy_Tree (Other_Components (From), Other_Components (To));
+
+                  Key_From := Perm_Tree_Maps.Get_First_Key
+                    (Component (From));
+                  while Key_From.Present loop
+                     Comp_From := Perm_Tree_Maps.Get
+                       (Component (From), Key_From.K);
+
+                     pragma Assert (Comp_From /= null);
+                     Son := new Perm_Tree_Wrapper;
+
+                     Copy_Tree (Comp_From, Son);
+
+                     Perm_Tree_Maps.Set
+                       (To.all.Tree.Component, Key_From.K, Son);
+
+                     Key_From := Perm_Tree_Maps.Get_Next_Key
+                       (Component (From));
+                  end loop;
+               end;
+         end case;
+      end Copy_Tree;
+
+      ------------------------------
+      -- Elaboration_Context_Hash --
+      ------------------------------
+
+      function Elaboration_Context_Hash
+        (Key : Entity_Id) return Elaboration_Context_Index
+      is
+      begin
+         return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
+      end Elaboration_Context_Hash;
+
+      --------------
+      -- Free_Env --
+      --------------
+
+      procedure Free_Env (PE : in out Perm_Env) is
+         CompO : Perm_Tree_Access;
+      begin
+         CompO := Get_First (PE);
+         while CompO /= null loop
+            Free_Perm_Tree (CompO);
+            CompO := Get_Next (PE);
+         end loop;
+      end Free_Env;
+
+      --------------------
+      -- Free_Perm_Tree --
+      --------------------
+
+      procedure Free_Perm_Tree
+        (PT : in out Perm_Tree_Access)
+      is
+         procedure Free_Perm_Tree_Dealloc is
+           new Ada.Unchecked_Deallocation
+             (Perm_Tree_Wrapper, Perm_Tree_Access);
+         --  The deallocator for permission_trees
+
+      begin
+         case Kind (PT) is
+            when Entire_Object =>
+               Free_Perm_Tree_Dealloc (PT);
+
+            when Reference =>
+               Free_Perm_Tree (PT.all.Tree.Get_All);
+               Free_Perm_Tree_Dealloc (PT);
+
+            when Array_Component =>
+               Free_Perm_Tree (PT.all.Tree.Get_Elem);
+
+            when Record_Component =>
+               declare
+                  Comp : Perm_Tree_Access;
+
+               begin
+                  Free_Perm_Tree (PT.all.Tree.Other_Components);
+                  Comp := Perm_Tree_Maps.Get_First (Component (PT));
+                  while Comp /= null loop
+                     --  Free every Component subtree
+
+                     Free_Perm_Tree (Comp);
+                     Comp := Perm_Tree_Maps.Get_Next (Component (PT));
+                  end loop;
+               end;
+               Free_Perm_Tree_Dealloc (PT);
+         end case;
+      end Free_Perm_Tree;
+
+      -------------
+      -- Get_All --
+      -------------
+
+      function Get_All
+        (T : Perm_Tree_Access)
+          return Perm_Tree_Access
+      is
+      begin
+         return T.all.Tree.Get_All;
+      end Get_All;
+
+      --------------
+      -- Get_Elem --
+      --------------
+
+      function Get_Elem
+        (T : Perm_Tree_Access)
+          return Perm_Tree_Access
+      is
+      begin
+         return T.all.Tree.Get_Elem;
+      end Get_Elem;
+
+      ------------------
+      -- Is_Node_Deep --
+      ------------------
+
+      function Is_Node_Deep
+        (T : Perm_Tree_Access)
+          return Boolean
+      is
+      begin
+         return T.all.Tree.Is_Node_Deep;
+      end Is_Node_Deep;
+
+      ----------
+      -- Kind --
+      ----------
+
+      function Kind
+        (T : Perm_Tree_Access)
+          return Path_Kind
+      is
+      begin
+         return T.all.Tree.Kind;
+      end Kind;
+
+      ----------------------
+      -- Other_Components --
+      ----------------------
+
+      function Other_Components
+        (T : Perm_Tree_Access)
+          return Perm_Tree_Access
+      is
+      begin
+         return T.all.Tree.Other_Components;
+      end Other_Components;
+
+      ----------------
+      -- Permission --
+      ----------------
+
+      function Permission
+        (T : Perm_Tree_Access)
+          return Perm_Kind
+      is
+      begin
+         return T.all.Tree.Permission;
+      end Permission;
+
+      -------------------
+      -- Perm_Mismatch --
+      -------------------
+
+      procedure Perm_Mismatch
+        (Exp_Perm, Act_Perm : Perm_Kind;
+         N                   : Node_Id)
+      is
+      begin
+         Error_Msg_N ("\expected at least `"
+                      & Perm_Kind'Image (Exp_Perm) & "`, got `"
+                      & Perm_Kind'Image (Act_Perm) & "`", N);
+      end Perm_Mismatch;
+
+   end Permissions;
+
+   use Permissions;
+
+   --------------------------------------
+   -- Analysis modes for AST traversal --
+   --------------------------------------
+
+   --  The different modes for analysis. This allows to checking whether a path
+   --  found in the code should be moved, borrowed, or observed.
+
+   type Checking_Mode is
+
+     (Read,
+      --  Default mode. Checks that paths have Read_Perm permission.
+
+      Move,
+      --  Regular moving semantics (not under 'Access). Checks that paths have
+      --  Read_Write permission. After moving a path, its permission is set to
+      --  Write_Only and the permission of its extensions is set to No_Access.
+
+      Assign,
+      --  Used for the target of an assignment, or an actual parameter with
+      --  mode OUT. Checks that paths have Write_Perm permission. After
+      --  assigning to a path, its permission is set to Read_Write.
+
+      Super_Move,
+      --  Enhanced moving semantics (under 'Access). Checks that paths have
+      --  Read_Write permission. After moving a path, its permission is set
+      --  to No_Access, as well as the permission of its extensions and the
+      --  permission of its prefixes up to the first Reference node.
+
+      Borrow_Out,
+      --  Used for actual OUT parameters. Checks that paths have Write_Perm
+      --  permission. After checking a path, its permission is set to Read_Only
+      --  when of a by-copy type, to No_Access otherwise. After the call, its
+      --  permission is set to Read_Write.
+
+      Observe
+      --  Used for actual IN parameters of a scalar type. Checks that paths
+      --  have Read_Perm permission. After checking a path, its permission
+      --  is set to Read_Only.
+      --
+      --  Also used for formal IN parameters
+     );
+
+   type Result_Kind is (Folded, Unfolded, Function_Call);
+   --  The type declaration to discriminate in the Perm_Or_Tree type
+
+   --  The result type of the function Get_Perm_Or_Tree. This returns either a
+   --  tree when it found the appropriate tree, or a permission when the search
+   --  finds a leaf and the subtree we are looking for is folded. In the last
+   --  case, we return instead the Children_Permission field of the leaf.
+
+   type Perm_Or_Tree (R : Result_Kind) is record
+      case R is
+         when Folded        => Found_Permission : Perm_Kind;
+         when Unfolded      => Tree_Access : Perm_Tree_Access;
+         when Function_Call => null;
+      end case;
+   end record;
+
+   -----------------------
+   -- Local subprograms --
+   -----------------------
+
+   function "<=" (P1, P2 : Perm_Kind) return Boolean;
+   function ">=" (P1, P2 : Perm_Kind) return Boolean;
+   function Glb  (P1, P2 : Perm_Kind) return Perm_Kind;
+   function Lub  (P1, P2 : Perm_Kind) return Perm_Kind;
+
+   --  Checking proceduress for safe pointer usage. These procedures traverse
+   --  the AST, check nodes for correct permissions according to SPARK RM
+   --  6.4.2, and update permissions depending on the node kind.
+
+   procedure Check_Call_Statement (Call : Node_Id);
+
+   procedure Check_Callable_Body (Body_N : Node_Id);
+   --  We are not in End_Of_Callee mode, hence we will save the environment
+   --  and start from a new one. We will add in the environment all formal
+   --  parameters as well as global used during the subprogram, with the
+   --  appropriate permissions (write-only for out, read-only for observed,
+   --  read-write for others).
+   --
+   --  After that we analyze the body of the function, and finaly, we check
+   --  that each borrowed parameter and global has read-write permission. We
+   --  then clean up the environment and put back the saved environment.
+
+   procedure Check_Declaration (Decl : Node_Id);
+
+   procedure Check_Expression (Expr : Node_Id);
+
+   procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode);
+   --  This procedure takes a global pragma and checks depending on mode:
+   --  Mode Read: every in global is readable
+   --  Mode Observe: same as Check_Param_Observes but on globals
+   --  Mode Borrow_Out: Check_Param_Outs for globals
+   --  Mode Move: Check_Param for globals with mode Read
+   --  Mode Assign: Check_Param for globals with mode Assign
+
+   procedure Check_List (L : List_Id);
+   --  Calls Check_Node on each element of the list
+
+   procedure Check_Loop_Statement (Loop_N : Node_Id);
+
+   procedure Check_Node (N : Node_Id);
+   --  Main traversal procedure to check safe pointer usage. This procedure is
+   --  mutually recursive with the specialized procedures that follow.
+
+   procedure Check_Package_Body (Pack : Node_Id);
+
+   procedure Check_Param (Formal : Entity_Id; Actual : Node_Id);
+   --  This procedure takes a formal and an actual parameter and calls the
+   --  analyze node if the parameter is borrowed with mode in out, with the
+   --  appropriate Checking_Mode (Move).
+
+   procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id);
+   --  This procedure takes a formal and an actual parameter and calls
+   --  the analyze node if the parameter is observed, with the appropriate
+   --  Checking_Mode.
+
+   procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id);
+   --  This procedure takes a formal and an actual parameter and calls the
+   --  analyze node if the parameter is of mode out, with the appropriate
+   --  Checking_Mode.
+
+   procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id);
+   --  This procedure takes a formal and an actual parameter and checks the
+   --  readability of every in-mode parameter. This includes observed in, and
+   --  also borrowed in, that are then checked afterwards.
+
+   procedure Check_Statement (Stmt : Node_Id);
+
+   function Get_Perm (N : Node_Id) return Perm_Kind;
+   --  The function that takes a name as input and returns a permission
+   --  associated to it.
+
+   function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
+   --  This function gets a Node_Id and looks recursively to find the
+   --  appropriate subtree for that Node_Id. If the tree is folded on
+   --  that node, then it returns the permission given at the right level.
+
+   function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
+   --  This function gets a Node_Id and looks recursively to find the
+   --  appropriate subtree for that Node_Id. If the tree is folded, then
+   --  it unrolls the tree up to the appropriate level.
+
+   function Has_Alias
+     (N : Node_Id)
+       return Boolean;
+   --  Function that returns whether the path given as parameter contains an
+   --  extension that is declared as aliased.
+
+   function Has_Array_Component (N : Node_Id) return Boolean;
+   --  This function gets a Node_Id and looks recursively to find if the given
+   --  path has any array component.
+
+   function Has_Function_Component (N : Node_Id) return Boolean;
+   --  This function gets a Node_Id and looks recursively to find if the given
+   --  path has any function component.
+
+   procedure Hp (P : Perm_Env);
+   --  A procedure that outputs the hash table. This function is used only in
+   --  the debugger to look into a hash table.
+   pragma Unreferenced (Hp);
+
+   procedure Illegal_Global_Usage (N : Node_Or_Entity_Id);
+   pragma No_Return (Illegal_Global_Usage);
+   --  A procedure that is called when deep globals or aliased globals are used
+   --  without any global aspect.
+
+   function Is_Borrowed_In (E : Entity_Id) return Boolean;
+   --  Function that tells if the given entity is a borrowed in a formal
+   --  parameter, that is, if it is an access-to-variable type.
+
+   function Is_Deep (E : Entity_Id) return Boolean;
+   --  A function that can tell if a type is deep or not. Returns true if the
+   --  type passed as argument is deep.
+
+   function Is_Shallow (E : Entity_Id) return Boolean;
+   --  A function that can tell if a type is shallow or not. Returns true if
+   --  the type passed as argument is shallow.
+
+   function Loop_Of_Exit (N : Node_Id) return Entity_Id;
+   --  A function that takes an exit statement node and returns the entity of
+   --  the loop that this statement is exiting from.
+
+   procedure Merge_Envs (Target : in out Perm_Env; Source : in out Perm_Env);
+   --  Merge Target and Source into Target, and then deallocate the Source
+
+   procedure Perm_Error
+     (N : Node_Id;
+      Perm : Perm_Kind;
+      Found_Perm : Perm_Kind);
+   --  A procedure that is called when the permissions found contradict the
+   --  rules established by the RM. This function is called with the node, its
+   --  entity and the permission that was expected, and adds an error message
+   --  with the appropriate values.
+
+   procedure Perm_Error_Subprogram_End
+     (E          : Entity_Id;
+      Subp       : Entity_Id;
+      Perm       : Perm_Kind;
+      Found_Perm : Perm_Kind);
+   --  A procedure that is called when the permissions found contradict the
+   --  rules established by the RM at the end of subprograms. This function
+   --  is called with the node, its entity, the node of the returning function
+   --  and the permission that was expected, and adds an error message with the
+   --  appropriate values.
+
+   procedure Process_Path (N : Node_Id);
+
+   procedure Return_Declarations (L : List_Id);
+   --  Check correct permissions on every declared object at the end of a
+   --  callee. Used at the end of the body of a callable entity. Checks that
+   --  paths of all borrowed formal parameters and global have Read_Write
+   --  permission.
+
+   procedure Return_Globals (Subp : Entity_Id);
+   --  Takes a subprogram as input, and checks that all borrowed global items
+   --  of the subprogram indeed have RW permission at the end of the subprogram
+   --  execution.
+
+   procedure Return_Parameter_Or_Global
+     (Id   : Entity_Id;
+      Mode : Formal_Kind;
+      Subp : Entity_Id);
+   --  Auxiliary procedure to Return_Parameters and Return_Globals
+
+   procedure Return_Parameters (Subp : Entity_Id);
+   --  Takes a subprogram as input, and checks that all borrowed parameters of
+   --  the subprogram indeed have RW permission at the end of the subprogram
+   --  execution.
+
+   procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind);
+   --  This procedure takes an access to a permission tree and modifies the
+   --  tree so that any strict extensions of the given tree become of the
+   --  access specified by parameter P.
+
+   procedure Set_Perm_Extensions_Move (T : Perm_Tree_Access; E : Entity_Id);
+   --  Set permissions to
+   --    No for any extension with more .all
+   --    W for any deep extension with same number of .all
+   --    RW for any shallow extension with same number of .all
+
+   function Set_Perm_Prefixes_Assign (N : Node_Id) return Perm_Tree_Access;
+   --  This function takes a name as an input and sets in the permission
+   --  tree the given permission to the given name. The general rule here is
+   --  that everybody updates the permission of the subtree it is returning.
+   --  The permission of the assigned path has been set to RW by the caller.
+   --
+   --  Case where we have to normalize a tree after the correct permissions
+   --  have been assigned already. We look for the right subtree at the given
+   --  path, actualize its permissions, and then call the normalization on its
+   --  parent.
+   --
+   --  Example: We assign x.y and x.z then during Set_Perm_Prefixes_Move will
+   --  change the permission of x to RW because all of its components have
+   --  permission have permission RW.
+
+   function Set_Perm_Prefixes_Borrow_Out (N : Node_Id) return Perm_Tree_Access;
+   --  This function modifies the permissions of a given node_id in the
+   --  permission environment as well as in all the prefixes of the path,
+   --  given that the path is borrowed with mode out.
+
+   function Set_Perm_Prefixes_Move
+     (N : Node_Id; Mode : Checking_Mode)
+      return Perm_Tree_Access;
+   pragma Precondition (Mode = Move or Mode = Super_Move);
+   --  Given a node and a mode (that can be either Move or Super_Move), this
+   --  function modifies the permissions of a given node_id in the permission
+   --  environment as well as all the prefixes of the path, given that the path
+   --  is moved with or without 'Access. The general rule here is everybody
+   --  updates the permission of the subtree they are returning.
+   --
+   --  This case describes a move either under 'Access or without 'Access.
+
+   function Set_Perm_Prefixes_Observe (N : Node_Id) return Perm_Tree_Access;
+   --  This function modifies the permissions of a given node_id in the
+   --  permission environment as well as all the prefixes of the path,
+   --  given that the path is observed.
+
+   procedure Setup_Globals (Subp : Entity_Id);
+   --  Takes a subprogram as input, and sets up the environment by adding
+   --  global items with appropriate permissions.
+
+   procedure Setup_Parameter_Or_Global
+     (Id   : Entity_Id;
+      Mode : Formal_Kind);
+   --  Auxiliary procedure to Setup_Parameters and Setup_Globals
+
+   procedure Setup_Parameters (Subp : Entity_Id);
+   --  Takes a subprogram as input, and sets up the environment by adding
+   --  formal parameters with appropriate permissions.
+
+   ----------------------
+   -- Global Variables --
+   ----------------------
+
+   Current_Perm_Env : Perm_Env;
+   --  The permission environment that is used for the analysis. This
+   --  environment can be saved, modified, reinitialized, but should be the
+   --  only one valid from which to extract the permissions of the paths in
+   --  scope. The analysis ensures at each point that this variables contains
+   --  a valid permission environment with all bindings in scope.
+
+   Current_Checking_Mode : Checking_Mode := Read;
+   --  The current analysis mode. This global variable indicates at each point
+   --  of the analysis whether the node being analyzed is moved, borrowed,
+   --  assigned, read, ... The full list of possible values can be found in
+   --  the declaration of type Checking_Mode.
+
+   Current_Loops_Envs : Env_Backups;
+   --  This variable contains saves of permission environments at each loop the
+   --  analysis entered. Each saved environment can be reached with the label
+   --  of the loop.
+
+   Current_Loops_Accumulators : Env_Backups;
+   --  This variable contains the environments used as accumulators for loops,
+   --  that consist of the merge of all environments at each exit point of
+   --  the loop (which can also be the entry point of the loop in the case of
+   --  non-infinite loops), each of them reachable from the label of the loop.
+   --  We require that the environment stored in the accumulator be less
+   --  restrictive than the saved environment at the beginning of the loop, and
+   --  the permission environment after the loop is equal to the accumulator.
+
+   Current_Initialization_Map : Initialization_Map;
+   --  This variable contains a map that binds each variable of the analyzed
+   --  source code to a boolean that becomes true whenever the variable is used
+   --  after declaration. Hence we can exclude from analysis variables that
+   --  are just declared and never accessed, typically at package declaration.
+
+   ----------
+   -- "<=" --
+   ----------
+
+   function "<=" (P1, P2 : Perm_Kind) return Boolean
+   is
+   begin
+      return P2 >= P1;
+   end "<=";
+
+   ----------
+   -- ">=" --
+   ----------
+
+   function ">=" (P1, P2 : Perm_Kind) return Boolean
+   is
+   begin
+      case P2 is
+         when No_Access  => return True;
+         when Read_Only  => return P1 in Read_Perm;
+         when Write_Only => return P1 in Write_Perm;
+         when Read_Write => return P1 = Read_Write;
+      end case;
+   end ">=";
+
+   --------------------------
+   -- Check_Call_Statement --
+   --------------------------
+
+   procedure Check_Call_Statement (Call : Node_Id) is
+      Saved_Env : Perm_Env;
+
+      procedure Iterate_Call is new
+        Iterate_Call_Parameters (Check_Param);
+      procedure Iterate_Call_Observes is new
+        Iterate_Call_Parameters (Check_Param_Observes);
+      procedure Iterate_Call_Outs is new
+        Iterate_Call_Parameters (Check_Param_Outs);
+      procedure Iterate_Call_Read is new
+        Iterate_Call_Parameters (Check_Param_Read);
+
+   begin
+      --  Save environment, so that the modifications done by analyzing the
+      --  parameters are not kept at the end of the call.
+      Copy_Env (Current_Perm_Env,
+                Saved_Env);
+
+      --  We first check the Read access on every in parameter
+
+      Current_Checking_Mode := Read;
+      Iterate_Call_Read (Call);
+      Check_Globals (Get_Pragma
+                       (Get_Called_Entity (Call), Pragma_Global), Read);
+
+      --  We first observe, then borrow with mode out, and then with other
+      --  modes. This ensures that we do not have to check for by-copy types
+      --  specially, because we read them before borrowing them.
+
+      Iterate_Call_Observes (Call);
+      Check_Globals (Get_Pragma
+                       (Get_Called_Entity (Call), Pragma_Global),
+                       Observe);
+
+      Iterate_Call_Outs (Call);
+      Check_Globals (Get_Pragma
+                       (Get_Called_Entity (Call), Pragma_Global),
+                       Borrow_Out);
+
+      Iterate_Call (Call);
+      Check_Globals (Get_Pragma
+                       (Get_Called_Entity (Call), Pragma_Global), Move);
+
+      --  Restore environment, because after borrowing/observing actual
+      --  parameters, they get their permission reverted to the ones before
+      --  the call.
+
+      Free_Env (Current_Perm_Env);
+
+      Copy_Env (Saved_Env,
+                Current_Perm_Env);
+
+      Free_Env (Saved_Env);
+
+      --  We assign the out parameters (necessarily borrowed per RM)
+      Current_Checking_Mode := Assign;
+      Iterate_Call (Call);
+      Check_Globals (Get_Pragma
+                       (Get_Called_Entity (Call), Pragma_Global),
+                       Assign);
+
+   end Check_Call_Statement;
+
+   -------------------------
+   -- Check_Callable_Body --
+   -------------------------
+
+   procedure Check_Callable_Body (Body_N : Node_Id) is
+
+      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+
+      Saved_Env : Perm_Env;
+      Saved_Init_Map : Initialization_Map;
+
+      New_Env : Perm_Env;
+
+      Body_Id : constant Entity_Id := Defining_Entity (Body_N);
+      Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
+
+   begin
+      --  Check if SPARK pragma is not set to Off
+
+      if Present (SPARK_Pragma (Defining_Entity (Body_N))) then
+         if Get_SPARK_Mode_From_Annotation
+           (SPARK_Pragma (Defining_Entity (Body_N, False))) /= Opt.On
+         then
+            return;
+         end if;
+      else
+         return;
+      end if;
+
+      --  Save environment and put a new one in place
+
+      Copy_Env (Current_Perm_Env, Saved_Env);
+
+      --  Save initialization map
+
+      Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map);
+
+      Current_Checking_Mode := Read;
+      Current_Perm_Env := New_Env;
+
+      --  Add formals and globals to the environment with adequate permissions
+
+      if Is_Subprogram_Or_Entry (Spec_Id) then
+         Setup_Parameters (Spec_Id);
+         Setup_Globals (Spec_Id);
+      end if;
+
+      --  Analyze the body of the function
+
+      Check_List (Declarations (Body_N));
+      Check_Node (Handled_Statement_Sequence (Body_N));
+
+      --  Check the read-write permissions of borrowed parameters/globals
+
+      if Ekind_In (Spec_Id, E_Procedure, E_Entry)
+        and then not No_Return (Spec_Id)
+      then
+         Return_Parameters (Spec_Id);
+         Return_Globals (Spec_Id);
+      end if;
+
+      --  Free the environments
+
+      Free_Env (Current_Perm_Env);
+
+      Copy_Env (Saved_Env,
+                Current_Perm_Env);
+
+      Free_Env (Saved_Env);
+
+      --  Restore initialization map
+
+      Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map);
+
+      Reset (Saved_Init_Map);
+
+      --  The assignment of all out parameters will be done by caller
+
+      Current_Checking_Mode := Mode_Before;
+   end Check_Callable_Body;
+
+   -----------------------
+   -- Check_Declaration --
+   -----------------------
+
+   procedure Check_Declaration (Decl : Node_Id) is
+   begin
+      case N_Declaration'(Nkind (Decl)) is
+         when N_Full_Type_Declaration =>
+            --  Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE
+            null;
+
+         when N_Object_Declaration =>
+            --  First move the right-hand side
+            Current_Checking_Mode := Move;
+            Check_Node (Expression (Decl));
+
+            declare
+               Elem : Perm_Tree_Access;
+
+            begin
+               Elem := new Perm_Tree_Wrapper'
+                 (Tree =>
+                    (Kind                => Entire_Object,
+                     Is_Node_Deep        =>
+                       Is_Deep (Etype (Defining_Identifier (Decl))),
+                     Permission          => Read_Write,
+                     Children_Permission => Read_Write));
+
+               --  If unitialized declaration, then set to Write_Only. If a
+               --  pointer declaration, it has a null default initialization.
+               if Nkind (Expression (Decl)) = N_Empty
+                 and then not Has_Full_Default_Initialization
+                   (Etype (Defining_Identifier (Decl)))
+                 and then not Is_Access_Type
+                   (Etype (Defining_Identifier (Decl)))
+               then
+                  Elem.all.Tree.Permission := Write_Only;
+                  Elem.all.Tree.Children_Permission := Write_Only;
+               end if;
+
+               --  Create new tree for defining identifier
+
+               Set (Current_Perm_Env,
+                    Unique_Entity (Defining_Identifier (Decl)),
+                    Elem);
+
+               pragma Assert (Get_First (Current_Perm_Env)
+                              /= null);
+
+            end;
+
+         when N_Subtype_Declaration =>
+            Check_Node (Subtype_Indication (Decl));
+
+         when N_Iterator_Specification =>
+            pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl))));
+            null;
+
+         when N_Loop_Parameter_Specification =>
+            pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl))));
+            null;
+
+         --  Checking should not be called directly on these nodes
+
+         when N_Component_Declaration
+            | N_Function_Specification
+            | N_Entry_Declaration
+            | N_Procedure_Specification
+         =>
+            raise Program_Error;
+
+         --  Ignored constructs for pointer checking
+
+         when N_Formal_Object_Declaration
+            | N_Formal_Type_Declaration
+            | N_Incomplete_Type_Declaration
+            | N_Private_Extension_Declaration
+            | N_Private_Type_Declaration
+            | N_Protected_Type_Declaration
+         =>
+            null;
+
+         --  The following nodes are rewritten by semantic analysis
+
+         when N_Expression_Function =>
+            raise Program_Error;
+      end case;
+   end Check_Declaration;
+
+   ----------------------
+   -- Check_Expression --
+   ----------------------
+
+   procedure Check_Expression (Expr : Node_Id) is
+      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+   begin
+      case N_Subexpr'(Nkind (Expr)) is
+         when N_Procedure_Call_Statement =>
+            Check_Call_Statement (Expr);
+
+         when N_Identifier
+            | N_Expanded_Name
+         =>
+            --  Check if identifier is pointing to nothing (On/Off/...)
+            if not Present (Entity (Expr)) then
+               return;
+            end if;
+
+            --  Do not analyze things that are not of object Kind
+            if Ekind (Entity (Expr)) not in Object_Kind then
+               return;
+            end if;
+
+            --  Consider as ident
+            Process_Path (Expr);
+
+         --  Switch to read mode and then check the readability of each operand
+
+         when N_Binary_Op =>
+
+            Current_Checking_Mode := Read;
+            Check_Node (Left_Opnd (Expr));
+            Check_Node (Right_Opnd (Expr));
+
+         --  Switch to read mode and then check the readability of each operand
+
+         when N_Op_Abs
+            | N_Op_Minus
+            | N_Op_Not
+            | N_Op_Plus
+         =>
+            pragma Assert (Is_Shallow (Etype (Expr)));
+            Current_Checking_Mode := Read;
+            Check_Node (Right_Opnd (Expr));
+
+         --  Forbid all deep expressions for Attribute ???
+
+         when N_Attribute_Reference =>
+            case Attribute_Name (Expr) is
+               when Name_Access =>
+                  case Current_Checking_Mode is
+                     when Read =>
+                        Check_Node (Prefix (Expr));
+
+                     when Move =>
+                        Current_Checking_Mode := Super_Move;
+                        Check_Node (Prefix (Expr));
+
+                     --  Only assign names, not expressions
+
+                     when Assign =>
+                        raise Program_Error;
+
+                     --  Prefix in Super_Move should be a name, error here
+
+                     when Super_Move =>
+                        raise Program_Error;
+
+                     --  Could only borrow names of mode out, not n'Access
+
+                     when Borrow_Out =>
+                        raise Program_Error;
+
+                     when Observe =>
+                        Check_Node (Prefix (Expr));
+                  end case;
+
+               when Name_Last
+                  | Name_First
+               =>
+                  Current_Checking_Mode := Read;
+                  Check_Node (Prefix (Expr));
+
+               when Name_Min =>
+                  Current_Checking_Mode := Read;
+                  Check_Node (Prefix (Expr));
+
+               when Name_Image =>
+                  Check_Node (Prefix (Expr));
+
+               when Name_SPARK_Mode =>
+                  null;
+
+               when Name_Value =>
+                  Current_Checking_Mode := Read;
+                  Check_Node (Prefix (Expr));
+
+               when Name_Update =>
+                  Check_List (Expressions (Expr));
+                  Check_Node (Prefix (Expr));
+
+               when Name_Pred
+                   | Name_Succ
+               =>
+                  Check_List (Expressions (Expr));
+                  Check_Node (Prefix (Expr));
+
+               when Name_Length =>
+                  Current_Checking_Mode := Read;
+                  Check_Node (Prefix (Expr));
+
+               --  Any Attribute referring to the underlying memory is ignored
+               --  in the analysis. This means that taking the address of a
+               --  variable makes a silent alias that is not rejected by the
+               --  analysis.
+
+               when Name_Address
+                   | Name_Alignment
+                   | Name_Component_Size
+                   | Name_First_Bit
+                   | Name_Last_Bit
+                   | Name_Size
+                   | Name_Position
+               =>
+                  null;
+
+               --  Attributes referring to types (get values from types), hence
+               --  no need to check either for borrows or any loans.
+
+               when Name_Base
+                  | Name_Val
+               =>
+                  null;
+
+               --  Other attributes that fall out of the scope of the analysis
+
+               when others =>
+                  null;
+            end case;
+
+         when N_In =>
+            Current_Checking_Mode := Read;
+            Check_Node (Left_Opnd (Expr));
+            Check_Node (Right_Opnd (Expr));
+
+         when N_Not_In =>
+            Current_Checking_Mode := Read;
+            Check_Node (Left_Opnd (Expr));
+            Check_Node (Right_Opnd (Expr));
+
+         --  Switch to read mode and then check the readability of each operand
+
+         when N_And_Then
+            | N_Or_Else
+         =>
+            pragma Assert (Is_Shallow (Etype (Expr)));
+            Current_Checking_Mode := Read;
+            Check_Node (Left_Opnd (Expr));
+            Check_Node (Right_Opnd (Expr));
+
+         --  Check the arguments of the call
+
+         when N_Function_Call =>
+            Current_Checking_Mode := Read;
+            Check_List (Parameter_Associations (Expr));
+
+         when N_Explicit_Dereference =>
+            Process_Path (Expr);
+
+         --  Copy environment, run on each branch, and then merge
+
+         when N_If_Expression =>
+            declare
+               Saved_Env : Perm_Env;
+
+               --  Accumulator for the different branches
+
+               New_Env : Perm_Env;
+
+               Elmt : Node_Id := First (Expressions (Expr));
+
+            begin
+               Current_Checking_Mode := Read;
+
+               Check_Node (Elmt);
+
+               Current_Checking_Mode := Mode_Before;
+
+               --  Save environment
+
+               Copy_Env (Current_Perm_Env,
+                                 Saved_Env);
+
+               --  Here we have the original env in saved, current with a fresh
+               --  copy, and new aliased.
+
+               --  THEN PART
+
+               Next (Elmt);
+               Check_Node (Elmt);
+
+               --  Here the new_environment contains curr env after then block
+
+               --  ELSE part
+
+               --  Restore environment before if
+               Copy_Env (Current_Perm_Env,
+                                 New_Env);
+
+               Free_Env (Current_Perm_Env);
+
+               Copy_Env (Saved_Env,
+                                 Current_Perm_Env);
+
+               --  Here new environment contains the environment after then and
+               --  current the fresh copy of old one.
+
+               Next (Elmt);
+               Check_Node (Elmt);
+
+               Merge_Envs (New_Env,
+                                   Current_Perm_Env);
+
+               --  CLEANUP
+
+               Copy_Env (New_Env,
+                                 Current_Perm_Env);
+
+               Free_Env (New_Env);
+               Free_Env (Saved_Env);
+            end;
+
+         when N_Indexed_Component =>
+            Process_Path (Expr);
+
+         --  Analyze the expression that is getting qualified
+
+         when N_Qualified_Expression =>
+            Check_Node (Expression (Expr));
+
+         when N_Quantified_Expression =>
+            declare
+               Saved_Env : Perm_Env;
+            begin
+               Copy_Env (Current_Perm_Env, Saved_Env);
+               Current_Checking_Mode := Read;
+               Check_Node (Iterator_Specification (Expr));
+               Check_Node (Loop_Parameter_Specification (Expr));
+
+               Check_Node (Condition (Expr));
+               Free_Env (Current_Perm_Env);
+               Copy_Env (Saved_Env, Current_Perm_Env);
+               Free_Env (Saved_Env);
+            end;
+
+         --  Analyze the list of associations in the aggregate
+
+         when N_Aggregate =>
+            Check_List (Expressions (Expr));
+            Check_List (Component_Associations (Expr));
+
+         when N_Allocator =>
+            Check_Node (Expression (Expr));
+
+         when N_Case_Expression =>
+            declare
+               Saved_Env : Perm_Env;
+
+               --  Accumulator for the different branches
+
+               New_Env : Perm_Env;
+
+               Elmt : Node_Id := First (Alternatives (Expr));
+
+            begin
+               Current_Checking_Mode := Read;
+               Check_Node (Expression (Expr));
+
+               Current_Checking_Mode := Mode_Before;
+
+               --  Save environment
+
+               Copy_Env (Current_Perm_Env,
+                                 Saved_Env);
+
+               --  Here we have the original env in saved, current with a fresh
+               --  copy, and new aliased.
+
+               --  First alternative
+
+               Check_Node (Elmt);
+               Next (Elmt);
+
+               Copy_Env (Current_Perm_Env,
+                                 New_Env);
+
+               Free_Env (Current_Perm_Env);
+
+               --  Other alternatives
+
+               while Present (Elmt) loop
+                  --  Restore environment
+
+                  Copy_Env (Saved_Env,
+                                    Current_Perm_Env);
+
+                  Check_Node (Elmt);
+
+                  --  Merge Current_Perm_Env into New_Env
+
+                  Merge_Envs (New_Env,
+                                      Current_Perm_Env);
+
+                  Next (Elmt);
+               end loop;
+
+               --  CLEANUP
+               Copy_Env (New_Env,
+                                 Current_Perm_Env);
+
+               Free_Env (New_Env);
+               Free_Env (Saved_Env);
+            end;
+
+         --  Analyze the list of associates in the aggregate as well as the
+         --  ancestor part.
+
+         when N_Extension_Aggregate =>
+
+            Check_Node (Ancestor_Part (Expr));
+            Check_List (Expressions (Expr));
+
+         when N_Range =>
+            Check_Node (Low_Bound (Expr));
+            Check_Node (High_Bound (Expr));
+
+         --  We arrived at a path. Process it.
+
+         when N_Selected_Component =>
+            Process_Path (Expr);
+
+         when N_Slice =>
+            Process_Path (Expr);
+
+         when N_Type_Conversion =>
+            Check_Node (Expression (Expr));
+
+         when N_Unchecked_Type_Conversion =>
+            Check_Node (Expression (Expr));
+
+         --  Checking should not be called directly on these nodes
+
+         when N_Target_Name =>
+            raise Program_Error;
+
+         --  Unsupported constructs in SPARK
+
+         when N_Delta_Aggregate =>
+            Error_Msg_N ("unsupported construct in SPARK", Expr);
+
+         --  Ignored constructs for pointer checking
+
+         when N_Character_Literal
+            | N_Null
+            | N_Numeric_Or_String_Literal
+            | N_Operator_Symbol
+            | N_Raise_Expression
+            | N_Raise_xxx_Error
+         =>
+            null;
+
+         --  The following nodes are never generated in GNATprove mode
+
+         when N_Expression_With_Actions
+            | N_Reference
+            | N_Unchecked_Expression
+         =>
+            raise Program_Error;
+
+      end case;
+   end Check_Expression;
+
+   -------------------
+   -- Check_Globals --
+   -------------------
+
+   procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode) is
+   begin
+      if Nkind (N) = N_Empty then
+         return;
+      end if;
+
+      declare
+         pragma Assert
+           (List_Length (Pragma_Argument_Associations (N)) = 1);
+
+         PAA      : constant Node_Id :=
+           First (Pragma_Argument_Associations (N));
+         pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association);
+
+         Row      : Node_Id;
+         The_Mode : Name_Id;
+         RHS      : Node_Id;
+
+         procedure Process (Mode   : Name_Id;
+                            The_Global : Entity_Id);
+
+         procedure Process (Mode   : Name_Id;
+                            The_Global : Node_Id)
+         is
+            Ident_Elt : constant Entity_Id :=
+              Unique_Entity (Entity (The_Global));
+
+            Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+
+         begin
+            if Ekind (Ident_Elt) = E_Abstract_State then
+               return;
+            end if;
+
+            case Check_Mode is
+               when Read =>
+                  case Mode is
+                     when Name_Input
+                        | Name_Proof_In
+                     =>
+                        Check_Node (The_Global);
+
+                     when Name_Output
+                        | Name_In_Out
+                     =>
+                        null;
+
+                     when others =>
+                        raise Program_Error;
+
+                  end case;
+
+               when Observe =>
+                  case Mode is
+                     when Name_Input
+                        | Name_Proof_In
+                     =>
+                        if not Is_Borrowed_In (Ident_Elt) then
+                           --  Observed in
+
+                           Current_Checking_Mode := Observe;
+                           Check_Node (The_Global);
+                        end if;
+
+                     when others =>
+                        null;
+
+                  end case;
+
+               when Borrow_Out =>
+
+                  case Mode is
+                     when Name_Output =>
+                        --  Borrowed out
+                        Current_Checking_Mode := Borrow_Out;
+                        Check_Node (The_Global);
+
+                     when others =>
+                        null;
+
+                  end case;
+
+               when Move =>
+                  case Mode is
+                     when Name_Input
+                        | Name_Proof_In
+                     =>
+                        if Is_Borrowed_In (Ident_Elt) then
+                           --  Borrowed in
+
+                           Current_Checking_Mode := Move;
+                        else
+                           --  Observed
+
+                           return;
+                        end if;
+
+                     when Name_Output =>
+                        return;
+
+                     when Name_In_Out =>
+                        --  Borrowed in out
+
+                        Current_Checking_Mode := Move;
+
+                     when others =>
+                        raise Program_Error;
+                  end case;
+
+                  Check_Node (The_Global);
+               when Assign =>
+                  case Mode is
+                     when Name_Input
+                        | Name_Proof_In
+                     =>
+                        null;
+
+                     when Name_Output
+                        | Name_In_Out
+                     =>
+                        --  Borrowed out or in out
+
+                        Process_Path (The_Global);
+
+                     when others =>
+                        raise Program_Error;
+                  end case;
+
+               when others =>
+                  raise Program_Error;
+            end case;
+
+            Current_Checking_Mode := Mode_Before;
+         end Process;
+
+      begin
+         if Nkind (Expression (PAA)) = N_Null then
+            --  global => null
+            --  No globals, nothing to do
+            return;
+
+         elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
+            --  global => foo
+            --  A single input
+            Process (Name_Input, Expression (PAA));
+
+         elsif Nkind (Expression (PAA)) = N_Aggregate
+           and then Expressions (Expression (PAA)) /= No_List
+         then
+            --  global => (foo, bar)
+            --  Inputs
+            RHS := First (Expressions (Expression (PAA)));
+            while Present (RHS) loop
+               case Nkind (RHS) is
+                  when N_Identifier
+                     | N_Expanded_Name
+                  =>
+                     Process (Name_Input, RHS);
+
+                  when N_Numeric_Or_String_Literal =>
+                     Process (Name_Input, Original_Node (RHS));
+
+                  when others =>
+                     raise Program_Error;
+
+               end case;
+               RHS := Next (RHS);
+            end loop;
+
+         elsif Nkind (Expression (PAA)) = N_Aggregate
+           and then Component_Associations (Expression (PAA)) /= No_List
+         then
+            --  global => (mode => foo,
+            --             mode => (bar, baz))
+            --  A mixture of things
+
+            declare
+               CA : constant List_Id :=
+                 Component_Associations (Expression (PAA));
+            begin
+               Row := First (CA);
+               while Present (Row) loop
+                  pragma Assert (List_Length (Choices (Row)) = 1);
+                  The_Mode := Chars (First (Choices (Row)));
+
+                  RHS := Expression (Row);
+                  case Nkind (RHS) is
+                     when N_Aggregate =>
+                        RHS := First (Expressions (RHS));
+                        while Present (RHS) loop
+                           case Nkind (RHS) is
+                              when N_Numeric_Or_String_Literal =>
+                                 Process (The_Mode, Original_Node (RHS));
+
+                              when others =>
+                                 Process (The_Mode, RHS);
+
+                           end case;
+                           RHS := Next (RHS);
+                        end loop;
+
+                     when N_Identifier
+                        | N_Expanded_Name
+                     =>
+                        Process (The_Mode, RHS);
+
+                     when N_Null =>
+                        null;
+
+                     when N_Numeric_Or_String_Literal =>
+                        Process (The_Mode, Original_Node (RHS));
+
+                     when others =>
+                        raise Program_Error;
+
+                  end case;
+
+                  Row := Next (Row);
+               end loop;
+            end;
+
+         else
+            raise Program_Error;
+         end if;
+      end;
+   end Check_Globals;
+
+   ----------------
+   -- Check_List --
+   ----------------
+
+   procedure Check_List (L : List_Id) is
+      N : Node_Id;
+   begin
+      N := First (L);
+      while Present (N) loop
+         Check_Node (N);
+         Next (N);
+      end loop;
+   end Check_List;
+
+   --------------------------
+   -- Check_Loop_Statement --
+   --------------------------
+
+   procedure Check_Loop_Statement (Loop_N : Node_Id) is
+
+      --  Local Subprograms
+
+      procedure Check_Is_Less_Restrictive_Env
+        (Exiting_Env : Perm_Env;
+         Entry_Env   : Perm_Env);
+      --  This procedure checks that the Exiting_Env environment is less
+      --  restrictive than the Entry_Env environment.
+
+      procedure Check_Is_Less_Restrictive_Tree
+        (New_Tree  : Perm_Tree_Access;
+         Orig_Tree : Perm_Tree_Access;
+         E         : Entity_Id);
+      --  Auxiliary procedure to check that the tree New_Tree is less
+      --  restrictive than the tree Orig_Tree for the entity E.
+
+      procedure Perm_Error_Loop_Exit
+        (E          : Entity_Id;
+         Loop_Id    : Node_Id;
+         Perm       : Perm_Kind;
+         Found_Perm : Perm_Kind);
+      --  A procedure that is called when the permissions found contradict
+      --  the rules established by the RM at the exit of loops. This function
+      --  is called with the entity, the node of the enclosing loop, the
+      --  permission that was expected and the permission found, and issues
+      --  an appropriate error message.
+
+      -----------------------------------
+      -- Check_Is_Less_Restrictive_Env --
+      -----------------------------------
+
+      procedure Check_Is_Less_Restrictive_Env
+        (Exiting_Env : Perm_Env;
+         Entry_Env   : Perm_Env)
+      is
+         Comp_Entry : Perm_Tree_Maps.Key_Option;
+         Iter_Entry, Iter_Exit : Perm_Tree_Access;
+
+      begin
+         Comp_Entry := Get_First_Key (Entry_Env);
+         while Comp_Entry.Present loop
+            Iter_Entry := Get (Entry_Env, Comp_Entry.K);
+            pragma Assert (Iter_Entry /= null);
+            Iter_Exit := Get (Exiting_Env, Comp_Entry.K);
+            pragma Assert (Iter_Exit /= null);
+            Check_Is_Less_Restrictive_Tree
+              (New_Tree  => Iter_Exit,
+               Orig_Tree => Iter_Entry,
+               E         => Comp_Entry.K);
+            Comp_Entry := Get_Next_Key (Entry_Env);
+         end loop;
+      end Check_Is_Less_Restrictive_Env;
+
+      ------------------------------------
+      -- Check_Is_Less_Restrictive_Tree --
+      ------------------------------------
+
+      procedure Check_Is_Less_Restrictive_Tree
+        (New_Tree  : Perm_Tree_Access;
+         Orig_Tree : Perm_Tree_Access;
+         E         : Entity_Id)
+      is
+         -----------------------
+         -- Local Subprograms --
+         -----------------------
+
+         procedure Check_Is_Less_Restrictive_Tree_Than
+           (Tree : Perm_Tree_Access;
+            Perm : Perm_Kind;
+            E    : Entity_Id);
+         --  Auxiliary procedure to check that the tree N is less restrictive
+         --  than the given permission P.
+
+         procedure Check_Is_More_Restrictive_Tree_Than
+           (Tree : Perm_Tree_Access;
+            Perm : Perm_Kind;
+            E    : Entity_Id);
+         --  Auxiliary procedure to check that the tree N is more restrictive
+         --  than the given permission P.
+
+         -----------------------------------------
+         -- Check_Is_Less_Restrictive_Tree_Than --
+         -----------------------------------------
+
+         procedure Check_Is_Less_Restrictive_Tree_Than
+           (Tree : Perm_Tree_Access;
+            Perm : Perm_Kind;
+            E    : Entity_Id)
+         is
+         begin
+            if not (Permission (Tree) >= Perm) then
+               Perm_Error_Loop_Exit
+                 (E, Loop_N, Permission (Tree), Perm);
+            end if;
+
+            case Kind (Tree) is
+               when Entire_Object =>
+                  if not (Children_Permission (Tree) >= Perm) then
+                     Perm_Error_Loop_Exit
+                       (E, Loop_N, Children_Permission (Tree), Perm);
+
+                  end if;
+
+               when Reference =>
+                  Check_Is_Less_Restrictive_Tree_Than
+                    (Get_All (Tree), Perm, E);
+
+               when Array_Component =>
+                  Check_Is_Less_Restrictive_Tree_Than
+                    (Get_Elem (Tree), Perm, E);
+
+               when Record_Component =>
+                  declare
+                     Comp : Perm_Tree_Access;
+                  begin
+                     Comp := Perm_Tree_Maps.Get_First (Component (Tree));
+                     while Comp /= null loop
+                        Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E);
+                        Comp :=
+                          Perm_Tree_Maps.Get_Next (Component (Tree));
+                     end loop;
+
+                     Check_Is_Less_Restrictive_Tree_Than
+                       (Other_Components (Tree), Perm, E);
+                  end;
+            end case;
+         end Check_Is_Less_Restrictive_Tree_Than;
+
+         -----------------------------------------
+         -- Check_Is_More_Restrictive_Tree_Than --
+         -----------------------------------------
+
+         procedure Check_Is_More_Restrictive_Tree_Than
+           (Tree : Perm_Tree_Access;
+            Perm : Perm_Kind;
+            E    : Entity_Id)
+         is
+         begin
+            if not (Perm >= Permission (Tree)) then
+               Perm_Error_Loop_Exit
+                 (E, Loop_N, Permission (Tree), Perm);
+            end if;
+
+            case Kind (Tree) is
+               when Entire_Object =>
+                  if not (Perm >= Children_Permission (Tree)) then
+                     Perm_Error_Loop_Exit
+                       (E, Loop_N, Children_Permission (Tree), Perm);
+                  end if;
+
+               when Reference =>
+                  Check_Is_More_Restrictive_Tree_Than
+                    (Get_All (Tree), Perm, E);
+
+               when Array_Component =>
+                  Check_Is_More_Restrictive_Tree_Than
+                    (Get_Elem (Tree), Perm, E);
+
+               when Record_Component =>
+                  declare
+                     Comp : Perm_Tree_Access;
+                  begin
+                     Comp := Perm_Tree_Maps.Get_First (Component (Tree));
+                     while Comp /= null loop
+                        Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E);
+                        Comp :=
+                          Perm_Tree_Maps.Get_Next (Component (Tree));
+                     end loop;
+
+                     Check_Is_More_Restrictive_Tree_Than
+                       (Other_Components (Tree), Perm, E);
+                  end;
+            end case;
+         end Check_Is_More_Restrictive_Tree_Than;
+
+      --  Start of processing for Check_Is_Less_Restrictive_Tree
+
+      begin
+         if not (Permission (New_Tree) <= Permission (Orig_Tree)) then
+            Perm_Error_Loop_Exit
+              (E          => E,
+               Loop_Id    => Loop_N,
+               Perm       => Permission (New_Tree),
+               Found_Perm => Permission (Orig_Tree));
+         end if;
+
+         case Kind (New_Tree) is
+
+            --  Potentially folded tree. We check the other tree Orig_Tree to
+            --  check whether it is folded or not. If folded we just compare
+            --  their Permission and Children_Permission, if not, then we
+            --  look at the Children_Permission of the folded tree against
+            --  the unfolded tree Orig_Tree.
+
+            when Entire_Object =>
+               case Kind (Orig_Tree) is
+               when Entire_Object =>
+                  if not (Children_Permission (New_Tree) <=
+                          Children_Permission (Orig_Tree))
+                  then
+                     Perm_Error_Loop_Exit
+                       (E, Loop_N,
+                        Children_Permission (New_Tree),
+                        Children_Permission (Orig_Tree));
+                  end if;
+
+               when Reference =>
+                  Check_Is_More_Restrictive_Tree_Than
+                    (Get_All (Orig_Tree), Children_Permission (New_Tree), E);
+
+               when Array_Component =>
+                  Check_Is_More_Restrictive_Tree_Than
+                    (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E);
+
+               when Record_Component =>
+                  declare
+                     Comp : Perm_Tree_Access;
+                  begin
+                     Comp := Perm_Tree_Maps.Get_First
+                       (Component (Orig_Tree));
+                     while Comp /= null loop
+                        Check_Is_More_Restrictive_Tree_Than
+                          (Comp, Children_Permission (New_Tree), E);
+                        Comp := Perm_Tree_Maps.Get_Next
+                          (Component (Orig_Tree));
+                     end loop;
+
+                     Check_Is_More_Restrictive_Tree_Than
+                       (Other_Components (Orig_Tree),
+                        Children_Permission (New_Tree), E);
+                  end;
+               end case;
+
+            when Reference =>
+               case Kind (Orig_Tree) is
+               when Entire_Object =>
+                  Check_Is_Less_Restrictive_Tree_Than
+                    (Get_All (New_Tree), Children_Permission (Orig_Tree), E);
+
+               when Reference =>
+                  Check_Is_Less_Restrictive_Tree
+                    (Get_All (New_Tree), Get_All (Orig_Tree), E);
+
+               when others =>
+                  raise Program_Error;
+               end case;
+
+            when Array_Component =>
+               case Kind (Orig_Tree) is
+               when Entire_Object =>
+                  Check_Is_Less_Restrictive_Tree_Than
+                    (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E);
+
+               when Array_Component =>
+                  Check_Is_Less_Restrictive_Tree
+                    (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E);
+
+               when others =>
+                  raise Program_Error;
+               end case;
+
+            when Record_Component =>
+               declare
+                  CompN : Perm_Tree_Access;
+               begin
+                  CompN :=
+                    Perm_Tree_Maps.Get_First (Component (New_Tree));
+                  case Kind (Orig_Tree) is
+                  when Entire_Object =>
+                     while CompN /= null loop
+                        Check_Is_Less_Restrictive_Tree_Than
+                          (CompN, Children_Permission (Orig_Tree), E);
+
+                        CompN :=
+                          Perm_Tree_Maps.Get_Next (Component (New_Tree));
+                     end loop;
+
+                     Check_Is_Less_Restrictive_Tree_Than
+                       (Other_Components (New_Tree),
+                        Children_Permission (Orig_Tree),
+                        E);
+
+                  when Record_Component =>
+                     declare
+
+                        KeyO : Perm_Tree_Maps.Key_Option;
+                        CompO : Perm_Tree_Access;
+                     begin
+                        KeyO := Perm_Tree_Maps.Get_First_Key
+                          (Component (Orig_Tree));
+                        while KeyO.Present loop
+                           pragma Assert (CompO /= null);
+
+                           Check_Is_Less_Restrictive_Tree (CompN, CompO, E);
+
+                           KeyO := Perm_Tree_Maps.Get_Next_Key
+                             (Component (Orig_Tree));
+                           CompN := Perm_Tree_Maps.Get
+                             (Component (New_Tree), KeyO.K);
+                           CompO := Perm_Tree_Maps.Get
+                             (Component (Orig_Tree), KeyO.K);
+                        end loop;
+
+                        Check_Is_Less_Restrictive_Tree
+                          (Other_Components (New_Tree),
+                           Other_Components (Orig_Tree),
+                           E);
+                     end;
+
+                  when others =>
+                     raise Program_Error;
+                  end case;
+               end;
+         end case;
+      end Check_Is_Less_Restrictive_Tree;
+
+      --------------------------
+      -- Perm_Error_Loop_Exit --
+      --------------------------
+
+      procedure Perm_Error_Loop_Exit
+        (E          : Entity_Id;
+         Loop_Id    : Node_Id;
+         Perm       : Perm_Kind;
+         Found_Perm : Perm_Kind)
+      is
+      begin
+         Error_Msg_Node_2 := Loop_Id;
+         Error_Msg_N ("insufficient permission for & when exiting loop &", E);
+         Perm_Mismatch (Exp_Perm => Perm,
+                        Act_Perm => Found_Perm,
+                        N        => Loop_Id);
+      end Perm_Error_Loop_Exit;
+
+      --  Local variables
+
+      Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
+      Loop_Env  : constant Perm_Env_Access := new Perm_Env;
+
+   begin
+      --  Save environment prior to the loop
+
+      Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
+
+      --  Add saved environment to loop environment
+
+      Set (Current_Loops_Envs, Loop_Name, Loop_Env);
+
+      --  If the loop is not a plain-loop, then it may either never be entered,
+      --  or it may be exited after a number of iterations. Hence add the
+      --  current permission environment as the initial loop exit environment.
+      --  Otherwise, the loop exit environment remains empty until it is
+      --  populated by analyzing exit statements.
+
+      if Present (Iteration_Scheme (Loop_N)) then
+         declare
+            Exit_Env  : constant Perm_Env_Access := new Perm_Env;
+         begin
+            Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
+            Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
+         end;
+      end if;
+
+      --  Analyze loop
+
+      Check_Node (Iteration_Scheme (Loop_N));
+      Check_List (Statements (Loop_N));
+
+      --  Check that environment gets less restrictive at end of loop
+
+      Check_Is_Less_Restrictive_Env
+        (Exiting_Env => Current_Perm_Env,
+         Entry_Env   => Loop_Env.all);
+
+      --  Set environment to the one for exiting the loop
+
+      declare
+         Exit_Env : constant Perm_Env_Access :=
+           Get (Current_Loops_Accumulators, Loop_Name);
+      begin
+         Free_Env (Current_Perm_Env);
+
+         --  In the normal case, Exit_Env is not null and we use it. In the
+         --  degraded case of a plain-loop without exit statements, Exit_Env is
+         --  null, and we use the initial permission environment at the start
+         --  of the loop to continue analysis. Any environment would be fine
+         --  here, since the code after the loop is dead code, but this way we
+         --  avoid spurious errors by having at least variables in scope inside
+         --  the environment.
+
+         if Exit_Env /= null then
+            Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
+         else
+            Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
+         end if;
+
+         Free_Env (Loop_Env.all);
+         Free_Env (Exit_Env.all);
+      end;
+   end Check_Loop_Statement;
+
+   ----------------
+   -- Check_Node --
+   ----------------
+
+   procedure Check_Node (N : Node_Id) is
+      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+   begin
+      case Nkind (N) is
+         when N_Declaration =>
+            Check_Declaration (N);
+
+         when N_Subexpr =>
+            Check_Expression (N);
+
+         when N_Subtype_Indication =>
+            Check_Node (Constraint (N));
+
+         when N_Body_Stub =>
+            Check_Node (Get_Body_From_Stub (N));
+
+         when N_Statement_Other_Than_Procedure_Call =>
+            Check_Statement (N);
+
+         when N_Package_Body =>
+            Check_Package_Body (N);
+
+         when N_Subprogram_Body
+            | N_Entry_Body
+            | N_Task_Body
+         =>
+            Check_Callable_Body (N);
+
+         when N_Protected_Body =>
+            Check_List (Declarations (N));
+
+         when N_Package_Declaration =>
+            declare
+               Spec : constant Node_Id := Specification (N);
+            begin
+               Current_Checking_Mode := Read;
+               Check_List (Visible_Declarations (Spec));
+               Check_List (Private_Declarations (Spec));
+
+               Return_Declarations (Visible_Declarations (Spec));
+               Return_Declarations (Private_Declarations (Spec));
+            end;
+
+         when N_Iteration_Scheme =>
+            Current_Checking_Mode := Read;
+            Check_Node (Condition (N));
+            Check_Node (Iterator_Specification (N));
+            Check_Node (Loop_Parameter_Specification (N));
+
+         when N_Case_Expression_Alternative =>
+            Current_Checking_Mode := Read;
+            Check_List (Discrete_Choices (N));
+            Current_Checking_Mode := Mode_Before;
+            Check_Node (Expression (N));
+
+         when N_Case_Statement_Alternative =>
+            Current_Checking_Mode := Read;
+            Check_List (Discrete_Choices (N));
+            Current_Checking_Mode := Mode_Before;
+            Check_List (Statements (N));
+
+         when N_Component_Association =>
+            Check_Node (Expression (N));
+
+         when N_Handled_Sequence_Of_Statements =>
+            Check_List (Statements (N));
+
+         when N_Parameter_Association =>
+            Check_Node (Explicit_Actual_Parameter (N));
+
+         when N_Range_Constraint =>
+            Check_Node (Range_Expression (N));
+
+         when N_Index_Or_Discriminant_Constraint =>
+            Check_List (Constraints (N));
+
+         --  Checking should not be called directly on these nodes
+
+         when N_Abortable_Part
+            | N_Accept_Alternative
+            | N_Access_Definition
+            | N_Access_Function_Definition
+            | N_Access_Procedure_Definition
+            | N_Access_To_Object_Definition
+            | N_Aspect_Specification
+            | N_Compilation_Unit
+            | N_Compilation_Unit_Aux
+            | N_Component_Clause
+            | N_Component_Definition
+            | N_Component_List
+            | N_Constrained_Array_Definition
+            | N_Contract
+            | N_Decimal_Fixed_Point_Definition
+            | N_Defining_Character_Literal
+            | N_Defining_Identifier
+            | N_Defining_Operator_Symbol
+            | N_Defining_Program_Unit_Name
+            | N_Delay_Alternative
+            | N_Derived_Type_Definition
+            | N_Designator
+            | N_Discriminant_Association
+            | N_Discriminant_Specification
+            | N_Elsif_Part
+            | N_Entry_Body_Formal_Part
+            | N_Enumeration_Type_Definition
+            | N_Entry_Call_Alternative
+            | N_Entry_Index_Specification
+            | N_Error
+            | N_Exception_Handler
+            | N_Floating_Point_Definition
+            | N_Formal_Decimal_Fixed_Point_Definition
+            | N_Formal_Derived_Type_Definition
+            | N_Formal_Discrete_Type_Definition
+            | N_Formal_Floating_Point_Definition
+            | N_Formal_Incomplete_Type_Definition
+            | N_Formal_Modular_Type_Definition
+            | N_Formal_Ordinary_Fixed_Point_Definition
+            | N_Formal_Private_Type_Definition
+            | N_Formal_Signed_Integer_Type_Definition
+            | N_Generic_Association
+            | N_Mod_Clause
+            | N_Modular_Type_Definition
+            | N_Ordinary_Fixed_Point_Definition
+            | N_Package_Specification
+            | N_Parameter_Specification
+            | N_Pragma_Argument_Association
+            | N_Protected_Definition
+            | N_Push_Pop_xxx_Label
+            | N_Real_Range_Specification
+            | N_Record_Definition
+            | N_SCIL_Dispatch_Table_Tag_Init
+            | N_SCIL_Dispatching_Call
+            | N_SCIL_Membership_Test
+            | N_Signed_Integer_Type_Definition
+            | N_Subunit
+            | N_Task_Definition
+            | N_Terminate_Alternative
+            | N_Triggering_Alternative
+            | N_Unconstrained_Array_Definition
+            | N_Unused_At_Start
+            | N_Unused_At_End
+            | N_Variant
+            | N_Variant_Part
+         =>
+            raise Program_Error;
+
+         --  Unsupported constructs in SPARK
+
+         when N_Iterated_Component_Association =>
+            Error_Msg_N ("unsupported construct in SPARK", N);
+
+         --  Ignored constructs for pointer checking
+
+         when N_Abstract_Subprogram_Declaration
+            | N_At_Clause
+            | N_Attribute_Definition_Clause
+            | N_Delta_Constraint
+            | N_Digits_Constraint
+            | N_Empty
+            | N_Enumeration_Representation_Clause
+            | N_Exception_Declaration
+            | N_Exception_Renaming_Declaration
+            | N_Formal_Package_Declaration
+            | N_Formal_Subprogram_Declaration
+            | N_Freeze_Entity
+            | N_Freeze_Generic_Entity
+            | N_Function_Instantiation
+            | N_Generic_Function_Renaming_Declaration
+            | N_Generic_Package_Declaration
+            | N_Generic_Package_Renaming_Declaration
+            | N_Generic_Procedure_Renaming_Declaration
+            | N_Generic_Subprogram_Declaration
+            | N_Implicit_Label_Declaration
+            | N_Itype_Reference
+            | N_Label
+            | N_Number_Declaration
+            | N_Object_Renaming_Declaration
+            | N_Others_Choice
+            | N_Package_Instantiation
+            | N_Package_Renaming_Declaration
+            | N_Pragma
+            | N_Procedure_Instantiation
+            | N_Record_Representation_Clause
+            | N_Subprogram_Declaration
+            | N_Subprogram_Renaming_Declaration
+            | N_Task_Type_Declaration
+            | N_Use_Package_Clause
+            | N_With_Clause
+            | N_Use_Type_Clause
+            | N_Validate_Unchecked_Conversion
+         =>
+            null;
+
+         --  The following nodes are rewritten by semantic analysis
+
+         when N_Single_Protected_Declaration
+            | N_Single_Task_Declaration
+         =>
+            raise Program_Error;
+      end case;
+
+      Current_Checking_Mode := Mode_Before;
+   end Check_Node;
+
+   ------------------------
+   -- Check_Package_Body --
+   ------------------------
+
+   procedure Check_Package_Body (Pack : Node_Id) is
+      Saved_Env : Perm_Env;
+      CorSp : Node_Id;
+
+   begin
+      if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
+         if Get_SPARK_Mode_From_Annotation
+           (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
+         then
+            return;
+         end if;
+      else
+         return;
+      end if;
+
+      CorSp := Parent (Corresponding_Spec (Pack));
+      while Nkind (CorSp) /= N_Package_Specification loop
+         CorSp := Parent (CorSp);
+      end loop;
+
+      Check_List (Visible_Declarations (CorSp));
+
+      --  Save environment
+
+      Copy_Env (Current_Perm_Env,
+                Saved_Env);
+
+      Check_List (Private_Declarations (CorSp));
+
+      --  Set mode to Read, and then analyze declarations and statements
+
+      Current_Checking_Mode := Read;
+
+      Check_List (Declarations (Pack));
+      Check_Node (Handled_Statement_Sequence (Pack));
+
+      --  Check RW for every stateful variable (i.e. in declarations)
+
+      Return_Declarations (Private_Declarations (CorSp));
+      Return_Declarations (Visible_Declarations (CorSp));
+      Return_Declarations (Declarations (Pack));
+
+      --  Restore previous environment (i.e. delete every nonvisible
+      --  declaration) from environment.
+
+      Free_Env (Current_Perm_Env);
+      Copy_Env (Saved_Env,
+                Current_Perm_Env);
+   end Check_Package_Body;
+
+   -----------------
+   -- Check_Param --
+   -----------------
+
+   procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
+      Mode : constant Entity_Kind := Ekind (Formal);
+      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+
+   begin
+      case Current_Checking_Mode is
+         when Read =>
+            case Formal_Kind'(Mode) is
+               when E_In_Parameter =>
+                  if Is_Borrowed_In (Formal) then
+                     --  Borrowed in
+
+                     Current_Checking_Mode := Move;
+                  else
+                     --  Observed
+
+                     return;
+                  end if;
+
+               when E_Out_Parameter =>
+                  return;
+
+               when E_In_Out_Parameter =>
+                  --  Borrowed in out
+
+                  Current_Checking_Mode := Move;
+
+            end case;
+
+            Check_Node (Actual);
+
+         when Assign =>
+            case Formal_Kind'(Mode) is
+               when E_In_Parameter =>
+                  null;
+
+               when E_Out_Parameter
+                  | E_In_Out_Parameter
+               =>
+                  --  Borrowed out or in out
+
+                  Process_Path (Actual);
+
+            end case;
+
+         when others =>
+            raise Program_Error;
+
+      end case;
+      Current_Checking_Mode := Mode_Before;
+   end Check_Param;
+
+   --------------------------
+   -- Check_Param_Observes --
+   --------------------------
+
+   procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is
+      Mode : constant Entity_Kind := Ekind (Formal);
+      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+
+   begin
+      case Mode is
+         when E_In_Parameter =>
+            if not Is_Borrowed_In (Formal) then
+               --  Observed in
+
+               Current_Checking_Mode := Observe;
+               Check_Node (Actual);
+            end if;
+
+         when others =>
+            null;
+
+      end case;
+
+      Current_Checking_Mode := Mode_Before;
+   end Check_Param_Observes;
+
+   ----------------------
+   -- Check_Param_Outs --
+   ----------------------
+
+   procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is
+      Mode : constant Entity_Kind := Ekind (Formal);
+      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+
+   begin
+
+      case Mode is
+         when E_Out_Parameter =>
+            --  Borrowed out
+            Current_Checking_Mode := Borrow_Out;
+            Check_Node (Actual);
+
+         when others =>
+            null;
+
+      end case;
+
+      Current_Checking_Mode := Mode_Before;
+   end Check_Param_Outs;
+
+   ----------------------
+   -- Check_Param_Read --
+   ----------------------
+
+   procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is
+      Mode : constant Entity_Kind := Ekind (Formal);
+
+   begin
+      pragma Assert (Current_Checking_Mode = Read);
+
+      case Formal_Kind'(Mode) is
+         when E_In_Parameter =>
+            Check_Node (Actual);
+
+         when E_Out_Parameter
+            | E_In_Out_Parameter
+         =>
+            null;
+
+      end case;
+   end Check_Param_Read;
+
+   -------------------------
+   -- Check_Safe_Pointers --
+   -------------------------
+
+   procedure Check_Safe_Pointers (N : Node_Id) is
+
+      --  Local subprograms
+
+      procedure Check_List (L : List_Id);
+      --  Call the main analysis procedure on each element of the list
+
+      procedure Initialize;
+      --  Initialize global variables before starting the analysis of a body
+
+      ----------------
+      -- Check_List --
+      ----------------
+
+      procedure Check_List (L : List_Id) is
+         N : Node_Id;
+      begin
+         N := First (L);
+         while Present (N) loop
+            Check_Safe_Pointers (N);
+            Next (N);
+         end loop;
+      end Check_List;
+
+      ----------------
+      -- Initialize --
+      ----------------
+
+      procedure Initialize is
+      begin
+         Reset (Current_Loops_Envs);
+         Reset (Current_Loops_Accumulators);
+         Reset (Current_Perm_Env);
+         Reset (Current_Initialization_Map);
+      end Initialize;
+
+      --  Local variables
+
+      Prag : Node_Id;
+      --  SPARK_Mode pragma in application
+
+   --  Start of processing for Check_Safe_Pointers
+
+   begin
+      Initialize;
+
+      case Nkind (N) is
+         when N_Compilation_Unit =>
+            Check_Safe_Pointers (Unit (N));
+
+         when N_Package_Body
+            | N_Package_Declaration
+            | N_Subprogram_Body
+         =>
+            Prag := SPARK_Pragma (Defining_Entity (N));
+            if Present (Prag) then
+               if Get_SPARK_Mode_From_Annotation (Prag) = Opt.Off then
+                  return;
+               else
+                  Check_Node (N);
+               end if;
+
+            elsif Nkind (N) = N_Package_Body then
+               Check_List (Declarations (N));
+
+            elsif Nkind (N) = N_Package_Declaration then
+               Check_List (Private_Declarations (Specification (N)));
+               Check_List (Visible_Declarations (Specification (N)));
+            end if;
+
+         when others =>
+            null;
+      end case;
+   end Check_Safe_Pointers;
+
+   ---------------------
+   -- Check_Statement --
+   ---------------------
+
+   procedure Check_Statement (Stmt : Node_Id) is
+      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+   begin
+      case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is
+         when N_Entry_Call_Statement =>
+            Check_Call_Statement (Stmt);
+
+         --  Move right-hand side first, and then assign left-hand side
+
+         when N_Assignment_Statement =>
+            if Is_Deep (Etype (Expression (Stmt))) then
+               Current_Checking_Mode := Move;
+            else
+               Current_Checking_Mode := Read;
+            end if;
+
+            Check_Node (Expression (Stmt));
+            Current_Checking_Mode := Assign;
+            Check_Node (Name (Stmt));
+
+         when N_Block_Statement =>
+            declare
+               Saved_Env : Perm_Env;
+
+            begin
+               --  Save environment
+
+               Copy_Env (Current_Perm_Env,
+                                 Saved_Env);
+
+               --  Analyze declarations and Handled_Statement_Sequences
+
+               Current_Checking_Mode := Read;
+               Check_List (Declarations (Stmt));
+               Check_Node (Handled_Statement_Sequence (Stmt));
+
+               --  Restore environment
+
+               Free_Env (Current_Perm_Env);
+               Copy_Env (Saved_Env,
+                                 Current_Perm_Env);
+            end;
+
+         when N_Case_Statement =>
+            declare
+               Saved_Env : Perm_Env;
+
+               --  Accumulator for the different branches
+
+               New_Env : Perm_Env;
+
+               Elmt : Node_Id := First (Alternatives (Stmt));
+
+            begin
+               Current_Checking_Mode := Read;
+               Check_Node (Expression (Stmt));
+               Current_Checking_Mode := Mode_Before;
+
+               --  Save environment
+
+               Copy_Env (Current_Perm_Env,
+                                 Saved_Env);
+
+               --  Here we have the original env in saved, current with a fresh
+               --  copy, and new aliased.
+
+               --  First alternative
+
+               Check_Node (Elmt);
+               Next (Elmt);
+
+               Copy_Env (Current_Perm_Env,
+                                 New_Env);
+               Free_Env (Current_Perm_Env);
+
+               --  Other alternatives
+
+               while Present (Elmt) loop
+                  --  Restore environment
+
+                  Copy_Env (Saved_Env,
+                                    Current_Perm_Env);
+
+                  Check_Node (Elmt);
+
+                  --  Merge Current_Perm_Env into New_Env
+
+                  Merge_Envs (New_Env,
+                                      Current_Perm_Env);
+
+                  Next (Elmt);
+               end loop;
+
+               --  CLEANUP
+               Copy_Env (New_Env,
+                                 Current_Perm_Env);
+
+               Free_Env (New_Env);
+               Free_Env (Saved_Env);
+            end;
+
+         when N_Delay_Relative_Statement =>
+            Check_Node (Expression (Stmt));
+
+         when N_Delay_Until_Statement =>
+            Check_Node (Expression (Stmt));
+
+         when N_Loop_Statement =>
+            Check_Loop_Statement (Stmt);
+
+         --  If deep type expression, then move, else read
+
+         when N_Simple_Return_Statement =>
+            case Nkind (Expression (Stmt)) is
+               when N_Empty =>
+                  declare
+                     --  ??? This does not take into account the fact that
+                     --  a simple return inside an extended return statement
+                     --  applies to the extended return statement.
+                     Subp : constant Entity_Id :=
+                       Return_Applies_To (Return_Statement_Entity (Stmt));
+                  begin
+                     Return_Parameters (Subp);
+                     Return_Globals (Subp);
+                  end;
+
+               when others =>
+                  if Is_Deep (Etype (Expression (Stmt))) then
+                     Current_Checking_Mode := Move;
+                  elsif Is_Shallow (Etype (Expression (Stmt))) then
+                     Current_Checking_Mode := Read;
+                  else
+                     raise Program_Error;
+                  end if;
+
+                  Check_Node (Expression (Stmt));
+            end case;
+
+         when N_Extended_Return_Statement =>
+            Check_List (Return_Object_Declarations (Stmt));
+            Check_Node (Handled_Statement_Sequence (Stmt));
+
+            Return_Declarations (Return_Object_Declarations (Stmt));
+
+            declare
+               --  ??? This does not take into account the fact that a simple
+               --  return inside an extended return statement applies to the
+               --  extended return statement.
+               Subp : constant Entity_Id :=
+                 Return_Applies_To (Return_Statement_Entity (Stmt));
+            begin
+               Return_Parameters (Subp);
+               Return_Globals (Subp);
+            end;
+
+         --  Merge the current_Perm_Env with the accumulator for the given loop
+
+         when N_Exit_Statement =>
+            declare
+               Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
+
+               Saved_Accumulator : constant Perm_Env_Access :=
+                 Get (Current_Loops_Accumulators, Loop_Name);
+
+               Environment_Copy : constant Perm_Env_Access :=
+                 new Perm_Env;
+            begin
+
+               Copy_Env (Current_Perm_Env,
+                                 Environment_Copy.all);
+
+               if Saved_Accumulator = null then
+                  Set (Current_Loops_Accumulators,
+                       Loop_Name, Environment_Copy);
+               else
+                  Merge_Envs (Saved_Accumulator.all,
+                                      Environment_Copy.all);
+               end if;
+            end;
+
+         --  Copy environment, run on each branch, and then merge
+
+         when N_If_Statement =>
+            declare
+               Saved_Env : Perm_Env;
+
+               --  Accumulator for the different branches
+
+               New_Env : Perm_Env;
+
+            begin
+
+               Check_Node (Condition (Stmt));
+
+               --  Save environment
+
+               Copy_Env (Current_Perm_Env,
+                                 Saved_Env);
+
+               --  Here we have the original env in saved, current with a fresh
+               --  copy.
+
+               --  THEN PART
+
+               Check_List (Then_Statements (Stmt));
+
+               Copy_Env (Current_Perm_Env,
+                                 New_Env);
+
+               Free_Env (Current_Perm_Env);
+
+               --  Here the new_environment contains curr env after then block
+
+               --  ELSIF part
+               declare
+                  Elmt : Node_Id;
+
+               begin
+                  Elmt := First (Elsif_Parts (Stmt));
+                  while Present (Elmt) loop
+                     --  Transfer into accumulator, and restore from save
+
+                     Copy_Env (Saved_Env,
+                                       Current_Perm_Env);
+
+                     Check_Node (Condition (Elmt));
+                     Check_List (Then_Statements (Stmt));
+
+                     --  Merge Current_Perm_Env into New_Env
+
+                     Merge_Envs (New_Env,
+                                         Current_Perm_Env);
+
+                     Next (Elmt);
+                  end loop;
+               end;
+
+               --  ELSE part
+
+               --  Restore environment before if
+
+               Copy_Env (Saved_Env,
+                                 Current_Perm_Env);
+
+               --  Here new environment contains the environment after then and
+               --  current the fresh copy of old one.
+
+               Check_List (Else_Statements (Stmt));
+
+               Merge_Envs (New_Env,
+                                   Current_Perm_Env);
+
+               --  CLEANUP
+
+               Copy_Env (New_Env,
+                                 Current_Perm_Env);
+
+               Free_Env (New_Env);
+               Free_Env (Saved_Env);
+            end;
+
+         --  Unsupported constructs in SPARK
+
+         when N_Abort_Statement
+            | N_Accept_Statement
+            | N_Asynchronous_Select
+            | N_Code_Statement
+            | N_Conditional_Entry_Call
+            | N_Goto_Statement
+            | N_Requeue_Statement
+            | N_Selective_Accept
+            | N_Timed_Entry_Call
+         =>
+            Error_Msg_N ("unsupported construct in SPARK", Stmt);
+
+         --  Ignored constructs for pointer checking
+
+         when N_Null_Statement
+            | N_Raise_Statement
+         =>
+            null;
+
+         --  The following nodes are never generated in GNATprove mode
+
+         when N_Compound_Statement
+            | N_Free_Statement
+         =>
+            raise Program_Error;
+      end case;
+   end Check_Statement;
+
+   --------------
+   -- Get_Perm --
+   --------------
+
+   function Get_Perm (N : Node_Id) return Perm_Kind is
+      Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
+
+   begin
+      case Tree_Or_Perm.R is
+         when Folded =>
+            return Tree_Or_Perm.Found_Permission;
+
+         when Unfolded =>
+            pragma Assert (Tree_Or_Perm.Tree_Access /= null);
+            return Permission (Tree_Or_Perm.Tree_Access);
+
+         --  We encoutered a function call, hence the memory area is fresh,
+         --  which means that the association permission is RW.
+
+         when Function_Call =>
+            return Read_Write;
+
+      end case;
+   end Get_Perm;
+
+   ----------------------
+   -- Get_Perm_Or_Tree --
+   ----------------------
+
+   function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
+   begin
+      case Nkind (N) is
+
+         --  Base identifier. Normally those are the roots of the trees stored
+         --  in the permission environment.
+
+         when N_Defining_Identifier =>
+            raise Program_Error;
+
+         when N_Identifier
+            | N_Expanded_Name
+         =>
+            declare
+               P : constant Entity_Id := Entity (N);
+
+               C : constant Perm_Tree_Access :=
+                 Get (Current_Perm_Env, Unique_Entity (P));
+
+            begin
+               --  Setting the initialization map to True, so that this
+               --  variable cannot be ignored anymore when looking at end
+               --  of elaboration of package.
+
+               Set (Current_Initialization_Map, Unique_Entity (P), True);
+
+               if C = null then
+                  --  No null possible here, there are no parents for the path.
+                  --  This means we are using a global variable without adding
+                  --  it in environment with a global aspect.
+
+                  Illegal_Global_Usage (N);
+               else
+                  return (R => Unfolded, Tree_Access => C);
+               end if;
+            end;
+
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+            | N_Qualified_Expression
+         =>
+            return Get_Perm_Or_Tree (Expression (N));
+
+         --  Happening when we try to get the permission of a variable that
+         --  is a formal parameter. We get instead the defining identifier
+         --  associated with the parameter (which is the one that has been
+         --  stored for indexing).
+
+         when N_Parameter_Specification =>
+            return Get_Perm_Or_Tree (Defining_Identifier (N));
+
+         --  We get the permission tree of its prefix, and then get either the
+         --  subtree associated with that specific selection, or if we have a
+         --  leaf that folds its children, we take the children's permission
+         --  and return it using the discriminant Folded.
+
+         when N_Selected_Component =>
+            declare
+               C : constant Perm_Or_Tree :=
+                 Get_Perm_Or_Tree (Prefix (N));
+
+            begin
+               case C.R is
+                  when Folded
+                     | Function_Call
+                  =>
+                     return C;
+
+                  when Unfolded =>
+                     pragma Assert (C.Tree_Access /= null);
+
+                     pragma Assert (Kind (C.Tree_Access) = Entire_Object
+                                    or else
+                                    Kind (C.Tree_Access) = Record_Component);
+
+                     if Kind (C.Tree_Access) = Record_Component then
+                        declare
+                           Selected_Component : constant Entity_Id :=
+                             Entity (Selector_Name (N));
+
+                           Selected_C : constant Perm_Tree_Access :=
+                             Perm_Tree_Maps.Get
+                               (Component (C.Tree_Access), Selected_Component);
+
+                        begin
+                           if Selected_C = null then
+                              return (R => Unfolded,
+                                      Tree_Access =>
+                                        Other_Components (C.Tree_Access));
+                           else
+                              return (R => Unfolded,
+                                      Tree_Access => Selected_C);
+                           end if;
+                        end;
+                     elsif Kind (C.Tree_Access) = Entire_Object then
+                        return (R => Folded, Found_Permission =>
+                                  Children_Permission (C.Tree_Access));
+                     else
+                        raise Program_Error;
+                     end if;
+               end case;
+            end;
+
+         --  We get the permission tree of its prefix, and then get either the
+         --  subtree associated with that specific selection, or if we have a
+         --  leaf that folds its children, we take the children's permission
+         --  and return it using the discriminant Folded.
+
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            declare
+               C : constant Perm_Or_Tree :=
+                 Get_Perm_Or_Tree (Prefix (N));
+
+            begin
+               case C.R is
+                  when Folded
+                     | Function_Call
+                  =>
+                     return C;
+
+                  when Unfolded =>
+                     pragma Assert (C.Tree_Access /= null);
+
+                     pragma Assert (Kind (C.Tree_Access) = Entire_Object
+                                    or else
+                                    Kind (C.Tree_Access) = Array_Component);
+
+                     if Kind (C.Tree_Access) = Array_Component then
+                        pragma Assert (Get_Elem (C.Tree_Access) /= null);
+
+                        return (R => Unfolded,
+                                Tree_Access => Get_Elem (C.Tree_Access));
+                     elsif Kind (C.Tree_Access) = Entire_Object then
+                        return (R => Folded, Found_Permission =>
+                                  Children_Permission (C.Tree_Access));
+                     else
+                        raise Program_Error;
+                     end if;
+               end case;
+            end;
+
+         --  We get the permission tree of its prefix, and then get either the
+         --  subtree associated with that specific selection, or if we have a
+         --  leaf that folds its children, we take the children's permission
+         --  and return it using the discriminant Folded.
+
+         when N_Explicit_Dereference =>
+            declare
+               C : constant Perm_Or_Tree :=
+                 Get_Perm_Or_Tree (Prefix (N));
+
+            begin
+               case C.R is
+                  when Folded
+                     | Function_Call
+                  =>
+                     return C;
+
+                  when Unfolded =>
+                     pragma Assert (C.Tree_Access /= null);
+
+                     pragma Assert (Kind (C.Tree_Access) = Entire_Object
+                                    or else
+                                    Kind (C.Tree_Access) = Reference);
+
+                     if Kind (C.Tree_Access) = Reference then
+                        if Get_All (C.Tree_Access) = null then
+                           --  Hash_Table_Error
+                           raise Program_Error;
+                        else
+                           return
+                             (R => Unfolded,
+                              Tree_Access => Get_All (C.Tree_Access));
+                        end if;
+                     elsif Kind (C.Tree_Access) = Entire_Object then
+                        return (R => Folded, Found_Permission =>
+                                  Children_Permission (C.Tree_Access));
+                     else
+                        raise Program_Error;
+                     end if;
+               end case;
+            end;
+
+         --  The name contains a function call, hence the given path is always
+         --  new. We do not have to check for anything.
+
+         when N_Function_Call =>
+            return (R => Function_Call);
+
+         when others =>
+            raise Program_Error;
+      end case;
+   end Get_Perm_Or_Tree;
+
+   -------------------
+   -- Get_Perm_Tree --
+   -------------------
+
+   function Get_Perm_Tree
+     (N : Node_Id)
+       return Perm_Tree_Access
+   is
+   begin
+      case Nkind (N) is
+
+         --  Base identifier. Normally those are the roots of the trees stored
+         --  in the permission environment.
+
+         when N_Defining_Identifier =>
+            raise Program_Error;
+
+         when N_Identifier
+            | N_Expanded_Name
+         =>
+            declare
+               P : constant Node_Id := Entity (N);
+
+               C : constant Perm_Tree_Access :=
+                 Get (Current_Perm_Env, Unique_Entity (P));
+
+            begin
+               --  Setting the initialization map to True, so that this
+               --  variable cannot be ignored anymore when looking at end
+               --  of elaboration of package.
+
+               Set (Current_Initialization_Map, Unique_Entity (P), True);
+
+               if C = null then
+                  --  No null possible here, there are no parents for the path.
+                  --  This means we are using a global variable without adding
+                  --  it in environment with a global aspect.
+
+                  Illegal_Global_Usage (N);
+               else
+                  return C;
+               end if;
+            end;
+
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+            | N_Qualified_Expression
+         =>
+            return Get_Perm_Tree (Expression (N));
+
+         when N_Parameter_Specification =>
+            return Get_Perm_Tree (Defining_Identifier (N));
+
+         --  We get the permission tree of its prefix, and then get either the
+         --  subtree associated with that specific selection, or if we have a
+         --  leaf that folds its children, we unroll it in one step.
+
+         when N_Selected_Component =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Get_Perm_Tree (Prefix (N));
+
+            begin
+               if C = null then
+                  --  If null then it means we went through a function call
+
+                  return null;
+               end if;
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Record_Component);
+
+               if Kind (C) = Record_Component then
+                  --  The tree is unfolded. We just return the subtree.
+
+                  declare
+                     Selected_Component : constant Entity_Id :=
+                       Entity (Selector_Name (N));
+                     Selected_C : constant Perm_Tree_Access :=
+                       Perm_Tree_Maps.Get
+                         (Component (C), Selected_Component);
+
+                  begin
+                     if Selected_C = null then
+                        return Other_Components (C);
+                     end if;
+
+                     return Selected_C;
+                  end;
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace the node with
+                     --  Record_Component.
+
+                     Elem : Node_Id;
+
+                     --  Create the unrolled nodes
+
+                     Son : Perm_Tree_Access;
+
+                     Child_Perm : constant Perm_Kind :=
+                       Children_Permission (C);
+
+                  begin
+
+                     --  We change the current node from Entire_Object to
+                     --  Record_Component with same permission and an empty
+                     --  hash table as component list.
+
+                     C.all.Tree :=
+                       (Kind             => Record_Component,
+                        Is_Node_Deep     => Is_Node_Deep (C),
+                        Permission       => Permission (C),
+                        Component        => Perm_Tree_Maps.Nil,
+                        Other_Components =>
+                           new Perm_Tree_Wrapper'
+                          (Tree =>
+                               (Kind                => Entire_Object,
+                                --  Is_Node_Deep is true, to be conservative
+                                Is_Node_Deep        => True,
+                                Permission          => Child_Perm,
+                                Children_Permission => Child_Perm)
+                          )
+                       );
+
+                     --  We fill the hash table with all sons of the record,
+                     --  with basic Entire_Objects nodes.
+                     Elem := First_Component_Or_Discriminant
+                       (Etype (Prefix (N)));
+
+                     while Present (Elem) loop
+                        Son := new Perm_Tree_Wrapper'
+                          (Tree =>
+                             (Kind                => Entire_Object,
+                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
+                              Permission          => Child_Perm,
+                              Children_Permission => Child_Perm));
+
+                        Perm_Tree_Maps.Set
+                          (C.all.Tree.Component, Elem, Son);
+
+                        Next_Component_Or_Discriminant (Elem);
+                     end loop;
+
+                     --  we return the tree to the sons, so that the recursion
+                     --  can continue.
+
+                     declare
+                        Selected_Component : constant Entity_Id :=
+                          Entity (Selector_Name (N));
+
+                        Selected_C : constant Perm_Tree_Access :=
+                          Perm_Tree_Maps.Get
+                            (Component (C), Selected_Component);
+
+                     begin
+                        pragma Assert (Selected_C /= null);
+
+                        return Selected_C;
+                     end;
+
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+         --  We set the permission tree of its prefix, and then we extract from
+         --  the returned pointer the subtree. If folded, we unroll the tree at
+         --  one step.
+
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Get_Perm_Tree (Prefix (N));
+
+            begin
+               if C = null then
+                  --  If null then we went through a function call
+
+                  return null;
+               end if;
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Array_Component);
+
+               if Kind (C) = Array_Component then
+                  --  The tree is unfolded. We just return the elem subtree
+
+                  pragma Assert (Get_Elem (C) = null);
+
+                  return Get_Elem (C);
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace node with Array_Component.
+
+                     Son : Perm_Tree_Access;
+
+                  begin
+                     Son := new Perm_Tree_Wrapper'
+                       (Tree =>
+                          (Kind                => Entire_Object,
+                           Is_Node_Deep        => Is_Node_Deep (C),
+                           Permission          => Children_Permission (C),
+                           Children_Permission => Children_Permission (C)));
+
+                     --  We change the current node from Entire_Object
+                     --  to Array_Component with same permission and the
+                     --  previously defined son.
+
+                     C.all.Tree := (Kind         => Array_Component,
+                                    Is_Node_Deep => Is_Node_Deep (C),
+                                    Permission   => Permission (C),
+                                    Get_Elem     => Son);
+
+                     return Get_Elem (C);
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+         --  We get the permission tree of its prefix, and then get either the
+         --  subtree associated with that specific selection, or if we have a
+         --  leaf that folds its children, we unroll the tree.
+
+         when N_Explicit_Dereference =>
+            declare
+               C : Perm_Tree_Access;
+
+            begin
+               C := Get_Perm_Tree (Prefix (N));
+
+               if C = null then
+                  --  If null, we went through a function call
+
+                  return null;
+               end if;
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Reference);
+
+               if Kind (C) = Reference then
+                  --  The tree is unfolded. We return the elem subtree
+
+                  if Get_All (C) = null then
+                     --  Hash_Table_Error
+                     raise Program_Error;
+                  end if;
+
+                  return Get_All (C);
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace the node with Reference.
+
+                     Son : Perm_Tree_Access;
+
+                  begin
+                     Son := new Perm_Tree_Wrapper'
+                       (Tree =>
+                          (Kind                => Entire_Object,
+                           Is_Node_Deep        => Is_Deep (Etype (N)),
+                           Permission          => Children_Permission (C),
+                           Children_Permission => Children_Permission (C)));
+
+                     --  We change the current node from Entire_Object to
+                     --  Reference with same permission and the previous son.
+
+                     pragma Assert (Is_Node_Deep (C));
+
+                     C.all.Tree := (Kind         => Reference,
+                                    Is_Node_Deep => Is_Node_Deep (C),
+                                    Permission   => Permission (C),
+                                    Get_All      => Son);
+
+                     return Get_All (C);
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+         --  No permission tree for function calls
+
+         when N_Function_Call =>
+            return null;
+
+         when others =>
+            raise Program_Error;
+      end case;
+   end Get_Perm_Tree;
+
+   ---------
+   -- Glb --
+   ---------
+
+   function Glb (P1, P2 : Perm_Kind) return Perm_Kind
+   is
+   begin
+      case P1 is
+         when No_Access =>
+            return No_Access;
+
+         when Read_Only =>
+            case P2 is
+               when No_Access
+                  | Write_Only
+               =>
+                  return No_Access;
+
+               when Read_Perm =>
+                  return Read_Only;
+            end case;
+
+         when Write_Only =>
+            case P2 is
+               when No_Access
+                  | Read_Only
+               =>
+                  return No_Access;
+
+               when Write_Perm =>
+                  return Write_Only;
+            end case;
+
+         when Read_Write =>
+            return P2;
+      end case;
+   end Glb;
+
+   ---------------
+   -- Has_Alias --
+   ---------------
+
+   function Has_Alias
+     (N : Node_Id)
+       return Boolean
+   is
+      function Has_Alias_Deep (Typ : Entity_Id) return Boolean;
+      function Has_Alias_Deep (Typ : Entity_Id) return Boolean
+      is
+         Comp : Node_Id;
+      begin
+
+         if Is_Array_Type (Typ)
+           and then Has_Aliased_Components (Typ)
+         then
+            return True;
+
+            --  Note: Has_Aliased_Components applies only to arrays
+
+         elsif Is_Record_Type (Typ) then
+            --  It is possible to have an aliased discriminant, so they must be
+            --  checked along with normal components.
+
+            Comp := First_Component_Or_Discriminant (Typ);
+            while Present (Comp) loop
+               if Is_Aliased (Comp)
+                 or else Is_Aliased (Etype (Comp))
+               then
+                  return True;
+               end if;
+
+               if Has_Alias_Deep (Etype (Comp)) then
+                  return True;
+               end if;
+
+               Next_Component_Or_Discriminant (Comp);
+            end loop;
+            return False;
+         else
+            return Is_Aliased (Typ);
+         end if;
+      end Has_Alias_Deep;
+
+   begin
+      case Nkind (N) is
+
+         when N_Identifier
+            | N_Expanded_Name
+         =>
+            return Has_Alias_Deep (Etype (N));
+
+         when N_Defining_Identifier =>
+            return Has_Alias_Deep (Etype (N));
+
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+            | N_Qualified_Expression
+         =>
+            return Has_Alias (Expression (N));
+
+         when N_Parameter_Specification =>
+            return Has_Alias (Defining_Identifier (N));
+
+         when N_Selected_Component =>
+            case Nkind (Selector_Name (N)) is
+               when N_Identifier =>
+                  if Is_Aliased (Entity (Selector_Name (N))) then
+                     return True;
+                  end if;
+
+               when others => null;
+
+            end case;
+
+            return Has_Alias (Prefix (N));
+
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            return Has_Alias (Prefix (N));
+
+         when N_Explicit_Dereference =>
+            return True;
+
+         when N_Function_Call =>
+            return False;
+
+         when N_Attribute_Reference =>
+            if Is_Deep (Etype (Prefix (N))) then
+               raise Program_Error;
+            end if;
+            return False;
+
+         when others =>
+            return False;
+      end case;
+   end Has_Alias;
+
+   -------------------------
+   -- Has_Array_Component --
+   -------------------------
+
+   function Has_Array_Component (N : Node_Id) return Boolean is
+   begin
+      case Nkind (N) is
+         --  Base identifier. There is no array component here.
+
+         when N_Identifier
+            | N_Expanded_Name
+            | N_Defining_Identifier
+         =>
+            return False;
+
+         --  We check if the expression inside the conversion has an array
+         --  component.
+
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+            | N_Qualified_Expression
+         =>
+            return Has_Array_Component (Expression (N));
+
+         --  We check if the prefix has an array component
+
+         when N_Selected_Component =>
+            return Has_Array_Component (Prefix (N));
+
+         --  We found the array component, return True
+
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            return True;
+
+         --  We check if the prefix has an array component
+
+         when N_Explicit_Dereference =>
+            return Has_Array_Component (Prefix (N));
+
+         when N_Function_Call =>
+            return False;
+
+         when others =>
+            raise Program_Error;
+      end case;
+   end Has_Array_Component;
+
+   ----------------------------
+   -- Has_Function_Component --
+   ----------------------------
+
+   function Has_Function_Component (N : Node_Id) return Boolean is
+   begin
+      case Nkind (N) is
+         --  Base identifier. There is no function component here.
+
+         when N_Identifier
+            | N_Expanded_Name
+            | N_Defining_Identifier
+         =>
+            return False;
+
+         --  We check if the expression inside the conversion has a function
+         --  component.
+
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+            | N_Qualified_Expression
+         =>
+            return Has_Function_Component (Expression (N));
+
+         --  We check if the prefix has a function component
+
+         when N_Selected_Component =>
+            return Has_Function_Component (Prefix (N));
+
+         --  We check if the prefix has a function component
+
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            return Has_Function_Component (Prefix (N));
+
+         --  We check if the prefix has a function component
+
+         when N_Explicit_Dereference =>
+            return Has_Function_Component (Prefix (N));
+
+         --  We found the function component, return True
+
+         when N_Function_Call =>
+            return True;
+
+         when others =>
+            raise Program_Error;
+
+      end case;
+   end Has_Function_Component;
+
+   --------
+   -- Hp --
+   --------
+
+   procedure Hp (P : Perm_Env) is
+      Elem : Perm_Tree_Maps.Key_Option;
+
+   begin
+      Elem := Get_First_Key (P);
+      while Elem.Present loop
+         Print_Node_Briefly (Elem.K);
+         Elem := Get_Next_Key (P);
+      end loop;
+   end Hp;
+
+   --------------------------
+   -- Illegal_Global_Usage --
+   --------------------------
+
+   procedure Illegal_Global_Usage (N : Node_Or_Entity_Id)  is
+   begin
+      Error_Msg_NE ("cannot use global variable & of deep type", N, N);
+      Error_Msg_N ("\without prior declaration in a Global aspect", N);
+
+      Errout.Finalize (Last_Call => True);
+      Errout.Output_Messages;
+      Exit_Program (E_Errors);
+   end Illegal_Global_Usage;
+
+   --------------------
+   -- Is_Borrowed_In --
+   --------------------
+
+   function Is_Borrowed_In (E : Entity_Id) return Boolean is
+   begin
+      return Is_Access_Type (Etype (E))
+        and then not Is_Access_Constant (Etype (E));
+   end Is_Borrowed_In;
+
+   -------------
+   -- Is_Deep --
+   -------------
+
+   function Is_Deep (E : Entity_Id) return Boolean is
+      function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean;
+
+      function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is
+         Decl : Node_Id;
+         Pack_Decl : Node_Id;
+
+      begin
+         if Is_Itype (E) then
+            Decl := Associated_Node_For_Itype (E);
+         else
+            Decl := Parent (E);
+         end if;
+
+         Pack_Decl := Parent (Parent (Decl));
+
+         if Nkind (Pack_Decl) /= N_Package_Declaration then
+            return False;
+         end if;
+
+         return
+           Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl)))
+           and then Get_SPARK_Mode_From_Annotation
+             (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off;
+      end Is_Private_Entity_Mode_Off;
+   begin
+      pragma Assert (Is_Type (E));
+
+      case Ekind (E) is
+         when Scalar_Kind =>
+            return False;
+
+         when Access_Kind =>
+            return True;
+
+         --  Just check the depth of its component type
+
+         when E_Array_Type
+            | E_Array_Subtype
+         =>
+            return Is_Deep (Component_Type (E));
+
+         when E_String_Literal_Subtype =>
+            return False;
+
+         --  Per RM 8.11 for class-wide types
+
+         when E_Class_Wide_Subtype
+            | E_Class_Wide_Type
+         =>
+            return True;
+
+         --  ??? What about hidden components
+
+         when E_Record_Type
+            | E_Record_Subtype
+            =>
+            declare
+               Elmt : Entity_Id;
+
+            begin
+               Elmt := First_Component_Or_Discriminant (E);
+               while Present (Elmt) loop
+                  if Is_Deep (Etype (Elmt)) then
+                     return True;
+                  else
+                     Next_Component_Or_Discriminant (Elmt);
+                  end if;
+               end loop;
+
+               return False;
+            end;
+
+         when Private_Kind =>
+            if Is_Private_Entity_Mode_Off (E) then
+               return False;
+            else
+               if Present (Full_View (E)) then
+                  return Is_Deep (Full_View (E));
+               else
+                  return True;
+               end if;
+            end if;
+
+         when E_Incomplete_Type =>
+            return True;
+
+         when E_Incomplete_Subtype =>
+            return True;
+
+         --  No problem with synchronized types
+
+         when E_Protected_Type
+            | E_Protected_Subtype
+            | E_Task_Subtype
+            | E_Task_Type
+          =>
+            return False;
+
+         when E_Exception_Type =>
+            return False;
+
+         when others =>
+            raise Program_Error;
+      end case;
+   end Is_Deep;
+
+   ----------------
+   -- Is_Shallow --
+   ----------------
+
+   function Is_Shallow (E : Entity_Id) return Boolean is
+   begin
+      pragma Assert (Is_Type (E));
+      return not Is_Deep (E);
+   end Is_Shallow;
+
+   ------------------
+   -- Loop_Of_Exit --
+   ------------------
+
+   function Loop_Of_Exit (N : Node_Id) return Entity_Id is
+      Nam : Node_Id := Name (N);
+      Stmt : Node_Id := N;
+   begin
+      if No (Nam) then
+         while Present (Stmt) loop
+            Stmt := Parent (Stmt);
+            if Nkind (Stmt) = N_Loop_Statement then
+               Nam := Identifier (Stmt);
+               exit;
+            end if;
+         end loop;
+      end if;
+      return Entity (Nam);
+   end Loop_Of_Exit;
+   ---------
+   -- Lub --
+   ---------
+
+   function Lub (P1, P2 : Perm_Kind) return Perm_Kind
+   is
+   begin
+      case P1 is
+         when No_Access =>
+            return P2;
+
+         when Read_Only =>
+            case P2 is
+               when No_Access
+                  | Read_Only
+               =>
+                  return Read_Only;
+
+               when Write_Perm =>
+                  return Read_Write;
+            end case;
+
+         when Write_Only =>
+            case P2 is
+               when No_Access
+                  | Write_Only
+               =>
+                  return Write_Only;
+
+               when Read_Perm =>
+                  return Read_Write;
+            end case;
+
+         when Read_Write =>
+            return Read_Write;
+      end case;
+   end Lub;
+
+   ----------------
+   -- Merge_Envs --
+   ----------------
+
+   procedure Merge_Envs
+     (Target : in out Perm_Env;
+      Source : in out Perm_Env)
+   is
+      procedure Merge_Trees
+        (Target : Perm_Tree_Access;
+         Source : Perm_Tree_Access);
+
+      procedure Merge_Trees
+        (Target : Perm_Tree_Access;
+         Source : Perm_Tree_Access)
+      is
+         procedure Apply_Glb_Tree
+           (A : Perm_Tree_Access;
+            P : Perm_Kind);
+
+         procedure Apply_Glb_Tree
+           (A : Perm_Tree_Access;
+            P : Perm_Kind)
+         is
+         begin
+            A.all.Tree.Permission := Glb (Permission (A), P);
+
+            case Kind (A) is
+               when Entire_Object =>
+                  A.all.Tree.Children_Permission :=
+                    Glb (Children_Permission (A), P);
+
+               when Reference =>
+                  Apply_Glb_Tree (Get_All (A), P);
+
+               when Array_Component =>
+                  Apply_Glb_Tree (Get_Elem (A), P);
+
+               when Record_Component =>
+                  declare
+                     Comp : Perm_Tree_Access;
+                  begin
+                     Comp := Perm_Tree_Maps.Get_First (Component (A));
+                     while Comp /= null loop
+                        Apply_Glb_Tree (Comp, P);
+                        Comp := Perm_Tree_Maps.Get_Next (Component (A));
+                     end loop;
+
+                     Apply_Glb_Tree (Other_Components (A), P);
+                  end;
+            end case;
+         end Apply_Glb_Tree;
+
+         Perm : constant Perm_Kind :=
+           Glb (Permission (Target), Permission (Source));
+
+      begin
+         pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
+         Target.all.Tree.Permission := Perm;
+
+         case Kind (Target) is
+            when Entire_Object =>
+               declare
+                  Child_Perm : constant Perm_Kind :=
+                    Children_Permission (Target);
+
+               begin
+                  case Kind (Source) is
+                  when Entire_Object =>
+                     Target.all.Tree.Children_Permission :=
+                       Glb (Child_Perm, Children_Permission (Source));
+
+                  when Reference =>
+                     Copy_Tree (Source, Target);
+                     Target.all.Tree.Permission := Perm;
+                     Apply_Glb_Tree (Get_All (Target), Child_Perm);
+
+                  when Array_Component =>
+                     Copy_Tree (Source, Target);
+                     Target.all.Tree.Permission := Perm;
+                     Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
+
+                  when Record_Component =>
+                     Copy_Tree (Source, Target);
+                     Target.all.Tree.Permission := Perm;
+                     declare
+                        Comp : Perm_Tree_Access;
+
+                     begin
+                        Comp :=
+                          Perm_Tree_Maps.Get_First (Component (Target));
+                        while Comp /= null loop
+                           --  Apply glb tree on every component subtree
+
+                           Apply_Glb_Tree (Comp, Child_Perm);
+                           Comp := Perm_Tree_Maps.Get_Next
+                             (Component (Target));
+                        end loop;
+                     end;
+                     Apply_Glb_Tree (Other_Components (Target), Child_Perm);
+
+                  end case;
+               end;
+            when Reference =>
+               case Kind (Source) is
+               when Entire_Object =>
+                  Apply_Glb_Tree (Get_All (Target),
+                                  Children_Permission (Source));
+
+               when Reference =>
+                  Merge_Trees (Get_All (Target), Get_All (Source));
+
+               when others =>
+                  raise Program_Error;
+
+               end case;
+
+            when Array_Component =>
+               case Kind (Source) is
+               when Entire_Object =>
+                  Apply_Glb_Tree (Get_Elem (Target),
+                                  Children_Permission (Source));
+
+               when Array_Component =>
+                  Merge_Trees (Get_Elem (Target), Get_Elem (Source));
+
+               when others =>
+                  raise Program_Error;
+
+               end case;
+
+            when Record_Component =>
+               case Kind (Source) is
+               when Entire_Object =>
+                  declare
+                     Child_Perm : constant Perm_Kind :=
+                       Children_Permission (Source);
+
+                     Comp : Perm_Tree_Access;
+
+                  begin
+                     Comp := Perm_Tree_Maps.Get_First
+                       (Component (Target));
+                     while Comp /= null loop
+                        --  Apply glb tree on every component subtree
+
+                        Apply_Glb_Tree (Comp, Child_Perm);
+                        Comp :=
+                          Perm_Tree_Maps.Get_Next (Component (Target));
+                     end loop;
+                     Apply_Glb_Tree (Other_Components (Target), Child_Perm);
+                  end;
+
+               when Record_Component =>
+                  declare
+                     Key_Source : Perm_Tree_Maps.Key_Option;
+                     CompTarget : Perm_Tree_Access;
+                     CompSource : Perm_Tree_Access;
+
+                  begin
+                     Key_Source := Perm_Tree_Maps.Get_First_Key
+                       (Component (Source));
+
+                     while Key_Source.Present loop
+                        CompSource := Perm_Tree_Maps.Get
+                          (Component (Source), Key_Source.K);
+                        CompTarget := Perm_Tree_Maps.Get
+                          (Component (Target), Key_Source.K);
+
+                        pragma Assert (CompSource /= null);
+                        Merge_Trees (CompTarget, CompSource);
+
+                        Key_Source := Perm_Tree_Maps.Get_Next_Key
+                          (Component (Source));
+                     end loop;
+
+                     Merge_Trees (Other_Components (Target),
+                                  Other_Components (Source));
+                  end;
+
+               when others =>
+                  raise Program_Error;
+
+               end case;
+         end case;
+      end Merge_Trees;
+
+      CompTarget : Perm_Tree_Access;
+      CompSource : Perm_Tree_Access;
+      KeyTarget : Perm_Tree_Maps.Key_Option;
+
+   begin
+      KeyTarget := Get_First_Key (Target);
+      --  Iterate over every tree of the environment in the target, and merge
+      --  it with the source if there is such a similar one that exists. If
+      --  there is none, then skip.
+      while KeyTarget.Present loop
+
+         CompSource := Get (Source, KeyTarget.K);
+         CompTarget := Get (Target, KeyTarget.K);
+
+         pragma Assert (CompTarget /= null);
+
+         if CompSource /= null then
+            Merge_Trees (CompTarget, CompSource);
+            Remove (Source, KeyTarget.K);
+         end if;
+
+         KeyTarget := Get_Next_Key (Target);
+      end loop;
+
+      --  Iterate over every tree of the environment of the source. And merge
+      --  again. If there is not any tree of the target then just copy the tree
+      --  from source to target.
+      declare
+         KeySource : Perm_Tree_Maps.Key_Option;
+      begin
+         KeySource := Get_First_Key (Source);
+         while KeySource.Present loop
+
+            CompSource := Get (Source, KeySource.K);
+            CompTarget := Get (Target, KeySource.K);
+
+            if CompTarget = null then
+               CompTarget := new Perm_Tree_Wrapper'(CompSource.all);
+               Copy_Tree (CompSource, CompTarget);
+               Set (Target, KeySource.K, CompTarget);
+            else
+               Merge_Trees (CompTarget, CompSource);
+            end if;
+
+            KeySource := Get_Next_Key (Source);
+         end loop;
+      end;
+
+      Free_Env (Source);
+   end Merge_Envs;
+
+   ----------------
+   -- Perm_Error --
+   ----------------
+
+   procedure Perm_Error
+     (N : Node_Id;
+      Perm : Perm_Kind;
+      Found_Perm : Perm_Kind)
+   is
+      procedure Set_Root_Object
+        (Path  : Node_Id;
+         Obj   : out Entity_Id;
+         Deref : out Boolean);
+      --  Set the root object Obj, and whether the path contains a dereference,
+      --  from a path Path.
+
+      ---------------------
+      -- Set_Root_Object --
+      ---------------------
+
+      procedure Set_Root_Object
+        (Path  : Node_Id;
+         Obj   : out Entity_Id;
+         Deref : out Boolean)
+      is
+      begin
+         case Nkind (Path) is
+            when N_Identifier
+               | N_Expanded_Name
+            =>
+               Obj := Entity (Path);
+               Deref := False;
+
+            when N_Type_Conversion
+               | N_Unchecked_Type_Conversion
+               | N_Qualified_Expression
+            =>
+               Set_Root_Object (Expression (Path), Obj, Deref);
+
+            when N_Indexed_Component
+               | N_Selected_Component
+               | N_Slice
+            =>
+               Set_Root_Object (Prefix (Path), Obj, Deref);
+
+            when N_Explicit_Dereference =>
+               Set_Root_Object (Prefix (Path), Obj, Deref);
+               Deref := True;
+
+            when others =>
+               raise Program_Error;
+         end case;
+      end Set_Root_Object;
+
+      --  Local variables
+
+      Root : Entity_Id;
+      Is_Deref : Boolean;
+
+   --  Start of processing for Perm_Error
+
+   begin
+      Set_Root_Object (N, Root, Is_Deref);
+
+      if Is_Deref then
+         Error_Msg_NE
+           ("insufficient permission on dereference from &", N, Root);
+      else
+         Error_Msg_NE ("insufficient permission for &", N, Root);
+      end if;
+
+      Perm_Mismatch (Perm, Found_Perm, N);
+   end Perm_Error;
+
+   -------------------------------
+   -- Perm_Error_Subprogram_End --
+   -------------------------------
+
+   procedure Perm_Error_Subprogram_End
+     (E          : Entity_Id;
+      Subp       : Entity_Id;
+      Perm       : Perm_Kind;
+      Found_Perm : Perm_Kind)
+   is
+   begin
+      Error_Msg_Node_2 := Subp;
+      Error_Msg_NE ("insufficient permission for & when returning from &",
+                    Subp, E);
+      Perm_Mismatch (Perm, Found_Perm, Subp);
+   end Perm_Error_Subprogram_End;
+
+   ------------------
+   -- Process_Path --
+   ------------------
+
+   procedure Process_Path (N : Node_Id) is
+      Root : constant Entity_Id := Get_Enclosing_Object (N);
+   begin
+      --  We ignore if yielding to synchronized
+
+      if Present (Root)
+        and then Is_Synchronized_Object (Root)
+      then
+         return;
+      end if;
+
+      --  We ignore shallow unaliased. They are checked in flow analysis,
+      --  allowing backward compatibility.
+
+      if not Has_Alias (N)
+        and then Is_Shallow (Etype (N))
+      then
+         return;
+      end if;
+
+      declare
+         Perm_N : constant Perm_Kind := Get_Perm (N);
+
+      begin
+
+         case Current_Checking_Mode is
+            --  Check permission R, do nothing
+
+            when Read =>
+               if Perm_N not in Read_Perm then
+                  Perm_Error (N, Read_Only, Perm_N);
+               end if;
+
+            --  If shallow type no need for RW, only R
+
+            when Move =>
+               if Is_Shallow (Etype (N)) then
+                  if Perm_N not in Read_Perm then
+                     Perm_Error (N, Read_Only, Perm_N);
+                  end if;
+               else
+                  --  Check permission RW if deep
+
+                  if Perm_N /= Read_Write then
+                     Perm_Error (N, Read_Write, Perm_N);
+                  end if;
+
+                  declare
+                     --  Set permission to W to the path and any of its prefix
+
+                     Tree : constant Perm_Tree_Access :=
+                       Set_Perm_Prefixes_Move (N, Move);
+
+                  begin
+                     if Tree = null then
+                        --  We went through a function call, no permission to
+                        --  modify.
+
+                        return;
+                     end if;
+
+                     --  Set permissions to
+                     --  No for any extension with more .all
+                     --  W for any deep extension with same number of .all
+                     --  RW for any shallow extension with same number of .all
+
+                     Set_Perm_Extensions_Move (Tree, Etype (N));
+                  end;
+               end if;
+
+            --  Check permission RW
+
+            when Super_Move =>
+               if Perm_N /= Read_Write then
+                  Perm_Error (N, Read_Write, Perm_N);
+               end if;
+
+               declare
+                  --  Set permission to No to the path and any of its prefix up
+                  --  to the first .all and then W.
+
+                  Tree : constant Perm_Tree_Access :=
+                    Set_Perm_Prefixes_Move (N, Super_Move);
+
+               begin
+                  if Tree = null then
+                     --  We went through a function call, no permission to
+                     --  modify.
+
+                     return;
+                  end if;
+
+                  --  Set permissions to No on any strict extension of the path
+
+                  Set_Perm_Extensions (Tree, No_Access);
+               end;
+
+            --  Check permission W
+
+            when Assign =>
+               if Perm_N not in Write_Perm then
+                  Perm_Error (N, Write_Only, Perm_N);
+               end if;
+
+               --  If the tree has an array component, then the permissions do
+               --  not get modified by the assignment.
+
+               if Has_Array_Component (N) then
+                  return;
+               end if;
+
+               --  Same if has function component
+
+               if Has_Function_Component (N) then
+                  return;
+               end if;
+
+               declare
+                  --  Get the permission tree for the path
+
+                  Tree : constant Perm_Tree_Access :=
+                    Get_Perm_Tree (N);
+
+                  Dummy : Perm_Tree_Access;
+
+               begin
+                  if Tree = null then
+                     --  We went through a function call, no permission to
+                     --  modify.
+
+                     return;
+                  end if;
+
+                  --  Set permission RW for it and all of its extensions
+
+                  Tree.all.Tree.Permission := Read_Write;
+
+                  Set_Perm_Extensions (Tree, Read_Write);
+
+                  --  Normalize the permission tree
+
+                  Dummy := Set_Perm_Prefixes_Assign (N);
+               end;
+
+            --  Check permission W
+
+            when Borrow_Out =>
+               if Perm_N not in Write_Perm then
+                  Perm_Error (N, Write_Only, Perm_N);
+               end if;
+
+               declare
+                  --  Set permission to No to the path and any of its prefixes
+
+                  Tree : constant Perm_Tree_Access :=
+                    Set_Perm_Prefixes_Borrow_Out (N);
+
+               begin
+                  if Tree = null then
+                     --  We went through a function call, no permission to
+                     --  modify.
+
+                     return;
+                  end if;
+
+                  --  Set permissions to No on any strict extension of the path
+
+                  Set_Perm_Extensions (Tree, No_Access);
+               end;
+
+            when Observe =>
+               if Perm_N not in Read_Perm then
+                  Perm_Error (N, Read_Only, Perm_N);
+               end if;
+
+               if Is_By_Copy_Type (Etype (N)) then
+                  return;
+               end if;
+
+               declare
+                  --  Set permission to No on the path and any of its prefixes
+
+                  Tree : constant Perm_Tree_Access :=
+                    Set_Perm_Prefixes_Observe (N);
+
+               begin
+                  if Tree = null then
+                     --  We went through a function call, no permission to
+                     --  modify.
+
+                     return;
+                  end if;
+
+                  --  Set permissions to No on any strict extension of the path
+
+                  Set_Perm_Extensions (Tree, Read_Only);
+               end;
+         end case;
+      end;
+   end Process_Path;
+
+   -------------------------
+   -- Return_Declarations --
+   -------------------------
+
+   procedure Return_Declarations (L : List_Id) is
+
+      procedure Return_Declaration (Decl : Node_Id);
+      --  Check correct permissions for every declared object
+
+      ------------------------
+      -- Return_Declaration --
+      ------------------------
+
+      procedure Return_Declaration (Decl : Node_Id) is
+      begin
+         if Nkind (Decl) = N_Object_Declaration then
+            --  Check RW for object declared, unless the object has never been
+            --  initialized.
+
+            if Get (Current_Initialization_Map,
+                    Unique_Entity (Defining_Identifier (Decl))) = False
+            then
+               return;
+            end if;
+
+            --  We ignore shallow unaliased. They are checked in flow analysis,
+            --  allowing backward compatibility.
+
+            if not Has_Alias (Defining_Identifier (Decl))
+              and then Is_Shallow (Etype (Defining_Identifier (Decl)))
+            then
+               return;
+            end if;
+
+            declare
+               Elem : constant Perm_Tree_Access :=
+                 Get (Current_Perm_Env,
+                      Unique_Entity (Defining_Identifier (Decl)));
+
+            begin
+               if Elem = null then
+                  --  Here we are on a declaration. Hence it should have been
+                  --  added in the environment when analyzing this node with
+                  --  mode Read. Hence it is not possible to find a null
+                  --  pointer here.
+
+                  --  Hash_Table_Error
+                  raise Program_Error;
+               end if;
+
+               if Permission (Elem) /= Read_Write then
+                  Perm_Error (Decl, Read_Write, Permission (Elem));
+               end if;
+            end;
+         end if;
+      end Return_Declaration;
+
+      --  Local Variables
+
+      N : Node_Id;
+
+   --  Start of processing for Return_Declarations
+
+   begin
+      N := First (L);
+      while Present (N) loop
+         Return_Declaration (N);
+         Next (N);
+      end loop;
+   end Return_Declarations;
+
+   --------------------
+   -- Return_Globals --
+   --------------------
+
+   procedure Return_Globals (Subp : Entity_Id) is
+
+      procedure Return_Globals_From_List
+        (First_Item : Node_Id;
+         Kind       : Formal_Kind);
+      --  Return global items from the list starting at Item
+
+      procedure Return_Globals_Of_Mode (Global_Mode : Name_Id);
+      --  Return global items for the mode Global_Mode
+
+      ------------------------------
+      -- Return_Globals_From_List --
+      ------------------------------
+
+      procedure Return_Globals_From_List
+        (First_Item : Node_Id;
+         Kind       : Formal_Kind)
+      is
+         Item : Node_Id := First_Item;
+         E    : Entity_Id;
+
+      begin
+         while Present (Item) loop
+            E := Entity (Item);
+
+            --  Ignore abstract states, which play no role in pointer aliasing
+
+            if Ekind (E) = E_Abstract_State then
+               null;
+            else
+               Return_Parameter_Or_Global (E, Kind, Subp);
+            end if;
+            Next_Global (Item);
+         end loop;
+      end Return_Globals_From_List;
+
+      ----------------------------
+      -- Return_Globals_Of_Mode --
+      ----------------------------
+
+      procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is
+         Kind : Formal_Kind;
+
+      begin
+         case Global_Mode is
+            when Name_Input | Name_Proof_In =>
+               Kind := E_In_Parameter;
+            when Name_Output =>
+               Kind := E_Out_Parameter;
+            when Name_In_Out =>
+               Kind := E_In_Out_Parameter;
+            when others =>
+               raise Program_Error;
+         end case;
+
+         --  Return both global items from Global and Refined_Global pragmas
+
+         Return_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
+         Return_Globals_From_List
+           (First_Global (Subp, Global_Mode, Refined => True), Kind);
+      end Return_Globals_Of_Mode;
+
+   --  Start of processing for Return_Globals
+
+   begin
+      Return_Globals_Of_Mode (Name_Proof_In);
+      Return_Globals_Of_Mode (Name_Input);
+      Return_Globals_Of_Mode (Name_Output);
+      Return_Globals_Of_Mode (Name_In_Out);
+   end Return_Globals;
+
+   --------------------------------
+   -- Return_Parameter_Or_Global --
+   --------------------------------
+
+   procedure Return_Parameter_Or_Global
+     (Id   : Entity_Id;
+      Mode : Formal_Kind;
+      Subp : Entity_Id)
+   is
+      Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
+      pragma Assert (Elem /= null);
+
+   begin
+      --  Shallow unaliased parameters and globals cannot introduce pointer
+      --  aliasing.
+
+      if not Has_Alias (Id) and then Is_Shallow (Etype (Id)) then
+         null;
+
+      --  Observed IN parameters and globals need not return a permission to
+      --  the caller.
+
+      elsif Mode = E_In_Parameter and then not Is_Borrowed_In (Id) then
+         null;
+
+      --  All other parameters and globals should return with mode RW to the
+      --  caller.
+
+      else
+         if Permission (Elem) /= Read_Write then
+            Perm_Error_Subprogram_End
+              (E          => Id,
+               Subp       => Subp,
+               Perm       => Read_Write,
+               Found_Perm => Permission (Elem));
+         end if;
+      end if;
+   end Return_Parameter_Or_Global;
+
+   -----------------------
+   -- Return_Parameters --
+   -----------------------
+
+   procedure Return_Parameters (Subp : Entity_Id) is
+      Formal : Entity_Id;
+
+   begin
+      Formal := First_Formal (Subp);
+      while Present (Formal) loop
+         Return_Parameter_Or_Global (Formal, Ekind (Formal), Subp);
+         Next_Formal (Formal);
+      end loop;
+   end Return_Parameters;
+
+   -------------------------
+   -- Set_Perm_Extensions --
+   -------------------------
+
+   procedure Set_Perm_Extensions
+     (T : Perm_Tree_Access;
+      P : Perm_Kind)
+   is
+      procedure Free_Perm_Tree_Children (T : Perm_Tree_Access);
+
+      procedure Free_Perm_Tree_Children (T : Perm_Tree_Access)
+      is
+      begin
+         case Kind (T) is
+            when Entire_Object =>
+               null;
+
+            when Reference =>
+               Free_Perm_Tree (T.all.Tree.Get_All);
+
+            when Array_Component =>
+               Free_Perm_Tree (T.all.Tree.Get_Elem);
+
+            --  Free every Component subtree
+
+            when Record_Component =>
+               declare
+                  Comp : Perm_Tree_Access;
+
+               begin
+                  Comp := Perm_Tree_Maps.Get_First (Component (T));
+                  while Comp /= null loop
+                     Free_Perm_Tree (Comp);
+                     Comp := Perm_Tree_Maps.Get_Next (Component (T));
+                  end loop;
+
+                  Free_Perm_Tree (T.all.Tree.Other_Components);
+               end;
+         end case;
+      end Free_Perm_Tree_Children;
+
+      Son : constant Perm_Tree :=
+        Perm_Tree'
+          (Kind                => Entire_Object,
+           Is_Node_Deep        => Is_Node_Deep (T),
+           Permission          => Permission (T),
+           Children_Permission => P);
+
+   begin
+      Free_Perm_Tree_Children (T);
+      T.all.Tree := Son;
+   end Set_Perm_Extensions;
+
+   ------------------------------
+   -- Set_Perm_Extensions_Move --
+   ------------------------------
+
+   procedure Set_Perm_Extensions_Move
+     (T : Perm_Tree_Access;
+      E : Entity_Id)
+   is
+   begin
+      if not Is_Node_Deep (T) then
+         --  We are a shallow extension with same number of .all
+
+         Set_Perm_Extensions (T, Read_Write);
+         return;
+      end if;
+
+      --  We are a deep extension here (or the moved deep path)
+
+      T.all.Tree.Permission := Write_Only;
+
+      case T.all.Tree.Kind is
+         --  Unroll the tree depending on the type
+
+         when Entire_Object =>
+            case Ekind (E) is
+               when Scalar_Kind
+                  | E_String_Literal_Subtype
+               =>
+                  Set_Perm_Extensions (T, No_Access);
+
+               --  No need to unroll here, directly put sons to No_Access
+
+               when Access_Kind =>
+                  if Ekind (E) in Access_Subprogram_Kind then
+                     null;
+                  else
+                     Set_Perm_Extensions (T, No_Access);
+                  end if;
+
+               --  No unrolling done, too complicated
+
+               when E_Class_Wide_Subtype
+                  | E_Class_Wide_Type
+                  | E_Incomplete_Type
+                  | E_Incomplete_Subtype
+                  | E_Exception_Type
+                  | E_Task_Type
+                  | E_Task_Subtype
+               =>
+                  Set_Perm_Extensions (T, No_Access);
+
+               --  Expand the tree. Replace the node with Array component.
+
+               when E_Array_Type
+                  | E_Array_Subtype =>
+                  declare
+                     Son : Perm_Tree_Access;
+
+                  begin
+                     Son := new Perm_Tree_Wrapper'
+                       (Tree =>
+                          (Kind                => Entire_Object,
+                           Is_Node_Deep        => Is_Node_Deep (T),
+                           Permission          => Read_Write,
+                           Children_Permission => Read_Write));
+
+                     Set_Perm_Extensions_Move (Son, Component_Type (E));
+
+                     --  We change the current node from Entire_Object to
+                     --  Reference with Write_Only and the previous son.
+
+                     pragma Assert (Is_Node_Deep (T));
+
+                     T.all.Tree := (Kind         => Array_Component,
+                                    Is_Node_Deep => Is_Node_Deep (T),
+                                    Permission   => Write_Only,
+                                    Get_Elem     => Son);
+                  end;
+
+               --  Unroll, and set permission extensions with component type
+
+               when E_Record_Type
+                  | E_Record_Subtype
+                  | E_Record_Type_With_Private
+                  | E_Record_Subtype_With_Private
+                  | E_Protected_Type
+                  | E_Protected_Subtype
+               =>
+                  declare
+                     --  Expand the tree. Replace the node with
+                     --  Record_Component.
+
+                     Elem : Node_Id;
+
+                     Son : Perm_Tree_Access;
+
+                  begin
+                     --  We change the current node from Entire_Object to
+                     --  Record_Component with same permission and an empty
+                     --  hash table as component list.
+
+                     pragma Assert (Is_Node_Deep (T));
+
+                     T.all.Tree :=
+                       (Kind             => Record_Component,
+                        Is_Node_Deep     => Is_Node_Deep (T),
+                        Permission       => Write_Only,
+                        Component        => Perm_Tree_Maps.Nil,
+                        Other_Components =>
+                           new Perm_Tree_Wrapper'
+                          (Tree =>
+                               (Kind                => Entire_Object,
+                                Is_Node_Deep        => True,
+                                Permission          => Read_Write,
+                                Children_Permission => Read_Write)
+                          )
+                       );
+
+                     --  We fill the hash table with all sons of the record,
+                     --  with basic Entire_Objects nodes.
+                     Elem := First_Component_Or_Discriminant (E);
+                     while Present (Elem) loop
+                        Son := new Perm_Tree_Wrapper'
+                          (Tree =>
+                             (Kind                => Entire_Object,
+                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
+                              Permission          => Read_Write,
+                              Children_Permission => Read_Write));
+
+                        Set_Perm_Extensions_Move (Son, Etype (Elem));
+
+                        Perm_Tree_Maps.Set
+                          (T.all.Tree.Component, Elem, Son);
+
+                        Next_Component_Or_Discriminant (Elem);
+                     end loop;
+                  end;
+
+               when E_Private_Type
+                  | E_Private_Subtype
+                  | E_Limited_Private_Type
+                  | E_Limited_Private_Subtype
+               =>
+                  Set_Perm_Extensions_Move (T, Underlying_Type (E));
+
+               when others =>
+                  raise Program_Error;
+            end case;
+
+         when Reference =>
+            --  Now the son does not have the same number of .all
+            Set_Perm_Extensions (T, No_Access);
+
+         when Array_Component =>
+            Set_Perm_Extensions_Move (Get_Elem (T), Component_Type (E));
+
+         when Record_Component =>
+            declare
+               Comp : Perm_Tree_Access;
+               It : Node_Id;
+
+            begin
+               It := First_Component_Or_Discriminant (E);
+               while It /= Empty loop
+                  Comp := Perm_Tree_Maps.Get (Component (T), It);
+                  pragma Assert (Comp /= null);
+                  Set_Perm_Extensions_Move (Comp, It);
+                  It := Next_Component_Or_Discriminant (E);
+               end loop;
+
+               Set_Perm_Extensions (Other_Components (T), No_Access);
+            end;
+      end case;
+   end Set_Perm_Extensions_Move;
+
+   ------------------------------
+   -- Set_Perm_Prefixes_Assign --
+   ------------------------------
+
+   function Set_Perm_Prefixes_Assign
+     (N : Node_Id)
+       return Perm_Tree_Access
+   is
+      C : constant Perm_Tree_Access := Get_Perm_Tree (N);
+
+   begin
+      pragma Assert (Current_Checking_Mode = Assign);
+
+      --  The function should not be called if has_function_component
+
+      pragma Assert (C /= null);
+
+      case Kind (C) is
+         when Entire_Object =>
+            pragma Assert (Children_Permission (C) = Read_Write);
+            C.all.Tree.Permission := Read_Write;
+
+         when Reference =>
+            pragma Assert (Get_All (C) /= null);
+
+            C.all.Tree.Permission :=
+              Lub (Permission (C), Permission (Get_All (C)));
+
+         when Array_Component =>
+            pragma Assert (C.all.Tree.Get_Elem /= null);
+
+            --  Given that it is not possible to know which element has been
+            --  assigned, then the permissions do not get changed in case of
+            --  Array_Component.
+
+            null;
+
+         when Record_Component =>
+            declare
+               Perm : Perm_Kind := Read_Write;
+
+               Comp : Perm_Tree_Access;
+
+            begin
+               --  We take the Glb of all the descendants, and then update the
+               --  permission of the node with it.
+               Comp := Perm_Tree_Maps.Get_First (Component (C));
+               while Comp /= null loop
+                  Perm := Glb (Perm, Permission (Comp));
+                  Comp := Perm_Tree_Maps.Get_Next (Component (C));
+               end loop;
+
+               Perm := Glb (Perm, Permission (Other_Components (C)));
+
+               C.all.Tree.Permission := Lub (Permission (C), Perm);
+            end;
+      end case;
+
+      case Nkind (N) is
+         --  Base identifier. End recursion here.
+
+         when N_Identifier
+            | N_Expanded_Name
+            | N_Defining_Identifier
+         =>
+            return null;
+
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+            | N_Qualified_Expression
+         =>
+            return Set_Perm_Prefixes_Assign (Expression (N));
+
+         when N_Parameter_Specification =>
+            raise Program_Error;
+
+         --  Continue recursion on prefix
+
+         when N_Selected_Component =>
+            return Set_Perm_Prefixes_Assign (Prefix (N));
+
+         --  Continue recursion on prefix
+
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            return Set_Perm_Prefixes_Assign (Prefix (N));
+
+         --  Continue recursion on prefix
+
+         when N_Explicit_Dereference =>
+            return Set_Perm_Prefixes_Assign (Prefix (N));
+
+         when N_Function_Call =>
+            raise Program_Error;
+
+         when others =>
+            raise Program_Error;
+
+      end case;
+   end Set_Perm_Prefixes_Assign;
+
+   ----------------------------------
+   -- Set_Perm_Prefixes_Borrow_Out --
+   ----------------------------------
+
+   function Set_Perm_Prefixes_Borrow_Out
+     (N : Node_Id)
+       return Perm_Tree_Access
+   is
+   begin
+      pragma Assert (Current_Checking_Mode = Borrow_Out);
+
+      case Nkind (N) is
+         --  Base identifier. Set permission to No.
+
+         when N_Identifier
+            | N_Expanded_Name
+         =>
+            declare
+               P : constant Node_Id := Entity (N);
+
+               C : constant Perm_Tree_Access :=
+                 Get (Current_Perm_Env, Unique_Entity (P));
+
+               pragma Assert (C /= null);
+
+            begin
+               --  Setting the initialization map to True, so that this
+               --  variable cannot be ignored anymore when looking at end
+               --  of elaboration of package.
+
+               Set (Current_Initialization_Map, Unique_Entity (P), True);
+
+               C.all.Tree.Permission := No_Access;
+               return C;
+            end;
+
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+            | N_Qualified_Expression
+         =>
+            return Set_Perm_Prefixes_Borrow_Out (Expression (N));
+
+         when N_Parameter_Specification
+            | N_Defining_Identifier
+         =>
+            raise Program_Error;
+
+            --  We set the permission tree of its prefix, and then we extract
+            --  our subtree from the returned pointer and assign an adequate
+            --  permission to it, if unfolded. If folded, we unroll the tree
+            --  in one step.
+
+         when N_Selected_Component =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Set_Perm_Prefixes_Borrow_Out (Prefix (N));
+
+            begin
+               if C = null then
+                  --  We went through a function call, do nothing
+
+                  return null;
+               end if;
+
+               --  The permission of the returned node should be No
+
+               pragma Assert (Permission (C) = No_Access);
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Record_Component);
+
+               if Kind (C) = Record_Component then
+                  --  The tree is unfolded. We just modify the permission and
+                  --  return the record subtree.
+
+                  declare
+                     Selected_Component : constant Entity_Id :=
+                       Entity (Selector_Name (N));
+
+                     Selected_C : Perm_Tree_Access :=
+                       Perm_Tree_Maps.Get
+                         (Component (C), Selected_Component);
+
+                  begin
+                     if Selected_C = null then
+                        Selected_C := Other_Components (C);
+                     end if;
+
+                     pragma Assert (Selected_C /= null);
+
+                     Selected_C.all.Tree.Permission := No_Access;
+
+                     return Selected_C;
+                  end;
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace the node with
+                     --  Record_Component.
+
+                     Elem : Node_Id;
+
+                     --  Create an empty hash table
+
+                     Hashtbl : Perm_Tree_Maps.Instance;
+
+                     --  We create the unrolled nodes, that will all have same
+                     --  permission than parent.
+
+                     Son : Perm_Tree_Access;
+
+                     ChildrenPerm : constant Perm_Kind :=
+                       Children_Permission (C);
+
+                  begin
+                     --  We change the current node from Entire_Object to
+                     --  Record_Component with same permission and an empty
+                     --  hash table as component list.
+
+                     C.all.Tree :=
+                       (Kind         => Record_Component,
+                        Is_Node_Deep => Is_Node_Deep (C),
+                        Permission   => Permission (C),
+                        Component    => Hashtbl,
+                        Other_Components =>
+                           new Perm_Tree_Wrapper'
+                          (Tree =>
+                               (Kind                => Entire_Object,
+                                Is_Node_Deep        => True,
+                                Permission          => ChildrenPerm,
+                                Children_Permission => ChildrenPerm)
+                          ));
+
+                     --  We fill the hash table with all sons of the record,
+                     --  with basic Entire_Objects nodes.
+                     Elem := First_Component_Or_Discriminant
+                       (Etype (Prefix (N)));
+
+                     while Present (Elem) loop
+                        Son := new Perm_Tree_Wrapper'
+                          (Tree =>
+                             (Kind                => Entire_Object,
+                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
+                              Permission          => ChildrenPerm,
+                              Children_Permission => ChildrenPerm));
+
+                        Perm_Tree_Maps.Set
+                          (C.all.Tree.Component, Elem, Son);
+
+                        Next_Component_Or_Discriminant (Elem);
+                     end loop;
+
+                     --  Now we set the right field to No_Access, and then we
+                     --  return the tree to the sons, so that the recursion can
+                     --  continue.
+
+                     declare
+                        Selected_Component : constant Entity_Id :=
+                          Entity (Selector_Name (N));
+
+                        Selected_C : Perm_Tree_Access :=
+                          Perm_Tree_Maps.Get
+                            (Component (C), Selected_Component);
+
+                     begin
+                        if Selected_C = null then
+                           Selected_C := Other_Components (C);
+                        end if;
+
+                        pragma Assert (Selected_C /= null);
+
+                        Selected_C.all.Tree.Permission := No_Access;
+
+                        return Selected_C;
+                     end;
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+            --  We set the permission tree of its prefix, and then we extract
+            --  from the returned pointer the subtree and assign an adequate
+            --  permission to it, if unfolded. If folded, we unroll the tree in
+            --  one step.
+
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Set_Perm_Prefixes_Borrow_Out (Prefix (N));
+
+            begin
+               if C = null then
+                  --  We went through a function call, do nothing
+
+                  return null;
+               end if;
+
+               --  The permission of the returned node should be either W
+               --  (because the recursive call sets <= Write_Only) or No
+               --  (if another path has been moved with 'Access).
+
+               pragma Assert (Permission (C) = No_Access);
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Array_Component);
+
+               if Kind (C) = Array_Component then
+                  --  The tree is unfolded. We just modify the permission and
+                  --  return the elem subtree.
+
+                  pragma Assert (Get_Elem (C) /= null);
+
+                  C.all.Tree.Get_Elem.all.Tree.Permission := No_Access;
+
+                  return Get_Elem (C);
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace node with Array_Component.
+
+                     Son : Perm_Tree_Access;
+
+                  begin
+                     Son := new Perm_Tree_Wrapper'
+                       (Tree =>
+                          (Kind                => Entire_Object,
+                           Is_Node_Deep        => Is_Node_Deep (C),
+                           Permission          => No_Access,
+                           Children_Permission => Children_Permission (C)));
+
+                     --  We change the current node from Entire_Object
+                     --  to Array_Component with same permission and the
+                     --  previously defined son.
+
+                     C.all.Tree := (Kind         => Array_Component,
+                                    Is_Node_Deep => Is_Node_Deep (C),
+                                    Permission   => No_Access,
+                                    Get_Elem     => Son);
+
+                     return Get_Elem (C);
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+            --  We set the permission tree of its prefix, and then we extract
+            --  from the returned pointer the subtree and assign an adequate
+            --  permission to it, if unfolded. If folded, we unroll the tree
+            --  at one step.
+
+         when N_Explicit_Dereference =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Set_Perm_Prefixes_Borrow_Out (Prefix (N));
+
+            begin
+               if C = null then
+                  --  We went through a function call. Do nothing.
+
+                  return null;
+               end if;
+
+               --  The permission of the returned node should be No
+
+               pragma Assert (Permission (C) = No_Access);
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Reference);
+
+               if Kind (C) = Reference then
+                  --  The tree is unfolded. We just modify the permission and
+                  --  return the elem subtree.
+
+                  pragma Assert (Get_All (C) /= null);
+
+                  C.all.Tree.Get_All.all.Tree.Permission := No_Access;
+
+                  return Get_All (C);
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace the node with Reference.
+
+                     Son : Perm_Tree_Access;
+
+                  begin
+                     Son := new Perm_Tree_Wrapper'
+                       (Tree =>
+                          (Kind                => Entire_Object,
+                           Is_Node_Deep        => Is_Deep (Etype (N)),
+                           Permission          => No_Access,
+                           Children_Permission => Children_Permission (C)));
+
+                     --  We change the current node from Entire_Object to
+                     --  Reference with No_Access and the previous son.
+
+                     pragma Assert (Is_Node_Deep (C));
+
+                     C.all.Tree := (Kind         => Reference,
+                                    Is_Node_Deep => Is_Node_Deep (C),
+                                    Permission   => No_Access,
+                                    Get_All      => Son);
+
+                     return Get_All (C);
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+         when N_Function_Call =>
+            return null;
+
+         when others =>
+            raise Program_Error;
+      end case;
+   end Set_Perm_Prefixes_Borrow_Out;
+
+   ----------------------------
+   -- Set_Perm_Prefixes_Move --
+   ----------------------------
+
+   function Set_Perm_Prefixes_Move
+     (N : Node_Id; Mode : Checking_Mode)
+       return Perm_Tree_Access
+   is
+   begin
+      case Nkind (N) is
+         --  Base identifier. Set permission to W or No depending on Mode.
+
+         when N_Identifier
+            | N_Expanded_Name
+         =>
+            declare
+               P : constant Node_Id := Entity (N);
+
+               C : constant Perm_Tree_Access :=
+                 Get (Current_Perm_Env, Unique_Entity (P));
+
+            begin
+               --  The base tree can be RW (first move from this base path) or
+               --  W (already some extensions values moved), or even No_Access
+               --  (extensions moved with 'Access). But it cannot be Read_Only
+               --  (we get an error).
+
+               if Permission (C) = Read_Only then
+                  raise Unrecoverable_Error;
+               end if;
+
+               --  Setting the initialization map to True, so that this
+               --  variable cannot be ignored anymore when looking at end
+               --  of elaboration of package.
+
+               Set (Current_Initialization_Map, Unique_Entity (P), True);
+
+               if C = null then
+                  --  No null possible here, there are no parents for the path.
+                  --  This means we are using a global variable without adding
+                  --  it in environment with a global aspect.
+
+                  Illegal_Global_Usage (N);
+               end if;
+
+               if Mode = Super_Move then
+                  C.all.Tree.Permission := No_Access;
+               else
+                  C.all.Tree.Permission := Glb (Write_Only, Permission (C));
+               end if;
+
+               return C;
+            end;
+
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+            | N_Qualified_Expression
+         =>
+            return Set_Perm_Prefixes_Move (Expression (N), Mode);
+
+         when N_Parameter_Specification
+            | N_Defining_Identifier
+         =>
+            raise Program_Error;
+
+            --  We set the permission tree of its prefix, and then we extract
+            --  from the returned pointer our subtree and assign an adequate
+            --  permission to it, if unfolded. If folded, we unroll the tree
+            --  at one step.
+
+         when N_Selected_Component =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Set_Perm_Prefixes_Move (Prefix (N), Mode);
+
+            begin
+               if C = null then
+                  --  We went through a function call, do nothing
+
+                  return null;
+               end if;
+
+               --  The permission of the returned node should be either W
+               --  (because the recursive call sets <= Write_Only) or No
+               --  (if another path has been moved with 'Access).
+
+               pragma Assert (Permission (C) = No_Access
+                              or else Permission (C) = Write_Only);
+
+               if Mode = Super_Move then
+                  --  The permission of the returned node should be No (thanks
+                  --  to the recursion).
+
+                  pragma Assert (Permission (C) = No_Access);
+                  null;
+               end if;
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Record_Component);
+
+               if Kind (C) = Record_Component then
+                  --  The tree is unfolded. We just modify the permission and
+                  --  return the record subtree.
+
+                  declare
+                     Selected_Component : constant Entity_Id :=
+                       Entity (Selector_Name (N));
+
+                     Selected_C : Perm_Tree_Access :=
+                       Perm_Tree_Maps.Get
+                         (Component (C), Selected_Component);
+
+                  begin
+                     if Selected_C = null then
+                        --  If the hash table returns no element, then we fall
+                        --  into the part of Other_Components.
+                        pragma Assert (Is_Tagged_Type (Etype (Prefix (N))));
+
+                        Selected_C := Other_Components (C);
+                     end if;
+
+                     pragma Assert (Selected_C /= null);
+
+                     --  The Selected_C can have permissions:
+                     --  RW : first move in this path
+                     --  W  : Already other moves in this path
+                     --  No : Already other moves with 'Access
+
+                     pragma Assert (Permission (Selected_C) /= Read_Only);
+                     if Mode = Super_Move then
+                        Selected_C.all.Tree.Permission := No_Access;
+                     else
+                        Selected_C.all.Tree.Permission :=
+                          Glb (Write_Only, Permission (Selected_C));
+
+                     end if;
+
+                     return Selected_C;
+                  end;
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace the node with
+                     --  Record_Component.
+
+                     Elem : Node_Id;
+
+                     --  Create an empty hash table
+
+                     Hashtbl : Perm_Tree_Maps.Instance;
+
+                     --  We are in Move or Super_Move mode, hence we can assume
+                     --  that the Children_permission is RW, given that there
+                     --  are no other paths that could have been moved.
+
+                     pragma Assert (Children_Permission (C) = Read_Write);
+
+                     --  We create the unrolled nodes, that will all have RW
+                     --  permission given that we are in move mode. We will
+                     --  then set the right node to W.
+
+                     Son : Perm_Tree_Access;
+
+                  begin
+                     --  We change the current node from Entire_Object to
+                     --  Record_Component with same permission and an empty
+                     --  hash table as component list.
+
+                     C.all.Tree :=
+                       (Kind             => Record_Component,
+                        Is_Node_Deep     => Is_Node_Deep (C),
+                        Permission       => Permission (C),
+                        Component        => Hashtbl,
+                        Other_Components =>
+                           new Perm_Tree_Wrapper'
+                          (Tree =>
+                               (Kind                => Entire_Object,
+                                Is_Node_Deep        => True,
+                                Permission          => Read_Write,
+                                Children_Permission => Read_Write)
+                          ));
+
+                     --  We fill the hash table with all sons of the record,
+                     --  with basic Entire_Objects nodes.
+                     Elem := First_Component_Or_Discriminant
+                       (Etype (Prefix (N)));
+
+                     while Present (Elem) loop
+                        Son := new Perm_Tree_Wrapper'
+                          (Tree =>
+                             (Kind                => Entire_Object,
+                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
+                              Permission          => Read_Write,
+                              Children_Permission => Read_Write));
+
+                        Perm_Tree_Maps.Set
+                          (C.all.Tree.Component, Elem, Son);
+
+                        Next_Component_Or_Discriminant (Elem);
+                     end loop;
+
+                     --  Now we set the right field to Write_Only or No_Access
+                     --  depending on mode, and then we return the tree to the
+                     --  sons, so that the recursion can continue.
+
+                     declare
+                        Selected_Component : constant Entity_Id :=
+                          Entity (Selector_Name (N));
+
+                        Selected_C : Perm_Tree_Access :=
+                          Perm_Tree_Maps.Get
+                            (Component (C), Selected_Component);
+
+                     begin
+                        if Selected_C = null then
+                           Selected_C := Other_Components (C);
+                        end if;
+
+                        pragma Assert (Selected_C /= null);
+
+                        --  Given that this is a newly created Select_C, we can
+                        --  safely assume that its permission is Read_Write.
+
+                        pragma Assert (Permission (Selected_C) =
+                                         Read_Write);
+
+                        if Mode = Super_Move then
+                           Selected_C.all.Tree.Permission := No_Access;
+                        else
+                           Selected_C.all.Tree.Permission := Write_Only;
+                        end if;
+
+                        return Selected_C;
+                     end;
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+            --  We set the permission tree of its prefix, and then we extract
+            --  from the returned pointer the subtree and assign an adequate
+            --  permission to it, if unfolded. If folded, we unroll the tree
+            --  at one step.
+
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Set_Perm_Prefixes_Move (Prefix (N), Mode);
+
+            begin
+               if C = null then
+                  --  We went through a function call, do nothing
+
+                  return null;
+               end if;
+
+               --  The permission of the returned node should be either
+               --  W (because the recursive call sets <= Write_Only)
+               --  or No (if another path has been moved with 'Access)
+
+               if Mode = Super_Move then
+                  pragma Assert (Permission (C) = No_Access);
+                  null;
+               else
+                  pragma Assert (Permission (C) = Write_Only
+                                 or else Permission (C) = No_Access);
+                  null;
+               end if;
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Array_Component);
+
+               if Kind (C) = Array_Component then
+                  --  The tree is unfolded. We just modify the permission and
+                  --  return the elem subtree.
+
+                  if Get_Elem (C) = null then
+                     --  Hash_Table_Error
+                     raise Program_Error;
+                  end if;
+
+                  --  The Get_Elem can have permissions :
+                  --  RW : first move in this path
+                  --  W  : Already other moves in this path
+                  --  No : Already other moves with 'Access
+
+                  pragma Assert (Permission (Get_Elem (C)) /= Read_Only);
+
+                  if Mode = Super_Move then
+                     C.all.Tree.Get_Elem.all.Tree.Permission := No_Access;
+                  else
+                     C.all.Tree.Get_Elem.all.Tree.Permission :=
+                       Glb (Write_Only, Permission (Get_Elem (C)));
+                  end if;
+
+                  return Get_Elem (C);
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace node with Array_Component.
+
+                     --  We are in move mode, hence we can assume that the
+                     --  Children_permission is RW.
+
+                     pragma Assert (Children_Permission (C) = Read_Write);
+
+                     Son : Perm_Tree_Access;
+
+                  begin
+                     Son := new Perm_Tree_Wrapper'
+                       (Tree =>
+                          (Kind                => Entire_Object,
+                           Is_Node_Deep        => Is_Node_Deep (C),
+                           Permission          => Read_Write,
+                           Children_Permission => Read_Write));
+
+                     if Mode = Super_Move then
+                        Son.all.Tree.Permission := No_Access;
+                     else
+                        Son.all.Tree.Permission := Write_Only;
+                     end if;
+
+                     --  We change the current node from Entire_Object
+                     --  to Array_Component with same permission and the
+                     --  previously defined son.
+
+                     C.all.Tree := (Kind         => Array_Component,
+                                    Is_Node_Deep => Is_Node_Deep (C),
+                                    Permission   => Permission (C),
+                                    Get_Elem     => Son);
+
+                     return Get_Elem (C);
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+            --  We set the permission tree of its prefix, and then we extract
+            --  from the returned pointer the subtree and assign an adequate
+            --  permission to it, if unfolded. If folded, we unroll the tree
+            --  at one step.
+
+         when N_Explicit_Dereference =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Set_Perm_Prefixes_Move (Prefix (N), Move);
+
+            begin
+               if C = null then
+                  --  We went through a function call: do nothing
+
+                  return null;
+               end if;
+
+               --  The permission of the returned node should be only
+               --  W (because the recursive call sets <= Write_Only)
+               --  No is NOT POSSIBLE here
+
+               pragma Assert (Permission (C) = Write_Only);
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Reference);
+
+               if Kind (C) = Reference then
+                  --  The tree is unfolded. We just modify the permission and
+                  --  return the elem subtree.
+
+                  if Get_All (C) = null then
+                     --  Hash_Table_Error
+                     raise Program_Error;
+                  end if;
+
+                  --  The Get_All can have permissions :
+                  --  RW : first move in this path
+                  --  W  : Already other moves in this path
+                  --  No : Already other moves with 'Access
+
+                  pragma Assert (Permission (Get_All (C)) /= Read_Only);
+
+                  if Mode = Super_Move then
+                     C.all.Tree.Get_All.all.Tree.Permission := No_Access;
+                  else
+                     Get_All (C).all.Tree.Permission :=
+                       Glb (Write_Only, Permission (Get_All (C)));
+                  end if;
+                  return Get_All (C);
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace the node with Reference.
+
+                     --  We are in Move or Super_Move mode, hence we can assume
+                     --  that the Children_permission is RW.
+
+                     pragma Assert (Children_Permission (C) = Read_Write);
+
+                     Son : Perm_Tree_Access;
+
+                  begin
+                     Son := new Perm_Tree_Wrapper'
+                       (Tree =>
+                          (Kind                => Entire_Object,
+                           Is_Node_Deep        => Is_Deep (Etype (N)),
+                           Permission          => Read_Write,
+                           Children_Permission => Read_Write));
+
+                     if Mode = Super_Move then
+                        Son.all.Tree.Permission := No_Access;
+                     else
+                        Son.all.Tree.Permission := Write_Only;
+                     end if;
+
+                     --  We change the current node from Entire_Object to
+                     --  Reference with Write_Only and the previous son.
+
+                     pragma Assert (Is_Node_Deep (C));
+
+                     C.all.Tree := (Kind         => Reference,
+                                    Is_Node_Deep => Is_Node_Deep (C),
+                                    Permission   => Write_Only,
+                                    --  Write_only is equal to C.Permission
+                                    Get_All      => Son);
+
+                     return Get_All (C);
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+         when N_Function_Call =>
+            return null;
+
+         when others =>
+            raise Program_Error;
+      end case;
+
+   end Set_Perm_Prefixes_Move;
+
+   -------------------------------
+   -- Set_Perm_Prefixes_Observe --
+   -------------------------------
+
+   function Set_Perm_Prefixes_Observe
+     (N : Node_Id)
+      return Perm_Tree_Access
+   is
+   begin
+      pragma Assert (Current_Checking_Mode = Observe);
+
+      case Nkind (N) is
+         --  Base identifier. Set permission to R.
+
+         when N_Identifier
+            | N_Expanded_Name
+            | N_Defining_Identifier
+         =>
+            declare
+               P : Node_Id;
+               C : Perm_Tree_Access;
+
+            begin
+               if Nkind (N) = N_Defining_Identifier then
+                  P := N;
+               else
+                  P := Entity (N);
+               end if;
+
+               C := Get (Current_Perm_Env, Unique_Entity (P));
+               --  Setting the initialization map to True, so that this
+               --  variable cannot be ignored anymore when looking at end
+               --  of elaboration of package.
+
+               Set (Current_Initialization_Map, Unique_Entity (P), True);
+
+               if C = null then
+                  --  No null possible here, there are no parents for the path.
+                  --  This means we are using a global variable without adding
+                  --  it in environment with a global aspect.
+
+                  Illegal_Global_Usage (N);
+               end if;
+
+               C.all.Tree.Permission := Glb (Read_Only, Permission (C));
+
+               return C;
+            end;
+
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+            | N_Qualified_Expression
+         =>
+            return Set_Perm_Prefixes_Observe (Expression (N));
+
+         when N_Parameter_Specification =>
+            raise Program_Error;
+
+            --  We set the permission tree of its prefix, and then we extract
+            --  from the returned pointer our subtree and assign an adequate
+            --  permission to it, if unfolded. If folded, we unroll the tree
+            --  at one step.
+
+         when N_Selected_Component =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Set_Perm_Prefixes_Observe (Prefix (N));
+
+            begin
+               if C = null then
+                  --  We went through a function call, do nothing
+
+                  return null;
+               end if;
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Record_Component);
+
+               if Kind (C) = Record_Component then
+                  --  The tree is unfolded. We just modify the permission and
+                  --  return the record subtree. We put the permission to the
+                  --  glb of read_only and its current permission, to consider
+                  --  the case of observing x.y while x.z has been moved. Then
+                  --  x should be No_Access.
+
+                  declare
+                     Selected_Component : constant Entity_Id :=
+                       Entity (Selector_Name (N));
+
+                     Selected_C : Perm_Tree_Access :=
+                       Perm_Tree_Maps.Get
+                         (Component (C), Selected_Component);
+
+                  begin
+                     if Selected_C = null then
+                        Selected_C := Other_Components (C);
+                     end if;
+
+                     pragma Assert (Selected_C /= null);
+
+                     Selected_C.all.Tree.Permission :=
+                       Glb (Read_Only, Permission (Selected_C));
+
+                     return Selected_C;
+                  end;
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace the node with
+                     --  Record_Component.
+
+                     Elem : Node_Id;
+
+                     --  Create an empty hash table
+
+                     Hashtbl : Perm_Tree_Maps.Instance;
+
+                     --  We create the unrolled nodes, that will all have RW
+                     --  permission given that we are in move mode. We will
+                     --  then set the right node to W.
+
+                     Son : Perm_Tree_Access;
+
+                     Child_Perm : constant Perm_Kind :=
+                       Children_Permission (C);
+
+                  begin
+                     --  We change the current node from Entire_Object to
+                     --  Record_Component with same permission and an empty
+                     --  hash table as component list.
+
+                     C.all.Tree :=
+                       (Kind             => Record_Component,
+                        Is_Node_Deep     => Is_Node_Deep (C),
+                        Permission       => Permission (C),
+                        Component        => Hashtbl,
+                        Other_Components =>
+                           new Perm_Tree_Wrapper'
+                          (Tree =>
+                               (Kind                => Entire_Object,
+                                Is_Node_Deep        => True,
+                                Permission          => Child_Perm,
+                                Children_Permission => Child_Perm)
+                          ));
+
+                     --  We fill the hash table with all sons of the record,
+                     --  with basic Entire_Objects nodes.
+                     Elem := First_Component_Or_Discriminant
+                       (Etype (Prefix (N)));
+
+                     while Present (Elem) loop
+                        Son := new Perm_Tree_Wrapper'
+                          (Tree =>
+                             (Kind                => Entire_Object,
+                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
+                              Permission          => Child_Perm,
+                              Children_Permission => Child_Perm));
+
+                        Perm_Tree_Maps.Set
+                          (C.all.Tree.Component, Elem, Son);
+
+                        Next_Component_Or_Discriminant (Elem);
+                     end loop;
+
+                     --  Now we set the right field to Read_Only. and then we
+                     --  return the tree to the sons, so that the recursion can
+                     --  continue.
+
+                     declare
+                        Selected_Component : constant Entity_Id :=
+                          Entity (Selector_Name (N));
+
+                        Selected_C : Perm_Tree_Access :=
+                          Perm_Tree_Maps.Get
+                            (Component (C), Selected_Component);
+
+                     begin
+                        if Selected_C = null then
+                           Selected_C := Other_Components (C);
+                        end if;
+
+                        pragma Assert (Selected_C /= null);
+
+                        Selected_C.all.Tree.Permission :=
+                          Glb (Read_Only, Child_Perm);
+
+                        return Selected_C;
+                     end;
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+         --  We set the permission tree of its prefix, and then we extract from
+         --  the returned pointer the subtree and assign an adequate permission
+         --  to it, if unfolded. If folded, we unroll the tree at one step.
+
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Set_Perm_Prefixes_Observe (Prefix (N));
+
+            begin
+               if C = null then
+                  --  We went through a function call, do nothing
+
+                  return null;
+               end if;
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Array_Component);
+
+               if Kind (C) = Array_Component then
+                  --  The tree is unfolded. We just modify the permission and
+                  --  return the elem subtree.
+
+                  pragma Assert (Get_Elem (C) /= null);
+
+                  C.all.Tree.Get_Elem.all.Tree.Permission :=
+                    Glb (Read_Only, Permission (Get_Elem (C)));
+
+                  return Get_Elem (C);
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace node with Array_Component.
+
+                     Son : Perm_Tree_Access;
+
+                     Child_Perm : constant Perm_Kind :=
+                       Glb (Read_Only, Children_Permission (C));
+
+                  begin
+                     Son := new Perm_Tree_Wrapper'
+                       (Tree =>
+                          (Kind                => Entire_Object,
+                           Is_Node_Deep        => Is_Node_Deep (C),
+                           Permission          => Child_Perm,
+                           Children_Permission => Child_Perm));
+
+                     --  We change the current node from Entire_Object
+                     --  to Array_Component with same permission and the
+                     --  previously defined son.
+
+                     C.all.Tree := (Kind         => Array_Component,
+                                    Is_Node_Deep => Is_Node_Deep (C),
+                                    Permission   => Child_Perm,
+                                    Get_Elem     => Son);
+
+                     return Get_Elem (C);
+                  end;
+
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+         --  We set the permission tree of its prefix, and then we extract from
+         --  the returned pointer the subtree and assign an adequate permission
+         --  to it, if unfolded. If folded, we unroll the tree at one step.
+
+         when N_Explicit_Dereference =>
+            declare
+               C : constant Perm_Tree_Access :=
+                 Set_Perm_Prefixes_Observe (Prefix (N));
+
+            begin
+               if C = null then
+                  --  We went through a function call, do nothing
+
+                  return null;
+               end if;
+
+               pragma Assert (Kind (C) = Entire_Object
+                              or else Kind (C) = Reference);
+
+               if Kind (C) = Reference then
+                  --  The tree is unfolded. We just modify the permission and
+                  --  return the elem subtree.
+
+                  pragma Assert (Get_All (C) /= null);
+
+                  C.all.Tree.Get_All.all.Tree.Permission :=
+                    Glb (Read_Only, Permission (Get_All (C)));
+
+                  return Get_All (C);
+               elsif Kind (C) = Entire_Object then
+                  declare
+                     --  Expand the tree. Replace the node with Reference.
+
+                     Son : Perm_Tree_Access;
+
+                     Child_Perm : constant Perm_Kind :=
+                       Glb (Read_Only, Children_Permission (C));
+
+                  begin
+                     Son := new Perm_Tree_Wrapper'
+                       (Tree =>
+                          (Kind                => Entire_Object,
+                           Is_Node_Deep        => Is_Deep (Etype (N)),
+                           Permission          => Child_Perm,
+                           Children_Permission => Child_Perm));
+
+                     --  We change the current node from Entire_Object to
+                     --  Reference with Write_Only and the previous son.
+
+                     pragma Assert (Is_Node_Deep (C));
+
+                     C.all.Tree := (Kind         => Reference,
+                                    Is_Node_Deep => Is_Node_Deep (C),
+                                    Permission   => Child_Perm,
+                                    Get_All      => Son);
+
+                     return Get_All (C);
+                  end;
+               else
+                  raise Program_Error;
+               end if;
+            end;
+
+         when N_Function_Call =>
+            return null;
+
+         when others =>
+            raise Program_Error;
+
+      end case;
+   end Set_Perm_Prefixes_Observe;
+
+   -------------------
+   -- Setup_Globals --
+   -------------------
+
+   procedure Setup_Globals (Subp : Entity_Id) is
+
+      procedure Setup_Globals_From_List
+        (First_Item : Node_Id;
+         Kind       : Formal_Kind);
+      --  Set up global items from the list starting at Item
+
+      procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
+      --  Set up global items for the mode Global_Mode
+
+      -----------------------------
+      -- Setup_Globals_From_List --
+      -----------------------------
+
+      procedure Setup_Globals_From_List
+        (First_Item : Node_Id;
+         Kind       : Formal_Kind)
+      is
+         Item : Node_Id := First_Item;
+         E    : Entity_Id;
+
+      begin
+         while Present (Item) loop
+            E := Entity (Item);
+
+            --  Ignore abstract states, which play no role in pointer aliasing
+
+            if Ekind (E) = E_Abstract_State then
+               null;
+            else
+               Setup_Parameter_Or_Global (E, Kind);
+            end if;
+            Next_Global (Item);
+         end loop;
+      end Setup_Globals_From_List;
+
+      ---------------------------
+      -- Setup_Globals_Of_Mode --
+      ---------------------------
+
+      procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
+         Kind : Formal_Kind;
+
+      begin
+         case Global_Mode is
+            when Name_Input | Name_Proof_In =>
+               Kind := E_In_Parameter;
+            when Name_Output =>
+               Kind := E_Out_Parameter;
+            when Name_In_Out =>
+               Kind := E_In_Out_Parameter;
+            when others =>
+               raise Program_Error;
+         end case;
+
+         --  Set up both global items from Global and Refined_Global pragmas
+
+         Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
+         Setup_Globals_From_List
+           (First_Global (Subp, Global_Mode, Refined => True), Kind);
+      end Setup_Globals_Of_Mode;
+
+   --  Start of processing for Setup_Globals
+
+   begin
+      Setup_Globals_Of_Mode (Name_Proof_In);
+      Setup_Globals_Of_Mode (Name_Input);
+      Setup_Globals_Of_Mode (Name_Output);
+      Setup_Globals_Of_Mode (Name_In_Out);
+   end Setup_Globals;
+
+   -------------------------------
+   -- Setup_Parameter_Or_Global --
+   -------------------------------
+
+   procedure Setup_Parameter_Or_Global
+     (Id   : Entity_Id;
+      Mode : Formal_Kind)
+   is
+      Elem : Perm_Tree_Access;
+
+   begin
+      Elem := new Perm_Tree_Wrapper'
+        (Tree =>
+           (Kind                => Entire_Object,
+            Is_Node_Deep        => Is_Deep (Etype (Id)),
+            Permission          => Read_Write,
+            Children_Permission => Read_Write));
+
+      case Mode is
+         when E_In_Parameter =>
+
+            --  Borrowed IN: RW for everybody
+
+            if Is_Borrowed_In (Id) then
+               Elem.all.Tree.Permission := Read_Write;
+               Elem.all.Tree.Children_Permission := Read_Write;
+
+            --  Observed IN: R for everybody
+
+            else
+               Elem.all.Tree.Permission := Read_Only;
+               Elem.all.Tree.Children_Permission := Read_Only;
+            end if;
+
+         --  OUT: borrow, but callee has W only
+
+         when E_Out_Parameter =>
+            Elem.all.Tree.Permission := Write_Only;
+            Elem.all.Tree.Children_Permission := Write_Only;
+
+         --  IN OUT: borrow and callee has RW
+
+         when E_In_Out_Parameter =>
+            Elem.all.Tree.Permission := Read_Write;
+            Elem.all.Tree.Children_Permission := Read_Write;
+      end case;
+
+      Set (Current_Perm_Env, Id, Elem);
+   end Setup_Parameter_Or_Global;
+
+   ----------------------
+   -- Setup_Parameters --
+   ----------------------
+
+   procedure Setup_Parameters (Subp : Entity_Id) is
+      Formal : Entity_Id;
+
+   begin
+      Formal := First_Formal (Subp);
+      while Present (Formal) loop
+         Setup_Parameter_Or_Global (Formal, Ekind (Formal));
+         Next_Formal (Formal);
+      end loop;
+   end Setup_Parameters;
+
+end Sem_SPARK;
Index: sem_spark.ads
===================================================================
--- sem_spark.ads	(revision 0)
+++ sem_spark.ads	(revision 0)
@@ -0,0 +1,143 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                            S E M _ S P A R K                             --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--              Copyright (C) 2017, Free Software Foundation, Inc.          --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT 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 GNAT; see file COPYING3.  If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license.          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package implements an anti-aliasing analysis for access types. The
+--  rules that are enforced are defined in the anti-aliasing section of the
+--  SPARK RM 6.4.2
+--
+--  Analyze_SPARK is called by Gnat1drv, when GNATprove mode is activated. It
+--  does an analysis of the source code, looking for code that is considered
+--  as SPARK and launches another function called Analyze_Node that will do
+--  the whole analysis.
+--
+--  A path is an abstraction of a name, of which all indices, slices (for
+--  indexed components) and function calls have been abstracted and all
+--  dereferences are made explicit. A path is the atomic element viewed by the
+--  analysis, with the notion of prefixes and extensions of different paths.
+--
+--  The analysis explores the AST, and looks for different constructs
+--  that may involve aliasing. These main constructs are assignments
+--  (N_Assignment_Statement, N_Object_Declaration, ...), or calls
+--  (N_Procedure_Call_Statement, N_Entry_Call_Statement, N_Function_Call).
+--  The analysis checks the permissions of each construct and updates them
+--  according to the SPARK RM. This can follow three main different types
+--  of operations: move, borrow, and observe.
+
+----------------------------
+-- Deep and shallow types --
+----------------------------
+
+--  The analysis focuses on objects that can cause problems in terms of pointer
+--  aliasing. These objects have types that are called deep. Deep types are
+--  defined as being either types with an access part or class-wide types
+--  (which may have an access part in a derived type). Non-deep types are
+--  called shallow. Some objects of shallow type may cause pointer aliasing
+--  problems when they are explicitely marked as aliased (and then the aliasing
+--  occurs when we take the Access to this object and store it in a pointer).
+
+----------
+-- Move --
+----------
+
+--  Moves can happen at several points in the program: during assignment (and
+--  any similar statement such as object declaration with initial value), or
+--  during return statements.
+--
+--  The underlying concept consists of transferring the ownership of any path
+--  on the right-hand side to the left-hand side. There are some details that
+--  should be taken into account so as not to transfer paths that appear only
+--  as intermediate results of a more complex expression.
+
+--  More specifically, the SPARK RM defines moved expressions, and any moved
+--  expression that points directly to a path is then checked and sees its
+--  permissions updated accordingly.
+
+------------
+-- Borrow --
+------------
+
+--  Borrows can happen in subprogram calls. They consist of a temporary
+--  transfer of ownership from a caller to a callee. Expressions that can be
+--  borrowed can be found in either procedure or entry actual parameters, and
+--  consist of parameters of mode either "out" or "in out", or parameters of
+--  mode "in" that are of type nonconstant access-to-variable. We consider
+--  global variables as implicit parameters to subprograms, with their mode
+--  given by the Global contract associated to the subprogram. Note that the
+--  analysis looks for such a Global contract mentioning any global variable
+--  of deep type accessed directly in the subprogram, and it raises an error if
+--  there is no Global contract, or if the Global contract does not mention the
+--  variable.
+--
+--  A borrow of a parameter X is equivalent in terms of aliasing to moving
+--  X'Access to the callee, and then assigning back X at the end of the call.
+--
+--  Borrowed parameters should have read-write permission (or write-only for
+--  "out" parameters), and should all have read-write permission at the end
+--  of the call (this guarantee is ensured by the callee).
+
+-------------
+-- Observe --
+-------------
+
+--  Observed parameters are all the other parameters that are not borrowed and
+--  that may cause problems with aliasing. They are considered as being sent to
+--  the callee with Read-Only permission, so that they can be aliased safely.
+--  This is the only construct that allows aliasing that does not prevent
+--  accessing the old path that is being aliased. However, this comes with
+--  the restriction that those aliased path cannot be written in the callee.
+
+--------------------
+-- Implementation --
+--------------------
+
+--  The implementation is based on trees that represent the possible paths
+--  in the source code. Those trees can be unbounded in depth, hence they are
+--  represented using lazy data structures, whose laziness is handled manually.
+--  Each time an identifier is declared, its path is added to the permission
+--  environment as a tree with only one node, the declared identifier. Each
+--  time a path is checked or updated, we look in the tree at the adequate
+--  node, unfolding the tree whenever needed.
+
+--  For this, each node has several variables that indicate whether it is
+--  deep (Is_Node_Deep), what permission it has (Permission), and what is
+--  the lowest permission of all its descendants (Children_Permission). After
+--  unfolding the tree, we update the permissions of each node, deleting the
+--  Children_Permission, and specifying new ones for the leaves of the unfolded
+--  tree.
+
+--  After assigning a path, the descendants of the assigned path are dumped
+--  (and hence the tree is folded back), given that all descendants directly
+--  get read-write permission, which can be specified using the node's
+--  Children_Permission field.
+
+with Types; use Types;
+
+package Sem_SPARK is
+
+   procedure Check_Safe_Pointers (N : Node_Id);
+   --  The entry point of this package. It analyzes a node and reports errors
+   --  when there are violations of aliasing rules.
+
+end Sem_SPARK;
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 251999)
+++ sem_util.adb	(working copy)
@@ -8093,6 +8093,124 @@
       end if;
    end First_Actual;
 
+   ------------------
+   -- First_Global --
+   ------------------
+
+   function First_Global
+     (Subp        : Entity_Id;
+      Global_Mode : Name_Id;
+      Refined     : Boolean := False) return Node_Id
+   is
+      function First_From_Global_List
+        (List        : Node_Id;
+         Global_Mode : Name_Id := Name_Input) return Entity_Id;
+      --  Get the first item with suitable mode from List
+
+      ----------------------------
+      -- First_From_Global_List --
+      ----------------------------
+
+      function First_From_Global_List
+        (List        : Node_Id;
+         Global_Mode : Name_Id := Name_Input) return Entity_Id
+      is
+         Assoc : Node_Id;
+
+      begin
+         --  Empty list (no global items)
+
+         if Nkind (List) = N_Null then
+            return Empty;
+
+         --  Single global item declaration (only input items)
+
+         elsif Nkind_In (List, N_Expanded_Name,
+                               N_Identifier,
+                               N_Selected_Component)
+         then
+            if Global_Mode = Name_Input then
+               return List;
+            else
+               return Empty;
+            end if;
+
+         --  Simple global list (only input items) or moded global list
+         --  declaration.
+
+         elsif Nkind (List) = N_Aggregate then
+            if Present (Expressions (List)) then
+               if Global_Mode = Name_Input then
+                  return First (Expressions (List));
+               else
+                  return Empty;
+               end if;
+
+            else
+               Assoc := First (Component_Associations (List));
+               while Present (Assoc) loop
+
+                  --  When we find the desired mode in an association, call
+                  --  recursively First_From_Global_List as if the mode was
+                  --  Name_Input, in order to reuse the existing machinery
+                  --  for the other cases.
+
+                  if Chars (First (Choices (Assoc))) = Global_Mode then
+                     return First_From_Global_List (Expression (Assoc));
+                  end if;
+
+                  Next (Assoc);
+               end loop;
+
+               return Empty;
+            end if;
+
+            --  To accommodate partial decoration of disabled SPARK features,
+            --  this routine may be called with illegal input. If this is the
+            --  case, do not raise Program_Error.
+
+         else
+            return Empty;
+         end if;
+      end First_From_Global_List;
+
+      --  Local variables
+
+      Global  : Node_Id := Empty;
+      Body_Id : Entity_Id;
+
+   begin
+      pragma Assert (Global_Mode = Name_Input
+                      or else Global_Mode = Name_Output
+                      or else Global_Mode = Name_In_Out
+                      or else Global_Mode = Name_Proof_In);
+
+      --  Retrieve the suitable pragma Global or Refined_Global. In the second
+      --  case, it can only be located on the body entity.
+
+      if Refined then
+         Body_Id := Subprogram_Body_Entity (Subp);
+         if Present (Body_Id) then
+            Global := Get_Pragma (Body_Id, Pragma_Refined_Global);
+         end if;
+      else
+         Global := Get_Pragma (Subp, Pragma_Global);
+      end if;
+
+      --  No corresponding global if pragma is not present
+
+      if No (Global) then
+         return Empty;
+
+      --  Otherwise retrieve the corresponding list of items depending on the
+      --  Global_Mode.
+
+      else
+         return First_From_Global_List
+           (Expression (Get_Argument (Global, Subp)), Global_Mode);
+      end if;
+   end First_Global;
+
    -------------
    -- Fix_Msg --
    -------------
@@ -18980,6 +19098,27 @@
       Actual_Id := Next_Actual (Actual_Id);
    end Next_Actual;
 
+   -----------------
+   -- Next_Global --
+   -----------------
+
+   function Next_Global (Node : Node_Id) return Node_Id is
+   begin
+      --  The global item may either be in a list, or by itself, in which case
+      --  there is no next global item with the same mode.
+
+      if Is_List_Member (Node) then
+         return Next (Node);
+      else
+         return Empty;
+      end if;
+   end Next_Global;
+
+   procedure Next_Global (Node : in out Node_Id) is
+   begin
+      Node := Next_Global (Node);
+   end Next_Global;
+
    ----------------------------------
    -- New_Requires_Transient_Scope --
    ----------------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 251998)
+++ sem_util.ads	(working copy)
@@ -885,6 +885,17 @@
    --  Note that the value returned is always the expression (not the
    --  N_Parameter_Association nodes, even if named association is used).
 
+   function First_Global
+     (Subp        : Entity_Id;
+      Global_Mode : Name_Id;
+      Refined     : Boolean := False) return Node_Id;
+   --  Returns the first global item of mode Global_Mode (which can be
+   --  Name_Input, Name_Output, Name_In_Out or Name_Proof_In) associated to
+   --  subprogram Subp, or Empty otherwise. If Refined is True, the global item
+   --  is retrieved from the Refined_Global aspect/pragma associated to the
+   --  body of Subp if present. Next_Global can be used to get the next global
+   --  item with the same mode.
+
    function Fix_Msg (Id : Entity_Id; Msg : String) return String;
    --  Replace all occurrences of a particular word in string Msg depending on
    --  the Ekind of Id as follows:
@@ -2177,6 +2188,16 @@
    --  Note that the result produced is always an expression, not a parameter
    --  association node, even if named notation was used.
 
+   procedure Next_Global (Node : in out Node_Id);
+   pragma Inline (Next_Actual);
+   --  Next_Global (N) is equivalent to N := Next_Global (N). Note that we
+   --  inline this procedural form, but not the functional form that follows.
+
+   function Next_Global (Node : Node_Id) return Node_Id;
+   --  Node is a global item from a list, obtained through calling First_Global
+   --  and possibly Next_Global a number of times. Returns the next global item
+   --  with the same mode.
+
    function No_Heap_Finalization (Typ : Entity_Id) return Boolean;
    --  Determine whether type Typ is subject to pragma No_Heap_Finalization
 
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb	(revision 251998)
+++ gnat1drv.adb	(working copy)
@@ -61,6 +61,7 @@
 with Sem_Ch13;
 with Sem_Elim;
 with Sem_Eval;
+with Sem_SPARK; use Sem_SPARK;
 with Sem_Type;
 with Set_Targ;
 with Sinfo;    use Sinfo;
@@ -1449,12 +1450,19 @@
 
       Prepcomp.Add_Dependencies;
 
-      --  In gnatprove mode we're writing the ALI much earlier than usual
-      --  as flow analysis needs the file present in order to append its
-      --  own globals to it.
-
       if GNATprove_Mode then
 
+         --  Perform the new SPARK checking rules for pointer aliasing. This is
+         --  only activated in GNATprove mode and on SPARK code.
+
+         if Debug_Flag_FF then
+            Check_Safe_Pointers (Main_Unit_Node);
+         end if;
+
+         --  In GNATprove mode we're writing the ALI much earlier than usual
+         --  as flow analysis needs the file present in order to append its
+         --  own globals to it.
+
          --  Note: In GNATprove mode, an "object" file is always generated as
          --  the result of calling gnat1 or gnat2why, although this is not the
          --  same as the object file produced for compilation.
Index: debug.adb
===================================================================
--- debug.adb	(revision 251998)
+++ debug.adb	(working copy)
@@ -69,7 +69,7 @@
    --  dC   Output debugging information on check suppression
    --  dD   Delete elaboration checks in inner level routines
    --  dE   Apply elaboration checks to predefined units
-   --  dF
+   --  dF   Perform the new SPARK checking rules for pointer aliasing
    --  dG   Generate all warnings including those normally suppressed
    --  dH   Hold (kill) call to gigi
    --  dI   Inhibit internal name numbering in gnatG listing
@@ -383,6 +383,11 @@
    --  dE   Apply compile time elaboration checking for with relations between
    --       predefined units. Normally no checks are made.
 
+   --  dF   Perform the new SPARK checking rules for pointer aliasing. This is
+   --       only activated in GNATprove mode and on SPARK code. These rules are
+   --       not yet part of the official SPARK language, but are expected to be
+   --       included in a future version of SPARK.
+
    --  dG   Generate all warnings. Normally Errout suppresses warnings on
    --       units that are not part of the main extended source, and also
    --       suppresses warnings on instantiations in the main extended
Index: libgnat/system.ads
===================================================================
--- libgnat/system.ads	(revision 251998)
+++ libgnat/system.ads	(working copy)
@@ -44,6 +44,12 @@
 --  which prevent execution of code on the stack, e.g. in windows environments
 --  with DEP (Data Execution Protection) enabled.
 
+pragma Restrictions (No_Finalization);
+--  Use restriction No_Finalization to avoid pulling finalization (not allowed
+--  in GNAT) inside sem_spark.adb, when defining type Perm_Tree_Access as an
+--  access type on incomplete type Perm_Tree_Wrapper (which is required for
+--  defining a recursive type).
+
 package System is
    pragma Pure;
    --  Note that we take advantage of the implementation permission to make
Index: gcc-interface/Make-lang.in
===================================================================
--- gcc-interface/Make-lang.in	(revision 251998)
+++ gcc-interface/Make-lang.in	(working copy)
@@ -312,6 +312,7 @@
  ada/freeze.o	\
  ada/frontend.o	\
  ada/libgnat/g-byorma.o	\
+ ada/libgnat/g-dynhta.o	\
  ada/libgnat/g-hesora.o	\
  ada/libgnat/g-htable.o	\
  ada/libgnat/g-spchge.o	\
@@ -443,6 +444,7 @@
  ada/sem_res.o	\
  ada/sem_scil.o	\
  ada/sem_smem.o	\
+ ada/sem_spark.o	\
  ada/sem_type.o	\
  ada/sem_util.o	\
  ada/sem_warn.o	\
