1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT COMPILER COMPONENTS                         --
4--                                                                          --
5--                            S E M _ S P A R K                             --
6--                                                                          --
7--                                 B o d y                                  --
8--                                                                          --
9--          Copyright (C) 2017-2018, Free Software Foundation, Inc.         --
10--                                                                          --
11-- GNAT is free software;  you can  redistribute it  and/or modify it under --
12-- terms of the  GNU General Public License as published  by the Free Soft- --
13-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
14-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
15-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
16-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
17-- for  more details.  You should have  received  a copy of the GNU General --
18-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
19-- http://www.gnu.org/licenses for a complete copy of the license.          --
20--                                                                          --
21-- GNAT was originally developed  by the GNAT team at  New York University. --
22-- Extensive contributions were provided by Ada Core Technologies Inc.      --
23--                                                                          --
24------------------------------------------------------------------------------
25
26with Atree;    use Atree;
27with Einfo;    use Einfo;
28with Errout;   use Errout;
29with Namet;    use Namet;
30with Nlists;   use Nlists;
31with Opt;      use Opt;
32with Osint;    use Osint;
33with Sem_Prag; use Sem_Prag;
34with Sem_Util; use Sem_Util;
35with Sem_Aux;  use Sem_Aux;
36with Sinfo;    use Sinfo;
37with Snames;   use Snames;
38with Treepr;   use Treepr;
39
40with Ada.Unchecked_Deallocation;
41with GNAT.Dynamic_HTables; use GNAT.Dynamic_HTables;
42
43package body Sem_SPARK is
44
45   -------------------------------------------------
46   -- Handling of Permissions Associated to Paths --
47   -------------------------------------------------
48
49   package Permissions is
50      Elaboration_Context_Max : constant := 1009;
51      --  The hash range
52
53      type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
54
55      function Elaboration_Context_Hash
56        (Key : Entity_Id) return Elaboration_Context_Index;
57      --  Function to hash any node of the AST
58
59      type Perm_Kind is (No_Access, Read_Only, Read_Write, Write_Only);
60      --  Permission type associated with paths
61
62      subtype Read_Perm is Perm_Kind range Read_Only .. Read_Write;
63      subtype Write_Perm is Perm_Kind range Read_Write .. Write_Only;
64
65      type Perm_Tree_Wrapper;
66
67      type Perm_Tree_Access is access Perm_Tree_Wrapper;
68      --  A tree of permissions is defined, where the root is a whole object
69      --  and tree branches follow access paths in memory. As Perm_Tree is a
70      --  discriminated record, a wrapper type is used for the access type
71      --  designating a subtree, to make it unconstrained so that it can be
72      --  updated.
73
74      --  Nodes in the permission tree are of different kinds
75
76      type Path_Kind is
77        (Entire_Object,    --  Scalar object, or folded object of any type
78         Reference,        --  Unfolded object of access type
79         Array_Component,  --  Unfolded object of array type
80         Record_Component  --  Unfolded object of record type
81        );
82
83      package Perm_Tree_Maps is new Simple_HTable
84        (Header_Num => Elaboration_Context_Index,
85         Key        => Node_Id,
86         Element    => Perm_Tree_Access,
87         No_Element => null,
88         Hash       => Elaboration_Context_Hash,
89         Equal      => "=");
90      --  The instantation of a hash table, with keys being nodes and values
91      --  being pointers to trees. This is used to reference easily all
92      --  extensions of a Record_Component node (that can have name x, y, ...).
93
94      --  The definition of permission trees. This is a tree, which has a
95      --  permission at each node, and depending on the type of the node,
96      --  can have zero, one, or more children pointed to by an access to tree.
97      type Perm_Tree (Kind : Path_Kind := Entire_Object) is record
98         Permission : Perm_Kind;
99         --  Permission at this level in the path
100
101         Is_Node_Deep : Boolean;
102         --  Whether this node is of a deep type, to be used when moving the
103         --  path.
104
105         case Kind is
106
107            --  An entire object is either a leaf (an object which cannot be
108            --  extended further in a path) or a subtree in folded form (which
109            --  could later be unfolded further in another kind of node). The
110            --  field Children_Permission specifies a permission for every
111            --  extension of that node if that permission is different from
112            --  the node's permission.
113
114            when Entire_Object    =>
115               Children_Permission : Perm_Kind;
116
117            --  Unfolded path of access type. The permission of the object
118            --  pointed to is given in Get_All.
119
120            when Reference        =>
121               Get_All : Perm_Tree_Access;
122
123            --  Unfolded path of array type. The permission of the elements is
124            --  given in Get_Elem.
125
126            when Array_Component  =>
127               Get_Elem : Perm_Tree_Access;
128
129            --  Unfolded path of record type. The permission of the regular
130            --  components is given in Component. The permission of unknown
131            --  components (for objects of tagged type) is given in
132            --  Other_Components.
133
134            when Record_Component =>
135               Component : Perm_Tree_Maps.Instance;
136               Other_Components : Perm_Tree_Access;
137         end case;
138      end record;
139
140      type Perm_Tree_Wrapper is record
141         Tree : Perm_Tree;
142      end record;
143      --  We use this wrapper in order to have unconstrained discriminants
144
145      type Perm_Env is new Perm_Tree_Maps.Instance;
146      --  The definition of a permission environment for the analysis. This
147      --  is just a hash table of permission trees, each of them rooted with
148      --  an Identifier/Expanded_Name.
149
150      type Perm_Env_Access is access Perm_Env;
151      --  Access to permission environments
152
153      package Env_Maps is new Simple_HTable
154        (Header_Num => Elaboration_Context_Index,
155         Key        => Entity_Id,
156         Element    => Perm_Env_Access,
157         No_Element => null,
158         Hash       => Elaboration_Context_Hash,
159         Equal      => "=");
160      --  The instantiation of a hash table whose elements are permission
161      --  environments. This hash table is used to save the environments at
162      --  the entry of each loop, with the key being the loop label.
163
164      type Env_Backups is new Env_Maps.Instance;
165      --  The type defining the hash table saving the environments at the entry
166      --  of each loop.
167
168      package Boolean_Variables_Maps is new Simple_HTable
169        (Header_Num => Elaboration_Context_Index,
170         Key        => Entity_Id,
171         Element    => Boolean,
172         No_Element => False,
173         Hash       => Elaboration_Context_Hash,
174         Equal      => "=");
175      --  These maps allow tracking the variables that have been declared but
176      --  never used anywhere in the source code. Especially, we do not raise
177      --  an error if the variable stays write-only and is declared at package
178      --  level, because there is no risk that the variable has been moved,
179      --  because it has never been used.
180
181      type Initialization_Map is new Boolean_Variables_Maps.Instance;
182
183      --------------------
184      -- Simple Getters --
185      --------------------
186
187      --  Simple getters to avoid having .all.Tree.Field everywhere. Of course,
188      --  that's only for the top access, as otherwise this reverses the order
189      --  in accesses visually.
190
191      function Children_Permission (T : Perm_Tree_Access) return Perm_Kind;
192      function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance;
193      function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access;
194      function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access;
195      function Is_Node_Deep (T : Perm_Tree_Access) return Boolean;
196      function Kind (T : Perm_Tree_Access) return Path_Kind;
197      function Other_Components (T : Perm_Tree_Access) return Perm_Tree_Access;
198      function Permission (T : Perm_Tree_Access) return Perm_Kind;
199
200      -----------------------
201      -- Memory Management --
202      -----------------------
203
204      procedure Copy_Env
205        (From : Perm_Env;
206         To : in out Perm_Env);
207      --  Procedure to copy a permission environment
208
209      procedure Copy_Init_Map
210        (From : Initialization_Map;
211         To : in out Initialization_Map);
212      --  Procedure to copy an initialization map
213
214      procedure Copy_Tree
215        (From : Perm_Tree_Access;
216         To : Perm_Tree_Access);
217      --  Procedure to copy a permission tree
218
219      procedure Free_Env
220        (PE : in out Perm_Env);
221      --  Procedure to free a permission environment
222
223      procedure Free_Perm_Tree
224        (PT : in out Perm_Tree_Access);
225      --  Procedure to free a permission tree
226
227      --------------------
228      -- Error Messages --
229      --------------------
230
231      procedure Perm_Mismatch
232        (Exp_Perm, Act_Perm : Perm_Kind;
233         N                   : Node_Id);
234      --  Issues a continuation error message about a mismatch between a
235      --  desired permission Exp_Perm and a permission obtained Act_Perm. N
236      --  is the node on which the error is reported.
237
238   end Permissions;
239
240   package body Permissions is
241
242      -------------------------
243      -- Children_Permission --
244      -------------------------
245
246      function Children_Permission
247        (T : Perm_Tree_Access)
248          return Perm_Kind
249      is
250      begin
251         return T.all.Tree.Children_Permission;
252      end Children_Permission;
253
254      ---------------
255      -- Component --
256      ---------------
257
258      function Component
259        (T : Perm_Tree_Access)
260          return Perm_Tree_Maps.Instance
261      is
262      begin
263         return T.all.Tree.Component;
264      end Component;
265
266      --------------
267      -- Copy_Env --
268      --------------
269
270      procedure Copy_Env
271        (From : Perm_Env;
272         To : in out Perm_Env)
273      is
274         Comp_From : Perm_Tree_Access;
275         Key_From : Perm_Tree_Maps.Key_Option;
276         Son : Perm_Tree_Access;
277
278      begin
279         Reset (To);
280         Key_From := Get_First_Key (From);
281         while Key_From.Present loop
282            Comp_From := Get (From, Key_From.K);
283            pragma Assert (Comp_From /= null);
284
285            Son := new Perm_Tree_Wrapper;
286            Copy_Tree (Comp_From, Son);
287
288            Set (To, Key_From.K, Son);
289            Key_From := Get_Next_Key (From);
290         end loop;
291      end Copy_Env;
292
293      -------------------
294      -- Copy_Init_Map --
295      -------------------
296
297      procedure Copy_Init_Map
298        (From : Initialization_Map;
299         To : in out Initialization_Map)
300      is
301         Comp_From : Boolean;
302         Key_From : Boolean_Variables_Maps.Key_Option;
303
304      begin
305         Reset (To);
306         Key_From := Get_First_Key (From);
307         while Key_From.Present loop
308            Comp_From := Get (From, Key_From.K);
309            Set (To, Key_From.K, Comp_From);
310            Key_From := Get_Next_Key (From);
311         end loop;
312      end Copy_Init_Map;
313
314      ---------------
315      -- Copy_Tree --
316      ---------------
317
318      procedure Copy_Tree
319        (From : Perm_Tree_Access;
320         To : Perm_Tree_Access)
321      is
322      begin
323         To.all := From.all;
324
325         case Kind (From) is
326            when Entire_Object =>
327               null;
328
329            when Reference =>
330               To.all.Tree.Get_All := new Perm_Tree_Wrapper;
331
332               Copy_Tree (Get_All (From), Get_All (To));
333
334            when Array_Component =>
335               To.all.Tree.Get_Elem := new Perm_Tree_Wrapper;
336
337               Copy_Tree (Get_Elem (From), Get_Elem (To));
338
339            when Record_Component =>
340               declare
341                  Comp_From : Perm_Tree_Access;
342                  Key_From : Perm_Tree_Maps.Key_Option;
343                  Son : Perm_Tree_Access;
344                  Hash_Table : Perm_Tree_Maps.Instance;
345               begin
346               --  We put a new hash table, so that it gets dealiased from the
347               --  Component (From) hash table.
348                  To.all.Tree.Component := Hash_Table;
349
350                  To.all.Tree.Other_Components :=
351                    new Perm_Tree_Wrapper'(Other_Components (From).all);
352
353                  Copy_Tree (Other_Components (From), Other_Components (To));
354
355                  Key_From := Perm_Tree_Maps.Get_First_Key
356                    (Component (From));
357                  while Key_From.Present loop
358                     Comp_From := Perm_Tree_Maps.Get
359                       (Component (From), Key_From.K);
360
361                     pragma Assert (Comp_From /= null);
362                     Son := new Perm_Tree_Wrapper;
363
364                     Copy_Tree (Comp_From, Son);
365
366                     Perm_Tree_Maps.Set
367                       (To.all.Tree.Component, Key_From.K, Son);
368
369                     Key_From := Perm_Tree_Maps.Get_Next_Key
370                       (Component (From));
371                  end loop;
372               end;
373         end case;
374      end Copy_Tree;
375
376      ------------------------------
377      -- Elaboration_Context_Hash --
378      ------------------------------
379
380      function Elaboration_Context_Hash
381        (Key : Entity_Id) return Elaboration_Context_Index
382      is
383      begin
384         return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
385      end Elaboration_Context_Hash;
386
387      --------------
388      -- Free_Env --
389      --------------
390
391      procedure Free_Env (PE : in out Perm_Env) is
392         CompO : Perm_Tree_Access;
393      begin
394         CompO := Get_First (PE);
395         while CompO /= null loop
396            Free_Perm_Tree (CompO);
397            CompO := Get_Next (PE);
398         end loop;
399      end Free_Env;
400
401      --------------------
402      -- Free_Perm_Tree --
403      --------------------
404
405      procedure Free_Perm_Tree
406        (PT : in out Perm_Tree_Access)
407      is
408         procedure Free_Perm_Tree_Dealloc is
409           new Ada.Unchecked_Deallocation
410             (Perm_Tree_Wrapper, Perm_Tree_Access);
411         --  The deallocator for permission_trees
412
413      begin
414         case Kind (PT) is
415            when Entire_Object =>
416               Free_Perm_Tree_Dealloc (PT);
417
418            when Reference =>
419               Free_Perm_Tree (PT.all.Tree.Get_All);
420               Free_Perm_Tree_Dealloc (PT);
421
422            when Array_Component =>
423               Free_Perm_Tree (PT.all.Tree.Get_Elem);
424
425            when Record_Component =>
426               declare
427                  Comp : Perm_Tree_Access;
428
429               begin
430                  Free_Perm_Tree (PT.all.Tree.Other_Components);
431                  Comp := Perm_Tree_Maps.Get_First (Component (PT));
432                  while Comp /= null loop
433                     --  Free every Component subtree
434
435                     Free_Perm_Tree (Comp);
436                     Comp := Perm_Tree_Maps.Get_Next (Component (PT));
437                  end loop;
438               end;
439               Free_Perm_Tree_Dealloc (PT);
440         end case;
441      end Free_Perm_Tree;
442
443      -------------
444      -- Get_All --
445      -------------
446
447      function Get_All
448        (T : Perm_Tree_Access)
449          return Perm_Tree_Access
450      is
451      begin
452         return T.all.Tree.Get_All;
453      end Get_All;
454
455      --------------
456      -- Get_Elem --
457      --------------
458
459      function Get_Elem
460        (T : Perm_Tree_Access)
461          return Perm_Tree_Access
462      is
463      begin
464         return T.all.Tree.Get_Elem;
465      end Get_Elem;
466
467      ------------------
468      -- Is_Node_Deep --
469      ------------------
470
471      function Is_Node_Deep
472        (T : Perm_Tree_Access)
473          return Boolean
474      is
475      begin
476         return T.all.Tree.Is_Node_Deep;
477      end Is_Node_Deep;
478
479      ----------
480      -- Kind --
481      ----------
482
483      function Kind
484        (T : Perm_Tree_Access)
485          return Path_Kind
486      is
487      begin
488         return T.all.Tree.Kind;
489      end Kind;
490
491      ----------------------
492      -- Other_Components --
493      ----------------------
494
495      function Other_Components
496        (T : Perm_Tree_Access)
497          return Perm_Tree_Access
498      is
499      begin
500         return T.all.Tree.Other_Components;
501      end Other_Components;
502
503      ----------------
504      -- Permission --
505      ----------------
506
507      function Permission
508        (T : Perm_Tree_Access)
509          return Perm_Kind
510      is
511      begin
512         return T.all.Tree.Permission;
513      end Permission;
514
515      -------------------
516      -- Perm_Mismatch --
517      -------------------
518
519      procedure Perm_Mismatch
520        (Exp_Perm, Act_Perm : Perm_Kind;
521         N                   : Node_Id)
522      is
523      begin
524         Error_Msg_N ("\expected at least `"
525                      & Perm_Kind'Image (Exp_Perm) & "`, got `"
526                      & Perm_Kind'Image (Act_Perm) & "`", N);
527      end Perm_Mismatch;
528
529   end Permissions;
530
531   use Permissions;
532
533   --------------------------------------
534   -- Analysis modes for AST traversal --
535   --------------------------------------
536
537   --  The different modes for analysis. This allows to checking whether a path
538   --  found in the code should be moved, borrowed, or observed.
539
540   type Checking_Mode is
541
542     (Read,
543      --  Default mode. Checks that paths have Read_Perm permission.
544
545      Move,
546      --  Regular moving semantics (not under 'Access). Checks that paths have
547      --  Read_Write permission. After moving a path, its permission is set to
548      --  Write_Only and the permission of its extensions is set to No_Access.
549
550      Assign,
551      --  Used for the target of an assignment, or an actual parameter with
552      --  mode OUT. Checks that paths have Write_Perm permission. After
553      --  assigning to a path, its permission is set to Read_Write.
554
555      Super_Move,
556      --  Enhanced moving semantics (under 'Access). Checks that paths have
557      --  Read_Write permission. After moving a path, its permission is set
558      --  to No_Access, as well as the permission of its extensions and the
559      --  permission of its prefixes up to the first Reference node.
560
561      Borrow_Out,
562      --  Used for actual OUT parameters. Checks that paths have Write_Perm
563      --  permission. After checking a path, its permission is set to Read_Only
564      --  when of a by-copy type, to No_Access otherwise. After the call, its
565      --  permission is set to Read_Write.
566
567      Observe
568      --  Used for actual IN parameters of a scalar type. Checks that paths
569      --  have Read_Perm permission. After checking a path, its permission
570      --  is set to Read_Only.
571      --
572      --  Also used for formal IN parameters
573     );
574
575   type Result_Kind is (Folded, Unfolded, Function_Call);
576   --  The type declaration to discriminate in the Perm_Or_Tree type
577
578   --  The result type of the function Get_Perm_Or_Tree. This returns either a
579   --  tree when it found the appropriate tree, or a permission when the search
580   --  finds a leaf and the subtree we are looking for is folded. In the last
581   --  case, we return instead the Children_Permission field of the leaf.
582
583   type Perm_Or_Tree (R : Result_Kind) is record
584      case R is
585         when Folded        => Found_Permission : Perm_Kind;
586         when Unfolded      => Tree_Access : Perm_Tree_Access;
587         when Function_Call => null;
588      end case;
589   end record;
590
591   -----------------------
592   -- Local subprograms --
593   -----------------------
594
595   function "<=" (P1, P2 : Perm_Kind) return Boolean;
596   function ">=" (P1, P2 : Perm_Kind) return Boolean;
597   function Glb  (P1, P2 : Perm_Kind) return Perm_Kind;
598   function Lub  (P1, P2 : Perm_Kind) return Perm_Kind;
599
600   --  Checking proceduress for safe pointer usage. These procedures traverse
601   --  the AST, check nodes for correct permissions according to SPARK RM
602   --  6.4.2, and update permissions depending on the node kind.
603
604   procedure Check_Call_Statement (Call : Node_Id);
605
606   procedure Check_Callable_Body (Body_N : Node_Id);
607   --  We are not in End_Of_Callee mode, hence we will save the environment
608   --  and start from a new one. We will add in the environment all formal
609   --  parameters as well as global used during the subprogram, with the
610   --  appropriate permissions (write-only for out, read-only for observed,
611   --  read-write for others).
612   --
613   --  After that we analyze the body of the function, and finaly, we check
614   --  that each borrowed parameter and global has read-write permission. We
615   --  then clean up the environment and put back the saved environment.
616
617   procedure Check_Declaration (Decl : Node_Id);
618
619   procedure Check_Expression (Expr : Node_Id);
620
621   procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode);
622   --  This procedure takes a global pragma and checks depending on mode:
623   --  Mode Read: every in global is readable
624   --  Mode Observe: same as Check_Param_Observes but on globals
625   --  Mode Borrow_Out: Check_Param_Outs for globals
626   --  Mode Move: Check_Param for globals with mode Read
627   --  Mode Assign: Check_Param for globals with mode Assign
628
629   procedure Check_List (L : List_Id);
630   --  Calls Check_Node on each element of the list
631
632   procedure Check_Loop_Statement (Loop_N : Node_Id);
633
634   procedure Check_Node (N : Node_Id);
635   --  Main traversal procedure to check safe pointer usage. This procedure is
636   --  mutually recursive with the specialized procedures that follow.
637
638   procedure Check_Package_Body (Pack : Node_Id);
639
640   procedure Check_Param (Formal : Entity_Id; Actual : Node_Id);
641   --  This procedure takes a formal and an actual parameter and calls the
642   --  analyze node if the parameter is borrowed with mode in out, with the
643   --  appropriate Checking_Mode (Move).
644
645   procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id);
646   --  This procedure takes a formal and an actual parameter and calls
647   --  the analyze node if the parameter is observed, with the appropriate
648   --  Checking_Mode.
649
650   procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id);
651   --  This procedure takes a formal and an actual parameter and calls the
652   --  analyze node if the parameter is of mode out, with the appropriate
653   --  Checking_Mode.
654
655   procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id);
656   --  This procedure takes a formal and an actual parameter and checks the
657   --  readability of every in-mode parameter. This includes observed in, and
658   --  also borrowed in, that are then checked afterwards.
659
660   procedure Check_Statement (Stmt : Node_Id);
661
662   function Get_Perm (N : Node_Id) return Perm_Kind;
663   --  The function that takes a name as input and returns a permission
664   --  associated to it.
665
666   function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
667   --  This function gets a Node_Id and looks recursively to find the
668   --  appropriate subtree for that Node_Id. If the tree is folded on
669   --  that node, then it returns the permission given at the right level.
670
671   function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
672   --  This function gets a Node_Id and looks recursively to find the
673   --  appropriate subtree for that Node_Id. If the tree is folded, then
674   --  it unrolls the tree up to the appropriate level.
675
676   function Has_Alias
677     (N : Node_Id)
678       return Boolean;
679   --  Function that returns whether the path given as parameter contains an
680   --  extension that is declared as aliased.
681
682   function Has_Array_Component (N : Node_Id) return Boolean;
683   --  This function gets a Node_Id and looks recursively to find if the given
684   --  path has any array component.
685
686   function Has_Function_Component (N : Node_Id) return Boolean;
687   --  This function gets a Node_Id and looks recursively to find if the given
688   --  path has any function component.
689
690   procedure Hp (P : Perm_Env);
691   --  A procedure that outputs the hash table. This function is used only in
692   --  the debugger to look into a hash table.
693   pragma Unreferenced (Hp);
694
695   procedure Illegal_Global_Usage (N : Node_Or_Entity_Id);
696   pragma No_Return (Illegal_Global_Usage);
697   --  A procedure that is called when deep globals or aliased globals are used
698   --  without any global aspect.
699
700   function Is_Borrowed_In (E : Entity_Id) return Boolean;
701   --  Function that tells if the given entity is a borrowed in a formal
702   --  parameter, that is, if it is an access-to-variable type.
703
704   function Is_Deep (E : Entity_Id) return Boolean;
705   --  A function that can tell if a type is deep or not. Returns true if the
706   --  type passed as argument is deep.
707
708   function Is_Shallow (E : Entity_Id) return Boolean;
709   --  A function that can tell if a type is shallow or not. Returns true if
710   --  the type passed as argument is shallow.
711
712   function Loop_Of_Exit (N : Node_Id) return Entity_Id;
713   --  A function that takes an exit statement node and returns the entity of
714   --  the loop that this statement is exiting from.
715
716   procedure Merge_Envs (Target : in out Perm_Env; Source : in out Perm_Env);
717   --  Merge Target and Source into Target, and then deallocate the Source
718
719   procedure Perm_Error
720     (N : Node_Id;
721      Perm : Perm_Kind;
722      Found_Perm : Perm_Kind);
723   --  A procedure that is called when the permissions found contradict the
724   --  rules established by the RM. This function is called with the node, its
725   --  entity and the permission that was expected, and adds an error message
726   --  with the appropriate values.
727
728   procedure Perm_Error_Subprogram_End
729     (E          : Entity_Id;
730      Subp       : Entity_Id;
731      Perm       : Perm_Kind;
732      Found_Perm : Perm_Kind);
733   --  A procedure that is called when the permissions found contradict the
734   --  rules established by the RM at the end of subprograms. This function
735   --  is called with the node, its entity, the node of the returning function
736   --  and the permission that was expected, and adds an error message with the
737   --  appropriate values.
738
739   procedure Process_Path (N : Node_Id);
740
741   procedure Return_Declarations (L : List_Id);
742   --  Check correct permissions on every declared object at the end of a
743   --  callee. Used at the end of the body of a callable entity. Checks that
744   --  paths of all borrowed formal parameters and global have Read_Write
745   --  permission.
746
747   procedure Return_Globals (Subp : Entity_Id);
748   --  Takes a subprogram as input, and checks that all borrowed global items
749   --  of the subprogram indeed have RW permission at the end of the subprogram
750   --  execution.
751
752   procedure Return_Parameter_Or_Global
753     (Id   : Entity_Id;
754      Mode : Formal_Kind;
755      Subp : Entity_Id);
756   --  Auxiliary procedure to Return_Parameters and Return_Globals
757
758   procedure Return_Parameters (Subp : Entity_Id);
759   --  Takes a subprogram as input, and checks that all borrowed parameters of
760   --  the subprogram indeed have RW permission at the end of the subprogram
761   --  execution.
762
763   procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind);
764   --  This procedure takes an access to a permission tree and modifies the
765   --  tree so that any strict extensions of the given tree become of the
766   --  access specified by parameter P.
767
768   procedure Set_Perm_Extensions_Move (T : Perm_Tree_Access; E : Entity_Id);
769   --  Set permissions to
770   --    No for any extension with more .all
771   --    W for any deep extension with same number of .all
772   --    RW for any shallow extension with same number of .all
773
774   function Set_Perm_Prefixes_Assign (N : Node_Id) return Perm_Tree_Access;
775   --  This function takes a name as an input and sets in the permission
776   --  tree the given permission to the given name. The general rule here is
777   --  that everybody updates the permission of the subtree it is returning.
778   --  The permission of the assigned path has been set to RW by the caller.
779   --
780   --  Case where we have to normalize a tree after the correct permissions
781   --  have been assigned already. We look for the right subtree at the given
782   --  path, actualize its permissions, and then call the normalization on its
783   --  parent.
784   --
785   --  Example: We assign x.y and x.z then during Set_Perm_Prefixes_Move will
786   --  change the permission of x to RW because all of its components have
787   --  permission have permission RW.
788
789   function Set_Perm_Prefixes_Borrow_Out (N : Node_Id) return Perm_Tree_Access;
790   --  This function modifies the permissions of a given node_id in the
791   --  permission environment as well as in all the prefixes of the path,
792   --  given that the path is borrowed with mode out.
793
794   function Set_Perm_Prefixes_Move
795     (N : Node_Id; Mode : Checking_Mode)
796      return Perm_Tree_Access;
797   pragma Precondition (Mode = Move or Mode = Super_Move);
798   --  Given a node and a mode (that can be either Move or Super_Move), this
799   --  function modifies the permissions of a given node_id in the permission
800   --  environment as well as all the prefixes of the path, given that the path
801   --  is moved with or without 'Access. The general rule here is everybody
802   --  updates the permission of the subtree they are returning.
803   --
804   --  This case describes a move either under 'Access or without 'Access.
805
806   function Set_Perm_Prefixes_Observe (N : Node_Id) return Perm_Tree_Access;
807   --  This function modifies the permissions of a given node_id in the
808   --  permission environment as well as all the prefixes of the path,
809   --  given that the path is observed.
810
811   procedure Setup_Globals (Subp : Entity_Id);
812   --  Takes a subprogram as input, and sets up the environment by adding
813   --  global items with appropriate permissions.
814
815   procedure Setup_Parameter_Or_Global
816     (Id   : Entity_Id;
817      Mode : Formal_Kind);
818   --  Auxiliary procedure to Setup_Parameters and Setup_Globals
819
820   procedure Setup_Parameters (Subp : Entity_Id);
821   --  Takes a subprogram as input, and sets up the environment by adding
822   --  formal parameters with appropriate permissions.
823
824   ----------------------
825   -- Global Variables --
826   ----------------------
827
828   Current_Perm_Env : Perm_Env;
829   --  The permission environment that is used for the analysis. This
830   --  environment can be saved, modified, reinitialized, but should be the
831   --  only one valid from which to extract the permissions of the paths in
832   --  scope. The analysis ensures at each point that this variables contains
833   --  a valid permission environment with all bindings in scope.
834
835   Current_Checking_Mode : Checking_Mode := Read;
836   --  The current analysis mode. This global variable indicates at each point
837   --  of the analysis whether the node being analyzed is moved, borrowed,
838   --  assigned, read, ... The full list of possible values can be found in
839   --  the declaration of type Checking_Mode.
840
841   Current_Loops_Envs : Env_Backups;
842   --  This variable contains saves of permission environments at each loop the
843   --  analysis entered. Each saved environment can be reached with the label
844   --  of the loop.
845
846   Current_Loops_Accumulators : Env_Backups;
847   --  This variable contains the environments used as accumulators for loops,
848   --  that consist of the merge of all environments at each exit point of
849   --  the loop (which can also be the entry point of the loop in the case of
850   --  non-infinite loops), each of them reachable from the label of the loop.
851   --  We require that the environment stored in the accumulator be less
852   --  restrictive than the saved environment at the beginning of the loop, and
853   --  the permission environment after the loop is equal to the accumulator.
854
855   Current_Initialization_Map : Initialization_Map;
856   --  This variable contains a map that binds each variable of the analyzed
857   --  source code to a boolean that becomes true whenever the variable is used
858   --  after declaration. Hence we can exclude from analysis variables that
859   --  are just declared and never accessed, typically at package declaration.
860
861   ----------
862   -- "<=" --
863   ----------
864
865   function "<=" (P1, P2 : Perm_Kind) return Boolean
866   is
867   begin
868      return P2 >= P1;
869   end "<=";
870
871   ----------
872   -- ">=" --
873   ----------
874
875   function ">=" (P1, P2 : Perm_Kind) return Boolean
876   is
877   begin
878      case P2 is
879         when No_Access  => return True;
880         when Read_Only  => return P1 in Read_Perm;
881         when Write_Only => return P1 in Write_Perm;
882         when Read_Write => return P1 = Read_Write;
883      end case;
884   end ">=";
885
886   --------------------------
887   -- Check_Call_Statement --
888   --------------------------
889
890   procedure Check_Call_Statement (Call : Node_Id) is
891      Saved_Env : Perm_Env;
892
893      procedure Iterate_Call is new
894        Iterate_Call_Parameters (Check_Param);
895      procedure Iterate_Call_Observes is new
896        Iterate_Call_Parameters (Check_Param_Observes);
897      procedure Iterate_Call_Outs is new
898        Iterate_Call_Parameters (Check_Param_Outs);
899      procedure Iterate_Call_Read is new
900        Iterate_Call_Parameters (Check_Param_Read);
901
902   begin
903      --  Save environment, so that the modifications done by analyzing the
904      --  parameters are not kept at the end of the call.
905      Copy_Env (Current_Perm_Env,
906                Saved_Env);
907
908      --  We first check the Read access on every in parameter
909
910      Current_Checking_Mode := Read;
911      Iterate_Call_Read (Call);
912      Check_Globals (Get_Pragma
913                       (Get_Called_Entity (Call), Pragma_Global), Read);
914
915      --  We first observe, then borrow with mode out, and then with other
916      --  modes. This ensures that we do not have to check for by-copy types
917      --  specially, because we read them before borrowing them.
918
919      Iterate_Call_Observes (Call);
920      Check_Globals (Get_Pragma
921                       (Get_Called_Entity (Call), Pragma_Global),
922                       Observe);
923
924      Iterate_Call_Outs (Call);
925      Check_Globals (Get_Pragma
926                       (Get_Called_Entity (Call), Pragma_Global),
927                       Borrow_Out);
928
929      Iterate_Call (Call);
930      Check_Globals (Get_Pragma
931                       (Get_Called_Entity (Call), Pragma_Global), Move);
932
933      --  Restore environment, because after borrowing/observing actual
934      --  parameters, they get their permission reverted to the ones before
935      --  the call.
936
937      Free_Env (Current_Perm_Env);
938
939      Copy_Env (Saved_Env,
940                Current_Perm_Env);
941
942      Free_Env (Saved_Env);
943
944      --  We assign the out parameters (necessarily borrowed per RM)
945      Current_Checking_Mode := Assign;
946      Iterate_Call (Call);
947      Check_Globals (Get_Pragma
948                       (Get_Called_Entity (Call), Pragma_Global),
949                       Assign);
950
951   end Check_Call_Statement;
952
953   -------------------------
954   -- Check_Callable_Body --
955   -------------------------
956
957   procedure Check_Callable_Body (Body_N : Node_Id) is
958
959      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
960
961      Saved_Env : Perm_Env;
962      Saved_Init_Map : Initialization_Map;
963
964      New_Env : Perm_Env;
965
966      Body_Id : constant Entity_Id := Defining_Entity (Body_N);
967      Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
968
969   begin
970      --  Check if SPARK pragma is not set to Off
971
972      if Present (SPARK_Pragma (Defining_Entity (Body_N))) then
973         if Get_SPARK_Mode_From_Annotation
974           (SPARK_Pragma (Defining_Entity (Body_N, False))) /= Opt.On
975         then
976            return;
977         end if;
978      else
979         return;
980      end if;
981
982      --  Save environment and put a new one in place
983
984      Copy_Env (Current_Perm_Env, Saved_Env);
985
986      --  Save initialization map
987
988      Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map);
989
990      Current_Checking_Mode := Read;
991      Current_Perm_Env := New_Env;
992
993      --  Add formals and globals to the environment with adequate permissions
994
995      if Is_Subprogram_Or_Entry (Spec_Id) then
996         Setup_Parameters (Spec_Id);
997         Setup_Globals (Spec_Id);
998      end if;
999
1000      --  Analyze the body of the function
1001
1002      Check_List (Declarations (Body_N));
1003      Check_Node (Handled_Statement_Sequence (Body_N));
1004
1005      --  Check the read-write permissions of borrowed parameters/globals
1006
1007      if Ekind_In (Spec_Id, E_Procedure, E_Entry)
1008        and then not No_Return (Spec_Id)
1009      then
1010         Return_Parameters (Spec_Id);
1011         Return_Globals (Spec_Id);
1012      end if;
1013
1014      --  Free the environments
1015
1016      Free_Env (Current_Perm_Env);
1017
1018      Copy_Env (Saved_Env,
1019                Current_Perm_Env);
1020
1021      Free_Env (Saved_Env);
1022
1023      --  Restore initialization map
1024
1025      Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map);
1026
1027      Reset (Saved_Init_Map);
1028
1029      --  The assignment of all out parameters will be done by caller
1030
1031      Current_Checking_Mode := Mode_Before;
1032   end Check_Callable_Body;
1033
1034   -----------------------
1035   -- Check_Declaration --
1036   -----------------------
1037
1038   procedure Check_Declaration (Decl : Node_Id) is
1039   begin
1040      case N_Declaration'(Nkind (Decl)) is
1041         when N_Full_Type_Declaration =>
1042            --  Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE
1043            null;
1044
1045         when N_Object_Declaration =>
1046            --  First move the right-hand side
1047            Current_Checking_Mode := Move;
1048            Check_Node (Expression (Decl));
1049
1050            declare
1051               Elem : Perm_Tree_Access;
1052
1053            begin
1054               Elem := new Perm_Tree_Wrapper'
1055                 (Tree =>
1056                    (Kind                => Entire_Object,
1057                     Is_Node_Deep        =>
1058                       Is_Deep (Etype (Defining_Identifier (Decl))),
1059                     Permission          => Read_Write,
1060                     Children_Permission => Read_Write));
1061
1062               --  If unitialized declaration, then set to Write_Only. If a
1063               --  pointer declaration, it has a null default initialization.
1064               if Nkind (Expression (Decl)) = N_Empty
1065                 and then not Has_Full_Default_Initialization
1066                   (Etype (Defining_Identifier (Decl)))
1067                 and then not Is_Access_Type
1068                   (Etype (Defining_Identifier (Decl)))
1069               then
1070                  Elem.all.Tree.Permission := Write_Only;
1071                  Elem.all.Tree.Children_Permission := Write_Only;
1072               end if;
1073
1074               --  Create new tree for defining identifier
1075
1076               Set (Current_Perm_Env,
1077                    Unique_Entity (Defining_Identifier (Decl)),
1078                    Elem);
1079
1080               pragma Assert (Get_First (Current_Perm_Env)
1081                              /= null);
1082
1083            end;
1084
1085         when N_Subtype_Declaration =>
1086            Check_Node (Subtype_Indication (Decl));
1087
1088         when N_Iterator_Specification =>
1089            pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl))));
1090            null;
1091
1092         when N_Loop_Parameter_Specification =>
1093            pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl))));
1094            null;
1095
1096         --  Checking should not be called directly on these nodes
1097
1098         when N_Component_Declaration
1099            | N_Function_Specification
1100            | N_Entry_Declaration
1101            | N_Procedure_Specification
1102         =>
1103            raise Program_Error;
1104
1105         --  Ignored constructs for pointer checking
1106
1107         when N_Formal_Object_Declaration
1108            | N_Formal_Type_Declaration
1109            | N_Incomplete_Type_Declaration
1110            | N_Private_Extension_Declaration
1111            | N_Private_Type_Declaration
1112            | N_Protected_Type_Declaration
1113         =>
1114            null;
1115
1116         --  The following nodes are rewritten by semantic analysis
1117
1118         when N_Expression_Function =>
1119            raise Program_Error;
1120      end case;
1121   end Check_Declaration;
1122
1123   ----------------------
1124   -- Check_Expression --
1125   ----------------------
1126
1127   procedure Check_Expression (Expr : Node_Id) is
1128      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1129   begin
1130      case N_Subexpr'(Nkind (Expr)) is
1131         when N_Procedure_Call_Statement =>
1132            Check_Call_Statement (Expr);
1133
1134         when N_Identifier
1135            | N_Expanded_Name
1136         =>
1137            --  Check if identifier is pointing to nothing (On/Off/...)
1138            if not Present (Entity (Expr)) then
1139               return;
1140            end if;
1141
1142            --  Do not analyze things that are not of object Kind
1143            if Ekind (Entity (Expr)) not in Object_Kind then
1144               return;
1145            end if;
1146
1147            --  Consider as ident
1148            Process_Path (Expr);
1149
1150         --  Switch to read mode and then check the readability of each operand
1151
1152         when N_Binary_Op =>
1153
1154            Current_Checking_Mode := Read;
1155            Check_Node (Left_Opnd (Expr));
1156            Check_Node (Right_Opnd (Expr));
1157
1158         --  Switch to read mode and then check the readability of each operand
1159
1160         when N_Op_Abs
1161            | N_Op_Minus
1162            | N_Op_Not
1163            | N_Op_Plus
1164         =>
1165            pragma Assert (Is_Shallow (Etype (Expr)));
1166            Current_Checking_Mode := Read;
1167            Check_Node (Right_Opnd (Expr));
1168
1169         --  Forbid all deep expressions for Attribute ???
1170
1171         when N_Attribute_Reference =>
1172            case Attribute_Name (Expr) is
1173               when Name_Access =>
1174                  case Current_Checking_Mode is
1175                     when Read =>
1176                        Check_Node (Prefix (Expr));
1177
1178                     when Move =>
1179                        Current_Checking_Mode := Super_Move;
1180                        Check_Node (Prefix (Expr));
1181
1182                     --  Only assign names, not expressions
1183
1184                     when Assign =>
1185                        raise Program_Error;
1186
1187                     --  Prefix in Super_Move should be a name, error here
1188
1189                     when Super_Move =>
1190                        raise Program_Error;
1191
1192                     --  Could only borrow names of mode out, not n'Access
1193
1194                     when Borrow_Out =>
1195                        raise Program_Error;
1196
1197                     when Observe =>
1198                        Check_Node (Prefix (Expr));
1199                  end case;
1200
1201               when Name_Last
1202                  | Name_First
1203               =>
1204                  Current_Checking_Mode := Read;
1205                  Check_Node (Prefix (Expr));
1206
1207               when Name_Min =>
1208                  Current_Checking_Mode := Read;
1209                  Check_Node (Prefix (Expr));
1210
1211               when Name_Image =>
1212                  Check_Node (Prefix (Expr));
1213
1214               when Name_SPARK_Mode =>
1215                  null;
1216
1217               when Name_Value =>
1218                  Current_Checking_Mode := Read;
1219                  Check_Node (Prefix (Expr));
1220
1221               when Name_Update =>
1222                  Check_List (Expressions (Expr));
1223                  Check_Node (Prefix (Expr));
1224
1225               when Name_Pred
1226                   | Name_Succ
1227               =>
1228                  Check_List (Expressions (Expr));
1229                  Check_Node (Prefix (Expr));
1230
1231               when Name_Length =>
1232                  Current_Checking_Mode := Read;
1233                  Check_Node (Prefix (Expr));
1234
1235               --  Any Attribute referring to the underlying memory is ignored
1236               --  in the analysis. This means that taking the address of a
1237               --  variable makes a silent alias that is not rejected by the
1238               --  analysis.
1239
1240               when Name_Address
1241                   | Name_Alignment
1242                   | Name_Component_Size
1243                   | Name_First_Bit
1244                   | Name_Last_Bit
1245                   | Name_Size
1246                   | Name_Position
1247               =>
1248                  null;
1249
1250               --  Attributes referring to types (get values from types), hence
1251               --  no need to check either for borrows or any loans.
1252
1253               when Name_Base
1254                  | Name_Val
1255               =>
1256                  null;
1257
1258               --  Other attributes that fall out of the scope of the analysis
1259
1260               when others =>
1261                  null;
1262            end case;
1263
1264         when N_In =>
1265            Current_Checking_Mode := Read;
1266            Check_Node (Left_Opnd (Expr));
1267            Check_Node (Right_Opnd (Expr));
1268
1269         when N_Not_In =>
1270            Current_Checking_Mode := Read;
1271            Check_Node (Left_Opnd (Expr));
1272            Check_Node (Right_Opnd (Expr));
1273
1274         --  Switch to read mode and then check the readability of each operand
1275
1276         when N_And_Then
1277            | N_Or_Else
1278         =>
1279            pragma Assert (Is_Shallow (Etype (Expr)));
1280            Current_Checking_Mode := Read;
1281            Check_Node (Left_Opnd (Expr));
1282            Check_Node (Right_Opnd (Expr));
1283
1284         --  Check the arguments of the call
1285
1286         when N_Function_Call =>
1287            Current_Checking_Mode := Read;
1288            Check_List (Parameter_Associations (Expr));
1289
1290         when N_Explicit_Dereference =>
1291            Process_Path (Expr);
1292
1293         --  Copy environment, run on each branch, and then merge
1294
1295         when N_If_Expression =>
1296            declare
1297               Saved_Env : Perm_Env;
1298
1299               --  Accumulator for the different branches
1300
1301               New_Env : Perm_Env;
1302
1303               Elmt : Node_Id := First (Expressions (Expr));
1304
1305            begin
1306               Current_Checking_Mode := Read;
1307
1308               Check_Node (Elmt);
1309
1310               Current_Checking_Mode := Mode_Before;
1311
1312               --  Save environment
1313
1314               Copy_Env (Current_Perm_Env,
1315                                 Saved_Env);
1316
1317               --  Here we have the original env in saved, current with a fresh
1318               --  copy, and new aliased.
1319
1320               --  THEN PART
1321
1322               Next (Elmt);
1323               Check_Node (Elmt);
1324
1325               --  Here the new_environment contains curr env after then block
1326
1327               --  ELSE part
1328
1329               --  Restore environment before if
1330               Copy_Env (Current_Perm_Env,
1331                                 New_Env);
1332
1333               Free_Env (Current_Perm_Env);
1334
1335               Copy_Env (Saved_Env,
1336                                 Current_Perm_Env);
1337
1338               --  Here new environment contains the environment after then and
1339               --  current the fresh copy of old one.
1340
1341               Next (Elmt);
1342               Check_Node (Elmt);
1343
1344               Merge_Envs (New_Env,
1345                                   Current_Perm_Env);
1346
1347               --  CLEANUP
1348
1349               Copy_Env (New_Env,
1350                                 Current_Perm_Env);
1351
1352               Free_Env (New_Env);
1353               Free_Env (Saved_Env);
1354            end;
1355
1356         when N_Indexed_Component =>
1357            Process_Path (Expr);
1358
1359         --  Analyze the expression that is getting qualified
1360
1361         when N_Qualified_Expression =>
1362            Check_Node (Expression (Expr));
1363
1364         when N_Quantified_Expression =>
1365            declare
1366               Saved_Env : Perm_Env;
1367            begin
1368               Copy_Env (Current_Perm_Env, Saved_Env);
1369               Current_Checking_Mode := Read;
1370               Check_Node (Iterator_Specification (Expr));
1371               Check_Node (Loop_Parameter_Specification (Expr));
1372
1373               Check_Node (Condition (Expr));
1374               Free_Env (Current_Perm_Env);
1375               Copy_Env (Saved_Env, Current_Perm_Env);
1376               Free_Env (Saved_Env);
1377            end;
1378
1379         when N_Reduction_Expression =>
1380            null;
1381
1382         when N_Reduction_Expression_Parameter =>
1383            null;
1384
1385         --  Analyze the list of associations in the aggregate
1386
1387         when N_Aggregate =>
1388            Check_List (Expressions (Expr));
1389            Check_List (Component_Associations (Expr));
1390
1391         when N_Allocator =>
1392            Check_Node (Expression (Expr));
1393
1394         when N_Case_Expression =>
1395            declare
1396               Saved_Env : Perm_Env;
1397
1398               --  Accumulator for the different branches
1399
1400               New_Env : Perm_Env;
1401
1402               Elmt : Node_Id := First (Alternatives (Expr));
1403
1404            begin
1405               Current_Checking_Mode := Read;
1406               Check_Node (Expression (Expr));
1407
1408               Current_Checking_Mode := Mode_Before;
1409
1410               --  Save environment
1411
1412               Copy_Env (Current_Perm_Env,
1413                                 Saved_Env);
1414
1415               --  Here we have the original env in saved, current with a fresh
1416               --  copy, and new aliased.
1417
1418               --  First alternative
1419
1420               Check_Node (Elmt);
1421               Next (Elmt);
1422
1423               Copy_Env (Current_Perm_Env,
1424                                 New_Env);
1425
1426               Free_Env (Current_Perm_Env);
1427
1428               --  Other alternatives
1429
1430               while Present (Elmt) loop
1431                  --  Restore environment
1432
1433                  Copy_Env (Saved_Env,
1434                                    Current_Perm_Env);
1435
1436                  Check_Node (Elmt);
1437
1438                  --  Merge Current_Perm_Env into New_Env
1439
1440                  Merge_Envs (New_Env,
1441                                      Current_Perm_Env);
1442
1443                  Next (Elmt);
1444               end loop;
1445
1446               --  CLEANUP
1447               Copy_Env (New_Env,
1448                                 Current_Perm_Env);
1449
1450               Free_Env (New_Env);
1451               Free_Env (Saved_Env);
1452            end;
1453
1454         --  Analyze the list of associates in the aggregate as well as the
1455         --  ancestor part.
1456
1457         when N_Extension_Aggregate =>
1458
1459            Check_Node (Ancestor_Part (Expr));
1460            Check_List (Expressions (Expr));
1461
1462         when N_Range =>
1463            Check_Node (Low_Bound (Expr));
1464            Check_Node (High_Bound (Expr));
1465
1466         --  We arrived at a path. Process it.
1467
1468         when N_Selected_Component =>
1469            Process_Path (Expr);
1470
1471         when N_Slice =>
1472            Process_Path (Expr);
1473
1474         when N_Type_Conversion =>
1475            Check_Node (Expression (Expr));
1476
1477         when N_Unchecked_Type_Conversion =>
1478            Check_Node (Expression (Expr));
1479
1480         --  Checking should not be called directly on these nodes
1481
1482         when N_Target_Name =>
1483            raise Program_Error;
1484
1485         --  Unsupported constructs in SPARK
1486
1487         when N_Delta_Aggregate =>
1488            Error_Msg_N ("unsupported construct in SPARK", Expr);
1489
1490         --  Ignored constructs for pointer checking
1491
1492         when N_Character_Literal
1493            | N_Null
1494            | N_Numeric_Or_String_Literal
1495            | N_Operator_Symbol
1496            | N_Raise_Expression
1497            | N_Raise_xxx_Error
1498         =>
1499            null;
1500
1501         --  The following nodes are never generated in GNATprove mode
1502
1503         when N_Expression_With_Actions
1504            | N_Reference
1505            | N_Unchecked_Expression
1506         =>
1507            raise Program_Error;
1508
1509      end case;
1510   end Check_Expression;
1511
1512   -------------------
1513   -- Check_Globals --
1514   -------------------
1515
1516   procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode) is
1517   begin
1518      if Nkind (N) = N_Empty then
1519         return;
1520      end if;
1521
1522      declare
1523         pragma Assert
1524           (List_Length (Pragma_Argument_Associations (N)) = 1);
1525
1526         PAA      : constant Node_Id :=
1527           First (Pragma_Argument_Associations (N));
1528         pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association);
1529
1530         Row      : Node_Id;
1531         The_Mode : Name_Id;
1532         RHS      : Node_Id;
1533
1534         procedure Process (Mode   : Name_Id;
1535                            The_Global : Entity_Id);
1536
1537         procedure Process (Mode   : Name_Id;
1538                            The_Global : Node_Id)
1539         is
1540            Ident_Elt : constant Entity_Id :=
1541              Unique_Entity (Entity (The_Global));
1542
1543            Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1544
1545         begin
1546            if Ekind (Ident_Elt) = E_Abstract_State then
1547               return;
1548            end if;
1549
1550            case Check_Mode is
1551               when Read =>
1552                  case Mode is
1553                     when Name_Input
1554                        | Name_Proof_In
1555                     =>
1556                        Check_Node (The_Global);
1557
1558                     when Name_Output
1559                        | Name_In_Out
1560                     =>
1561                        null;
1562
1563                     when others =>
1564                        raise Program_Error;
1565
1566                  end case;
1567
1568               when Observe =>
1569                  case Mode is
1570                     when Name_Input
1571                        | Name_Proof_In
1572                     =>
1573                        if not Is_Borrowed_In (Ident_Elt) then
1574                           --  Observed in
1575
1576                           Current_Checking_Mode := Observe;
1577                           Check_Node (The_Global);
1578                        end if;
1579
1580                     when others =>
1581                        null;
1582
1583                  end case;
1584
1585               when Borrow_Out =>
1586
1587                  case Mode is
1588                     when Name_Output =>
1589                        --  Borrowed out
1590                        Current_Checking_Mode := Borrow_Out;
1591                        Check_Node (The_Global);
1592
1593                     when others =>
1594                        null;
1595
1596                  end case;
1597
1598               when Move =>
1599                  case Mode is
1600                     when Name_Input
1601                        | Name_Proof_In
1602                     =>
1603                        if Is_Borrowed_In (Ident_Elt) then
1604                           --  Borrowed in
1605
1606                           Current_Checking_Mode := Move;
1607                        else
1608                           --  Observed
1609
1610                           return;
1611                        end if;
1612
1613                     when Name_Output =>
1614                        return;
1615
1616                     when Name_In_Out =>
1617                        --  Borrowed in out
1618
1619                        Current_Checking_Mode := Move;
1620
1621                     when others =>
1622                        raise Program_Error;
1623                  end case;
1624
1625                  Check_Node (The_Global);
1626               when Assign =>
1627                  case Mode is
1628                     when Name_Input
1629                        | Name_Proof_In
1630                     =>
1631                        null;
1632
1633                     when Name_Output
1634                        | Name_In_Out
1635                     =>
1636                        --  Borrowed out or in out
1637
1638                        Process_Path (The_Global);
1639
1640                     when others =>
1641                        raise Program_Error;
1642                  end case;
1643
1644               when others =>
1645                  raise Program_Error;
1646            end case;
1647
1648            Current_Checking_Mode := Mode_Before;
1649         end Process;
1650
1651      begin
1652         if Nkind (Expression (PAA)) = N_Null then
1653            --  global => null
1654            --  No globals, nothing to do
1655            return;
1656
1657         elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
1658            --  global => foo
1659            --  A single input
1660            Process (Name_Input, Expression (PAA));
1661
1662         elsif Nkind (Expression (PAA)) = N_Aggregate
1663           and then Expressions (Expression (PAA)) /= No_List
1664         then
1665            --  global => (foo, bar)
1666            --  Inputs
1667            RHS := First (Expressions (Expression (PAA)));
1668            while Present (RHS) loop
1669               case Nkind (RHS) is
1670                  when N_Identifier
1671                     | N_Expanded_Name
1672                  =>
1673                     Process (Name_Input, RHS);
1674
1675                  when N_Numeric_Or_String_Literal =>
1676                     Process (Name_Input, Original_Node (RHS));
1677
1678                  when others =>
1679                     raise Program_Error;
1680
1681               end case;
1682               RHS := Next (RHS);
1683            end loop;
1684
1685         elsif Nkind (Expression (PAA)) = N_Aggregate
1686           and then Component_Associations (Expression (PAA)) /= No_List
1687         then
1688            --  global => (mode => foo,
1689            --             mode => (bar, baz))
1690            --  A mixture of things
1691
1692            declare
1693               CA : constant List_Id :=
1694                 Component_Associations (Expression (PAA));
1695            begin
1696               Row := First (CA);
1697               while Present (Row) loop
1698                  pragma Assert (List_Length (Choices (Row)) = 1);
1699                  The_Mode := Chars (First (Choices (Row)));
1700
1701                  RHS := Expression (Row);
1702                  case Nkind (RHS) is
1703                     when N_Aggregate =>
1704                        RHS := First (Expressions (RHS));
1705                        while Present (RHS) loop
1706                           case Nkind (RHS) is
1707                              when N_Numeric_Or_String_Literal =>
1708                                 Process (The_Mode, Original_Node (RHS));
1709
1710                              when others =>
1711                                 Process (The_Mode, RHS);
1712
1713                           end case;
1714                           RHS := Next (RHS);
1715                        end loop;
1716
1717                     when N_Identifier
1718                        | N_Expanded_Name
1719                     =>
1720                        Process (The_Mode, RHS);
1721
1722                     when N_Null =>
1723                        null;
1724
1725                     when N_Numeric_Or_String_Literal =>
1726                        Process (The_Mode, Original_Node (RHS));
1727
1728                     when others =>
1729                        raise Program_Error;
1730
1731                  end case;
1732
1733                  Row := Next (Row);
1734               end loop;
1735            end;
1736
1737         else
1738            raise Program_Error;
1739         end if;
1740      end;
1741   end Check_Globals;
1742
1743   ----------------
1744   -- Check_List --
1745   ----------------
1746
1747   procedure Check_List (L : List_Id) is
1748      N : Node_Id;
1749   begin
1750      N := First (L);
1751      while Present (N) loop
1752         Check_Node (N);
1753         Next (N);
1754      end loop;
1755   end Check_List;
1756
1757   --------------------------
1758   -- Check_Loop_Statement --
1759   --------------------------
1760
1761   procedure Check_Loop_Statement (Loop_N : Node_Id) is
1762
1763      --  Local Subprograms
1764
1765      procedure Check_Is_Less_Restrictive_Env
1766        (Exiting_Env : Perm_Env;
1767         Entry_Env   : Perm_Env);
1768      --  This procedure checks that the Exiting_Env environment is less
1769      --  restrictive than the Entry_Env environment.
1770
1771      procedure Check_Is_Less_Restrictive_Tree
1772        (New_Tree  : Perm_Tree_Access;
1773         Orig_Tree : Perm_Tree_Access;
1774         E         : Entity_Id);
1775      --  Auxiliary procedure to check that the tree New_Tree is less
1776      --  restrictive than the tree Orig_Tree for the entity E.
1777
1778      procedure Perm_Error_Loop_Exit
1779        (E          : Entity_Id;
1780         Loop_Id    : Node_Id;
1781         Perm       : Perm_Kind;
1782         Found_Perm : Perm_Kind);
1783      --  A procedure that is called when the permissions found contradict
1784      --  the rules established by the RM at the exit of loops. This function
1785      --  is called with the entity, the node of the enclosing loop, the
1786      --  permission that was expected and the permission found, and issues
1787      --  an appropriate error message.
1788
1789      -----------------------------------
1790      -- Check_Is_Less_Restrictive_Env --
1791      -----------------------------------
1792
1793      procedure Check_Is_Less_Restrictive_Env
1794        (Exiting_Env : Perm_Env;
1795         Entry_Env   : Perm_Env)
1796      is
1797         Comp_Entry : Perm_Tree_Maps.Key_Option;
1798         Iter_Entry, Iter_Exit : Perm_Tree_Access;
1799
1800      begin
1801         Comp_Entry := Get_First_Key (Entry_Env);
1802         while Comp_Entry.Present loop
1803            Iter_Entry := Get (Entry_Env, Comp_Entry.K);
1804            pragma Assert (Iter_Entry /= null);
1805            Iter_Exit := Get (Exiting_Env, Comp_Entry.K);
1806            pragma Assert (Iter_Exit /= null);
1807            Check_Is_Less_Restrictive_Tree
1808              (New_Tree  => Iter_Exit,
1809               Orig_Tree => Iter_Entry,
1810               E         => Comp_Entry.K);
1811            Comp_Entry := Get_Next_Key (Entry_Env);
1812         end loop;
1813      end Check_Is_Less_Restrictive_Env;
1814
1815      ------------------------------------
1816      -- Check_Is_Less_Restrictive_Tree --
1817      ------------------------------------
1818
1819      procedure Check_Is_Less_Restrictive_Tree
1820        (New_Tree  : Perm_Tree_Access;
1821         Orig_Tree : Perm_Tree_Access;
1822         E         : Entity_Id)
1823      is
1824         -----------------------
1825         -- Local Subprograms --
1826         -----------------------
1827
1828         procedure Check_Is_Less_Restrictive_Tree_Than
1829           (Tree : Perm_Tree_Access;
1830            Perm : Perm_Kind;
1831            E    : Entity_Id);
1832         --  Auxiliary procedure to check that the tree N is less restrictive
1833         --  than the given permission P.
1834
1835         procedure Check_Is_More_Restrictive_Tree_Than
1836           (Tree : Perm_Tree_Access;
1837            Perm : Perm_Kind;
1838            E    : Entity_Id);
1839         --  Auxiliary procedure to check that the tree N is more restrictive
1840         --  than the given permission P.
1841
1842         -----------------------------------------
1843         -- Check_Is_Less_Restrictive_Tree_Than --
1844         -----------------------------------------
1845
1846         procedure Check_Is_Less_Restrictive_Tree_Than
1847           (Tree : Perm_Tree_Access;
1848            Perm : Perm_Kind;
1849            E    : Entity_Id)
1850         is
1851         begin
1852            if not (Permission (Tree) >= Perm) then
1853               Perm_Error_Loop_Exit
1854                 (E, Loop_N, Permission (Tree), Perm);
1855            end if;
1856
1857            case Kind (Tree) is
1858               when Entire_Object =>
1859                  if not (Children_Permission (Tree) >= Perm) then
1860                     Perm_Error_Loop_Exit
1861                       (E, Loop_N, Children_Permission (Tree), Perm);
1862
1863                  end if;
1864
1865               when Reference =>
1866                  Check_Is_Less_Restrictive_Tree_Than
1867                    (Get_All (Tree), Perm, E);
1868
1869               when Array_Component =>
1870                  Check_Is_Less_Restrictive_Tree_Than
1871                    (Get_Elem (Tree), Perm, E);
1872
1873               when Record_Component =>
1874                  declare
1875                     Comp : Perm_Tree_Access;
1876                  begin
1877                     Comp := Perm_Tree_Maps.Get_First (Component (Tree));
1878                     while Comp /= null loop
1879                        Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E);
1880                        Comp :=
1881                          Perm_Tree_Maps.Get_Next (Component (Tree));
1882                     end loop;
1883
1884                     Check_Is_Less_Restrictive_Tree_Than
1885                       (Other_Components (Tree), Perm, E);
1886                  end;
1887            end case;
1888         end Check_Is_Less_Restrictive_Tree_Than;
1889
1890         -----------------------------------------
1891         -- Check_Is_More_Restrictive_Tree_Than --
1892         -----------------------------------------
1893
1894         procedure Check_Is_More_Restrictive_Tree_Than
1895           (Tree : Perm_Tree_Access;
1896            Perm : Perm_Kind;
1897            E    : Entity_Id)
1898         is
1899         begin
1900            if not (Perm >= Permission (Tree)) then
1901               Perm_Error_Loop_Exit
1902                 (E, Loop_N, Permission (Tree), Perm);
1903            end if;
1904
1905            case Kind (Tree) is
1906               when Entire_Object =>
1907                  if not (Perm >= Children_Permission (Tree)) then
1908                     Perm_Error_Loop_Exit
1909                       (E, Loop_N, Children_Permission (Tree), Perm);
1910                  end if;
1911
1912               when Reference =>
1913                  Check_Is_More_Restrictive_Tree_Than
1914                    (Get_All (Tree), Perm, E);
1915
1916               when Array_Component =>
1917                  Check_Is_More_Restrictive_Tree_Than
1918                    (Get_Elem (Tree), Perm, E);
1919
1920               when Record_Component =>
1921                  declare
1922                     Comp : Perm_Tree_Access;
1923                  begin
1924                     Comp := Perm_Tree_Maps.Get_First (Component (Tree));
1925                     while Comp /= null loop
1926                        Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E);
1927                        Comp :=
1928                          Perm_Tree_Maps.Get_Next (Component (Tree));
1929                     end loop;
1930
1931                     Check_Is_More_Restrictive_Tree_Than
1932                       (Other_Components (Tree), Perm, E);
1933                  end;
1934            end case;
1935         end Check_Is_More_Restrictive_Tree_Than;
1936
1937      --  Start of processing for Check_Is_Less_Restrictive_Tree
1938
1939      begin
1940         if not (Permission (New_Tree) <= Permission (Orig_Tree)) then
1941            Perm_Error_Loop_Exit
1942              (E          => E,
1943               Loop_Id    => Loop_N,
1944               Perm       => Permission (New_Tree),
1945               Found_Perm => Permission (Orig_Tree));
1946         end if;
1947
1948         case Kind (New_Tree) is
1949
1950            --  Potentially folded tree. We check the other tree Orig_Tree to
1951            --  check whether it is folded or not. If folded we just compare
1952            --  their Permission and Children_Permission, if not, then we
1953            --  look at the Children_Permission of the folded tree against
1954            --  the unfolded tree Orig_Tree.
1955
1956            when Entire_Object =>
1957               case Kind (Orig_Tree) is
1958               when Entire_Object =>
1959                  if not (Children_Permission (New_Tree) <=
1960                          Children_Permission (Orig_Tree))
1961                  then
1962                     Perm_Error_Loop_Exit
1963                       (E, Loop_N,
1964                        Children_Permission (New_Tree),
1965                        Children_Permission (Orig_Tree));
1966                  end if;
1967
1968               when Reference =>
1969                  Check_Is_More_Restrictive_Tree_Than
1970                    (Get_All (Orig_Tree), Children_Permission (New_Tree), E);
1971
1972               when Array_Component =>
1973                  Check_Is_More_Restrictive_Tree_Than
1974                    (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E);
1975
1976               when Record_Component =>
1977                  declare
1978                     Comp : Perm_Tree_Access;
1979                  begin
1980                     Comp := Perm_Tree_Maps.Get_First
1981                       (Component (Orig_Tree));
1982                     while Comp /= null loop
1983                        Check_Is_More_Restrictive_Tree_Than
1984                          (Comp, Children_Permission (New_Tree), E);
1985                        Comp := Perm_Tree_Maps.Get_Next
1986                          (Component (Orig_Tree));
1987                     end loop;
1988
1989                     Check_Is_More_Restrictive_Tree_Than
1990                       (Other_Components (Orig_Tree),
1991                        Children_Permission (New_Tree), E);
1992                  end;
1993               end case;
1994
1995            when Reference =>
1996               case Kind (Orig_Tree) is
1997               when Entire_Object =>
1998                  Check_Is_Less_Restrictive_Tree_Than
1999                    (Get_All (New_Tree), Children_Permission (Orig_Tree), E);
2000
2001               when Reference =>
2002                  Check_Is_Less_Restrictive_Tree
2003                    (Get_All (New_Tree), Get_All (Orig_Tree), E);
2004
2005               when others =>
2006                  raise Program_Error;
2007               end case;
2008
2009            when Array_Component =>
2010               case Kind (Orig_Tree) is
2011               when Entire_Object =>
2012                  Check_Is_Less_Restrictive_Tree_Than
2013                    (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E);
2014
2015               when Array_Component =>
2016                  Check_Is_Less_Restrictive_Tree
2017                    (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E);
2018
2019               when others =>
2020                  raise Program_Error;
2021               end case;
2022
2023            when Record_Component =>
2024               declare
2025                  CompN : Perm_Tree_Access;
2026               begin
2027                  CompN :=
2028                    Perm_Tree_Maps.Get_First (Component (New_Tree));
2029                  case Kind (Orig_Tree) is
2030                  when Entire_Object =>
2031                     while CompN /= null loop
2032                        Check_Is_Less_Restrictive_Tree_Than
2033                          (CompN, Children_Permission (Orig_Tree), E);
2034
2035                        CompN :=
2036                          Perm_Tree_Maps.Get_Next (Component (New_Tree));
2037                     end loop;
2038
2039                     Check_Is_Less_Restrictive_Tree_Than
2040                       (Other_Components (New_Tree),
2041                        Children_Permission (Orig_Tree),
2042                        E);
2043
2044                  when Record_Component =>
2045                     declare
2046
2047                        KeyO : Perm_Tree_Maps.Key_Option;
2048                        CompO : Perm_Tree_Access;
2049                     begin
2050                        KeyO := Perm_Tree_Maps.Get_First_Key
2051                          (Component (Orig_Tree));
2052                        while KeyO.Present loop
2053                           pragma Assert (CompO /= null);
2054
2055                           Check_Is_Less_Restrictive_Tree (CompN, CompO, E);
2056
2057                           KeyO := Perm_Tree_Maps.Get_Next_Key
2058                             (Component (Orig_Tree));
2059                           CompN := Perm_Tree_Maps.Get
2060                             (Component (New_Tree), KeyO.K);
2061                           CompO := Perm_Tree_Maps.Get
2062                             (Component (Orig_Tree), KeyO.K);
2063                        end loop;
2064
2065                        Check_Is_Less_Restrictive_Tree
2066                          (Other_Components (New_Tree),
2067                           Other_Components (Orig_Tree),
2068                           E);
2069                     end;
2070
2071                  when others =>
2072                     raise Program_Error;
2073                  end case;
2074               end;
2075         end case;
2076      end Check_Is_Less_Restrictive_Tree;
2077
2078      --------------------------
2079      -- Perm_Error_Loop_Exit --
2080      --------------------------
2081
2082      procedure Perm_Error_Loop_Exit
2083        (E          : Entity_Id;
2084         Loop_Id    : Node_Id;
2085         Perm       : Perm_Kind;
2086         Found_Perm : Perm_Kind)
2087      is
2088      begin
2089         Error_Msg_Node_2 := Loop_Id;
2090         Error_Msg_N ("insufficient permission for & when exiting loop &", E);
2091         Perm_Mismatch (Exp_Perm => Perm,
2092                        Act_Perm => Found_Perm,
2093                        N        => Loop_Id);
2094      end Perm_Error_Loop_Exit;
2095
2096      --  Local variables
2097
2098      Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
2099      Loop_Env  : constant Perm_Env_Access := new Perm_Env;
2100
2101   begin
2102      --  Save environment prior to the loop
2103
2104      Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
2105
2106      --  Add saved environment to loop environment
2107
2108      Set (Current_Loops_Envs, Loop_Name, Loop_Env);
2109
2110      --  If the loop is not a plain-loop, then it may either never be entered,
2111      --  or it may be exited after a number of iterations. Hence add the
2112      --  current permission environment as the initial loop exit environment.
2113      --  Otherwise, the loop exit environment remains empty until it is
2114      --  populated by analyzing exit statements.
2115
2116      if Present (Iteration_Scheme (Loop_N)) then
2117         declare
2118            Exit_Env  : constant Perm_Env_Access := new Perm_Env;
2119         begin
2120            Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
2121            Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
2122         end;
2123      end if;
2124
2125      --  Analyze loop
2126
2127      Check_Node (Iteration_Scheme (Loop_N));
2128      Check_List (Statements (Loop_N));
2129
2130      --  Check that environment gets less restrictive at end of loop
2131
2132      Check_Is_Less_Restrictive_Env
2133        (Exiting_Env => Current_Perm_Env,
2134         Entry_Env   => Loop_Env.all);
2135
2136      --  Set environment to the one for exiting the loop
2137
2138      declare
2139         Exit_Env : constant Perm_Env_Access :=
2140           Get (Current_Loops_Accumulators, Loop_Name);
2141      begin
2142         Free_Env (Current_Perm_Env);
2143
2144         --  In the normal case, Exit_Env is not null and we use it. In the
2145         --  degraded case of a plain-loop without exit statements, Exit_Env is
2146         --  null, and we use the initial permission environment at the start
2147         --  of the loop to continue analysis. Any environment would be fine
2148         --  here, since the code after the loop is dead code, but this way we
2149         --  avoid spurious errors by having at least variables in scope inside
2150         --  the environment.
2151
2152         if Exit_Env /= null then
2153            Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
2154         else
2155            Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
2156         end if;
2157
2158         Free_Env (Loop_Env.all);
2159         Free_Env (Exit_Env.all);
2160      end;
2161   end Check_Loop_Statement;
2162
2163   ----------------
2164   -- Check_Node --
2165   ----------------
2166
2167   procedure Check_Node (N : Node_Id) is
2168      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2169   begin
2170      case Nkind (N) is
2171         when N_Declaration =>
2172            Check_Declaration (N);
2173
2174         when N_Subexpr =>
2175            Check_Expression (N);
2176
2177         when N_Subtype_Indication =>
2178            Check_Node (Constraint (N));
2179
2180         when N_Body_Stub =>
2181            Check_Node (Get_Body_From_Stub (N));
2182
2183         when N_Statement_Other_Than_Procedure_Call =>
2184            Check_Statement (N);
2185
2186         when N_Package_Body =>
2187            Check_Package_Body (N);
2188
2189         when N_Subprogram_Body
2190            | N_Entry_Body
2191            | N_Task_Body
2192         =>
2193            Check_Callable_Body (N);
2194
2195         when N_Protected_Body =>
2196            Check_List (Declarations (N));
2197
2198         when N_Package_Declaration =>
2199            declare
2200               Spec : constant Node_Id := Specification (N);
2201            begin
2202               Current_Checking_Mode := Read;
2203               Check_List (Visible_Declarations (Spec));
2204               Check_List (Private_Declarations (Spec));
2205
2206               Return_Declarations (Visible_Declarations (Spec));
2207               Return_Declarations (Private_Declarations (Spec));
2208            end;
2209
2210         when N_Iteration_Scheme =>
2211            Current_Checking_Mode := Read;
2212            Check_Node (Condition (N));
2213            Check_Node (Iterator_Specification (N));
2214            Check_Node (Loop_Parameter_Specification (N));
2215
2216         when N_Case_Expression_Alternative =>
2217            Current_Checking_Mode := Read;
2218            Check_List (Discrete_Choices (N));
2219            Current_Checking_Mode := Mode_Before;
2220            Check_Node (Expression (N));
2221
2222         when N_Case_Statement_Alternative =>
2223            Current_Checking_Mode := Read;
2224            Check_List (Discrete_Choices (N));
2225            Current_Checking_Mode := Mode_Before;
2226            Check_List (Statements (N));
2227
2228         when N_Component_Association =>
2229            Check_Node (Expression (N));
2230
2231         when N_Handled_Sequence_Of_Statements =>
2232            Check_List (Statements (N));
2233
2234         when N_Parameter_Association =>
2235            Check_Node (Explicit_Actual_Parameter (N));
2236
2237         when N_Range_Constraint =>
2238            Check_Node (Range_Expression (N));
2239
2240         when N_Index_Or_Discriminant_Constraint =>
2241            Check_List (Constraints (N));
2242
2243         --  Checking should not be called directly on these nodes
2244
2245         when N_Abortable_Part
2246            | N_Accept_Alternative
2247            | N_Access_Definition
2248            | N_Access_Function_Definition
2249            | N_Access_Procedure_Definition
2250            | N_Access_To_Object_Definition
2251            | N_Aspect_Specification
2252            | N_Compilation_Unit
2253            | N_Compilation_Unit_Aux
2254            | N_Component_Clause
2255            | N_Component_Definition
2256            | N_Component_List
2257            | N_Constrained_Array_Definition
2258            | N_Contract
2259            | N_Decimal_Fixed_Point_Definition
2260            | N_Defining_Character_Literal
2261            | N_Defining_Identifier
2262            | N_Defining_Operator_Symbol
2263            | N_Defining_Program_Unit_Name
2264            | N_Delay_Alternative
2265            | N_Derived_Type_Definition
2266            | N_Designator
2267            | N_Discriminant_Association
2268            | N_Discriminant_Specification
2269            | N_Elsif_Part
2270            | N_Entry_Body_Formal_Part
2271            | N_Enumeration_Type_Definition
2272            | N_Entry_Call_Alternative
2273            | N_Entry_Index_Specification
2274            | N_Error
2275            | N_Exception_Handler
2276            | N_Floating_Point_Definition
2277            | N_Formal_Decimal_Fixed_Point_Definition
2278            | N_Formal_Derived_Type_Definition
2279            | N_Formal_Discrete_Type_Definition
2280            | N_Formal_Floating_Point_Definition
2281            | N_Formal_Incomplete_Type_Definition
2282            | N_Formal_Modular_Type_Definition
2283            | N_Formal_Ordinary_Fixed_Point_Definition
2284            | N_Formal_Private_Type_Definition
2285            | N_Formal_Signed_Integer_Type_Definition
2286            | N_Generic_Association
2287            | N_Mod_Clause
2288            | N_Modular_Type_Definition
2289            | N_Ordinary_Fixed_Point_Definition
2290            | N_Package_Specification
2291            | N_Parameter_Specification
2292            | N_Pragma_Argument_Association
2293            | N_Protected_Definition
2294            | N_Push_Pop_xxx_Label
2295            | N_Real_Range_Specification
2296            | N_Record_Definition
2297            | N_SCIL_Dispatch_Table_Tag_Init
2298            | N_SCIL_Dispatching_Call
2299            | N_SCIL_Membership_Test
2300            | N_Signed_Integer_Type_Definition
2301            | N_Subunit
2302            | N_Task_Definition
2303            | N_Terminate_Alternative
2304            | N_Triggering_Alternative
2305            | N_Unconstrained_Array_Definition
2306            | N_Unused_At_Start
2307            | N_Unused_At_End
2308            | N_Variant
2309            | N_Variant_Part
2310         =>
2311            raise Program_Error;
2312
2313         --  Unsupported constructs in SPARK
2314
2315         when N_Iterated_Component_Association =>
2316            Error_Msg_N ("unsupported construct in SPARK", N);
2317
2318         --  Ignored constructs for pointer checking
2319
2320         when N_Abstract_Subprogram_Declaration
2321            | N_At_Clause
2322            | N_Attribute_Definition_Clause
2323            | N_Call_Marker
2324            | N_Delta_Constraint
2325            | N_Digits_Constraint
2326            | N_Empty
2327            | N_Enumeration_Representation_Clause
2328            | N_Exception_Declaration
2329            | N_Exception_Renaming_Declaration
2330            | N_Formal_Package_Declaration
2331            | N_Formal_Subprogram_Declaration
2332            | N_Freeze_Entity
2333            | N_Freeze_Generic_Entity
2334            | N_Function_Instantiation
2335            | N_Generic_Function_Renaming_Declaration
2336            | N_Generic_Package_Declaration
2337            | N_Generic_Package_Renaming_Declaration
2338            | N_Generic_Procedure_Renaming_Declaration
2339            | N_Generic_Subprogram_Declaration
2340            | N_Implicit_Label_Declaration
2341            | N_Itype_Reference
2342            | N_Label
2343            | N_Number_Declaration
2344            | N_Object_Renaming_Declaration
2345            | N_Others_Choice
2346            | N_Package_Instantiation
2347            | N_Package_Renaming_Declaration
2348            | N_Pragma
2349            | N_Procedure_Instantiation
2350            | N_Record_Representation_Clause
2351            | N_Subprogram_Declaration
2352            | N_Subprogram_Renaming_Declaration
2353            | N_Task_Type_Declaration
2354            | N_Use_Package_Clause
2355            | N_With_Clause
2356            | N_Use_Type_Clause
2357            | N_Validate_Unchecked_Conversion
2358            | N_Variable_Reference_Marker
2359         =>
2360            null;
2361
2362         --  The following nodes are rewritten by semantic analysis
2363
2364         when N_Single_Protected_Declaration
2365            | N_Single_Task_Declaration
2366         =>
2367            raise Program_Error;
2368      end case;
2369
2370      Current_Checking_Mode := Mode_Before;
2371   end Check_Node;
2372
2373   ------------------------
2374   -- Check_Package_Body --
2375   ------------------------
2376
2377   procedure Check_Package_Body (Pack : Node_Id) is
2378      Saved_Env : Perm_Env;
2379      CorSp : Node_Id;
2380
2381   begin
2382      if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
2383         if Get_SPARK_Mode_From_Annotation
2384           (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
2385         then
2386            return;
2387         end if;
2388      else
2389         return;
2390      end if;
2391
2392      CorSp := Parent (Corresponding_Spec (Pack));
2393      while Nkind (CorSp) /= N_Package_Specification loop
2394         CorSp := Parent (CorSp);
2395      end loop;
2396
2397      Check_List (Visible_Declarations (CorSp));
2398
2399      --  Save environment
2400
2401      Copy_Env (Current_Perm_Env,
2402                Saved_Env);
2403
2404      Check_List (Private_Declarations (CorSp));
2405
2406      --  Set mode to Read, and then analyze declarations and statements
2407
2408      Current_Checking_Mode := Read;
2409
2410      Check_List (Declarations (Pack));
2411      Check_Node (Handled_Statement_Sequence (Pack));
2412
2413      --  Check RW for every stateful variable (i.e. in declarations)
2414
2415      Return_Declarations (Private_Declarations (CorSp));
2416      Return_Declarations (Visible_Declarations (CorSp));
2417      Return_Declarations (Declarations (Pack));
2418
2419      --  Restore previous environment (i.e. delete every nonvisible
2420      --  declaration) from environment.
2421
2422      Free_Env (Current_Perm_Env);
2423      Copy_Env (Saved_Env,
2424                Current_Perm_Env);
2425   end Check_Package_Body;
2426
2427   -----------------
2428   -- Check_Param --
2429   -----------------
2430
2431   procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
2432      Mode : constant Entity_Kind := Ekind (Formal);
2433      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2434
2435   begin
2436      case Current_Checking_Mode is
2437         when Read =>
2438            case Formal_Kind'(Mode) is
2439               when E_In_Parameter =>
2440                  if Is_Borrowed_In (Formal) then
2441                     --  Borrowed in
2442
2443                     Current_Checking_Mode := Move;
2444                  else
2445                     --  Observed
2446
2447                     return;
2448                  end if;
2449
2450               when E_Out_Parameter =>
2451                  return;
2452
2453               when E_In_Out_Parameter =>
2454                  --  Borrowed in out
2455
2456                  Current_Checking_Mode := Move;
2457
2458            end case;
2459
2460            Check_Node (Actual);
2461
2462         when Assign =>
2463            case Formal_Kind'(Mode) is
2464               when E_In_Parameter =>
2465                  null;
2466
2467               when E_Out_Parameter
2468                  | E_In_Out_Parameter
2469               =>
2470                  --  Borrowed out or in out
2471
2472                  Process_Path (Actual);
2473
2474            end case;
2475
2476         when others =>
2477            raise Program_Error;
2478
2479      end case;
2480      Current_Checking_Mode := Mode_Before;
2481   end Check_Param;
2482
2483   --------------------------
2484   -- Check_Param_Observes --
2485   --------------------------
2486
2487   procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is
2488      Mode : constant Entity_Kind := Ekind (Formal);
2489      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2490
2491   begin
2492      case Mode is
2493         when E_In_Parameter =>
2494            if not Is_Borrowed_In (Formal) then
2495               --  Observed in
2496
2497               Current_Checking_Mode := Observe;
2498               Check_Node (Actual);
2499            end if;
2500
2501         when others =>
2502            null;
2503
2504      end case;
2505
2506      Current_Checking_Mode := Mode_Before;
2507   end Check_Param_Observes;
2508
2509   ----------------------
2510   -- Check_Param_Outs --
2511   ----------------------
2512
2513   procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is
2514      Mode : constant Entity_Kind := Ekind (Formal);
2515      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2516
2517   begin
2518
2519      case Mode is
2520         when E_Out_Parameter =>
2521            --  Borrowed out
2522            Current_Checking_Mode := Borrow_Out;
2523            Check_Node (Actual);
2524
2525         when others =>
2526            null;
2527
2528      end case;
2529
2530      Current_Checking_Mode := Mode_Before;
2531   end Check_Param_Outs;
2532
2533   ----------------------
2534   -- Check_Param_Read --
2535   ----------------------
2536
2537   procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is
2538      Mode : constant Entity_Kind := Ekind (Formal);
2539
2540   begin
2541      pragma Assert (Current_Checking_Mode = Read);
2542
2543      case Formal_Kind'(Mode) is
2544         when E_In_Parameter =>
2545            Check_Node (Actual);
2546
2547         when E_Out_Parameter
2548            | E_In_Out_Parameter
2549         =>
2550            null;
2551
2552      end case;
2553   end Check_Param_Read;
2554
2555   -------------------------
2556   -- Check_Safe_Pointers --
2557   -------------------------
2558
2559   procedure Check_Safe_Pointers (N : Node_Id) is
2560
2561      --  Local subprograms
2562
2563      procedure Check_List (L : List_Id);
2564      --  Call the main analysis procedure on each element of the list
2565
2566      procedure Initialize;
2567      --  Initialize global variables before starting the analysis of a body
2568
2569      ----------------
2570      -- Check_List --
2571      ----------------
2572
2573      procedure Check_List (L : List_Id) is
2574         N : Node_Id;
2575      begin
2576         N := First (L);
2577         while Present (N) loop
2578            Check_Safe_Pointers (N);
2579            Next (N);
2580         end loop;
2581      end Check_List;
2582
2583      ----------------
2584      -- Initialize --
2585      ----------------
2586
2587      procedure Initialize is
2588      begin
2589         Reset (Current_Loops_Envs);
2590         Reset (Current_Loops_Accumulators);
2591         Reset (Current_Perm_Env);
2592         Reset (Current_Initialization_Map);
2593      end Initialize;
2594
2595      --  Local variables
2596
2597      Prag : Node_Id;
2598      --  SPARK_Mode pragma in application
2599
2600   --  Start of processing for Check_Safe_Pointers
2601
2602   begin
2603      Initialize;
2604
2605      case Nkind (N) is
2606         when N_Compilation_Unit =>
2607            Check_Safe_Pointers (Unit (N));
2608
2609         when N_Package_Body
2610            | N_Package_Declaration
2611            | N_Subprogram_Body
2612         =>
2613            Prag := SPARK_Pragma (Defining_Entity (N));
2614            if Present (Prag) then
2615               if Get_SPARK_Mode_From_Annotation (Prag) = Opt.Off then
2616                  return;
2617               else
2618                  Check_Node (N);
2619               end if;
2620
2621            elsif Nkind (N) = N_Package_Body then
2622               Check_List (Declarations (N));
2623
2624            elsif Nkind (N) = N_Package_Declaration then
2625               Check_List (Private_Declarations (Specification (N)));
2626               Check_List (Visible_Declarations (Specification (N)));
2627            end if;
2628
2629         when others =>
2630            null;
2631      end case;
2632   end Check_Safe_Pointers;
2633
2634   ---------------------
2635   -- Check_Statement --
2636   ---------------------
2637
2638   procedure Check_Statement (Stmt : Node_Id) is
2639      Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2640   begin
2641      case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is
2642         when N_Entry_Call_Statement =>
2643            Check_Call_Statement (Stmt);
2644
2645         --  Move right-hand side first, and then assign left-hand side
2646
2647         when N_Assignment_Statement =>
2648            if Is_Deep (Etype (Expression (Stmt))) then
2649               Current_Checking_Mode := Move;
2650            else
2651               Current_Checking_Mode := Read;
2652            end if;
2653
2654            Check_Node (Expression (Stmt));
2655            Current_Checking_Mode := Assign;
2656            Check_Node (Name (Stmt));
2657
2658         when N_Block_Statement =>
2659            declare
2660               Saved_Env : Perm_Env;
2661
2662            begin
2663               --  Save environment
2664
2665               Copy_Env (Current_Perm_Env,
2666                                 Saved_Env);
2667
2668               --  Analyze declarations and Handled_Statement_Sequences
2669
2670               Current_Checking_Mode := Read;
2671               Check_List (Declarations (Stmt));
2672               Check_Node (Handled_Statement_Sequence (Stmt));
2673
2674               --  Restore environment
2675
2676               Free_Env (Current_Perm_Env);
2677               Copy_Env (Saved_Env,
2678                                 Current_Perm_Env);
2679            end;
2680
2681         when N_Case_Statement =>
2682            declare
2683               Saved_Env : Perm_Env;
2684
2685               --  Accumulator for the different branches
2686
2687               New_Env : Perm_Env;
2688
2689               Elmt : Node_Id := First (Alternatives (Stmt));
2690
2691            begin
2692               Current_Checking_Mode := Read;
2693               Check_Node (Expression (Stmt));
2694               Current_Checking_Mode := Mode_Before;
2695
2696               --  Save environment
2697
2698               Copy_Env (Current_Perm_Env,
2699                                 Saved_Env);
2700
2701               --  Here we have the original env in saved, current with a fresh
2702               --  copy, and new aliased.
2703
2704               --  First alternative
2705
2706               Check_Node (Elmt);
2707               Next (Elmt);
2708
2709               Copy_Env (Current_Perm_Env,
2710                                 New_Env);
2711               Free_Env (Current_Perm_Env);
2712
2713               --  Other alternatives
2714
2715               while Present (Elmt) loop
2716                  --  Restore environment
2717
2718                  Copy_Env (Saved_Env,
2719                                    Current_Perm_Env);
2720
2721                  Check_Node (Elmt);
2722
2723                  --  Merge Current_Perm_Env into New_Env
2724
2725                  Merge_Envs (New_Env,
2726                                      Current_Perm_Env);
2727
2728                  Next (Elmt);
2729               end loop;
2730
2731               --  CLEANUP
2732               Copy_Env (New_Env,
2733                                 Current_Perm_Env);
2734
2735               Free_Env (New_Env);
2736               Free_Env (Saved_Env);
2737            end;
2738
2739         when N_Delay_Relative_Statement =>
2740            Check_Node (Expression (Stmt));
2741
2742         when N_Delay_Until_Statement =>
2743            Check_Node (Expression (Stmt));
2744
2745         when N_Loop_Statement =>
2746            Check_Loop_Statement (Stmt);
2747
2748         --  If deep type expression, then move, else read
2749
2750         when N_Simple_Return_Statement =>
2751            case Nkind (Expression (Stmt)) is
2752               when N_Empty =>
2753                  declare
2754                     --  ??? This does not take into account the fact that
2755                     --  a simple return inside an extended return statement
2756                     --  applies to the extended return statement.
2757                     Subp : constant Entity_Id :=
2758                       Return_Applies_To (Return_Statement_Entity (Stmt));
2759                  begin
2760                     Return_Parameters (Subp);
2761                     Return_Globals (Subp);
2762                  end;
2763
2764               when others =>
2765                  if Is_Deep (Etype (Expression (Stmt))) then
2766                     Current_Checking_Mode := Move;
2767                  elsif Is_Shallow (Etype (Expression (Stmt))) then
2768                     Current_Checking_Mode := Read;
2769                  else
2770                     raise Program_Error;
2771                  end if;
2772
2773                  Check_Node (Expression (Stmt));
2774            end case;
2775
2776         when N_Extended_Return_Statement =>
2777            Check_List (Return_Object_Declarations (Stmt));
2778            Check_Node (Handled_Statement_Sequence (Stmt));
2779
2780            Return_Declarations (Return_Object_Declarations (Stmt));
2781
2782            declare
2783               --  ??? This does not take into account the fact that a simple
2784               --  return inside an extended return statement applies to the
2785               --  extended return statement.
2786               Subp : constant Entity_Id :=
2787                 Return_Applies_To (Return_Statement_Entity (Stmt));
2788            begin
2789               Return_Parameters (Subp);
2790               Return_Globals (Subp);
2791            end;
2792
2793         --  Merge the current_Perm_Env with the accumulator for the given loop
2794
2795         when N_Exit_Statement =>
2796            declare
2797               Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
2798
2799               Saved_Accumulator : constant Perm_Env_Access :=
2800                 Get (Current_Loops_Accumulators, Loop_Name);
2801
2802               Environment_Copy : constant Perm_Env_Access :=
2803                 new Perm_Env;
2804            begin
2805
2806               Copy_Env (Current_Perm_Env,
2807                                 Environment_Copy.all);
2808
2809               if Saved_Accumulator = null then
2810                  Set (Current_Loops_Accumulators,
2811                       Loop_Name, Environment_Copy);
2812               else
2813                  Merge_Envs (Saved_Accumulator.all,
2814                                      Environment_Copy.all);
2815               end if;
2816            end;
2817
2818         --  Copy environment, run on each branch, and then merge
2819
2820         when N_If_Statement =>
2821            declare
2822               Saved_Env : Perm_Env;
2823
2824               --  Accumulator for the different branches
2825
2826               New_Env : Perm_Env;
2827
2828            begin
2829
2830               Check_Node (Condition (Stmt));
2831
2832               --  Save environment
2833
2834               Copy_Env (Current_Perm_Env,
2835                                 Saved_Env);
2836
2837               --  Here we have the original env in saved, current with a fresh
2838               --  copy.
2839
2840               --  THEN PART
2841
2842               Check_List (Then_Statements (Stmt));
2843
2844               Copy_Env (Current_Perm_Env,
2845                                 New_Env);
2846
2847               Free_Env (Current_Perm_Env);
2848
2849               --  Here the new_environment contains curr env after then block
2850
2851               --  ELSIF part
2852               declare
2853                  Elmt : Node_Id;
2854
2855               begin
2856                  Elmt := First (Elsif_Parts (Stmt));
2857                  while Present (Elmt) loop
2858                     --  Transfer into accumulator, and restore from save
2859
2860                     Copy_Env (Saved_Env,
2861                                       Current_Perm_Env);
2862
2863                     Check_Node (Condition (Elmt));
2864                     Check_List (Then_Statements (Stmt));
2865
2866                     --  Merge Current_Perm_Env into New_Env
2867
2868                     Merge_Envs (New_Env,
2869                                         Current_Perm_Env);
2870
2871                     Next (Elmt);
2872                  end loop;
2873               end;
2874
2875               --  ELSE part
2876
2877               --  Restore environment before if
2878
2879               Copy_Env (Saved_Env,
2880                                 Current_Perm_Env);
2881
2882               --  Here new environment contains the environment after then and
2883               --  current the fresh copy of old one.
2884
2885               Check_List (Else_Statements (Stmt));
2886
2887               Merge_Envs (New_Env,
2888                                   Current_Perm_Env);
2889
2890               --  CLEANUP
2891
2892               Copy_Env (New_Env,
2893                                 Current_Perm_Env);
2894
2895               Free_Env (New_Env);
2896               Free_Env (Saved_Env);
2897            end;
2898
2899         --  Unsupported constructs in SPARK
2900
2901         when N_Abort_Statement
2902            | N_Accept_Statement
2903            | N_Asynchronous_Select
2904            | N_Code_Statement
2905            | N_Conditional_Entry_Call
2906            | N_Goto_Statement
2907            | N_Requeue_Statement
2908            | N_Selective_Accept
2909            | N_Timed_Entry_Call
2910         =>
2911            Error_Msg_N ("unsupported construct in SPARK", Stmt);
2912
2913         --  Ignored constructs for pointer checking
2914
2915         when N_Null_Statement
2916            | N_Raise_Statement
2917         =>
2918            null;
2919
2920         --  The following nodes are never generated in GNATprove mode
2921
2922         when N_Compound_Statement
2923            | N_Free_Statement
2924         =>
2925            raise Program_Error;
2926      end case;
2927   end Check_Statement;
2928
2929   --------------
2930   -- Get_Perm --
2931   --------------
2932
2933   function Get_Perm (N : Node_Id) return Perm_Kind is
2934      Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
2935
2936   begin
2937      case Tree_Or_Perm.R is
2938         when Folded =>
2939            return Tree_Or_Perm.Found_Permission;
2940
2941         when Unfolded =>
2942            pragma Assert (Tree_Or_Perm.Tree_Access /= null);
2943            return Permission (Tree_Or_Perm.Tree_Access);
2944
2945         --  We encoutered a function call, hence the memory area is fresh,
2946         --  which means that the association permission is RW.
2947
2948         when Function_Call =>
2949            return Read_Write;
2950
2951      end case;
2952   end Get_Perm;
2953
2954   ----------------------
2955   -- Get_Perm_Or_Tree --
2956   ----------------------
2957
2958   function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
2959   begin
2960      case Nkind (N) is
2961
2962         --  Base identifier. Normally those are the roots of the trees stored
2963         --  in the permission environment.
2964
2965         when N_Defining_Identifier =>
2966            raise Program_Error;
2967
2968         when N_Identifier
2969            | N_Expanded_Name
2970         =>
2971            declare
2972               P : constant Entity_Id := Entity (N);
2973
2974               C : constant Perm_Tree_Access :=
2975                 Get (Current_Perm_Env, Unique_Entity (P));
2976
2977            begin
2978               --  Setting the initialization map to True, so that this
2979               --  variable cannot be ignored anymore when looking at end
2980               --  of elaboration of package.
2981
2982               Set (Current_Initialization_Map, Unique_Entity (P), True);
2983
2984               if C = null then
2985                  --  No null possible here, there are no parents for the path.
2986                  --  This means we are using a global variable without adding
2987                  --  it in environment with a global aspect.
2988
2989                  Illegal_Global_Usage (N);
2990               else
2991                  return (R => Unfolded, Tree_Access => C);
2992               end if;
2993            end;
2994
2995         when N_Type_Conversion
2996            | N_Unchecked_Type_Conversion
2997            | N_Qualified_Expression
2998         =>
2999            return Get_Perm_Or_Tree (Expression (N));
3000
3001         --  Happening when we try to get the permission of a variable that
3002         --  is a formal parameter. We get instead the defining identifier
3003         --  associated with the parameter (which is the one that has been
3004         --  stored for indexing).
3005
3006         when N_Parameter_Specification =>
3007            return Get_Perm_Or_Tree (Defining_Identifier (N));
3008
3009         --  We get the permission tree of its prefix, and then get either the
3010         --  subtree associated with that specific selection, or if we have a
3011         --  leaf that folds its children, we take the children's permission
3012         --  and return it using the discriminant Folded.
3013
3014         when N_Selected_Component =>
3015            declare
3016               C : constant Perm_Or_Tree :=
3017                 Get_Perm_Or_Tree (Prefix (N));
3018
3019            begin
3020               case C.R is
3021                  when Folded
3022                     | Function_Call
3023                  =>
3024                     return C;
3025
3026                  when Unfolded =>
3027                     pragma Assert (C.Tree_Access /= null);
3028
3029                     pragma Assert (Kind (C.Tree_Access) = Entire_Object
3030                                    or else
3031                                    Kind (C.Tree_Access) = Record_Component);
3032
3033                     if Kind (C.Tree_Access) = Record_Component then
3034                        declare
3035                           Selected_Component : constant Entity_Id :=
3036                             Entity (Selector_Name (N));
3037
3038                           Selected_C : constant Perm_Tree_Access :=
3039                             Perm_Tree_Maps.Get
3040                               (Component (C.Tree_Access), Selected_Component);
3041
3042                        begin
3043                           if Selected_C = null then
3044                              return (R => Unfolded,
3045                                      Tree_Access =>
3046                                        Other_Components (C.Tree_Access));
3047                           else
3048                              return (R => Unfolded,
3049                                      Tree_Access => Selected_C);
3050                           end if;
3051                        end;
3052                     elsif Kind (C.Tree_Access) = Entire_Object then
3053                        return (R => Folded, Found_Permission =>
3054                                  Children_Permission (C.Tree_Access));
3055                     else
3056                        raise Program_Error;
3057                     end if;
3058               end case;
3059            end;
3060
3061         --  We get the permission tree of its prefix, and then get either the
3062         --  subtree associated with that specific selection, or if we have a
3063         --  leaf that folds its children, we take the children's permission
3064         --  and return it using the discriminant Folded.
3065
3066         when N_Indexed_Component
3067            | N_Slice
3068         =>
3069            declare
3070               C : constant Perm_Or_Tree :=
3071                 Get_Perm_Or_Tree (Prefix (N));
3072
3073            begin
3074               case C.R is
3075                  when Folded
3076                     | Function_Call
3077                  =>
3078                     return C;
3079
3080                  when Unfolded =>
3081                     pragma Assert (C.Tree_Access /= null);
3082
3083                     pragma Assert (Kind (C.Tree_Access) = Entire_Object
3084                                    or else
3085                                    Kind (C.Tree_Access) = Array_Component);
3086
3087                     if Kind (C.Tree_Access) = Array_Component then
3088                        pragma Assert (Get_Elem (C.Tree_Access) /= null);
3089
3090                        return (R => Unfolded,
3091                                Tree_Access => Get_Elem (C.Tree_Access));
3092                     elsif Kind (C.Tree_Access) = Entire_Object then
3093                        return (R => Folded, Found_Permission =>
3094                                  Children_Permission (C.Tree_Access));
3095                     else
3096                        raise Program_Error;
3097                     end if;
3098               end case;
3099            end;
3100
3101         --  We get the permission tree of its prefix, and then get either the
3102         --  subtree associated with that specific selection, or if we have a
3103         --  leaf that folds its children, we take the children's permission
3104         --  and return it using the discriminant Folded.
3105
3106         when N_Explicit_Dereference =>
3107            declare
3108               C : constant Perm_Or_Tree :=
3109                 Get_Perm_Or_Tree (Prefix (N));
3110
3111            begin
3112               case C.R is
3113                  when Folded
3114                     | Function_Call
3115                  =>
3116                     return C;
3117
3118                  when Unfolded =>
3119                     pragma Assert (C.Tree_Access /= null);
3120
3121                     pragma Assert (Kind (C.Tree_Access) = Entire_Object
3122                                    or else
3123                                    Kind (C.Tree_Access) = Reference);
3124
3125                     if Kind (C.Tree_Access) = Reference then
3126                        if Get_All (C.Tree_Access) = null then
3127                           --  Hash_Table_Error
3128                           raise Program_Error;
3129                        else
3130                           return
3131                             (R => Unfolded,
3132                              Tree_Access => Get_All (C.Tree_Access));
3133                        end if;
3134                     elsif Kind (C.Tree_Access) = Entire_Object then
3135                        return (R => Folded, Found_Permission =>
3136                                  Children_Permission (C.Tree_Access));
3137                     else
3138                        raise Program_Error;
3139                     end if;
3140               end case;
3141            end;
3142
3143         --  The name contains a function call, hence the given path is always
3144         --  new. We do not have to check for anything.
3145
3146         when N_Function_Call =>
3147            return (R => Function_Call);
3148
3149         when others =>
3150            raise Program_Error;
3151      end case;
3152   end Get_Perm_Or_Tree;
3153
3154   -------------------
3155   -- Get_Perm_Tree --
3156   -------------------
3157
3158   function Get_Perm_Tree
3159     (N : Node_Id)
3160       return Perm_Tree_Access
3161   is
3162   begin
3163      case Nkind (N) is
3164
3165         --  Base identifier. Normally those are the roots of the trees stored
3166         --  in the permission environment.
3167
3168         when N_Defining_Identifier =>
3169            raise Program_Error;
3170
3171         when N_Identifier
3172            | N_Expanded_Name
3173         =>
3174            declare
3175               P : constant Node_Id := Entity (N);
3176
3177               C : constant Perm_Tree_Access :=
3178                 Get (Current_Perm_Env, Unique_Entity (P));
3179
3180            begin
3181               --  Setting the initialization map to True, so that this
3182               --  variable cannot be ignored anymore when looking at end
3183               --  of elaboration of package.
3184
3185               Set (Current_Initialization_Map, Unique_Entity (P), True);
3186
3187               if C = null then
3188                  --  No null possible here, there are no parents for the path.
3189                  --  This means we are using a global variable without adding
3190                  --  it in environment with a global aspect.
3191
3192                  Illegal_Global_Usage (N);
3193               else
3194                  return C;
3195               end if;
3196            end;
3197
3198         when N_Type_Conversion
3199            | N_Unchecked_Type_Conversion
3200            | N_Qualified_Expression
3201         =>
3202            return Get_Perm_Tree (Expression (N));
3203
3204         when N_Parameter_Specification =>
3205            return Get_Perm_Tree (Defining_Identifier (N));
3206
3207         --  We get the permission tree of its prefix, and then get either the
3208         --  subtree associated with that specific selection, or if we have a
3209         --  leaf that folds its children, we unroll it in one step.
3210
3211         when N_Selected_Component =>
3212            declare
3213               C : constant Perm_Tree_Access :=
3214                 Get_Perm_Tree (Prefix (N));
3215
3216            begin
3217               if C = null then
3218                  --  If null then it means we went through a function call
3219
3220                  return null;
3221               end if;
3222
3223               pragma Assert (Kind (C) = Entire_Object
3224                              or else Kind (C) = Record_Component);
3225
3226               if Kind (C) = Record_Component then
3227                  --  The tree is unfolded. We just return the subtree.
3228
3229                  declare
3230                     Selected_Component : constant Entity_Id :=
3231                       Entity (Selector_Name (N));
3232                     Selected_C : constant Perm_Tree_Access :=
3233                       Perm_Tree_Maps.Get
3234                         (Component (C), Selected_Component);
3235
3236                  begin
3237                     if Selected_C = null then
3238                        return Other_Components (C);
3239                     end if;
3240
3241                     return Selected_C;
3242                  end;
3243               elsif Kind (C) = Entire_Object then
3244                  declare
3245                     --  Expand the tree. Replace the node with
3246                     --  Record_Component.
3247
3248                     Elem : Node_Id;
3249
3250                     --  Create the unrolled nodes
3251
3252                     Son : Perm_Tree_Access;
3253
3254                     Child_Perm : constant Perm_Kind :=
3255                       Children_Permission (C);
3256
3257                  begin
3258
3259                     --  We change the current node from Entire_Object to
3260                     --  Record_Component with same permission and an empty
3261                     --  hash table as component list.
3262
3263                     C.all.Tree :=
3264                       (Kind             => Record_Component,
3265                        Is_Node_Deep     => Is_Node_Deep (C),
3266                        Permission       => Permission (C),
3267                        Component        => Perm_Tree_Maps.Nil,
3268                        Other_Components =>
3269                           new Perm_Tree_Wrapper'
3270                          (Tree =>
3271                               (Kind                => Entire_Object,
3272                                --  Is_Node_Deep is true, to be conservative
3273                                Is_Node_Deep        => True,
3274                                Permission          => Child_Perm,
3275                                Children_Permission => Child_Perm)
3276                          )
3277                       );
3278
3279                     --  We fill the hash table with all sons of the record,
3280                     --  with basic Entire_Objects nodes.
3281                     Elem := First_Component_Or_Discriminant
3282                       (Etype (Prefix (N)));
3283
3284                     while Present (Elem) loop
3285                        Son := new Perm_Tree_Wrapper'
3286                          (Tree =>
3287                             (Kind                => Entire_Object,
3288                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
3289                              Permission          => Child_Perm,
3290                              Children_Permission => Child_Perm));
3291
3292                        Perm_Tree_Maps.Set
3293                          (C.all.Tree.Component, Elem, Son);
3294
3295                        Next_Component_Or_Discriminant (Elem);
3296                     end loop;
3297
3298                     --  we return the tree to the sons, so that the recursion
3299                     --  can continue.
3300
3301                     declare
3302                        Selected_Component : constant Entity_Id :=
3303                          Entity (Selector_Name (N));
3304
3305                        Selected_C : constant Perm_Tree_Access :=
3306                          Perm_Tree_Maps.Get
3307                            (Component (C), Selected_Component);
3308
3309                     begin
3310                        pragma Assert (Selected_C /= null);
3311
3312                        return Selected_C;
3313                     end;
3314
3315                  end;
3316               else
3317                  raise Program_Error;
3318               end if;
3319            end;
3320
3321         --  We set the permission tree of its prefix, and then we extract from
3322         --  the returned pointer the subtree. If folded, we unroll the tree at
3323         --  one step.
3324
3325         when N_Indexed_Component
3326            | N_Slice
3327         =>
3328            declare
3329               C : constant Perm_Tree_Access :=
3330                 Get_Perm_Tree (Prefix (N));
3331
3332            begin
3333               if C = null then
3334                  --  If null then we went through a function call
3335
3336                  return null;
3337               end if;
3338
3339               pragma Assert (Kind (C) = Entire_Object
3340                              or else Kind (C) = Array_Component);
3341
3342               if Kind (C) = Array_Component then
3343                  --  The tree is unfolded. We just return the elem subtree
3344
3345                  pragma Assert (Get_Elem (C) = null);
3346
3347                  return Get_Elem (C);
3348               elsif Kind (C) = Entire_Object then
3349                  declare
3350                     --  Expand the tree. Replace node with Array_Component.
3351
3352                     Son : Perm_Tree_Access;
3353
3354                  begin
3355                     Son := new Perm_Tree_Wrapper'
3356                       (Tree =>
3357                          (Kind                => Entire_Object,
3358                           Is_Node_Deep        => Is_Node_Deep (C),
3359                           Permission          => Children_Permission (C),
3360                           Children_Permission => Children_Permission (C)));
3361
3362                     --  We change the current node from Entire_Object
3363                     --  to Array_Component with same permission and the
3364                     --  previously defined son.
3365
3366                     C.all.Tree := (Kind         => Array_Component,
3367                                    Is_Node_Deep => Is_Node_Deep (C),
3368                                    Permission   => Permission (C),
3369                                    Get_Elem     => Son);
3370
3371                     return Get_Elem (C);
3372                  end;
3373               else
3374                  raise Program_Error;
3375               end if;
3376            end;
3377
3378         --  We get the permission tree of its prefix, and then get either the
3379         --  subtree associated with that specific selection, or if we have a
3380         --  leaf that folds its children, we unroll the tree.
3381
3382         when N_Explicit_Dereference =>
3383            declare
3384               C : Perm_Tree_Access;
3385
3386            begin
3387               C := Get_Perm_Tree (Prefix (N));
3388
3389               if C = null then
3390                  --  If null, we went through a function call
3391
3392                  return null;
3393               end if;
3394
3395               pragma Assert (Kind (C) = Entire_Object
3396                              or else Kind (C) = Reference);
3397
3398               if Kind (C) = Reference then
3399                  --  The tree is unfolded. We return the elem subtree
3400
3401                  if Get_All (C) = null then
3402                     --  Hash_Table_Error
3403                     raise Program_Error;
3404                  end if;
3405
3406                  return Get_All (C);
3407               elsif Kind (C) = Entire_Object then
3408                  declare
3409                     --  Expand the tree. Replace the node with Reference.
3410
3411                     Son : Perm_Tree_Access;
3412
3413                  begin
3414                     Son := new Perm_Tree_Wrapper'
3415                       (Tree =>
3416                          (Kind                => Entire_Object,
3417                           Is_Node_Deep        => Is_Deep (Etype (N)),
3418                           Permission          => Children_Permission (C),
3419                           Children_Permission => Children_Permission (C)));
3420
3421                     --  We change the current node from Entire_Object to
3422                     --  Reference with same permission and the previous son.
3423
3424                     pragma Assert (Is_Node_Deep (C));
3425
3426                     C.all.Tree := (Kind         => Reference,
3427                                    Is_Node_Deep => Is_Node_Deep (C),
3428                                    Permission   => Permission (C),
3429                                    Get_All      => Son);
3430
3431                     return Get_All (C);
3432                  end;
3433               else
3434                  raise Program_Error;
3435               end if;
3436            end;
3437
3438         --  No permission tree for function calls
3439
3440         when N_Function_Call =>
3441            return null;
3442
3443         when others =>
3444            raise Program_Error;
3445      end case;
3446   end Get_Perm_Tree;
3447
3448   ---------
3449   -- Glb --
3450   ---------
3451
3452   function Glb (P1, P2 : Perm_Kind) return Perm_Kind
3453   is
3454   begin
3455      case P1 is
3456         when No_Access =>
3457            return No_Access;
3458
3459         when Read_Only =>
3460            case P2 is
3461               when No_Access
3462                  | Write_Only
3463               =>
3464                  return No_Access;
3465
3466               when Read_Perm =>
3467                  return Read_Only;
3468            end case;
3469
3470         when Write_Only =>
3471            case P2 is
3472               when No_Access
3473                  | Read_Only
3474               =>
3475                  return No_Access;
3476
3477               when Write_Perm =>
3478                  return Write_Only;
3479            end case;
3480
3481         when Read_Write =>
3482            return P2;
3483      end case;
3484   end Glb;
3485
3486   ---------------
3487   -- Has_Alias --
3488   ---------------
3489
3490   function Has_Alias
3491     (N : Node_Id)
3492       return Boolean
3493   is
3494      function Has_Alias_Deep (Typ : Entity_Id) return Boolean;
3495      function Has_Alias_Deep (Typ : Entity_Id) return Boolean
3496      is
3497         Comp : Node_Id;
3498      begin
3499
3500         if Is_Array_Type (Typ)
3501           and then Has_Aliased_Components (Typ)
3502         then
3503            return True;
3504
3505            --  Note: Has_Aliased_Components applies only to arrays
3506
3507         elsif Is_Record_Type (Typ) then
3508            --  It is possible to have an aliased discriminant, so they must be
3509            --  checked along with normal components.
3510
3511            Comp := First_Component_Or_Discriminant (Typ);
3512            while Present (Comp) loop
3513               if Is_Aliased (Comp)
3514                 or else Is_Aliased (Etype (Comp))
3515               then
3516                  return True;
3517               end if;
3518
3519               if Has_Alias_Deep (Etype (Comp)) then
3520                  return True;
3521               end if;
3522
3523               Next_Component_Or_Discriminant (Comp);
3524            end loop;
3525            return False;
3526         else
3527            return Is_Aliased (Typ);
3528         end if;
3529      end Has_Alias_Deep;
3530
3531   begin
3532      case Nkind (N) is
3533
3534         when N_Identifier
3535            | N_Expanded_Name
3536         =>
3537            return Has_Alias_Deep (Etype (N));
3538
3539         when N_Defining_Identifier =>
3540            return Has_Alias_Deep (Etype (N));
3541
3542         when N_Type_Conversion
3543            | N_Unchecked_Type_Conversion
3544            | N_Qualified_Expression
3545         =>
3546            return Has_Alias (Expression (N));
3547
3548         when N_Parameter_Specification =>
3549            return Has_Alias (Defining_Identifier (N));
3550
3551         when N_Selected_Component =>
3552            case Nkind (Selector_Name (N)) is
3553               when N_Identifier =>
3554                  if Is_Aliased (Entity (Selector_Name (N))) then
3555                     return True;
3556                  end if;
3557
3558               when others => null;
3559
3560            end case;
3561
3562            return Has_Alias (Prefix (N));
3563
3564         when N_Indexed_Component
3565            | N_Slice
3566         =>
3567            return Has_Alias (Prefix (N));
3568
3569         when N_Explicit_Dereference =>
3570            return True;
3571
3572         when N_Function_Call =>
3573            return False;
3574
3575         when N_Attribute_Reference =>
3576            if Is_Deep (Etype (Prefix (N))) then
3577               raise Program_Error;
3578            end if;
3579            return False;
3580
3581         when others =>
3582            return False;
3583      end case;
3584   end Has_Alias;
3585
3586   -------------------------
3587   -- Has_Array_Component --
3588   -------------------------
3589
3590   function Has_Array_Component (N : Node_Id) return Boolean is
3591   begin
3592      case Nkind (N) is
3593         --  Base identifier. There is no array component here.
3594
3595         when N_Identifier
3596            | N_Expanded_Name
3597            | N_Defining_Identifier
3598         =>
3599            return False;
3600
3601         --  We check if the expression inside the conversion has an array
3602         --  component.
3603
3604         when N_Type_Conversion
3605            | N_Unchecked_Type_Conversion
3606            | N_Qualified_Expression
3607         =>
3608            return Has_Array_Component (Expression (N));
3609
3610         --  We check if the prefix has an array component
3611
3612         when N_Selected_Component =>
3613            return Has_Array_Component (Prefix (N));
3614
3615         --  We found the array component, return True
3616
3617         when N_Indexed_Component
3618            | N_Slice
3619         =>
3620            return True;
3621
3622         --  We check if the prefix has an array component
3623
3624         when N_Explicit_Dereference =>
3625            return Has_Array_Component (Prefix (N));
3626
3627         when N_Function_Call =>
3628            return False;
3629
3630         when others =>
3631            raise Program_Error;
3632      end case;
3633   end Has_Array_Component;
3634
3635   ----------------------------
3636   -- Has_Function_Component --
3637   ----------------------------
3638
3639   function Has_Function_Component (N : Node_Id) return Boolean is
3640   begin
3641      case Nkind (N) is
3642         --  Base identifier. There is no function component here.
3643
3644         when N_Identifier
3645            | N_Expanded_Name
3646            | N_Defining_Identifier
3647         =>
3648            return False;
3649
3650         --  We check if the expression inside the conversion has a function
3651         --  component.
3652
3653         when N_Type_Conversion
3654            | N_Unchecked_Type_Conversion
3655            | N_Qualified_Expression
3656         =>
3657            return Has_Function_Component (Expression (N));
3658
3659         --  We check if the prefix has a function component
3660
3661         when N_Selected_Component =>
3662            return Has_Function_Component (Prefix (N));
3663
3664         --  We check if the prefix has a function component
3665
3666         when N_Indexed_Component
3667            | N_Slice
3668         =>
3669            return Has_Function_Component (Prefix (N));
3670
3671         --  We check if the prefix has a function component
3672
3673         when N_Explicit_Dereference =>
3674            return Has_Function_Component (Prefix (N));
3675
3676         --  We found the function component, return True
3677
3678         when N_Function_Call =>
3679            return True;
3680
3681         when others =>
3682            raise Program_Error;
3683
3684      end case;
3685   end Has_Function_Component;
3686
3687   --------
3688   -- Hp --
3689   --------
3690
3691   procedure Hp (P : Perm_Env) is
3692      Elem : Perm_Tree_Maps.Key_Option;
3693
3694   begin
3695      Elem := Get_First_Key (P);
3696      while Elem.Present loop
3697         Print_Node_Briefly (Elem.K);
3698         Elem := Get_Next_Key (P);
3699      end loop;
3700   end Hp;
3701
3702   --------------------------
3703   -- Illegal_Global_Usage --
3704   --------------------------
3705
3706   procedure Illegal_Global_Usage (N : Node_Or_Entity_Id)  is
3707   begin
3708      Error_Msg_NE ("cannot use global variable & of deep type", N, N);
3709      Error_Msg_N ("\without prior declaration in a Global aspect", N);
3710
3711      Errout.Finalize (Last_Call => True);
3712      Errout.Output_Messages;
3713      Exit_Program (E_Errors);
3714   end Illegal_Global_Usage;
3715
3716   --------------------
3717   -- Is_Borrowed_In --
3718   --------------------
3719
3720   function Is_Borrowed_In (E : Entity_Id) return Boolean is
3721   begin
3722      return Is_Access_Type (Etype (E))
3723        and then not Is_Access_Constant (Etype (E));
3724   end Is_Borrowed_In;
3725
3726   -------------
3727   -- Is_Deep --
3728   -------------
3729
3730   function Is_Deep (E : Entity_Id) return Boolean is
3731      function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean;
3732
3733      function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is
3734         Decl : Node_Id;
3735         Pack_Decl : Node_Id;
3736
3737      begin
3738         if Is_Itype (E) then
3739            Decl := Associated_Node_For_Itype (E);
3740         else
3741            Decl := Parent (E);
3742         end if;
3743
3744         Pack_Decl := Parent (Parent (Decl));
3745
3746         if Nkind (Pack_Decl) /= N_Package_Declaration then
3747            return False;
3748         end if;
3749
3750         return
3751           Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl)))
3752           and then Get_SPARK_Mode_From_Annotation
3753             (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off;
3754      end Is_Private_Entity_Mode_Off;
3755   begin
3756      pragma Assert (Is_Type (E));
3757
3758      case Ekind (E) is
3759         when Scalar_Kind =>
3760            return False;
3761
3762         when Access_Kind =>
3763            return True;
3764
3765         --  Just check the depth of its component type
3766
3767         when E_Array_Type
3768            | E_Array_Subtype
3769         =>
3770            return Is_Deep (Component_Type (E));
3771
3772         when E_String_Literal_Subtype =>
3773            return False;
3774
3775         --  Per RM 8.11 for class-wide types
3776
3777         when E_Class_Wide_Subtype
3778            | E_Class_Wide_Type
3779         =>
3780            return True;
3781
3782         --  ??? What about hidden components
3783
3784         when E_Record_Type
3785            | E_Record_Subtype
3786            =>
3787            declare
3788               Elmt : Entity_Id;
3789
3790            begin
3791               Elmt := First_Component_Or_Discriminant (E);
3792               while Present (Elmt) loop
3793                  if Is_Deep (Etype (Elmt)) then
3794                     return True;
3795                  else
3796                     Next_Component_Or_Discriminant (Elmt);
3797                  end if;
3798               end loop;
3799
3800               return False;
3801            end;
3802
3803         when Private_Kind =>
3804            if Is_Private_Entity_Mode_Off (E) then
3805               return False;
3806            else
3807               if Present (Full_View (E)) then
3808                  return Is_Deep (Full_View (E));
3809               else
3810                  return True;
3811               end if;
3812            end if;
3813
3814         when E_Incomplete_Type =>
3815            return True;
3816
3817         when E_Incomplete_Subtype =>
3818            return True;
3819
3820         --  No problem with synchronized types
3821
3822         when E_Protected_Type
3823            | E_Protected_Subtype
3824            | E_Task_Subtype
3825            | E_Task_Type
3826          =>
3827            return False;
3828
3829         when E_Exception_Type =>
3830            return False;
3831
3832         when others =>
3833            raise Program_Error;
3834      end case;
3835   end Is_Deep;
3836
3837   ----------------
3838   -- Is_Shallow --
3839   ----------------
3840
3841   function Is_Shallow (E : Entity_Id) return Boolean is
3842   begin
3843      pragma Assert (Is_Type (E));
3844      return not Is_Deep (E);
3845   end Is_Shallow;
3846
3847   ------------------
3848   -- Loop_Of_Exit --
3849   ------------------
3850
3851   function Loop_Of_Exit (N : Node_Id) return Entity_Id is
3852      Nam : Node_Id := Name (N);
3853      Stmt : Node_Id := N;
3854   begin
3855      if No (Nam) then
3856         while Present (Stmt) loop
3857            Stmt := Parent (Stmt);
3858            if Nkind (Stmt) = N_Loop_Statement then
3859               Nam := Identifier (Stmt);
3860               exit;
3861            end if;
3862         end loop;
3863      end if;
3864      return Entity (Nam);
3865   end Loop_Of_Exit;
3866   ---------
3867   -- Lub --
3868   ---------
3869
3870   function Lub (P1, P2 : Perm_Kind) return Perm_Kind
3871   is
3872   begin
3873      case P1 is
3874         when No_Access =>
3875            return P2;
3876
3877         when Read_Only =>
3878            case P2 is
3879               when No_Access
3880                  | Read_Only
3881               =>
3882                  return Read_Only;
3883
3884               when Write_Perm =>
3885                  return Read_Write;
3886            end case;
3887
3888         when Write_Only =>
3889            case P2 is
3890               when No_Access
3891                  | Write_Only
3892               =>
3893                  return Write_Only;
3894
3895               when Read_Perm =>
3896                  return Read_Write;
3897            end case;
3898
3899         when Read_Write =>
3900            return Read_Write;
3901      end case;
3902   end Lub;
3903
3904   ----------------
3905   -- Merge_Envs --
3906   ----------------
3907
3908   procedure Merge_Envs
3909     (Target : in out Perm_Env;
3910      Source : in out Perm_Env)
3911   is
3912      procedure Merge_Trees
3913        (Target : Perm_Tree_Access;
3914         Source : Perm_Tree_Access);
3915
3916      procedure Merge_Trees
3917        (Target : Perm_Tree_Access;
3918         Source : Perm_Tree_Access)
3919      is
3920         procedure Apply_Glb_Tree
3921           (A : Perm_Tree_Access;
3922            P : Perm_Kind);
3923
3924         procedure Apply_Glb_Tree
3925           (A : Perm_Tree_Access;
3926            P : Perm_Kind)
3927         is
3928         begin
3929            A.all.Tree.Permission := Glb (Permission (A), P);
3930
3931            case Kind (A) is
3932               when Entire_Object =>
3933                  A.all.Tree.Children_Permission :=
3934                    Glb (Children_Permission (A), P);
3935
3936               when Reference =>
3937                  Apply_Glb_Tree (Get_All (A), P);
3938
3939               when Array_Component =>
3940                  Apply_Glb_Tree (Get_Elem (A), P);
3941
3942               when Record_Component =>
3943                  declare
3944                     Comp : Perm_Tree_Access;
3945                  begin
3946                     Comp := Perm_Tree_Maps.Get_First (Component (A));
3947                     while Comp /= null loop
3948                        Apply_Glb_Tree (Comp, P);
3949                        Comp := Perm_Tree_Maps.Get_Next (Component (A));
3950                     end loop;
3951
3952                     Apply_Glb_Tree (Other_Components (A), P);
3953                  end;
3954            end case;
3955         end Apply_Glb_Tree;
3956
3957         Perm : constant Perm_Kind :=
3958           Glb (Permission (Target), Permission (Source));
3959
3960      begin
3961         pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
3962         Target.all.Tree.Permission := Perm;
3963
3964         case Kind (Target) is
3965            when Entire_Object =>
3966               declare
3967                  Child_Perm : constant Perm_Kind :=
3968                    Children_Permission (Target);
3969
3970               begin
3971                  case Kind (Source) is
3972                  when Entire_Object =>
3973                     Target.all.Tree.Children_Permission :=
3974                       Glb (Child_Perm, Children_Permission (Source));
3975
3976                  when Reference =>
3977                     Copy_Tree (Source, Target);
3978                     Target.all.Tree.Permission := Perm;
3979                     Apply_Glb_Tree (Get_All (Target), Child_Perm);
3980
3981                  when Array_Component =>
3982                     Copy_Tree (Source, Target);
3983                     Target.all.Tree.Permission := Perm;
3984                     Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
3985
3986                  when Record_Component =>
3987                     Copy_Tree (Source, Target);
3988                     Target.all.Tree.Permission := Perm;
3989                     declare
3990                        Comp : Perm_Tree_Access;
3991
3992                     begin
3993                        Comp :=
3994                          Perm_Tree_Maps.Get_First (Component (Target));
3995                        while Comp /= null loop
3996                           --  Apply glb tree on every component subtree
3997
3998                           Apply_Glb_Tree (Comp, Child_Perm);
3999                           Comp := Perm_Tree_Maps.Get_Next
4000                             (Component (Target));
4001                        end loop;
4002                     end;
4003                     Apply_Glb_Tree (Other_Components (Target), Child_Perm);
4004
4005                  end case;
4006               end;
4007            when Reference =>
4008               case Kind (Source) is
4009               when Entire_Object =>
4010                  Apply_Glb_Tree (Get_All (Target),
4011                                  Children_Permission (Source));
4012
4013               when Reference =>
4014                  Merge_Trees (Get_All (Target), Get_All (Source));
4015
4016               when others =>
4017                  raise Program_Error;
4018
4019               end case;
4020
4021            when Array_Component =>
4022               case Kind (Source) is
4023               when Entire_Object =>
4024                  Apply_Glb_Tree (Get_Elem (Target),
4025                                  Children_Permission (Source));
4026
4027               when Array_Component =>
4028                  Merge_Trees (Get_Elem (Target), Get_Elem (Source));
4029
4030               when others =>
4031                  raise Program_Error;
4032
4033               end case;
4034
4035            when Record_Component =>
4036               case Kind (Source) is
4037               when Entire_Object =>
4038                  declare
4039                     Child_Perm : constant Perm_Kind :=
4040                       Children_Permission (Source);
4041
4042                     Comp : Perm_Tree_Access;
4043
4044                  begin
4045                     Comp := Perm_Tree_Maps.Get_First
4046                       (Component (Target));
4047                     while Comp /= null loop
4048                        --  Apply glb tree on every component subtree
4049
4050                        Apply_Glb_Tree (Comp, Child_Perm);
4051                        Comp :=
4052                          Perm_Tree_Maps.Get_Next (Component (Target));
4053                     end loop;
4054                     Apply_Glb_Tree (Other_Components (Target), Child_Perm);
4055                  end;
4056
4057               when Record_Component =>
4058                  declare
4059                     Key_Source : Perm_Tree_Maps.Key_Option;
4060                     CompTarget : Perm_Tree_Access;
4061                     CompSource : Perm_Tree_Access;
4062
4063                  begin
4064                     Key_Source := Perm_Tree_Maps.Get_First_Key
4065                       (Component (Source));
4066
4067                     while Key_Source.Present loop
4068                        CompSource := Perm_Tree_Maps.Get
4069                          (Component (Source), Key_Source.K);
4070                        CompTarget := Perm_Tree_Maps.Get
4071                          (Component (Target), Key_Source.K);
4072
4073                        pragma Assert (CompSource /= null);
4074                        Merge_Trees (CompTarget, CompSource);
4075
4076                        Key_Source := Perm_Tree_Maps.Get_Next_Key
4077                          (Component (Source));
4078                     end loop;
4079
4080                     Merge_Trees (Other_Components (Target),
4081                                  Other_Components (Source));
4082                  end;
4083
4084               when others =>
4085                  raise Program_Error;
4086
4087               end case;
4088         end case;
4089      end Merge_Trees;
4090
4091      CompTarget : Perm_Tree_Access;
4092      CompSource : Perm_Tree_Access;
4093      KeyTarget : Perm_Tree_Maps.Key_Option;
4094
4095   begin
4096      KeyTarget := Get_First_Key (Target);
4097      --  Iterate over every tree of the environment in the target, and merge
4098      --  it with the source if there is such a similar one that exists. If
4099      --  there is none, then skip.
4100      while KeyTarget.Present loop
4101
4102         CompSource := Get (Source, KeyTarget.K);
4103         CompTarget := Get (Target, KeyTarget.K);
4104
4105         pragma Assert (CompTarget /= null);
4106
4107         if CompSource /= null then
4108            Merge_Trees (CompTarget, CompSource);
4109            Remove (Source, KeyTarget.K);
4110         end if;
4111
4112         KeyTarget := Get_Next_Key (Target);
4113      end loop;
4114
4115      --  Iterate over every tree of the environment of the source. And merge
4116      --  again. If there is not any tree of the target then just copy the tree
4117      --  from source to target.
4118      declare
4119         KeySource : Perm_Tree_Maps.Key_Option;
4120      begin
4121         KeySource := Get_First_Key (Source);
4122         while KeySource.Present loop
4123
4124            CompSource := Get (Source, KeySource.K);
4125            CompTarget := Get (Target, KeySource.K);
4126
4127            if CompTarget = null then
4128               CompTarget := new Perm_Tree_Wrapper'(CompSource.all);
4129               Copy_Tree (CompSource, CompTarget);
4130               Set (Target, KeySource.K, CompTarget);
4131            else
4132               Merge_Trees (CompTarget, CompSource);
4133            end if;
4134
4135            KeySource := Get_Next_Key (Source);
4136         end loop;
4137      end;
4138
4139      Free_Env (Source);
4140   end Merge_Envs;
4141
4142   ----------------
4143   -- Perm_Error --
4144   ----------------
4145
4146   procedure Perm_Error
4147     (N : Node_Id;
4148      Perm : Perm_Kind;
4149      Found_Perm : Perm_Kind)
4150   is
4151      procedure Set_Root_Object
4152        (Path  : Node_Id;
4153         Obj   : out Entity_Id;
4154         Deref : out Boolean);
4155      --  Set the root object Obj, and whether the path contains a dereference,
4156      --  from a path Path.
4157
4158      ---------------------
4159      -- Set_Root_Object --
4160      ---------------------
4161
4162      procedure Set_Root_Object
4163        (Path  : Node_Id;
4164         Obj   : out Entity_Id;
4165         Deref : out Boolean)
4166      is
4167      begin
4168         case Nkind (Path) is
4169            when N_Identifier
4170               | N_Expanded_Name
4171            =>
4172               Obj := Entity (Path);
4173               Deref := False;
4174
4175            when N_Type_Conversion
4176               | N_Unchecked_Type_Conversion
4177               | N_Qualified_Expression
4178            =>
4179               Set_Root_Object (Expression (Path), Obj, Deref);
4180
4181            when N_Indexed_Component
4182               | N_Selected_Component
4183               | N_Slice
4184            =>
4185               Set_Root_Object (Prefix (Path), Obj, Deref);
4186
4187            when N_Explicit_Dereference =>
4188               Set_Root_Object (Prefix (Path), Obj, Deref);
4189               Deref := True;
4190
4191            when others =>
4192               raise Program_Error;
4193         end case;
4194      end Set_Root_Object;
4195
4196      --  Local variables
4197
4198      Root : Entity_Id;
4199      Is_Deref : Boolean;
4200
4201   --  Start of processing for Perm_Error
4202
4203   begin
4204      Set_Root_Object (N, Root, Is_Deref);
4205
4206      if Is_Deref then
4207         Error_Msg_NE
4208           ("insufficient permission on dereference from &", N, Root);
4209      else
4210         Error_Msg_NE ("insufficient permission for &", N, Root);
4211      end if;
4212
4213      Perm_Mismatch (Perm, Found_Perm, N);
4214   end Perm_Error;
4215
4216   -------------------------------
4217   -- Perm_Error_Subprogram_End --
4218   -------------------------------
4219
4220   procedure Perm_Error_Subprogram_End
4221     (E          : Entity_Id;
4222      Subp       : Entity_Id;
4223      Perm       : Perm_Kind;
4224      Found_Perm : Perm_Kind)
4225   is
4226   begin
4227      Error_Msg_Node_2 := Subp;
4228      Error_Msg_NE ("insufficient permission for & when returning from &",
4229                    Subp, E);
4230      Perm_Mismatch (Perm, Found_Perm, Subp);
4231   end Perm_Error_Subprogram_End;
4232
4233   ------------------
4234   -- Process_Path --
4235   ------------------
4236
4237   procedure Process_Path (N : Node_Id) is
4238      Root : constant Entity_Id := Get_Enclosing_Object (N);
4239   begin
4240      --  We ignore if yielding to synchronized
4241
4242      if Present (Root)
4243        and then Is_Synchronized_Object (Root)
4244      then
4245         return;
4246      end if;
4247
4248      --  We ignore shallow unaliased. They are checked in flow analysis,
4249      --  allowing backward compatibility.
4250
4251      if not Has_Alias (N)
4252        and then Is_Shallow (Etype (N))
4253      then
4254         return;
4255      end if;
4256
4257      declare
4258         Perm_N : constant Perm_Kind := Get_Perm (N);
4259
4260      begin
4261
4262         case Current_Checking_Mode is
4263            --  Check permission R, do nothing
4264
4265            when Read =>
4266               if Perm_N not in Read_Perm then
4267                  Perm_Error (N, Read_Only, Perm_N);
4268               end if;
4269
4270            --  If shallow type no need for RW, only R
4271
4272            when Move =>
4273               if Is_Shallow (Etype (N)) then
4274                  if Perm_N not in Read_Perm then
4275                     Perm_Error (N, Read_Only, Perm_N);
4276                  end if;
4277               else
4278                  --  Check permission RW if deep
4279
4280                  if Perm_N /= Read_Write then
4281                     Perm_Error (N, Read_Write, Perm_N);
4282                  end if;
4283
4284                  declare
4285                     --  Set permission to W to the path and any of its prefix
4286
4287                     Tree : constant Perm_Tree_Access :=
4288                       Set_Perm_Prefixes_Move (N, Move);
4289
4290                  begin
4291                     if Tree = null then
4292                        --  We went through a function call, no permission to
4293                        --  modify.
4294
4295                        return;
4296                     end if;
4297
4298                     --  Set permissions to
4299                     --  No for any extension with more .all
4300                     --  W for any deep extension with same number of .all
4301                     --  RW for any shallow extension with same number of .all
4302
4303                     Set_Perm_Extensions_Move (Tree, Etype (N));
4304                  end;
4305               end if;
4306
4307            --  Check permission RW
4308
4309            when Super_Move =>
4310               if Perm_N /= Read_Write then
4311                  Perm_Error (N, Read_Write, Perm_N);
4312               end if;
4313
4314               declare
4315                  --  Set permission to No to the path and any of its prefix up
4316                  --  to the first .all and then W.
4317
4318                  Tree : constant Perm_Tree_Access :=
4319                    Set_Perm_Prefixes_Move (N, Super_Move);
4320
4321               begin
4322                  if Tree = null then
4323                     --  We went through a function call, no permission to
4324                     --  modify.
4325
4326                     return;
4327                  end if;
4328
4329                  --  Set permissions to No on any strict extension of the path
4330
4331                  Set_Perm_Extensions (Tree, No_Access);
4332               end;
4333
4334            --  Check permission W
4335
4336            when Assign =>
4337               if Perm_N not in Write_Perm then
4338                  Perm_Error (N, Write_Only, Perm_N);
4339               end if;
4340
4341               --  If the tree has an array component, then the permissions do
4342               --  not get modified by the assignment.
4343
4344               if Has_Array_Component (N) then
4345                  return;
4346               end if;
4347
4348               --  Same if has function component
4349
4350               if Has_Function_Component (N) then
4351                  return;
4352               end if;
4353
4354               declare
4355                  --  Get the permission tree for the path
4356
4357                  Tree : constant Perm_Tree_Access :=
4358                    Get_Perm_Tree (N);
4359
4360                  Dummy : Perm_Tree_Access;
4361
4362               begin
4363                  if Tree = null then
4364                     --  We went through a function call, no permission to
4365                     --  modify.
4366
4367                     return;
4368                  end if;
4369
4370                  --  Set permission RW for it and all of its extensions
4371
4372                  Tree.all.Tree.Permission := Read_Write;
4373
4374                  Set_Perm_Extensions (Tree, Read_Write);
4375
4376                  --  Normalize the permission tree
4377
4378                  Dummy := Set_Perm_Prefixes_Assign (N);
4379               end;
4380
4381            --  Check permission W
4382
4383            when Borrow_Out =>
4384               if Perm_N not in Write_Perm then
4385                  Perm_Error (N, Write_Only, Perm_N);
4386               end if;
4387
4388               declare
4389                  --  Set permission to No to the path and any of its prefixes
4390
4391                  Tree : constant Perm_Tree_Access :=
4392                    Set_Perm_Prefixes_Borrow_Out (N);
4393
4394               begin
4395                  if Tree = null then
4396                     --  We went through a function call, no permission to
4397                     --  modify.
4398
4399                     return;
4400                  end if;
4401
4402                  --  Set permissions to No on any strict extension of the path
4403
4404                  Set_Perm_Extensions (Tree, No_Access);
4405               end;
4406
4407            when Observe =>
4408               if Perm_N not in Read_Perm then
4409                  Perm_Error (N, Read_Only, Perm_N);
4410               end if;
4411
4412               if Is_By_Copy_Type (Etype (N)) then
4413                  return;
4414               end if;
4415
4416               declare
4417                  --  Set permission to No on the path and any of its prefixes
4418
4419                  Tree : constant Perm_Tree_Access :=
4420                    Set_Perm_Prefixes_Observe (N);
4421
4422               begin
4423                  if Tree = null then
4424                     --  We went through a function call, no permission to
4425                     --  modify.
4426
4427                     return;
4428                  end if;
4429
4430                  --  Set permissions to No on any strict extension of the path
4431
4432                  Set_Perm_Extensions (Tree, Read_Only);
4433               end;
4434         end case;
4435      end;
4436   end Process_Path;
4437
4438   -------------------------
4439   -- Return_Declarations --
4440   -------------------------
4441
4442   procedure Return_Declarations (L : List_Id) is
4443
4444      procedure Return_Declaration (Decl : Node_Id);
4445      --  Check correct permissions for every declared object
4446
4447      ------------------------
4448      -- Return_Declaration --
4449      ------------------------
4450
4451      procedure Return_Declaration (Decl : Node_Id) is
4452      begin
4453         if Nkind (Decl) = N_Object_Declaration then
4454            --  Check RW for object declared, unless the object has never been
4455            --  initialized.
4456
4457            if Get (Current_Initialization_Map,
4458                    Unique_Entity (Defining_Identifier (Decl))) = False
4459            then
4460               return;
4461            end if;
4462
4463            --  We ignore shallow unaliased. They are checked in flow analysis,
4464            --  allowing backward compatibility.
4465
4466            if not Has_Alias (Defining_Identifier (Decl))
4467              and then Is_Shallow (Etype (Defining_Identifier (Decl)))
4468            then
4469               return;
4470            end if;
4471
4472            declare
4473               Elem : constant Perm_Tree_Access :=
4474                 Get (Current_Perm_Env,
4475                      Unique_Entity (Defining_Identifier (Decl)));
4476
4477            begin
4478               if Elem = null then
4479                  --  Here we are on a declaration. Hence it should have been
4480                  --  added in the environment when analyzing this node with
4481                  --  mode Read. Hence it is not possible to find a null
4482                  --  pointer here.
4483
4484                  --  Hash_Table_Error
4485                  raise Program_Error;
4486               end if;
4487
4488               if Permission (Elem) /= Read_Write then
4489                  Perm_Error (Decl, Read_Write, Permission (Elem));
4490               end if;
4491            end;
4492         end if;
4493      end Return_Declaration;
4494
4495      --  Local Variables
4496
4497      N : Node_Id;
4498
4499   --  Start of processing for Return_Declarations
4500
4501   begin
4502      N := First (L);
4503      while Present (N) loop
4504         Return_Declaration (N);
4505         Next (N);
4506      end loop;
4507   end Return_Declarations;
4508
4509   --------------------
4510   -- Return_Globals --
4511   --------------------
4512
4513   procedure Return_Globals (Subp : Entity_Id) is
4514
4515      procedure Return_Globals_From_List
4516        (First_Item : Node_Id;
4517         Kind       : Formal_Kind);
4518      --  Return global items from the list starting at Item
4519
4520      procedure Return_Globals_Of_Mode (Global_Mode : Name_Id);
4521      --  Return global items for the mode Global_Mode
4522
4523      ------------------------------
4524      -- Return_Globals_From_List --
4525      ------------------------------
4526
4527      procedure Return_Globals_From_List
4528        (First_Item : Node_Id;
4529         Kind       : Formal_Kind)
4530      is
4531         Item : Node_Id := First_Item;
4532         E    : Entity_Id;
4533
4534      begin
4535         while Present (Item) loop
4536            E := Entity (Item);
4537
4538            --  Ignore abstract states, which play no role in pointer aliasing
4539
4540            if Ekind (E) = E_Abstract_State then
4541               null;
4542            else
4543               Return_Parameter_Or_Global (E, Kind, Subp);
4544            end if;
4545            Next_Global (Item);
4546         end loop;
4547      end Return_Globals_From_List;
4548
4549      ----------------------------
4550      -- Return_Globals_Of_Mode --
4551      ----------------------------
4552
4553      procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is
4554         Kind : Formal_Kind;
4555
4556      begin
4557         case Global_Mode is
4558            when Name_Input | Name_Proof_In =>
4559               Kind := E_In_Parameter;
4560            when Name_Output =>
4561               Kind := E_Out_Parameter;
4562            when Name_In_Out =>
4563               Kind := E_In_Out_Parameter;
4564            when others =>
4565               raise Program_Error;
4566         end case;
4567
4568         --  Return both global items from Global and Refined_Global pragmas
4569
4570         Return_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
4571         Return_Globals_From_List
4572           (First_Global (Subp, Global_Mode, Refined => True), Kind);
4573      end Return_Globals_Of_Mode;
4574
4575   --  Start of processing for Return_Globals
4576
4577   begin
4578      Return_Globals_Of_Mode (Name_Proof_In);
4579      Return_Globals_Of_Mode (Name_Input);
4580      Return_Globals_Of_Mode (Name_Output);
4581      Return_Globals_Of_Mode (Name_In_Out);
4582   end Return_Globals;
4583
4584   --------------------------------
4585   -- Return_Parameter_Or_Global --
4586   --------------------------------
4587
4588   procedure Return_Parameter_Or_Global
4589     (Id   : Entity_Id;
4590      Mode : Formal_Kind;
4591      Subp : Entity_Id)
4592   is
4593      Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
4594      pragma Assert (Elem /= null);
4595
4596   begin
4597      --  Shallow unaliased parameters and globals cannot introduce pointer
4598      --  aliasing.
4599
4600      if not Has_Alias (Id) and then Is_Shallow (Etype (Id)) then
4601         null;
4602
4603      --  Observed IN parameters and globals need not return a permission to
4604      --  the caller.
4605
4606      elsif Mode = E_In_Parameter and then not Is_Borrowed_In (Id) then
4607         null;
4608
4609      --  All other parameters and globals should return with mode RW to the
4610      --  caller.
4611
4612      else
4613         if Permission (Elem) /= Read_Write then
4614            Perm_Error_Subprogram_End
4615              (E          => Id,
4616               Subp       => Subp,
4617               Perm       => Read_Write,
4618               Found_Perm => Permission (Elem));
4619         end if;
4620      end if;
4621   end Return_Parameter_Or_Global;
4622
4623   -----------------------
4624   -- Return_Parameters --
4625   -----------------------
4626
4627   procedure Return_Parameters (Subp : Entity_Id) is
4628      Formal : Entity_Id;
4629
4630   begin
4631      Formal := First_Formal (Subp);
4632      while Present (Formal) loop
4633         Return_Parameter_Or_Global (Formal, Ekind (Formal), Subp);
4634         Next_Formal (Formal);
4635      end loop;
4636   end Return_Parameters;
4637
4638   -------------------------
4639   -- Set_Perm_Extensions --
4640   -------------------------
4641
4642   procedure Set_Perm_Extensions
4643     (T : Perm_Tree_Access;
4644      P : Perm_Kind)
4645   is
4646      procedure Free_Perm_Tree_Children (T : Perm_Tree_Access);
4647
4648      procedure Free_Perm_Tree_Children (T : Perm_Tree_Access)
4649      is
4650      begin
4651         case Kind (T) is
4652            when Entire_Object =>
4653               null;
4654
4655            when Reference =>
4656               Free_Perm_Tree (T.all.Tree.Get_All);
4657
4658            when Array_Component =>
4659               Free_Perm_Tree (T.all.Tree.Get_Elem);
4660
4661            --  Free every Component subtree
4662
4663            when Record_Component =>
4664               declare
4665                  Comp : Perm_Tree_Access;
4666
4667               begin
4668                  Comp := Perm_Tree_Maps.Get_First (Component (T));
4669                  while Comp /= null loop
4670                     Free_Perm_Tree (Comp);
4671                     Comp := Perm_Tree_Maps.Get_Next (Component (T));
4672                  end loop;
4673
4674                  Free_Perm_Tree (T.all.Tree.Other_Components);
4675               end;
4676         end case;
4677      end Free_Perm_Tree_Children;
4678
4679      Son : constant Perm_Tree :=
4680        Perm_Tree'
4681          (Kind                => Entire_Object,
4682           Is_Node_Deep        => Is_Node_Deep (T),
4683           Permission          => Permission (T),
4684           Children_Permission => P);
4685
4686   begin
4687      Free_Perm_Tree_Children (T);
4688      T.all.Tree := Son;
4689   end Set_Perm_Extensions;
4690
4691   ------------------------------
4692   -- Set_Perm_Extensions_Move --
4693   ------------------------------
4694
4695   procedure Set_Perm_Extensions_Move
4696     (T : Perm_Tree_Access;
4697      E : Entity_Id)
4698   is
4699   begin
4700      if not Is_Node_Deep (T) then
4701         --  We are a shallow extension with same number of .all
4702
4703         Set_Perm_Extensions (T, Read_Write);
4704         return;
4705      end if;
4706
4707      --  We are a deep extension here (or the moved deep path)
4708
4709      T.all.Tree.Permission := Write_Only;
4710
4711      case T.all.Tree.Kind is
4712         --  Unroll the tree depending on the type
4713
4714         when Entire_Object =>
4715            case Ekind (E) is
4716               when Scalar_Kind
4717                  | E_String_Literal_Subtype
4718               =>
4719                  Set_Perm_Extensions (T, No_Access);
4720
4721               --  No need to unroll here, directly put sons to No_Access
4722
4723               when Access_Kind =>
4724                  if Ekind (E) in Access_Subprogram_Kind then
4725                     null;
4726                  else
4727                     Set_Perm_Extensions (T, No_Access);
4728                  end if;
4729
4730               --  No unrolling done, too complicated
4731
4732               when E_Class_Wide_Subtype
4733                  | E_Class_Wide_Type
4734                  | E_Incomplete_Type
4735                  | E_Incomplete_Subtype
4736                  | E_Exception_Type
4737                  | E_Task_Type
4738                  | E_Task_Subtype
4739               =>
4740                  Set_Perm_Extensions (T, No_Access);
4741
4742               --  Expand the tree. Replace the node with Array component.
4743
4744               when E_Array_Type
4745                  | E_Array_Subtype =>
4746                  declare
4747                     Son : Perm_Tree_Access;
4748
4749                  begin
4750                     Son := new Perm_Tree_Wrapper'
4751                       (Tree =>
4752                          (Kind                => Entire_Object,
4753                           Is_Node_Deep        => Is_Node_Deep (T),
4754                           Permission          => Read_Write,
4755                           Children_Permission => Read_Write));
4756
4757                     Set_Perm_Extensions_Move (Son, Component_Type (E));
4758
4759                     --  We change the current node from Entire_Object to
4760                     --  Reference with Write_Only and the previous son.
4761
4762                     pragma Assert (Is_Node_Deep (T));
4763
4764                     T.all.Tree := (Kind         => Array_Component,
4765                                    Is_Node_Deep => Is_Node_Deep (T),
4766                                    Permission   => Write_Only,
4767                                    Get_Elem     => Son);
4768                  end;
4769
4770               --  Unroll, and set permission extensions with component type
4771
4772               when E_Record_Type
4773                  | E_Record_Subtype
4774                  | E_Record_Type_With_Private
4775                  | E_Record_Subtype_With_Private
4776                  | E_Protected_Type
4777                  | E_Protected_Subtype
4778               =>
4779                  declare
4780                     --  Expand the tree. Replace the node with
4781                     --  Record_Component.
4782
4783                     Elem : Node_Id;
4784
4785                     Son : Perm_Tree_Access;
4786
4787                  begin
4788                     --  We change the current node from Entire_Object to
4789                     --  Record_Component with same permission and an empty
4790                     --  hash table as component list.
4791
4792                     pragma Assert (Is_Node_Deep (T));
4793
4794                     T.all.Tree :=
4795                       (Kind             => Record_Component,
4796                        Is_Node_Deep     => Is_Node_Deep (T),
4797                        Permission       => Write_Only,
4798                        Component        => Perm_Tree_Maps.Nil,
4799                        Other_Components =>
4800                           new Perm_Tree_Wrapper'
4801                          (Tree =>
4802                               (Kind                => Entire_Object,
4803                                Is_Node_Deep        => True,
4804                                Permission          => Read_Write,
4805                                Children_Permission => Read_Write)
4806                          )
4807                       );
4808
4809                     --  We fill the hash table with all sons of the record,
4810                     --  with basic Entire_Objects nodes.
4811                     Elem := First_Component_Or_Discriminant (E);
4812                     while Present (Elem) loop
4813                        Son := new Perm_Tree_Wrapper'
4814                          (Tree =>
4815                             (Kind                => Entire_Object,
4816                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
4817                              Permission          => Read_Write,
4818                              Children_Permission => Read_Write));
4819
4820                        Set_Perm_Extensions_Move (Son, Etype (Elem));
4821
4822                        Perm_Tree_Maps.Set
4823                          (T.all.Tree.Component, Elem, Son);
4824
4825                        Next_Component_Or_Discriminant (Elem);
4826                     end loop;
4827                  end;
4828
4829               when E_Private_Type
4830                  | E_Private_Subtype
4831                  | E_Limited_Private_Type
4832                  | E_Limited_Private_Subtype
4833               =>
4834                  Set_Perm_Extensions_Move (T, Underlying_Type (E));
4835
4836               when others =>
4837                  raise Program_Error;
4838            end case;
4839
4840         when Reference =>
4841            --  Now the son does not have the same number of .all
4842            Set_Perm_Extensions (T, No_Access);
4843
4844         when Array_Component =>
4845            Set_Perm_Extensions_Move (Get_Elem (T), Component_Type (E));
4846
4847         when Record_Component =>
4848            declare
4849               Comp : Perm_Tree_Access;
4850               It : Node_Id;
4851
4852            begin
4853               It := First_Component_Or_Discriminant (E);
4854               while It /= Empty loop
4855                  Comp := Perm_Tree_Maps.Get (Component (T), It);
4856                  pragma Assert (Comp /= null);
4857                  Set_Perm_Extensions_Move (Comp, It);
4858                  It := Next_Component_Or_Discriminant (E);
4859               end loop;
4860
4861               Set_Perm_Extensions (Other_Components (T), No_Access);
4862            end;
4863      end case;
4864   end Set_Perm_Extensions_Move;
4865
4866   ------------------------------
4867   -- Set_Perm_Prefixes_Assign --
4868   ------------------------------
4869
4870   function Set_Perm_Prefixes_Assign
4871     (N : Node_Id)
4872       return Perm_Tree_Access
4873   is
4874      C : constant Perm_Tree_Access := Get_Perm_Tree (N);
4875
4876   begin
4877      pragma Assert (Current_Checking_Mode = Assign);
4878
4879      --  The function should not be called if has_function_component
4880
4881      pragma Assert (C /= null);
4882
4883      case Kind (C) is
4884         when Entire_Object =>
4885            pragma Assert (Children_Permission (C) = Read_Write);
4886            C.all.Tree.Permission := Read_Write;
4887
4888         when Reference =>
4889            pragma Assert (Get_All (C) /= null);
4890
4891            C.all.Tree.Permission :=
4892              Lub (Permission (C), Permission (Get_All (C)));
4893
4894         when Array_Component =>
4895            pragma Assert (C.all.Tree.Get_Elem /= null);
4896
4897            --  Given that it is not possible to know which element has been
4898            --  assigned, then the permissions do not get changed in case of
4899            --  Array_Component.
4900
4901            null;
4902
4903         when Record_Component =>
4904            declare
4905               Perm : Perm_Kind := Read_Write;
4906
4907               Comp : Perm_Tree_Access;
4908
4909            begin
4910               --  We take the Glb of all the descendants, and then update the
4911               --  permission of the node with it.
4912               Comp := Perm_Tree_Maps.Get_First (Component (C));
4913               while Comp /= null loop
4914                  Perm := Glb (Perm, Permission (Comp));
4915                  Comp := Perm_Tree_Maps.Get_Next (Component (C));
4916               end loop;
4917
4918               Perm := Glb (Perm, Permission (Other_Components (C)));
4919
4920               C.all.Tree.Permission := Lub (Permission (C), Perm);
4921            end;
4922      end case;
4923
4924      case Nkind (N) is
4925         --  Base identifier. End recursion here.
4926
4927         when N_Identifier
4928            | N_Expanded_Name
4929            | N_Defining_Identifier
4930         =>
4931            return null;
4932
4933         when N_Type_Conversion
4934            | N_Unchecked_Type_Conversion
4935            | N_Qualified_Expression
4936         =>
4937            return Set_Perm_Prefixes_Assign (Expression (N));
4938
4939         when N_Parameter_Specification =>
4940            raise Program_Error;
4941
4942         --  Continue recursion on prefix
4943
4944         when N_Selected_Component =>
4945            return Set_Perm_Prefixes_Assign (Prefix (N));
4946
4947         --  Continue recursion on prefix
4948
4949         when N_Indexed_Component
4950            | N_Slice
4951         =>
4952            return Set_Perm_Prefixes_Assign (Prefix (N));
4953
4954         --  Continue recursion on prefix
4955
4956         when N_Explicit_Dereference =>
4957            return Set_Perm_Prefixes_Assign (Prefix (N));
4958
4959         when N_Function_Call =>
4960            raise Program_Error;
4961
4962         when others =>
4963            raise Program_Error;
4964
4965      end case;
4966   end Set_Perm_Prefixes_Assign;
4967
4968   ----------------------------------
4969   -- Set_Perm_Prefixes_Borrow_Out --
4970   ----------------------------------
4971
4972   function Set_Perm_Prefixes_Borrow_Out
4973     (N : Node_Id)
4974       return Perm_Tree_Access
4975   is
4976   begin
4977      pragma Assert (Current_Checking_Mode = Borrow_Out);
4978
4979      case Nkind (N) is
4980         --  Base identifier. Set permission to No.
4981
4982         when N_Identifier
4983            | N_Expanded_Name
4984         =>
4985            declare
4986               P : constant Node_Id := Entity (N);
4987
4988               C : constant Perm_Tree_Access :=
4989                 Get (Current_Perm_Env, Unique_Entity (P));
4990
4991               pragma Assert (C /= null);
4992
4993            begin
4994               --  Setting the initialization map to True, so that this
4995               --  variable cannot be ignored anymore when looking at end
4996               --  of elaboration of package.
4997
4998               Set (Current_Initialization_Map, Unique_Entity (P), True);
4999
5000               C.all.Tree.Permission := No_Access;
5001               return C;
5002            end;
5003
5004         when N_Type_Conversion
5005            | N_Unchecked_Type_Conversion
5006            | N_Qualified_Expression
5007         =>
5008            return Set_Perm_Prefixes_Borrow_Out (Expression (N));
5009
5010         when N_Parameter_Specification
5011            | N_Defining_Identifier
5012         =>
5013            raise Program_Error;
5014
5015            --  We set the permission tree of its prefix, and then we extract
5016            --  our subtree from the returned pointer and assign an adequate
5017            --  permission to it, if unfolded. If folded, we unroll the tree
5018            --  in one step.
5019
5020         when N_Selected_Component =>
5021            declare
5022               C : constant Perm_Tree_Access :=
5023                 Set_Perm_Prefixes_Borrow_Out (Prefix (N));
5024
5025            begin
5026               if C = null then
5027                  --  We went through a function call, do nothing
5028
5029                  return null;
5030               end if;
5031
5032               --  The permission of the returned node should be No
5033
5034               pragma Assert (Permission (C) = No_Access);
5035
5036               pragma Assert (Kind (C) = Entire_Object
5037                              or else Kind (C) = Record_Component);
5038
5039               if Kind (C) = Record_Component then
5040                  --  The tree is unfolded. We just modify the permission and
5041                  --  return the record subtree.
5042
5043                  declare
5044                     Selected_Component : constant Entity_Id :=
5045                       Entity (Selector_Name (N));
5046
5047                     Selected_C : Perm_Tree_Access :=
5048                       Perm_Tree_Maps.Get
5049                         (Component (C), Selected_Component);
5050
5051                  begin
5052                     if Selected_C = null then
5053                        Selected_C := Other_Components (C);
5054                     end if;
5055
5056                     pragma Assert (Selected_C /= null);
5057
5058                     Selected_C.all.Tree.Permission := No_Access;
5059
5060                     return Selected_C;
5061                  end;
5062               elsif Kind (C) = Entire_Object then
5063                  declare
5064                     --  Expand the tree. Replace the node with
5065                     --  Record_Component.
5066
5067                     Elem : Node_Id;
5068
5069                     --  Create an empty hash table
5070
5071                     Hashtbl : Perm_Tree_Maps.Instance;
5072
5073                     --  We create the unrolled nodes, that will all have same
5074                     --  permission than parent.
5075
5076                     Son : Perm_Tree_Access;
5077
5078                     ChildrenPerm : constant Perm_Kind :=
5079                       Children_Permission (C);
5080
5081                  begin
5082                     --  We change the current node from Entire_Object to
5083                     --  Record_Component with same permission and an empty
5084                     --  hash table as component list.
5085
5086                     C.all.Tree :=
5087                       (Kind         => Record_Component,
5088                        Is_Node_Deep => Is_Node_Deep (C),
5089                        Permission   => Permission (C),
5090                        Component    => Hashtbl,
5091                        Other_Components =>
5092                           new Perm_Tree_Wrapper'
5093                          (Tree =>
5094                               (Kind                => Entire_Object,
5095                                Is_Node_Deep        => True,
5096                                Permission          => ChildrenPerm,
5097                                Children_Permission => ChildrenPerm)
5098                          ));
5099
5100                     --  We fill the hash table with all sons of the record,
5101                     --  with basic Entire_Objects nodes.
5102                     Elem := First_Component_Or_Discriminant
5103                       (Etype (Prefix (N)));
5104
5105                     while Present (Elem) loop
5106                        Son := new Perm_Tree_Wrapper'
5107                          (Tree =>
5108                             (Kind                => Entire_Object,
5109                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
5110                              Permission          => ChildrenPerm,
5111                              Children_Permission => ChildrenPerm));
5112
5113                        Perm_Tree_Maps.Set
5114                          (C.all.Tree.Component, Elem, Son);
5115
5116                        Next_Component_Or_Discriminant (Elem);
5117                     end loop;
5118
5119                     --  Now we set the right field to No_Access, and then we
5120                     --  return the tree to the sons, so that the recursion can
5121                     --  continue.
5122
5123                     declare
5124                        Selected_Component : constant Entity_Id :=
5125                          Entity (Selector_Name (N));
5126
5127                        Selected_C : Perm_Tree_Access :=
5128                          Perm_Tree_Maps.Get
5129                            (Component (C), Selected_Component);
5130
5131                     begin
5132                        if Selected_C = null then
5133                           Selected_C := Other_Components (C);
5134                        end if;
5135
5136                        pragma Assert (Selected_C /= null);
5137
5138                        Selected_C.all.Tree.Permission := No_Access;
5139
5140                        return Selected_C;
5141                     end;
5142                  end;
5143               else
5144                  raise Program_Error;
5145               end if;
5146            end;
5147
5148            --  We set the permission tree of its prefix, and then we extract
5149            --  from the returned pointer the subtree and assign an adequate
5150            --  permission to it, if unfolded. If folded, we unroll the tree in
5151            --  one step.
5152
5153         when N_Indexed_Component
5154            | N_Slice
5155         =>
5156            declare
5157               C : constant Perm_Tree_Access :=
5158                 Set_Perm_Prefixes_Borrow_Out (Prefix (N));
5159
5160            begin
5161               if C = null then
5162                  --  We went through a function call, do nothing
5163
5164                  return null;
5165               end if;
5166
5167               --  The permission of the returned node should be either W
5168               --  (because the recursive call sets <= Write_Only) or No
5169               --  (if another path has been moved with 'Access).
5170
5171               pragma Assert (Permission (C) = No_Access);
5172
5173               pragma Assert (Kind (C) = Entire_Object
5174                              or else Kind (C) = Array_Component);
5175
5176               if Kind (C) = Array_Component then
5177                  --  The tree is unfolded. We just modify the permission and
5178                  --  return the elem subtree.
5179
5180                  pragma Assert (Get_Elem (C) /= null);
5181
5182                  C.all.Tree.Get_Elem.all.Tree.Permission := No_Access;
5183
5184                  return Get_Elem (C);
5185               elsif Kind (C) = Entire_Object then
5186                  declare
5187                     --  Expand the tree. Replace node with Array_Component.
5188
5189                     Son : Perm_Tree_Access;
5190
5191                  begin
5192                     Son := new Perm_Tree_Wrapper'
5193                       (Tree =>
5194                          (Kind                => Entire_Object,
5195                           Is_Node_Deep        => Is_Node_Deep (C),
5196                           Permission          => No_Access,
5197                           Children_Permission => Children_Permission (C)));
5198
5199                     --  We change the current node from Entire_Object
5200                     --  to Array_Component with same permission and the
5201                     --  previously defined son.
5202
5203                     C.all.Tree := (Kind         => Array_Component,
5204                                    Is_Node_Deep => Is_Node_Deep (C),
5205                                    Permission   => No_Access,
5206                                    Get_Elem     => Son);
5207
5208                     return Get_Elem (C);
5209                  end;
5210               else
5211                  raise Program_Error;
5212               end if;
5213            end;
5214
5215            --  We set the permission tree of its prefix, and then we extract
5216            --  from the returned pointer the subtree and assign an adequate
5217            --  permission to it, if unfolded. If folded, we unroll the tree
5218            --  at one step.
5219
5220         when N_Explicit_Dereference =>
5221            declare
5222               C : constant Perm_Tree_Access :=
5223                 Set_Perm_Prefixes_Borrow_Out (Prefix (N));
5224
5225            begin
5226               if C = null then
5227                  --  We went through a function call. Do nothing.
5228
5229                  return null;
5230               end if;
5231
5232               --  The permission of the returned node should be No
5233
5234               pragma Assert (Permission (C) = No_Access);
5235               pragma Assert (Kind (C) = Entire_Object
5236                              or else Kind (C) = Reference);
5237
5238               if Kind (C) = Reference then
5239                  --  The tree is unfolded. We just modify the permission and
5240                  --  return the elem subtree.
5241
5242                  pragma Assert (Get_All (C) /= null);
5243
5244                  C.all.Tree.Get_All.all.Tree.Permission := No_Access;
5245
5246                  return Get_All (C);
5247               elsif Kind (C) = Entire_Object then
5248                  declare
5249                     --  Expand the tree. Replace the node with Reference.
5250
5251                     Son : Perm_Tree_Access;
5252
5253                  begin
5254                     Son := new Perm_Tree_Wrapper'
5255                       (Tree =>
5256                          (Kind                => Entire_Object,
5257                           Is_Node_Deep        => Is_Deep (Etype (N)),
5258                           Permission          => No_Access,
5259                           Children_Permission => Children_Permission (C)));
5260
5261                     --  We change the current node from Entire_Object to
5262                     --  Reference with No_Access and the previous son.
5263
5264                     pragma Assert (Is_Node_Deep (C));
5265
5266                     C.all.Tree := (Kind         => Reference,
5267                                    Is_Node_Deep => Is_Node_Deep (C),
5268                                    Permission   => No_Access,
5269                                    Get_All      => Son);
5270
5271                     return Get_All (C);
5272                  end;
5273               else
5274                  raise Program_Error;
5275               end if;
5276            end;
5277
5278         when N_Function_Call =>
5279            return null;
5280
5281         when others =>
5282            raise Program_Error;
5283      end case;
5284   end Set_Perm_Prefixes_Borrow_Out;
5285
5286   ----------------------------
5287   -- Set_Perm_Prefixes_Move --
5288   ----------------------------
5289
5290   function Set_Perm_Prefixes_Move
5291     (N : Node_Id; Mode : Checking_Mode)
5292       return Perm_Tree_Access
5293   is
5294   begin
5295      case Nkind (N) is
5296
5297         --  Base identifier. Set permission to W or No depending on Mode.
5298
5299         when N_Identifier
5300            | N_Expanded_Name
5301         =>
5302            declare
5303               P : constant Node_Id := Entity (N);
5304               C : constant Perm_Tree_Access :=
5305                     Get (Current_Perm_Env, Unique_Entity (P));
5306
5307            begin
5308               --  The base tree can be RW (first move from this base path) or
5309               --  W (already some extensions values moved), or even No_Access
5310               --  (extensions moved with 'Access). But it cannot be Read_Only
5311               --  (we get an error).
5312
5313               if Permission (C) = Read_Only then
5314                  raise Unrecoverable_Error;
5315               end if;
5316
5317               --  Setting the initialization map to True, so that this
5318               --  variable cannot be ignored anymore when looking at end
5319               --  of elaboration of package.
5320
5321               Set (Current_Initialization_Map, Unique_Entity (P), True);
5322
5323               if C = null then
5324                  --  No null possible here, there are no parents for the path.
5325                  --  This means we are using a global variable without adding
5326                  --  it in environment with a global aspect.
5327
5328                  Illegal_Global_Usage (N);
5329               end if;
5330
5331               if Mode = Super_Move then
5332                  C.all.Tree.Permission := No_Access;
5333               else
5334                  C.all.Tree.Permission := Glb (Write_Only, Permission (C));
5335               end if;
5336
5337               return C;
5338            end;
5339
5340         when N_Type_Conversion
5341            | N_Unchecked_Type_Conversion
5342            | N_Qualified_Expression
5343         =>
5344            return Set_Perm_Prefixes_Move (Expression (N), Mode);
5345
5346         when N_Parameter_Specification
5347            | N_Defining_Identifier
5348         =>
5349            raise Program_Error;
5350
5351            --  We set the permission tree of its prefix, and then we extract
5352            --  from the returned pointer our subtree and assign an adequate
5353            --  permission to it, if unfolded. If folded, we unroll the tree
5354            --  at one step.
5355
5356         when N_Selected_Component =>
5357            declare
5358               C : constant Perm_Tree_Access :=
5359                 Set_Perm_Prefixes_Move (Prefix (N), Mode);
5360
5361            begin
5362               if C = null then
5363                  --  We went through a function call, do nothing
5364
5365                  return null;
5366               end if;
5367
5368               --  The permission of the returned node should be either W
5369               --  (because the recursive call sets <= Write_Only) or No
5370               --  (if another path has been moved with 'Access).
5371
5372               pragma Assert (Permission (C) = No_Access
5373                              or else Permission (C) = Write_Only);
5374
5375               if Mode = Super_Move then
5376                  --  The permission of the returned node should be No (thanks
5377                  --  to the recursion).
5378
5379                  pragma Assert (Permission (C) = No_Access);
5380                  null;
5381               end if;
5382
5383               pragma Assert (Kind (C) = Entire_Object
5384                              or else Kind (C) = Record_Component);
5385
5386               if Kind (C) = Record_Component then
5387                  --  The tree is unfolded. We just modify the permission and
5388                  --  return the record subtree.
5389
5390                  declare
5391                     Selected_Component : constant Entity_Id :=
5392                       Entity (Selector_Name (N));
5393
5394                     Selected_C : Perm_Tree_Access :=
5395                       Perm_Tree_Maps.Get
5396                         (Component (C), Selected_Component);
5397
5398                  begin
5399                     if Selected_C = null then
5400                        --  If the hash table returns no element, then we fall
5401                        --  into the part of Other_Components.
5402                        pragma Assert (Is_Tagged_Type (Etype (Prefix (N))));
5403
5404                        Selected_C := Other_Components (C);
5405                     end if;
5406
5407                     pragma Assert (Selected_C /= null);
5408
5409                     --  The Selected_C can have permissions:
5410                     --  RW : first move in this path
5411                     --  W  : Already other moves in this path
5412                     --  No : Already other moves with 'Access
5413
5414                     pragma Assert (Permission (Selected_C) /= Read_Only);
5415                     if Mode = Super_Move then
5416                        Selected_C.all.Tree.Permission := No_Access;
5417                     else
5418                        Selected_C.all.Tree.Permission :=
5419                          Glb (Write_Only, Permission (Selected_C));
5420
5421                     end if;
5422
5423                     return Selected_C;
5424                  end;
5425               elsif Kind (C) = Entire_Object then
5426                  declare
5427                     --  Expand the tree. Replace the node with
5428                     --  Record_Component.
5429
5430                     Elem : Node_Id;
5431
5432                     --  Create an empty hash table
5433
5434                     Hashtbl : Perm_Tree_Maps.Instance;
5435
5436                     --  We are in Move or Super_Move mode, hence we can assume
5437                     --  that the Children_permission is RW, given that there
5438                     --  are no other paths that could have been moved.
5439
5440                     pragma Assert (Children_Permission (C) = Read_Write);
5441
5442                     --  We create the unrolled nodes, that will all have RW
5443                     --  permission given that we are in move mode. We will
5444                     --  then set the right node to W.
5445
5446                     Son : Perm_Tree_Access;
5447
5448                  begin
5449                     --  We change the current node from Entire_Object to
5450                     --  Record_Component with same permission and an empty
5451                     --  hash table as component list.
5452
5453                     C.all.Tree :=
5454                       (Kind             => Record_Component,
5455                        Is_Node_Deep     => Is_Node_Deep (C),
5456                        Permission       => Permission (C),
5457                        Component        => Hashtbl,
5458                        Other_Components =>
5459                           new Perm_Tree_Wrapper'
5460                          (Tree =>
5461                               (Kind                => Entire_Object,
5462                                Is_Node_Deep        => True,
5463                                Permission          => Read_Write,
5464                                Children_Permission => Read_Write)
5465                          ));
5466
5467                     --  We fill the hash table with all sons of the record,
5468                     --  with basic Entire_Objects nodes.
5469                     Elem := First_Component_Or_Discriminant
5470                       (Etype (Prefix (N)));
5471
5472                     while Present (Elem) loop
5473                        Son := new Perm_Tree_Wrapper'
5474                          (Tree =>
5475                             (Kind                => Entire_Object,
5476                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
5477                              Permission          => Read_Write,
5478                              Children_Permission => Read_Write));
5479
5480                        Perm_Tree_Maps.Set
5481                          (C.all.Tree.Component, Elem, Son);
5482
5483                        Next_Component_Or_Discriminant (Elem);
5484                     end loop;
5485
5486                     --  Now we set the right field to Write_Only or No_Access
5487                     --  depending on mode, and then we return the tree to the
5488                     --  sons, so that the recursion can continue.
5489
5490                     declare
5491                        Selected_Component : constant Entity_Id :=
5492                          Entity (Selector_Name (N));
5493
5494                        Selected_C : Perm_Tree_Access :=
5495                          Perm_Tree_Maps.Get
5496                            (Component (C), Selected_Component);
5497
5498                     begin
5499                        if Selected_C = null then
5500                           Selected_C := Other_Components (C);
5501                        end if;
5502
5503                        pragma Assert (Selected_C /= null);
5504
5505                        --  Given that this is a newly created Select_C, we can
5506                        --  safely assume that its permission is Read_Write.
5507
5508                        pragma Assert (Permission (Selected_C) =
5509                                         Read_Write);
5510
5511                        if Mode = Super_Move then
5512                           Selected_C.all.Tree.Permission := No_Access;
5513                        else
5514                           Selected_C.all.Tree.Permission := Write_Only;
5515                        end if;
5516
5517                        return Selected_C;
5518                     end;
5519                  end;
5520               else
5521                  raise Program_Error;
5522               end if;
5523            end;
5524
5525            --  We set the permission tree of its prefix, and then we extract
5526            --  from the returned pointer the subtree and assign an adequate
5527            --  permission to it, if unfolded. If folded, we unroll the tree
5528            --  at one step.
5529
5530         when N_Indexed_Component
5531            | N_Slice
5532         =>
5533            declare
5534               C : constant Perm_Tree_Access :=
5535                 Set_Perm_Prefixes_Move (Prefix (N), Mode);
5536
5537            begin
5538               if C = null then
5539                  --  We went through a function call, do nothing
5540
5541                  return null;
5542               end if;
5543
5544               --  The permission of the returned node should be either
5545               --  W (because the recursive call sets <= Write_Only)
5546               --  or No (if another path has been moved with 'Access)
5547
5548               if Mode = Super_Move then
5549                  pragma Assert (Permission (C) = No_Access);
5550                  null;
5551               else
5552                  pragma Assert (Permission (C) = Write_Only
5553                                 or else Permission (C) = No_Access);
5554                  null;
5555               end if;
5556
5557               pragma Assert (Kind (C) = Entire_Object
5558                              or else Kind (C) = Array_Component);
5559
5560               if Kind (C) = Array_Component then
5561                  --  The tree is unfolded. We just modify the permission and
5562                  --  return the elem subtree.
5563
5564                  if Get_Elem (C) = null then
5565                     --  Hash_Table_Error
5566                     raise Program_Error;
5567                  end if;
5568
5569                  --  The Get_Elem can have permissions :
5570                  --  RW : first move in this path
5571                  --  W  : Already other moves in this path
5572                  --  No : Already other moves with 'Access
5573
5574                  pragma Assert (Permission (Get_Elem (C)) /= Read_Only);
5575
5576                  if Mode = Super_Move then
5577                     C.all.Tree.Get_Elem.all.Tree.Permission := No_Access;
5578                  else
5579                     C.all.Tree.Get_Elem.all.Tree.Permission :=
5580                       Glb (Write_Only, Permission (Get_Elem (C)));
5581                  end if;
5582
5583                  return Get_Elem (C);
5584               elsif Kind (C) = Entire_Object then
5585                  declare
5586                     --  Expand the tree. Replace node with Array_Component.
5587
5588                     --  We are in move mode, hence we can assume that the
5589                     --  Children_permission is RW.
5590
5591                     pragma Assert (Children_Permission (C) = Read_Write);
5592
5593                     Son : Perm_Tree_Access;
5594
5595                  begin
5596                     Son := new Perm_Tree_Wrapper'
5597                       (Tree =>
5598                          (Kind                => Entire_Object,
5599                           Is_Node_Deep        => Is_Node_Deep (C),
5600                           Permission          => Read_Write,
5601                           Children_Permission => Read_Write));
5602
5603                     if Mode = Super_Move then
5604                        Son.all.Tree.Permission := No_Access;
5605                     else
5606                        Son.all.Tree.Permission := Write_Only;
5607                     end if;
5608
5609                     --  We change the current node from Entire_Object
5610                     --  to Array_Component with same permission and the
5611                     --  previously defined son.
5612
5613                     C.all.Tree := (Kind         => Array_Component,
5614                                    Is_Node_Deep => Is_Node_Deep (C),
5615                                    Permission   => Permission (C),
5616                                    Get_Elem     => Son);
5617
5618                     return Get_Elem (C);
5619                  end;
5620               else
5621                  raise Program_Error;
5622               end if;
5623            end;
5624
5625            --  We set the permission tree of its prefix, and then we extract
5626            --  from the returned pointer the subtree and assign an adequate
5627            --  permission to it, if unfolded. If folded, we unroll the tree
5628            --  at one step.
5629
5630         when N_Explicit_Dereference =>
5631            declare
5632               C : constant Perm_Tree_Access :=
5633                 Set_Perm_Prefixes_Move (Prefix (N), Move);
5634
5635            begin
5636               if C = null then
5637                  --  We went through a function call: do nothing
5638
5639                  return null;
5640               end if;
5641
5642               --  The permission of the returned node should be only
5643               --  W (because the recursive call sets <= Write_Only)
5644               --  No is NOT POSSIBLE here
5645
5646               pragma Assert (Permission (C) = Write_Only);
5647
5648               pragma Assert (Kind (C) = Entire_Object
5649                              or else Kind (C) = Reference);
5650
5651               if Kind (C) = Reference then
5652                  --  The tree is unfolded. We just modify the permission and
5653                  --  return the elem subtree.
5654
5655                  if Get_All (C) = null then
5656                     --  Hash_Table_Error
5657                     raise Program_Error;
5658                  end if;
5659
5660                  --  The Get_All can have permissions :
5661                  --  RW : first move in this path
5662                  --  W  : Already other moves in this path
5663                  --  No : Already other moves with 'Access
5664
5665                  pragma Assert (Permission (Get_All (C)) /= Read_Only);
5666
5667                  if Mode = Super_Move then
5668                     C.all.Tree.Get_All.all.Tree.Permission := No_Access;
5669                  else
5670                     Get_All (C).all.Tree.Permission :=
5671                       Glb (Write_Only, Permission (Get_All (C)));
5672                  end if;
5673                  return Get_All (C);
5674               elsif Kind (C) = Entire_Object then
5675                  declare
5676                     --  Expand the tree. Replace the node with Reference.
5677
5678                     --  We are in Move or Super_Move mode, hence we can assume
5679                     --  that the Children_permission is RW.
5680
5681                     pragma Assert (Children_Permission (C) = Read_Write);
5682
5683                     Son : Perm_Tree_Access;
5684
5685                  begin
5686                     Son := new Perm_Tree_Wrapper'
5687                       (Tree =>
5688                          (Kind                => Entire_Object,
5689                           Is_Node_Deep        => Is_Deep (Etype (N)),
5690                           Permission          => Read_Write,
5691                           Children_Permission => Read_Write));
5692
5693                     if Mode = Super_Move then
5694                        Son.all.Tree.Permission := No_Access;
5695                     else
5696                        Son.all.Tree.Permission := Write_Only;
5697                     end if;
5698
5699                     --  We change the current node from Entire_Object to
5700                     --  Reference with Write_Only and the previous son.
5701
5702                     pragma Assert (Is_Node_Deep (C));
5703
5704                     C.all.Tree := (Kind         => Reference,
5705                                    Is_Node_Deep => Is_Node_Deep (C),
5706                                    Permission   => Write_Only,
5707                                    --  Write_only is equal to C.Permission
5708                                    Get_All      => Son);
5709
5710                     return Get_All (C);
5711                  end;
5712               else
5713                  raise Program_Error;
5714               end if;
5715            end;
5716
5717         when N_Function_Call =>
5718            return null;
5719
5720         when others =>
5721            raise Program_Error;
5722      end case;
5723
5724   end Set_Perm_Prefixes_Move;
5725
5726   -------------------------------
5727   -- Set_Perm_Prefixes_Observe --
5728   -------------------------------
5729
5730   function Set_Perm_Prefixes_Observe
5731     (N : Node_Id)
5732      return Perm_Tree_Access
5733   is
5734   begin
5735      pragma Assert (Current_Checking_Mode = Observe);
5736
5737      case Nkind (N) is
5738         --  Base identifier. Set permission to R.
5739
5740         when N_Identifier
5741            | N_Expanded_Name
5742            | N_Defining_Identifier
5743         =>
5744            declare
5745               P : Node_Id;
5746               C : Perm_Tree_Access;
5747
5748            begin
5749               if Nkind (N) = N_Defining_Identifier then
5750                  P := N;
5751               else
5752                  P := Entity (N);
5753               end if;
5754
5755               C := Get (Current_Perm_Env, Unique_Entity (P));
5756               --  Setting the initialization map to True, so that this
5757               --  variable cannot be ignored anymore when looking at end
5758               --  of elaboration of package.
5759
5760               Set (Current_Initialization_Map, Unique_Entity (P), True);
5761
5762               if C = null then
5763                  --  No null possible here, there are no parents for the path.
5764                  --  This means we are using a global variable without adding
5765                  --  it in environment with a global aspect.
5766
5767                  Illegal_Global_Usage (N);
5768               end if;
5769
5770               C.all.Tree.Permission := Glb (Read_Only, Permission (C));
5771
5772               return C;
5773            end;
5774
5775         when N_Type_Conversion
5776            | N_Unchecked_Type_Conversion
5777            | N_Qualified_Expression
5778         =>
5779            return Set_Perm_Prefixes_Observe (Expression (N));
5780
5781         when N_Parameter_Specification =>
5782            raise Program_Error;
5783
5784            --  We set the permission tree of its prefix, and then we extract
5785            --  from the returned pointer our subtree and assign an adequate
5786            --  permission to it, if unfolded. If folded, we unroll the tree
5787            --  at one step.
5788
5789         when N_Selected_Component =>
5790            declare
5791               C : constant Perm_Tree_Access :=
5792                 Set_Perm_Prefixes_Observe (Prefix (N));
5793
5794            begin
5795               if C = null then
5796                  --  We went through a function call, do nothing
5797
5798                  return null;
5799               end if;
5800
5801               pragma Assert (Kind (C) = Entire_Object
5802                              or else Kind (C) = Record_Component);
5803
5804               if Kind (C) = Record_Component then
5805                  --  The tree is unfolded. We just modify the permission and
5806                  --  return the record subtree. We put the permission to the
5807                  --  glb of read_only and its current permission, to consider
5808                  --  the case of observing x.y while x.z has been moved. Then
5809                  --  x should be No_Access.
5810
5811                  declare
5812                     Selected_Component : constant Entity_Id :=
5813                       Entity (Selector_Name (N));
5814
5815                     Selected_C : Perm_Tree_Access :=
5816                       Perm_Tree_Maps.Get
5817                         (Component (C), Selected_Component);
5818
5819                  begin
5820                     if Selected_C = null then
5821                        Selected_C := Other_Components (C);
5822                     end if;
5823
5824                     pragma Assert (Selected_C /= null);
5825
5826                     Selected_C.all.Tree.Permission :=
5827                       Glb (Read_Only, Permission (Selected_C));
5828
5829                     return Selected_C;
5830                  end;
5831               elsif Kind (C) = Entire_Object then
5832                  declare
5833                     --  Expand the tree. Replace the node with
5834                     --  Record_Component.
5835
5836                     Elem : Node_Id;
5837
5838                     --  Create an empty hash table
5839
5840                     Hashtbl : Perm_Tree_Maps.Instance;
5841
5842                     --  We create the unrolled nodes, that will all have RW
5843                     --  permission given that we are in move mode. We will
5844                     --  then set the right node to W.
5845
5846                     Son : Perm_Tree_Access;
5847
5848                     Child_Perm : constant Perm_Kind :=
5849                       Children_Permission (C);
5850
5851                  begin
5852                     --  We change the current node from Entire_Object to
5853                     --  Record_Component with same permission and an empty
5854                     --  hash table as component list.
5855
5856                     C.all.Tree :=
5857                       (Kind             => Record_Component,
5858                        Is_Node_Deep     => Is_Node_Deep (C),
5859                        Permission       => Permission (C),
5860                        Component        => Hashtbl,
5861                        Other_Components =>
5862                           new Perm_Tree_Wrapper'
5863                          (Tree =>
5864                               (Kind                => Entire_Object,
5865                                Is_Node_Deep        => True,
5866                                Permission          => Child_Perm,
5867                                Children_Permission => Child_Perm)
5868                          ));
5869
5870                     --  We fill the hash table with all sons of the record,
5871                     --  with basic Entire_Objects nodes.
5872                     Elem := First_Component_Or_Discriminant
5873                       (Etype (Prefix (N)));
5874
5875                     while Present (Elem) loop
5876                        Son := new Perm_Tree_Wrapper'
5877                          (Tree =>
5878                             (Kind                => Entire_Object,
5879                              Is_Node_Deep        => Is_Deep (Etype (Elem)),
5880                              Permission          => Child_Perm,
5881                              Children_Permission => Child_Perm));
5882
5883                        Perm_Tree_Maps.Set
5884                          (C.all.Tree.Component, Elem, Son);
5885
5886                        Next_Component_Or_Discriminant (Elem);
5887                     end loop;
5888
5889                     --  Now we set the right field to Read_Only. and then we
5890                     --  return the tree to the sons, so that the recursion can
5891                     --  continue.
5892
5893                     declare
5894                        Selected_Component : constant Entity_Id :=
5895                          Entity (Selector_Name (N));
5896
5897                        Selected_C : Perm_Tree_Access :=
5898                          Perm_Tree_Maps.Get
5899                            (Component (C), Selected_Component);
5900
5901                     begin
5902                        if Selected_C = null then
5903                           Selected_C := Other_Components (C);
5904                        end if;
5905
5906                        pragma Assert (Selected_C /= null);
5907
5908                        Selected_C.all.Tree.Permission :=
5909                          Glb (Read_Only, Child_Perm);
5910
5911                        return Selected_C;
5912                     end;
5913                  end;
5914               else
5915                  raise Program_Error;
5916               end if;
5917            end;
5918
5919         --  We set the permission tree of its prefix, and then we extract from
5920         --  the returned pointer the subtree and assign an adequate permission
5921         --  to it, if unfolded. If folded, we unroll the tree at one step.
5922
5923         when N_Indexed_Component
5924            | N_Slice
5925         =>
5926            declare
5927               C : constant Perm_Tree_Access :=
5928                 Set_Perm_Prefixes_Observe (Prefix (N));
5929
5930            begin
5931               if C = null then
5932                  --  We went through a function call, do nothing
5933
5934                  return null;
5935               end if;
5936
5937               pragma Assert (Kind (C) = Entire_Object
5938                              or else Kind (C) = Array_Component);
5939
5940               if Kind (C) = Array_Component then
5941                  --  The tree is unfolded. We just modify the permission and
5942                  --  return the elem subtree.
5943
5944                  pragma Assert (Get_Elem (C) /= null);
5945
5946                  C.all.Tree.Get_Elem.all.Tree.Permission :=
5947                    Glb (Read_Only, Permission (Get_Elem (C)));
5948
5949                  return Get_Elem (C);
5950               elsif Kind (C) = Entire_Object then
5951                  declare
5952                     --  Expand the tree. Replace node with Array_Component.
5953
5954                     Son : Perm_Tree_Access;
5955
5956                     Child_Perm : constant Perm_Kind :=
5957                       Glb (Read_Only, Children_Permission (C));
5958
5959                  begin
5960                     Son := new Perm_Tree_Wrapper'
5961                       (Tree =>
5962                          (Kind                => Entire_Object,
5963                           Is_Node_Deep        => Is_Node_Deep (C),
5964                           Permission          => Child_Perm,
5965                           Children_Permission => Child_Perm));
5966
5967                     --  We change the current node from Entire_Object
5968                     --  to Array_Component with same permission and the
5969                     --  previously defined son.
5970
5971                     C.all.Tree := (Kind         => Array_Component,
5972                                    Is_Node_Deep => Is_Node_Deep (C),
5973                                    Permission   => Child_Perm,
5974                                    Get_Elem     => Son);
5975
5976                     return Get_Elem (C);
5977                  end;
5978
5979               else
5980                  raise Program_Error;
5981               end if;
5982            end;
5983
5984         --  We set the permission tree of its prefix, and then we extract from
5985         --  the returned pointer the subtree and assign an adequate permission
5986         --  to it, if unfolded. If folded, we unroll the tree at one step.
5987
5988         when N_Explicit_Dereference =>
5989            declare
5990               C : constant Perm_Tree_Access :=
5991                 Set_Perm_Prefixes_Observe (Prefix (N));
5992
5993            begin
5994               if C = null then
5995                  --  We went through a function call, do nothing
5996
5997                  return null;
5998               end if;
5999
6000               pragma Assert (Kind (C) = Entire_Object
6001                              or else Kind (C) = Reference);
6002
6003               if Kind (C) = Reference then
6004                  --  The tree is unfolded. We just modify the permission and
6005                  --  return the elem subtree.
6006
6007                  pragma Assert (Get_All (C) /= null);
6008
6009                  C.all.Tree.Get_All.all.Tree.Permission :=
6010                    Glb (Read_Only, Permission (Get_All (C)));
6011
6012                  return Get_All (C);
6013               elsif Kind (C) = Entire_Object then
6014                  declare
6015                     --  Expand the tree. Replace the node with Reference.
6016
6017                     Son : Perm_Tree_Access;
6018
6019                     Child_Perm : constant Perm_Kind :=
6020                       Glb (Read_Only, Children_Permission (C));
6021
6022                  begin
6023                     Son := new Perm_Tree_Wrapper'
6024                       (Tree =>
6025                          (Kind                => Entire_Object,
6026                           Is_Node_Deep        => Is_Deep (Etype (N)),
6027                           Permission          => Child_Perm,
6028                           Children_Permission => Child_Perm));
6029
6030                     --  We change the current node from Entire_Object to
6031                     --  Reference with Write_Only and the previous son.
6032
6033                     pragma Assert (Is_Node_Deep (C));
6034
6035                     C.all.Tree := (Kind         => Reference,
6036                                    Is_Node_Deep => Is_Node_Deep (C),
6037                                    Permission   => Child_Perm,
6038                                    Get_All      => Son);
6039
6040                     return Get_All (C);
6041                  end;
6042               else
6043                  raise Program_Error;
6044               end if;
6045            end;
6046
6047         when N_Function_Call =>
6048            return null;
6049
6050         when others =>
6051            raise Program_Error;
6052
6053      end case;
6054   end Set_Perm_Prefixes_Observe;
6055
6056   -------------------
6057   -- Setup_Globals --
6058   -------------------
6059
6060   procedure Setup_Globals (Subp : Entity_Id) is
6061
6062      procedure Setup_Globals_From_List
6063        (First_Item : Node_Id;
6064         Kind       : Formal_Kind);
6065      --  Set up global items from the list starting at Item
6066
6067      procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
6068      --  Set up global items for the mode Global_Mode
6069
6070      -----------------------------
6071      -- Setup_Globals_From_List --
6072      -----------------------------
6073
6074      procedure Setup_Globals_From_List
6075        (First_Item : Node_Id;
6076         Kind       : Formal_Kind)
6077      is
6078         Item : Node_Id := First_Item;
6079         E    : Entity_Id;
6080
6081      begin
6082         while Present (Item) loop
6083            E := Entity (Item);
6084
6085            --  Ignore abstract states, which play no role in pointer aliasing
6086
6087            if Ekind (E) = E_Abstract_State then
6088               null;
6089            else
6090               Setup_Parameter_Or_Global (E, Kind);
6091            end if;
6092            Next_Global (Item);
6093         end loop;
6094      end Setup_Globals_From_List;
6095
6096      ---------------------------
6097      -- Setup_Globals_Of_Mode --
6098      ---------------------------
6099
6100      procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
6101         Kind : Formal_Kind;
6102
6103      begin
6104         case Global_Mode is
6105            when Name_Input | Name_Proof_In =>
6106               Kind := E_In_Parameter;
6107            when Name_Output =>
6108               Kind := E_Out_Parameter;
6109            when Name_In_Out =>
6110               Kind := E_In_Out_Parameter;
6111            when others =>
6112               raise Program_Error;
6113         end case;
6114
6115         --  Set up both global items from Global and Refined_Global pragmas
6116
6117         Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
6118         Setup_Globals_From_List
6119           (First_Global (Subp, Global_Mode, Refined => True), Kind);
6120      end Setup_Globals_Of_Mode;
6121
6122   --  Start of processing for Setup_Globals
6123
6124   begin
6125      Setup_Globals_Of_Mode (Name_Proof_In);
6126      Setup_Globals_Of_Mode (Name_Input);
6127      Setup_Globals_Of_Mode (Name_Output);
6128      Setup_Globals_Of_Mode (Name_In_Out);
6129   end Setup_Globals;
6130
6131   -------------------------------
6132   -- Setup_Parameter_Or_Global --
6133   -------------------------------
6134
6135   procedure Setup_Parameter_Or_Global
6136     (Id   : Entity_Id;
6137      Mode : Formal_Kind)
6138   is
6139      Elem : Perm_Tree_Access;
6140
6141   begin
6142      Elem := new Perm_Tree_Wrapper'
6143        (Tree =>
6144           (Kind                => Entire_Object,
6145            Is_Node_Deep        => Is_Deep (Etype (Id)),
6146            Permission          => Read_Write,
6147            Children_Permission => Read_Write));
6148
6149      case Mode is
6150         when E_In_Parameter =>
6151
6152            --  Borrowed IN: RW for everybody
6153
6154            if Is_Borrowed_In (Id) then
6155               Elem.all.Tree.Permission := Read_Write;
6156               Elem.all.Tree.Children_Permission := Read_Write;
6157
6158            --  Observed IN: R for everybody
6159
6160            else
6161               Elem.all.Tree.Permission := Read_Only;
6162               Elem.all.Tree.Children_Permission := Read_Only;
6163            end if;
6164
6165         --  OUT: borrow, but callee has W only
6166
6167         when E_Out_Parameter =>
6168            Elem.all.Tree.Permission := Write_Only;
6169            Elem.all.Tree.Children_Permission := Write_Only;
6170
6171         --  IN OUT: borrow and callee has RW
6172
6173         when E_In_Out_Parameter =>
6174            Elem.all.Tree.Permission := Read_Write;
6175            Elem.all.Tree.Children_Permission := Read_Write;
6176      end case;
6177
6178      Set (Current_Perm_Env, Id, Elem);
6179   end Setup_Parameter_Or_Global;
6180
6181   ----------------------
6182   -- Setup_Parameters --
6183   ----------------------
6184
6185   procedure Setup_Parameters (Subp : Entity_Id) is
6186      Formal : Entity_Id;
6187
6188   begin
6189      Formal := First_Formal (Subp);
6190      while Present (Formal) loop
6191         Setup_Parameter_Or_Global (Formal, Ekind (Formal));
6192         Next_Formal (Formal);
6193      end loop;
6194   end Setup_Parameters;
6195
6196end Sem_SPARK;
6197