CbC/CbC_gcc: gcc/ada/sem_spark.adb comparison

comparison gcc/ada/sem_spark.adb @ 131:84e7813d76e9

gcc-8.2

author	mir3636
date	Thu, 25 Oct 2018 07:37:49 +0900
parents	04ced10e8804
children

comparison

equal deleted inserted replaced

-:04ced10e8804
+:84e7813d76e9
 --                                                                          --
 --                            S E M _ S P A R K                             --
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2017, Free Software Foundation, Inc.              --
+--          Copyright (C) 2017-2018, 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- --
 Elaboration_Context_Max : constant := 1009;
 --  The hash range
 type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
-function Elaboration_Context_Hash
+function Elaboration_Context_Hash (Key : Entity_Id)
-(Key : Entity_Id) return Elaboration_Context_Index;
+return Elaboration_Context_Index;
 --  Function to hash any node of the AST
-type Perm_Kind is (No_Access, Read_Only, Read_Write, Write_Only);
+type Perm_Kind is (Borrowed, Observed, Unrestricted, Moved);
---  Permission type associated with paths
+--  Permission type associated with paths. The Moved permission is
+--  equivalent to the Unrestricted one (same permissions). The Moved is
-subtype Read_Perm is Perm_Kind range Read_Only .. Read_Write;
+--  however used to mark the RHS after a move (which still unrestricted).
-subtype Write_Perm is Perm_Kind range Read_Write .. Write_Only;
+--  This way, we may generate warnings when manipulating the RHS
+--  afterwads since it is set to Null after the assignment.
 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
 --  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    =>
+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        =>
+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  =>
+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
 --------------------
 -- Error Messages --
 --------------------
 procedure Perm_Mismatch
-(Exp_Perm, Act_Perm : Perm_Kind;
+(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.
 -------------------------
 -- Children_Permission --
 -------------------------
-function Children_Permission
+function Children_Permission (T : Perm_Tree_Access) return Perm_Kind is
-(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
+procedure Copy_Env (From : Perm_Env; To : in out Perm_Env) is
-(From : Perm_Env;
-To : in out Perm_Env)
-is
 Comp_From : Perm_Tree_Access;
-Key_From : Perm_Tree_Maps.Key_Option;
+Key_From  : Perm_Tree_Maps.Key_Option;
-Son : Perm_Tree_Access;
+Son       : Perm_Tree_Access;
 begin
 Reset (To);
 Key_From := Get_First_Key (From);
 while Key_From.Present loop
 -- Copy_Init_Map --
 -------------------
 procedure Copy_Init_Map
 (From : Initialization_Map;
-To : in out Initialization_Map)
+To   : in out Initialization_Map)
 is
 Comp_From : Boolean;
 Key_From : Boolean_Variables_Maps.Key_Option;
 begin
 ---------------
 -- Copy_Tree --
 ---------------
-procedure Copy_Tree
+procedure Copy_Tree (From : Perm_Tree_Access; To : Perm_Tree_Access) is
-(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;
 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 --
 ------------------------------
 --------------------
 -- Free_Perm_Tree --
 --------------------
-procedure Free_Perm_Tree
+procedure Free_Perm_Tree (PT : in out Perm_Tree_Access) is
-(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
 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;
 -------------
 -- Get_All --
 -------------
-function Get_All
+function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access is
-(T : Perm_Tree_Access)
-return Perm_Tree_Access
-is
 begin
 return T.all.Tree.Get_All;
 end Get_All;
 --------------
 -- Get_Elem --
 --------------
-function Get_Elem
+function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access is
-(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
+function Is_Node_Deep (T : Perm_Tree_Access) return Boolean is
-(T : Perm_Tree_Access)
-return Boolean
-is
 begin
 return T.all.Tree.Is_Node_Deep;
 end Is_Node_Deep;
 ----------
 -- Kind --
 ----------
-function Kind
+function Kind (T : Perm_Tree_Access) return Path_Kind is
-(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
+function Permission (T : Perm_Tree_Access) return Perm_Kind is
-(T : Perm_Tree_Access)
-return Perm_Kind
-is
 begin
 return T.all.Tree.Permission;
 end Permission;
 -------------------
 -- Perm_Mismatch --
 -------------------
-procedure Perm_Mismatch
+procedure Perm_Mismatch (Exp_Perm, Act_Perm : Perm_Kind; N : Node_Id) is
-(Exp_Perm, Act_Perm : Perm_Kind;
-N                   : Node_Id)
-is
 begin
-Error_Msg_N ("\expected at least `"
+Error_Msg_N ("\expected state `"
-& Perm_Kind'Image (Exp_Perm) & "`, got `"
+& Perm_Kind'Image (Exp_Perm) & "` at least, got `"
 & Perm_Kind'Image (Act_Perm) & "`", N);
 end Perm_Mismatch;
 end Permissions;
 --  found in the code should be moved, borrowed, or observed.
 type Checking_Mode is
 (Read,
---  Default mode. Checks that paths have Read_Perm permission.
+--  Default mode
 Move,
---  Regular moving semantics (not under 'Access). Checks that paths have
+--  Regular moving semantics. Checks that paths have Unrestricted
---  Read_Write permission. After moving a path, its permission is set to
+--  permission. After moving a path, the permission of both it and
---  Write_Only and the permission of its extensions is set to No_Access.
+--  its extensions are set to Unrestricted.
 Assign,
 --  Used for the target of an assignment, or an actual parameter with
---  mode OUT. Checks that paths have Write_Perm permission. After
+--  mode OUT. Checks that paths have Unrestricted permission. After
---  assigning to a path, its permission is set to Read_Write.
+--  assigning to a path, its permission is set to Unrestricted.
-Super_Move,
+Borrow,
---  Enhanced moving semantics (under 'Access). Checks that paths have
+--  Used for the source of an assignement when initializes a stand alone
---  Read_Write permission. After moving a path, its permission is set
+--  object of anonymous type, constant, or IN parameter and also OUT
---  to No_Access, as well as the permission of its extensions and the
+--  or IN OUT composite object.
---  permission of its prefixes up to the first Reference node.
+--  In the borrowed state, the access object is completely "dead".
-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.
+--  is set to Observed.
 --
 --  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
 -----------------------
 -- 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,
+--  appropriate permissions (unrestricted for borrowed and moved, observed
---  read-write for others).
+--  for observed names).
---
---  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);
+procedure Check_Globals (N : Node_Id);
---  This procedure takes a global pragma and checks depending on mode:
+--  This procedure takes a global pragma and checks it
---  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);
 --  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);
+procedure Check_Param_In (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
+--  permission of every in-mode parameter. This includes Observing and
---  also borrowed in, that are then checked afterwards.
+--  Borrowing.
+procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id);
+--  This procedure takes a formal and an actual parameter and checks the
+--  state of every out-mode and in out-mode parameter. This includes
+--  Moving and Borrowing.
 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
 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;
+(N          : Node_Id;
-Perm : Perm_Kind;
+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 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
+--  paths of all borrowed formal parameters and global have Unrestricted
 --  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
+procedure Return_The_Global
 (Id   : Entity_Id;
 Mode : Formal_Kind;
 Subp : Entity_Id);
---  Auxiliary procedure to Return_Parameters and Return_Globals
+--  Auxiliary procedure to Return_Globals
+--  There is no need to return parameters because they will be reassigned
-procedure Return_Parameters (Subp : Entity_Id);
+--  their state once the subprogram returns. Local variables that have
---  Takes a subprogram as input, and checks that all borrowed parameters of
+--  borrowed, observed, or moved an actual parameter go out of the scope.
---  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);
+function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access;
---  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
+function Set_Perm_Prefixes
-(N : Node_Id; Mode : Checking_Mode)
+(N        : Node_Id;
+New_Perm : Perm_Kind)
 return Perm_Tree_Access;
-pragma Precondition (Mode = Move or Mode = Super_Move);
+--  This function sets the permissions of a given node_id in the
---  Given a node and a mode (that can be either Move or Super_Move), this
+--  permission environment as well as in all the prefixes of the path
---  function modifies the permissions of a given node_id in the permission
+--  to the one given in parameter (P).
---  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;
+(Id         : Entity_Id;
-Mode : Formal_Kind);
+Mode       : Formal_Kind;
+Global_Var : Boolean);
 --  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.
+function Has_Ownership_Aspect_True
+(N   : Node_Id;
+Msg : String)
+return Boolean;
+--  Takes a node as an input, and finds out whether it has ownership aspect
+--  True or False. This function is recursive whenever the node has a
+--  composite type. Access-to-objects have ownership aspect False if they
+--  have a general access type.
 ----------------------
 -- Global Variables --
 ----------------------
 --  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
+procedure Iterate_Call_In is new
-Iterate_Call_Parameters (Check_Param);
+Iterate_Call_Parameters (Check_Param_In);
-procedure Iterate_Call_Observes is new
+procedure Iterate_Call_Out is new
-Iterate_Call_Parameters (Check_Param_Observes);
+Iterate_Call_Parameters (Check_Param_Out);
-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);
+Copy_Env (Current_Perm_Env, Saved_Env);
---  We first check the Read access on every in parameter
+--  We first check the globals then parameters to handle the
+--  No_Parameter_Aliasing Restriction. An out or in-out global is
+--  considered as borrowing while a parameter with the same mode is
+--  a move. This order disallow passing a part of a variable to a
+--  subprogram if it is referenced as a global by the callable (when
+--  writable).
+--  For paremeters, we fisrt check in parameters and then the out ones.
+--  This is to avoid Observing or Borrowing objects that are already
+--  moved. This order is not mandatory but allows to catch runtime
+--  errors like null pointer dereferencement at the analysis time.
 Current_Checking_Mode := Read;
-Iterate_Call_Read (Call);
+Check_Globals (Get_Pragma (Get_Called_Entity (Call), Pragma_Global));
-Check_Globals (Get_Pragma
+Iterate_Call_In (Call);
-(Get_Called_Entity (Call), Pragma_Global), Read);
+Iterate_Call_Out (Call);
---  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);
-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;
+Mode_Before    : constant Checking_Mode := Current_Checking_Mode;
+Saved_Env      : Perm_Env;
-Saved_Env : Perm_Env;
 Saved_Init_Map : Initialization_Map;
+New_Env        : Perm_Env;
-New_Env : Perm_Env;
+Body_Id        : constant Entity_Id := Defining_Entity (Body_N);
+Spec_Id        : constant Entity_Id := Unique_Entity (Body_Id);
-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
 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;
+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);
 --  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);
-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;
 -----------------------
 -- Check_Declaration --
 -----------------------
 procedure Check_Declaration (Decl : Node_Id) is
+Target_Ent : constant Entity_Id := Defining_Identifier (Decl);
+Target_Typ : Node_Id renames Etype (Target_Ent);
+Target_View_Typ : Entity_Id;
+Check : Boolean := True;
 begin
+if Present (Full_View (Target_Typ)) then
+Target_View_Typ := Full_View (Target_Typ);
+else
+Target_View_Typ := Target_Typ;
+end if;
 case N_Declaration'(Nkind (Decl)) is
 when N_Full_Type_Declaration =>
---  Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE
+if not Has_Ownership_Aspect_True (Target_Ent, "type declaration")
-null;
+then
+Check := False;
+end if;
+--  ??? What about component declarations with defaults.
 when N_Object_Declaration =>
---  First move the right-hand side
+if (Is_Access_Type (Target_View_Typ)
-Current_Checking_Mode := Move;
+or else Is_Deep (Target_Typ))
-Check_Node (Expression (Decl));
+and then not Has_Ownership_Aspect_True
+(Target_Ent, "Object declaration ")
+then
+Check := False;
+end if;
+if Is_Anonymous_Access_Type (Target_View_Typ)
+and then not Present (Expression (Decl))
+then
+--  ??? Check the case of default value (AI)
+--  ??? How an anonymous access type can be with default exp?
+Error_Msg_NE ("? object declaration & has OAF (Anonymous "
+& "access-to-object with no initialization)",
+Decl, Target_Ent);
+--  If it it an initialization
+elsif Present (Expression (Decl)) and Check then
+--  Find out the operation to be done on the right-hand side
+--  Initializing object, access type
+if Is_Access_Type (Target_View_Typ) then
+--  Initializing object, constant access type
+if Is_Constant_Object (Target_Ent) then
+--  Initializing object, constant access to variable type
+if not Is_Access_Constant (Target_View_Typ) then
+Current_Checking_Mode := Borrow;
+--  Initializing object, constant access to constant type
+--  Initializing object,
+--  constant access to constant anonymous type.
+elsif Is_Anonymous_Access_Type (Target_View_Typ) then
+--  This is an object declaration so the target
+--  of the assignement is a stand-alone object.
+Current_Checking_Mode := Observe;
+--  Initializing object, constant access to constant
+--  named type.
+else
+--  If named then it is a general access type
+--  Hence, Has_Ownership_Aspec_True is False.
+raise Program_Error;
+end if;
+--  Initializing object, variable access type
+else
+--  Initializing object, variable access to variable type
+if not Is_Access_Constant (Target_View_Typ) then
+--  Initializing object, variable named access to
+--  variable type.
+if not Is_Anonymous_Access_Type (Target_View_Typ) then
+Current_Checking_Mode := Move;
+--  Initializing object, variable anonymous access to
+--  variable type.
+else
+--  This is an object declaration so the target
+--  object of the assignement is a stand-alone
+--  object.
+Current_Checking_Mode := Borrow;
+end if;
+--  Initializing object, variable access to constant type
+else
+--  Initializing object,
+--  variable named access to constant type.
+if not Is_Anonymous_Access_Type (Target_View_Typ) then
+Error_Msg_N ("assignment not allowed, Ownership "
+& "Aspect False (Anonymous Access "
+& "Object)", Decl);
+Check := False;
+--  Initializing object,
+--  variable anonymous access to constant type.
+else
+--  This is an object declaration so the target
+--  of the assignement is a stand-alone object.
+Current_Checking_Mode := Observe;
+end if;
+end if;
+end if;
+--  Initializing object, composite (deep) type
+elsif Is_Deep (Target_Typ) then
+--  Initializing object, constant composite type
+if Is_Constant_Object (Target_Ent) then
+Current_Checking_Mode := Observe;
+--  Initializing object, variable composite type
+else
+--  Initializing object, variable anonymous composite type
+if Nkind (Object_Definition (Decl)) =
+N_Constrained_Array_Definition
+--  An N_Constrained_Array_Definition is an anonymous
+--  array (to be checked). Record types are always
+--  named and are considered in the else part.
+then
+declare
+Com_Ty : constant Node_Id :=
+Component_Type (Etype (Target_Typ));
+begin
+if Is_Access_Type (Com_Ty) then
+--  If components are of anonymous type
+if Is_Anonymous_Access_Type (Com_Ty) then
+if Is_Access_Constant (Com_Ty) then
+Current_Checking_Mode := Observe;
+else
+Current_Checking_Mode := Borrow;
+end if;
+else
+Current_Checking_Mode := Move;
+end if;
+elsif Is_Deep (Com_Ty) then
+--  This is certainly named so it is a move
+Current_Checking_Mode := Move;
+end if;
+end;
+else
+Current_Checking_Mode := Move;
+end if;
+end if;
+end if;
+end if;
+if Check then
+Check_Node (Expression (Decl));
+end if;
+--  If lhs is not a pointer, we still give it the unrestricted
+--  state which is useless but not harmful.
 declare
 Elem : Perm_Tree_Access;
+Deep : constant Boolean := Is_Deep (Target_Typ);
 begin
-Elem := new Perm_Tree_Wrapper'
+--  Note that all declared variables are set to the unrestricted
-(Tree =>
+--  state.
-(Kind                => Entire_Object,
+--
-Is_Node_Deep        =>
+--  If variables are not initialized:
-Is_Deep (Etype (Defining_Identifier (Decl))),
+--  unrestricted to every declared object.
-Permission          => Read_Write,
+--  Exp:
-Children_Permission => Read_Write));
+--    R : Rec
+--    S : Rec := (...)
---  If unitialized declaration, then set to Write_Only. If a
+--    R := S
---  pointer declaration, it has a null default initialization.
+--  The assignement R := S is not allowed in the new rules
-if Nkind (Expression (Decl)) = N_Empty
+--  if R is not unrestricted.
-and then not Has_Full_Default_Initialization
+--
-(Etype (Defining_Identifier (Decl)))
+--  If variables are initialized:
-and then not Is_Access_Type
+--    If it is a move, then the target is unrestricted
-(Etype (Defining_Identifier (Decl)))
+--    If it is a borrow, then the target is unrestricted
-then
+--    If it is an observe, then the target should be observed
-Elem.all.Tree.Permission := Write_Only;
-Elem.all.Tree.Children_Permission := Write_Only;
+if Current_Checking_Mode = Observe then
+Elem := new Perm_Tree_Wrapper'
+(Tree =>
+(Kind                => Entire_Object,
+Is_Node_Deep        => Deep,
+Permission          => Observed,
+Children_Permission => Observed));
+else
+Elem := new Perm_Tree_Wrapper'
+(Tree =>
+(Kind                => Entire_Object,
+Is_Node_Deep        => Deep,
+Permission          => Unrestricted,
+Children_Permission => Unrestricted));
 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);
-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
+when N_Function_Specification
-| N_Function_Specification
 | N_Entry_Declaration
 | N_Procedure_Specification
+| N_Component_Declaration
 =>
 raise Program_Error;
 --  Ignored constructs for pointer checking
 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 =>
+when N_Procedure_Call_Statement
+| N_Function_Call
+=>
 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 ???
+--  What about generics? (formal parameters).
 when N_Attribute_Reference =>
 case Attribute_Name (Expr) is
 when Name_Access =>
-case Current_Checking_Mode is
+Error_Msg_N ("access attribute not allowed", Expr);
-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;
 when Name_Min =>
 Current_Checking_Mode := Read;
 Check_Node (Prefix (Expr));
 when Name_Image =>
+Check_List (Expressions (Expr));
+when Name_Img =>
 Check_Node (Prefix (Expr));
 when Name_SPARK_Mode =>
 null;
 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 =>
 --  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;
 --  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
 Saved_Env : Perm_Env;
 --  Accumulator for the different branches
 New_Env : Perm_Env;
+Elmt    : Node_Id := First (Expressions (Expr));
-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,
+Copy_Env (Current_Perm_Env, Saved_Env);
-Saved_Env);
 --  Here we have the original env in saved, current with a fresh
 --  copy, and new aliased.
 --  THEN PART
 Check_Node (Elmt);
 --  Here the new_environment contains curr env after then block
 --  ELSE part
 --  Restore environment before if
-Copy_Env (Current_Perm_Env,
+Copy_Env (Current_Perm_Env, New_Env);
-New_Env);
 Free_Env (Current_Perm_Env);
+Copy_Env (Saved_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,
+Copy_Env (New_Env, Current_Perm_Env);
-Current_Perm_Env);
 Free_Env (New_Env);
 Free_Env (Saved_Env);
 end;
 when N_Indexed_Component =>
 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));
 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,
+Copy_Env (Current_Perm_Env, Saved_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);
-Copy_Env (Current_Perm_Env,
-New_Env);
 Free_Env (Current_Perm_Env);
 --  Other alternatives
 while Present (Elmt) loop
 --  Restore environment
-Copy_Env (Saved_Env,
+Copy_Env (Saved_Env, Current_Perm_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);
+Copy_Env (Saved_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));
 | 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
+procedure Check_Globals (N : Node_Id) is
 begin
 if Nkind (N) = N_Empty then
 return;
 end if;
 declare
-pragma Assert
+pragma Assert (List_Length (Pragma_Argument_Associations (N)) = 1);
-(List_Length (Pragma_Argument_Associations (N)) = 1);
+PAA : constant Node_Id := First (Pragma_Argument_Associations (N));
-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;
+procedure Process (Mode : Name_Id; The_Global : Entity_Id);
-The_Global : Entity_Id);
+procedure Process (Mode : Name_Id; The_Global : Node_Id) is
+Ident_Elt   : constant 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 Mode is
-case Check_Mode is
+when Name_Input
-when Read =>
+| Name_Proof_In
-case Mode is
+=>
-when Name_Input
+Current_Checking_Mode := Observe;
-| 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_Output
-when Name_Input
+| Name_In_Out
-| Name_Proof_In
+=>
-=>
+--  ??? Borrow not Move?
-null;
+Current_Checking_Mode := Borrow;
+Check_Node (The_Global);
-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
 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
 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
 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
 -- 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;
 --  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 :=
 --  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);
+Free_Env (Loop_Env.all);
+Free_Env (Exit_Env.all);
 else
 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
+Free_Env (Loop_Env.all);
 end if;
-Free_Env (Loop_Env.all);
-Free_Env (Exit_Env.all);
 end;
 end Check_Loop_Statement;
 ----------------
 -- Check_Node --
 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));
 | 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_Task_Type_Declaration
 | N_Use_Package_Clause
 | N_With_Clause
 | N_Use_Type_Clause
 | N_Validate_Unchecked_Conversion
+| N_Variable_Reference_Marker
+| N_Discriminant_Association
+--  ??? check whether we should do sth special for
+--  N_Discriminant_Association, or maybe raise a program error.
 =>
 null;
 --  The following nodes are rewritten by semantic analysis
 when N_Single_Protected_Declaration
 | N_Single_Task_Declaration
 =>
 Check_List (Visible_Declarations (CorSp));
 --  Save environment
-Copy_Env (Current_Perm_Env,
+Copy_Env (Current_Perm_Env, Saved_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)
 --  Restore previous environment (i.e. delete every nonvisible
 --  declaration) from environment.
 Free_Env (Current_Perm_Env);
-Copy_Env (Saved_Env,
+Copy_Env (Saved_Env, Current_Perm_Env);
-Current_Perm_Env);
 end Check_Package_Body;
------------------
+--------------------
--- Check_Param --
+-- Check_Param_In --
------------------
+--------------------
-procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
+procedure Check_Param_In (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
+case Formal_Kind'(Mode) is
-when Read =>
-case Formal_Kind'(Mode) is
+--  Formal IN parameter
-when E_In_Parameter =>
-if Is_Borrowed_In (Formal) then
+when E_In_Parameter =>
---  Borrowed in
+--  Formal IN parameter, access type
-Current_Checking_Mode := Move;
+if Is_Access_Type (Etype (Formal)) then
+--  Formal IN parameter, access to variable type
+if not Is_Access_Constant (Etype (Formal)) then
+--  Formal IN parameter, named/anonymous access-to-variable
+--  type.
+--
+--  In SPARK, IN access-to-variable is an observe operation
+--  for a function, and a borrow operation for a procedure.
+if Ekind (Scope (Formal)) = E_Function then
+Current_Checking_Mode := Observe;
+Check_Node (Actual);
 else
---  Observed
+Current_Checking_Mode := Borrow;
+Check_Node (Actual);
-return;
 end if;
-when E_Out_Parameter =>
+--  Formal IN parameter, access-to-constant type
-return;
+--  Formal IN parameter, access-to-named-constant type
-when E_In_Out_Parameter =>
+elsif not Is_Anonymous_Access_Type (Etype (Formal)) then
---  Borrowed in out
+Error_Msg_N ("assignment not allowed, Ownership Aspect"
+& " False (Named general access type)",
-Current_Checking_Mode := Move;
+Formal);
-end case;
+--  Formal IN parameter, access to anonymous constant type
-Check_Node (Actual);
+else
+Current_Checking_Mode := Observe;
-when Assign =>
+Check_Node (Actual);
-case Formal_Kind'(Mode) is
+end if;
-when E_In_Parameter =>
-null;
+--  Formal IN parameter, composite type
-when E_Out_Parameter
+elsif Is_Deep (Etype (Formal)) then
-| E_In_Out_Parameter
-=>
+--  Composite formal types should be named
---  Borrowed out or in out
+--  Formal IN parameter, composite named type
-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;
+Current_Checking_Mode := Mode_Before;
+end Check_Param_In;
+----------------------
+-- Check_Param_Out --
+----------------------
+procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id) is
+Mode        : constant Entity_Kind := Ekind (Formal);
+Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+begin
+case Formal_Kind'(Mode) is
+--  Formal OUT/IN OUT parameter
+when E_Out_Parameter
+| E_In_Out_Parameter
+=>
+--  Formal OUT/IN OUT parameter, access type
+if Is_Access_Type (Etype (Formal)) then
+--  Formal OUT/IN OUT parameter, access to variable type
+if not Is_Access_Constant (Etype (Formal)) then
+--  Cannot have anonymous out access parameter
+--  Formal out/in out parameter, access to named variable
+--  type.
+Current_Checking_Mode := Move;
+Check_Node (Actual);
+--  Formal out/in out parameter, access to constant type
+else
+Error_Msg_N ("assignment not allowed, Ownership Aspect False"
+& " (Named general access type)", Formal);
+end if;
+--  Formal out/in out parameter, composite type
+elsif Is_Deep (Etype (Formal)) then
+--  Composite formal types should be named
+--  Formal out/in out Parameter, Composite Named type.
+Current_Checking_Mode := Borrow;
+Check_Node (Actual);
+end if;
+when E_In_Parameter =>
+null;
+end case;
+Current_Checking_Mode := Mode_Before;
+end Check_Param_Out;
 -------------------------
 -- Check_Safe_Pointers --
 -------------------------
 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
 -- Check_Statement --
 ---------------------
 procedure Check_Statement (Stmt : Node_Id) is
 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+State_N     : Perm_Kind;
+Check       : Boolean := True;
+St_Name     : Node_Id;
+Ty_St_Name  : Node_Id;
+function Get_Root (Comp_Stmt : Node_Id) return Node_Id;
+--  Return the root of the name given as input
+function Get_Root (Comp_Stmt : Node_Id) return Node_Id is
+begin
+case Nkind (Comp_Stmt) is
+when N_Identifier
+| N_Expanded_Name
+=> return Comp_Stmt;
+when N_Type_Conversion
+| N_Unchecked_Type_Conversion
+| N_Qualified_Expression
+=>
+return Get_Root (Expression (Comp_Stmt));
+when N_Parameter_Specification =>
+return Get_Root (Defining_Identifier (Comp_Stmt));
+when N_Selected_Component
+| N_Indexed_Component
+| N_Slice
+| N_Explicit_Dereference
+=>
+return Get_Root (Prefix (Comp_Stmt));
+when others =>
+raise Program_Error;
+end case;
+end Get_Root;
 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;
+St_Name    := Name (Stmt);
-else
+Ty_St_Name := Etype (Name (Stmt));
-Current_Checking_Mode := Read;
+--  Check that is not a *general* access type
+if Has_Ownership_Aspect_True (St_Name, "assigning to") then
+--  Assigning to access type
+if Is_Access_Type (Ty_St_Name) then
+--  Assigning to access to variable type
+if not Is_Access_Constant (Ty_St_Name) then
+--  Assigning to named access to variable type
+if not Is_Anonymous_Access_Type (Ty_St_Name) then
+Current_Checking_Mode := Move;
+--  Assigning to anonymous access to variable type
+else
+--  Target /= source root
+if Nkind_In (Expression (Stmt), N_Allocator, N_Null)
+or else Entity (St_Name) /=
+Entity (Get_Root (Expression (Stmt)))
+then
+Error_Msg_N ("assignment not allowed, anonymous "
+& "access Object with Different Root",
+Stmt);
+Check := False;
+--  Target = source root
+else
+--  Here we do nothing on the source nor on the
+--  target. However, we check the the legality rule:
+--  "The source shall be an owning access object
+--  denoted by a name that is not in the observed
+--  state".
+State_N := Get_Perm (Expression (Stmt));
+if State_N = Observed then
+Error_Msg_N ("assignment not allowed, Anonymous "
+& "access object with the same root"
+& " but source Observed", Stmt);
+Check := False;
+end if;
+end if;
+end if;
+--  else access-to-constant
+--  Assigning to anonymous access-to-constant type
+elsif Is_Anonymous_Access_Type (Ty_St_Name) then
+--  ??? Check the follwing condition. We may have to
+--  add that the root is in the observed state too.
+State_N := Get_Perm (Expression (Stmt));
+if State_N /= Observed then
+Error_Msg_N ("assignment not allowed, anonymous "
+& "access-to-constant object not in "
+& "the observed state)", Stmt);
+Check := False;
+else
+Error_Msg_N ("?here check accessibility level cited in"
+& " the second legality rule of assign",
+Stmt);
+Check := False;
+end if;
+--  Assigning to named access-to-constant type:
+--  This case should have been detected when checking
+--  Has_Onwership_Aspect_True (Name (Stmt), "msg").
+else
+raise Program_Error;
+end if;
+--  Assigning to composite (deep) type.
+elsif Is_Deep (Ty_St_Name) then
+if Ekind_In (Ty_St_Name,
+E_Record_Type,
+E_Record_Subtype)
+then
+declare
+Elmt : Entity_Id :=
+First_Component_Or_Discriminant (Ty_St_Name);
+begin
+while Present (Elmt) loop
+if Is_Anonymous_Access_Type (Etype (Elmt)) or
+Ekind (Elmt) = E_General_Access_Type
+then
+Error_Msg_N ("assignment not allowed, Ownership "
+& "Aspect False (Components have "
+& "Ownership Aspect False)", Stmt);
+Check := False;
+exit;
+end if;
+Next_Component_Or_Discriminant (Elmt);
+end loop;
+end;
+--  Record types are always named so this is a move
+if Check then
+Current_Checking_Mode := Move;
+end if;
+elsif Ekind_In (Ty_St_Name,
+E_Array_Type,
+E_Array_Subtype)
+and then Check
+then
+Current_Checking_Mode := Move;
+end if;
+--  Now handle legality rules of using a borrowed, observed,
+--  or moved name as a prefix in an assignment.
+else
+if Nkind_In (St_Name,
+N_Attribute_Reference,
+N_Expanded_Name,
+N_Explicit_Dereference,
+N_Indexed_Component,
+N_Reference,
+N_Selected_Component,
+N_Slice)
+then
+if Is_Access_Type (Etype (Prefix (St_Name))) or
+Is_Deep (Etype (Prefix (St_Name)))
+then
+--  We set the Check variable to True so that we can
+--  Check_Node of the expression and the name first
+--  under the assumption of Current_Checking_Mode =
+--  Read => nothing to be done for the RHS if the
+--  following check on the expression fails, and
+--  Current_Checking_Mode := Assign => the name should
+--  not be borrowed or observed so that we can use it
+--  as a prefix in the target of an assignement.
+--
+--  Note that we do not need to check the OA here
+--  because we are allowed to read and write "through"
+--  an object of OAF (example: traversing a DS).
+Check := True;
+end if;
+end if;
+if Nkind_In (Expression (Stmt),
+N_Attribute_Reference,
+N_Expanded_Name,
+N_Explicit_Dereference,
+N_Indexed_Component,
+N_Reference,
+N_Selected_Component,
+N_Slice)
+then
+if Is_Access_Type (Etype (Prefix (Expression (Stmt))))
+or else Is_Deep (Etype (Prefix (Expression (Stmt))))
+then
+Current_Checking_Mode := Observe;
+Check := True;
+end if;
+end if;
+end if;
+if Check then
+Check_Node (Expression (Stmt));
+Current_Checking_Mode := Assign;
+Check_Node (St_Name);
+end if;
 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,
+Copy_Env (Current_Perm_Env, Saved_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,
+Copy_Env (Saved_Env, Current_Perm_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,
+Copy_Env (Current_Perm_Env, Saved_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);
-Copy_Env (Current_Perm_Env,
-New_Env);
 Free_Env (Current_Perm_Env);
 --  Other alternatives
 while Present (Elmt) loop
 --  Restore environment
-Copy_Env (Saved_Env,
+Copy_Env (Saved_Env, Current_Perm_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 (Saved_Env, Current_Perm_Env);
-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_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
 --  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;
+Check := False;
 end if;
-Check_Node (Expression (Stmt));
+if Check then
+Check_Node (Expression (Stmt));
+end if;
 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
+--  Nothing to do when exiting a loop. No merge needed
 when N_Exit_Statement =>
-declare
+null;
-Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
+--  Copy environment, run on each branch
-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,
+Copy_Env (Current_Perm_Env, Saved_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);
-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,
+Copy_Env (Saved_Env, Current_Perm_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,
+Copy_Env (Saved_Env, Current_Perm_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,
+Copy_Env (Saved_Env, Current_Perm_Env);
-Current_Perm_Env);
 Free_Env (New_Env);
 Free_Env (Saved_Env);
 end;
 --  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;
+return Unrestricted;
 end case;
 end Get_Perm;
 ----------------------
 -- Get_Perm_Or_Tree --
 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;
 --  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 :=
+C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
-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,
+return (R           => Unfolded,
 Tree_Access =>
 Other_Components (C.Tree_Access));
 else
-return (R => Unfolded,
+return (R           => Unfolded,
 Tree_Access => Selected_C);
 end if;
 end;
 elsif Kind (C.Tree_Access) = Entire_Object then
-return (R => Folded, Found_Permission =>
+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 :=
+C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
-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 :=
+C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
-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);
 -------------------
 -- Get_Perm_Tree --
 -------------------
-function Get_Perm_Tree
+function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is
-(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_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;
 --  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 :=
+C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N));
-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));
 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.
 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 :=
 )
 );
 --  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'
 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 :=
 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 :=
+C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N));
-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;
 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 =>
 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;
 --  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 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
 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 =>
 --  ??? What about hidden components
 when E_Record_Type
 | E_Record_Subtype
 =>
 declare
 Elmt : Entity_Id;
 begin
 Elmt := First_Component_Or_Discriminant (E);
 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
 else
 return True;
 end if;
 end if;
-when E_Incomplete_Type =>
+when E_Incomplete_Type
-return True;
+| E_Incomplete_Subtype
+=>
-when E_Incomplete_Subtype =>
 return True;
 --  No problem with synchronized types
 when E_Protected_Type
 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 --
 ----------------
 when others =>
 raise Program_Error;
 end case;
 end Set_Root_Object;
 --  Local variables
 Root : Entity_Id;
 Is_Deref : Boolean;
 ------------------
 -- Process_Path --
 ------------------
 procedure Process_Path (N : Node_Id) is
-Root : constant Entity_Id := Get_Enclosing_Object (N);
+Root    : constant Entity_Id := Get_Enclosing_Object (N);
+State_N : Perm_Kind;
 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,
+State_N := Get_Perm (N);
---  allowing backward compatibility.
+case Current_Checking_Mode is
-if not Has_Alias (N)
-and then Is_Shallow (Etype (N))
+--  Check permission R, do nothing
-then
-return;
+when Read =>
-end if;
+--  This condition should be removed when removing the read
-declare
+--  checking mode.
-Perm_N : constant Perm_Kind := Get_Perm (N);
+return;
-begin
+when Move =>
-case Current_Checking_Mode is
---  Check permission R, do nothing
+--  The rhs object in an assignment statement (including copy in
+--  and copy back) should be in the Unrestricted or Moved state.
-when Read =>
+--  Otherwise the move is not allowed.
-if Perm_N not in Read_Perm then
+--  This applies to both stand-alone and composite objects.
-Perm_Error (N, Read_Only, Perm_N);
+--  If the state of the source is Moved, then a warning message
-end if;
+--  is prompt to make the user aware of reading a nullified
+--  object.
---  If shallow type no need for RW, only R
+if State_N /= Unrestricted and State_N /= Moved then
-when Move =>
+Perm_Error (N, Unrestricted, State_N);
-if Is_Shallow (Etype (N)) then
+return;
-if Perm_N not in Read_Perm then
+end if;
-Perm_Error (N, Read_Only, Perm_N);
-end if;
+--  In the AI, after moving a path nothing to do since the rhs
-else
+--  object was in the Unrestricted state and it shall be
---  Check permission RW if deep
+--  refreshed to Unrestricted. The object should be nullified
+--  however. To avoid moving again a name that has already been
-if Perm_N /= Read_Write then
+--  moved, in this implementation we set the state of the moved
-Perm_Error (N, Read_Write, Perm_N);
+--  object to "Moved". This shall be used to prompt a warning
-end if;
+--  when manipulating a null pointer and also to implement
+--  the no aliasing parameter restriction.
-declare
---  Set permission to W to the path and any of its prefix
+if State_N = Moved then
+Error_Msg_N ("?the source or one of its extensions has"
-Tree : constant Perm_Tree_Access :=
+& " already been moved", N);
-Set_Perm_Prefixes_Move (N, Move);
+end if;
-begin
+declare
-if Tree = null then
+--  Set state to Moved to the path and any of its prefixes
---  We went through a function call, no permission to
---  modify.
+Tree : constant Perm_Tree_Access :=
+Set_Perm_Prefixes (N, Moved);
-return;
-end if;
+begin
+if Tree = null then
---  Set permissions to
---  No for any extension with more .all
+--  We went through a function call, no permission to
---  W for any deep extension with same number of .all
+--  modify.
---  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
+--  Set state to Moved on any strict extension of the path
-if Has_Function_Component (N) then
+Set_Perm_Extensions (Tree, Moved);
+end;
+when Assign =>
+--  The lhs object in an assignment statement (including copy in
+--  and copy back) should be in the Unrestricted state.
+--  Otherwise the move is not allowed.
+--  This applies to both stand-alone and composite objects.
+if State_N /= Unrestricted and State_N /= Moved then
+Perm_Error (N, Unrestricted, State_N);
+return;
+end if;
+--  After assigning to a path nothing to do since it was in the
+--  Unrestricted state and it would be refreshed to
+--  Unrestricted.
+when Borrow =>
+--  Borrowing is only allowed on Unrestricted objects.
+if State_N /= Unrestricted and State_N /= Moved then
+Perm_Error (N, Unrestricted, State_N);
+end if;
+if State_N = Moved then
+Error_Msg_N ("?the source or one of its extensions has"
+& " already been moved", N);
+end if;
+declare
+--  Set state to Borrowed to the path and any of its prefixes
+Tree : constant Perm_Tree_Access :=
+Set_Perm_Prefixes (N, Borrowed);
+begin
+if Tree = null then
+--  We went through a function call, no permission to
+--  modify.
 return;
 end if;
-declare
+--  Set state to Borrowed on any strict extension of the path
---  Get the permission tree for the path
+Set_Perm_Extensions (Tree, Borrowed);
-Tree : constant Perm_Tree_Access :=
+end;
-Get_Perm_Tree (N);
+when Observe =>
-Dummy : Perm_Tree_Access;
+if State_N /= Unrestricted
+and then State_N /= Observed
-begin
+then
-if Tree = null then
+Perm_Error (N, Observed, State_N);
---  We went through a function call, no permission to
+end if;
---  modify.
+declare
-return;
+--  Set permission to Observed on the path and any of its
-end if;
+--  prefixes if it is of a deep type. Actually, some operation
+--  like reading from an object of access type is considered as
---  Set permission RW for it and all of its extensions
+--  observe while it should not affect the permissions of
+--  the considered tree.
-Tree.all.Tree.Permission := Read_Write;
+Tree : Perm_Tree_Access;
-Set_Perm_Extensions (Tree, Read_Write);
+begin
---  Normalize the permission tree
+if Is_Deep (Etype (N)) then
+Tree := Set_Perm_Prefixes (N, Observed);
-Dummy := Set_Perm_Prefixes_Assign (N);
+else
-end;
+Tree := null;
---  Check permission W
-when Borrow_Out =>
-if Perm_N not in Write_Perm then
-Perm_Error (N, Write_Only, Perm_N);
 end if;
-declare
+if Tree = null then
---  Set permission to No to the path and any of its prefixes
+--  We went through a function call, no permission to
-Tree : constant Perm_Tree_Access :=
+--  modify.
-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 permissions to No on any strict extension of the path
---  Set permission to No on the path and any of its prefixes
+Set_Perm_Extensions (Tree, Observed);
-Tree : constant Perm_Tree_Access :=
+end;
-Set_Perm_Prefixes_Observe (N);
+end case;
-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
+if Permission (Elem) /= Unrestricted then
-Perm_Error (Decl, Read_Write, Permission (Elem));
+Perm_Error (Decl, Unrestricted, Permission (Elem));
 end if;
 end;
 end if;
 end Return_Declaration;
 --  Local Variables
 N : Node_Id;
 --  Start of processing for 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
 --  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);
+Return_The_Global (E, Kind, Subp);
 end if;
 Next_Global (Item);
 end loop;
 end Return_Globals_From_List;
 procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is
 Kind : Formal_Kind;
 begin
 case Global_Mode is
-when Name_Input | Name_Proof_In =>
+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;
 --------------------------------
 -- Return_Parameter_Or_Global --
 --------------------------------
-procedure Return_Parameter_Or_Global
+procedure Return_The_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
+if Mode = E_In_Parameter
-null;
+--  Check this for read-only globals.
---  All other parameters and globals should return with mode RW to the
---  caller.
+then
+if Permission (Elem) /= Unrestricted
-else
+and then Permission (Elem) /= Observed
-if Permission (Elem) /= Read_Write then
+then
 Perm_Error_Subprogram_End
 (E          => Id,
 Subp       => Subp,
-Perm       => Read_Write,
+Perm       => Observed,
+Found_Perm => Permission (Elem));
+end if;
+--  All globals of mode out or in/out should return with mode
+--  Unrestricted.
+else
+if Permission (Elem) /= Unrestricted then
+Perm_Error_Subprogram_End
+(E          => Id,
+Subp       => Subp,
+Perm       => Unrestricted,
 Found_Perm => Permission (Elem));
 end if;
 end if;
-end Return_Parameter_Or_Global;
+end Return_The_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
+procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind) is
-(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
-procedure Free_Perm_Tree_Children (T : Perm_Tree_Access)
-is
 begin
 case Kind (T) is
 when Entire_Object =>
 null;
 Free_Perm_Tree_Children (T);
 T.all.Tree := Son;
 end Set_Perm_Extensions;
 ------------------------------
--- Set_Perm_Extensions_Move --
+-- Set_Perm_Prefixes --
 ------------------------------
-procedure Set_Perm_Extensions_Move
+function Set_Perm_Prefixes
-(T : Perm_Tree_Access;
+(N        : Node_Id;
-E : Entity_Id)
+New_Perm : Perm_Kind)
+return Perm_Tree_Access
 is
 begin
-if not Is_Node_Deep (T) then
---  We are a shallow extension with same number of .all
+case Nkind (N) is
-Set_Perm_Extensions (T, Read_Write);
+when N_Identifier
-return;
+| N_Expanded_Name
-end if;
+| N_Defining_Identifier
+=>
---  We are a deep extension here (or the moved deep path)
+if Nkind (N) = N_Defining_Identifier
+and then New_Perm = Borrowed
-T.all.Tree.Permission := Write_Only;
+then
+raise Program_Error;
-case T.all.Tree.Kind is
+end if;
---  Unroll the tree depending on the type
+declare
-when Entire_Object =>
+P : Node_Id;
-case Ekind (E) is
+C : Perm_Tree_Access;
-when Scalar_Kind
-| E_String_Literal_Subtype
+begin
-=>
+if Nkind (N) = N_Defining_Identifier then
-Set_Perm_Extensions (T, No_Access);
+P := N;
+else
---  No need to unroll here, directly put sons to No_Access
+P := Entity (N);
+end if;
-when Access_Kind =>
-if Ekind (E) in Access_Subprogram_Kind then
+C := Get (Current_Perm_Env, Unique_Entity (P));
-null;
+pragma Assert (C /= null);
-else
-Set_Perm_Extensions (T, No_Access);
+--  Setting the initialization map to True, so that this
-end if;
+--  variable cannot be ignored anymore when looking at end
+--  of elaboration of package.
---  No unrolling done, too complicated
+Set (Current_Initialization_Map, Unique_Entity (P), True);
-when E_Class_Wide_Subtype
+if New_Perm = Observed
-| E_Class_Wide_Type
+and then C = null
-| E_Incomplete_Type
+then
-| E_Incomplete_Subtype
-| E_Exception_Type
+--  No null possible here, there are no parents for the path.
-| E_Task_Type
+--  This means we are using a global variable without adding
-| E_Task_Subtype
+--  it in environment with a global aspect.
-=>
-Set_Perm_Extensions (T, No_Access);
+Illegal_Global_Usage (N);
+end if;
---  Expand the tree. Replace the node with Array component.
+C.all.Tree.Permission := New_Perm;
-when E_Array_Type
+return C;
-| E_Array_Subtype =>
+end;
+when N_Type_Conversion
+| N_Unchecked_Type_Conversion
+| N_Qualified_Expression
+=>
+return Set_Perm_Prefixes (Expression (N), New_Perm);
+when N_Parameter_Specification =>
+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 (Prefix (N), New_Perm);
+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.
 declare
-Son : Perm_Tree_Access;
+Selected_Component : constant Entity_Id :=
+Entity (Selector_Name (N));
+Selected_C : Perm_Tree_Access :=
+Perm_Tree_Maps.Get
+(Component (C), Selected_Component);
 begin
-Son := new Perm_Tree_Wrapper'
+if Selected_C = null then
-(Tree =>
+Selected_C := Other_Components (C);
-(Kind                => Entire_Object,
+end if;
-Is_Node_Deep        => Is_Node_Deep (T),
-Permission          => Read_Write,
+pragma Assert (Selected_C /= null);
-Children_Permission => Read_Write));
+Selected_C.all.Tree.Permission := New_Perm;
+return Selected_C;
-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
+elsif Kind (C) = Entire_Object then
-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;
+--  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;
+Children_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.
-pragma Assert (Is_Node_Deep (T));
+C.all.Tree :=
+(Kind         => Record_Component,
-T.all.Tree :=
+Is_Node_Deep => Is_Node_Deep (C),
-(Kind             => Record_Component,
+Permission   => Permission (C),
-Is_Node_Deep     => Is_Node_Deep (T),
+Component    => Hashtbl,
-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,
+Permission          => Children_Perm,
-Children_Permission => Read_Write)
+Children_Permission => Children_Perm)
-)
+));
-);
 --  We fill the hash table with all sons of the record,
 --  with basic Entire_Objects nodes.
-Elem := First_Component_Or_Discriminant (E);
+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,
+Permission          => Children_Perm,
-Children_Permission => Read_Write));
+Children_Permission => Children_Perm));
-Set_Perm_Extensions_Move (Son, Etype (Elem));
+Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
-Perm_Tree_Maps.Set
-(T.all.Tree.Component, Elem, Son);
 Next_Component_Or_Discriminant (Elem);
 end loop;
+--  Now we set the right field to Borrowed, 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 := New_Perm;
+return Selected_C;
+end;
 end;
+else
-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;
+end if;
-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;
+--  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
--- Set_Perm_Prefixes_Assign --
+--  one step.
-------------------------------
-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));
+declare
+C : constant Perm_Tree_Access :=
---  Continue recursion on prefix
+Set_Perm_Prefixes (Prefix (N), New_Perm);
+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 := New_Perm;
+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          => New_Perm,
+Children_Permission => Children_Permission (C)));
+--  Children_Permission => Children_Permission (C)
+--  this line should be checked maybe New_Perm
+--  instead of 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   => New_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 =>
-return Set_Perm_Prefixes_Assign (Prefix (N));
+declare
+C : constant Perm_Tree_Access :=
+Set_Perm_Prefixes (Prefix (N), New_Perm);
+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 := New_Perm;
+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          => New_Perm,
+Children_Permission => Children_Permission (C)));
+--  We change the current node from Entire_Object to
+--  Reference with Borrowed and the previous son.
+pragma Assert (Is_Node_Deep (C));
+C.all.Tree := (Kind         => Reference,
+Is_Node_Deep => Is_Node_Deep (C),
+Permission   => New_Perm,
+Get_All      => Son);
+return Get_All (C);
+end;
+else
+raise Program_Error;
+end if;
+end;
 when N_Function_Call =>
-raise Program_Error;
+return null;
 when others =>
 raise Program_Error;
 end case;
-end Set_Perm_Prefixes_Assign;
+end Set_Perm_Prefixes;
-----------------------------------
+------------------------------
--- Set_Perm_Prefixes_Borrow_Out --
+-- Set_Perm_Prefixes_Borrow --
-----------------------------------
+------------------------------
-function Set_Perm_Prefixes_Borrow_Out
+function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access
-(N : Node_Id)
-return Perm_Tree_Access
 is
 begin
-pragma Assert (Current_Checking_Mode = Borrow_Out);
+pragma Assert (Current_Checking_Mode = Borrow);
 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 := Borrowed;
-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));
+return Set_Perm_Prefixes_Borrow (Expression (N));
 when N_Parameter_Specification
 | N_Defining_Identifier
 =>
 raise Program_Error;
 --  in one step.
 when N_Selected_Component =>
 declare
 C : constant Perm_Tree_Access :=
-Set_Perm_Prefixes_Borrow_Out (Prefix (N));
+Set_Perm_Prefixes_Borrow (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 (Permission (C) = Borrowed);
 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 := Borrowed;
-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.
 --  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
 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);
-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
+--  Now we set the right field to Borrowed, 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
-Selected_C : Perm_Tree_Access :=
+(Component (C), Selected_Component);
-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 := Borrowed;
-Selected_C.all.Tree.Permission := No_Access;
 return Selected_C;
 end;
 end;
 else
 raise Program_Error;
 end if;
 end;
 when N_Indexed_Component
 | N_Slice
 =>
 declare
 C : constant Perm_Tree_Access :=
-Set_Perm_Prefixes_Borrow_Out (Prefix (N));
+Set_Perm_Prefixes_Borrow (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
+pragma Assert (Permission (C) = Borrowed);
---  (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 := Borrowed;
-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,
+Permission          => Borrowed,
 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,
+Permission   => Borrowed,
 Get_Elem     => Son);
 return Get_Elem (C);
 end;
 else
 raise Program_Error;
 end if;
 end;
 --  at one step.
 when N_Explicit_Dereference =>
 declare
 C : constant Perm_Tree_Access :=
-Set_Perm_Prefixes_Borrow_Out (Prefix (N));
+Set_Perm_Prefixes_Borrow (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 (Permission (C) = Borrowed);
 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 := Borrowed;
-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,
+Permission          => Borrowed,
 Children_Permission => Children_Permission (C)));
 --  We change the current node from Entire_Object to
---  Reference with No_Access and the previous son.
+--  Reference with Borrowed 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,
+Permission   => Borrowed,
 Get_All      => Son);
 return Get_All (C);
 end;
 else
 raise Program_Error;
 end if;
 end;
 return null;
 when others =>
 raise Program_Error;
 end case;
-end Set_Perm_Prefixes_Borrow_Out;
+end Set_Perm_Prefixes_Borrow;
-----------------------------
--- 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
 --  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);
+Setup_Parameter_Or_Global (E, Kind, Global_Var => True);
 end if;
 Next_Global (Item);
 end loop;
 end Setup_Globals_From_List;
 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
 Kind : Formal_Kind;
 begin
 case Global_Mode is
-when Name_Input | Name_Proof_In =>
+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_Parameter_Or_Global --
 -------------------------------
 procedure Setup_Parameter_Or_Global
-(Id   : Entity_Id;
+(Id         : Entity_Id;
-Mode : Formal_Kind)
+Mode       : Formal_Kind;
+Global_Var : Boolean)
 is
-Elem : Perm_Tree_Access;
+Elem     : Perm_Tree_Access;
+View_Typ : Entity_Id;
 begin
+if Present (Full_View (Etype (Id))) then
+View_Typ := Full_View (Etype (Id));
+else
+View_Typ := Etype (Id);
+end if;
 Elem := new Perm_Tree_Wrapper'
 (Tree =>
 (Kind                => Entire_Object,
 Is_Node_Deep        => Is_Deep (Etype (Id)),
-Permission          => Read_Write,
+Permission          => Unrestricted,
-Children_Permission => Read_Write));
+Children_Permission => Unrestricted));
 case Mode is
+--  All out and in out parameters are considered to be unrestricted.
+--  They are whether borrowed or moved. Ada Rules would restrict
+--  these permissions further. For example an in parameter cannot
+--  be written.
+--  In the following we deal with in parameters that can be observed.
+--  We only consider the observing cases.
 when E_In_Parameter =>
---  Borrowed IN: RW for everybody
+--  Handling global variables as IN parameters here.
+--  Remove the following condition once it's decided how globals
-if Is_Borrowed_In (Id) then
+--  should be considered. ???
-Elem.all.Tree.Permission := Read_Write;
+--
-Elem.all.Tree.Children_Permission := Read_Write;
+--  In SPARK, IN access-to-variable is an observe operation for
+--  a function, and a borrow operation for a procedure.
---  Observed IN: R for everybody
+if not Global_Var then
+if (Is_Access_Type (View_Typ)
+and then Is_Access_Constant (View_Typ)
+and then Is_Anonymous_Access_Type (View_Typ))
+or else
+(Is_Access_Type (View_Typ)
+and then Ekind (Scope (Id)) = E_Function)
+or else
+(not Is_Access_Type (View_Typ)
+and then Is_Deep (View_Typ)
+and then not Is_Anonymous_Access_Type (View_Typ))
+then
+Elem.all.Tree.Permission := Observed;
+Elem.all.Tree.Children_Permission := Observed;
+else
+Elem.all.Tree.Permission := Unrestricted;
+Elem.all.Tree.Children_Permission := Unrestricted;
+end if;
 else
-Elem.all.Tree.Permission := Read_Only;
+Elem.all.Tree.Permission := Observed;
-Elem.all.Tree.Children_Permission := Read_Only;
+Elem.all.Tree.Children_Permission := Observed;
 end if;
---  OUT: borrow, but callee has W only
+--  When out or in/out formal or global parameters, we set them to
+--  the Unrestricted state. "We want to be able to assume that all
-when E_Out_Parameter =>
+--  relevant writable globals are unrestricted when a subprogram
-Elem.all.Tree.Permission := Write_Only;
+--  starts executing". Formal parameters of mode out or in/out
-Elem.all.Tree.Children_Permission := Write_Only;
+--  are whether Borrowers or the targets of a move operation:
+--  they start theirs lives in the subprogram as Unrestricted.
---  IN OUT: borrow and callee has RW
+when others =>
-when E_In_Out_Parameter =>
+Elem.all.Tree.Permission := Unrestricted;
-Elem.all.Tree.Permission := Read_Write;
+Elem.all.Tree.Children_Permission := Unrestricted;
-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
+procedure Setup_Parameters (Subp : Entity_Id) is Formal : Entity_Id;
-Formal : Entity_Id;
 begin
 Formal := First_Formal (Subp);
 while Present (Formal) loop
-Setup_Parameter_Or_Global (Formal, Ekind (Formal));
+Setup_Parameter_Or_Global
+(Formal, Ekind (Formal), Global_Var => False);
 Next_Formal (Formal);
 end loop;
 end Setup_Parameters;
+-------------------------------
+-- Has_Ownership_Aspect_True --
+-------------------------------
+function Has_Ownership_Aspect_True
+(N   : Entity_Id;
+Msg : String)
+return Boolean
+is
+begin
+case Ekind (Etype (N)) is
+when Access_Kind =>
+if Ekind (Etype (N)) = E_General_Access_Type then
+Error_Msg_NE (Msg & " & not allowed " &
+"(Named General Access type)", N, N);
+return False;
+else
+return True;
+end if;
+when E_Array_Type
+| E_Array_Subtype
+=>
+declare
+Com_Ty : constant Node_Id := Component_Type (Etype (N));
+Ret    : Boolean :=  Has_Ownership_Aspect_True (Com_Ty, "");
+begin
+if Nkind (Parent (N)) = N_Full_Type_Declaration and
+Is_Anonymous_Access_Type (Com_Ty)
+then
+Ret := False;
+end if;
+if not Ret then
+Error_Msg_NE (Msg & " & not allowed "
+& "(Components of Named General Access type or"
+& " Anonymous type)", N, N);
+end if;
+return Ret;
+end;
+--  ??? What about hidden components
+when E_Record_Type
+| E_Record_Subtype
+=>
+declare
+Elmt        : Entity_Id;
+Elmt_T_Perm : Boolean := True;
+Elmt_Perm, Elmt_Anonym : Boolean;
+begin
+Elmt := First_Component_Or_Discriminant (Etype (N));
+while Present (Elmt) loop
+Elmt_Perm := Has_Ownership_Aspect_True (Elmt,
+"type of component");
+Elmt_Anonym := Is_Anonymous_Access_Type (Etype (Elmt));
+if Elmt_Anonym then
+Error_Msg_NE
+("type of component & not allowed"
+& " (Components of Anonymous type)", Elmt, Elmt);
+end if;
+Elmt_T_Perm := Elmt_T_Perm and Elmt_Perm and not Elmt_Anonym;
+Next_Component_Or_Discriminant (Elmt);
+end loop;
+if not Elmt_T_Perm then
+Error_Msg_NE
+(Msg & " & not allowed (One or "
+& "more components have Ownership Aspect False)",
+N, N);
+end if;
+return Elmt_T_Perm;
+end;
+when others =>
+return True;
+end case;
+end Has_Ownership_Aspect_True;
 end Sem_SPARK;

Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/sem_spark.adb @ 131:84e7813d76e9