1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- S E M _ S P A R K --
9 -- Copyright (C) 2017-2018, Free Software Foundation, Inc. --
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. --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
24 ------------------------------------------------------------------------------
26 with Atree
; use Atree
;
27 with Einfo
; use Einfo
;
28 with Errout
; use Errout
;
29 with Namet
; use Namet
;
30 with Nlists
; use Nlists
;
32 with Osint
; use Osint
;
33 with Sem_Prag
; use Sem_Prag
;
34 with Sem_Util
; use Sem_Util
;
35 with Sem_Aux
; use Sem_Aux
;
36 with Sinfo
; use Sinfo
;
37 with Snames
; use Snames
;
38 with Treepr
; use Treepr
;
40 with Ada
.Unchecked_Deallocation
;
41 with GNAT
.Dynamic_HTables
; use GNAT
.Dynamic_HTables
;
43 package body Sem_SPARK
is
45 -------------------------------------------------
46 -- Handling of Permissions Associated to Paths --
47 -------------------------------------------------
49 package Permissions
is
50 Elaboration_Context_Max
: constant := 1009;
53 type Elaboration_Context_Index
is range 0 .. Elaboration_Context_Max
- 1;
55 function Elaboration_Context_Hash
56 (Key
: Entity_Id
) return Elaboration_Context_Index
;
57 -- Function to hash any node of the AST
59 type Perm_Kind
is (No_Access
, Read_Only
, Read_Write
, Write_Only
);
60 -- Permission type associated with paths
62 subtype Read_Perm
is Perm_Kind
range Read_Only
.. Read_Write
;
63 subtype Write_Perm
is Perm_Kind
range Read_Write
.. Write_Only
;
65 type Perm_Tree_Wrapper
;
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
74 -- Nodes in the permission tree are of different kinds
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
83 package Perm_Tree_Maps
is new Simple_HTable
84 (Header_Num
=> Elaboration_Context_Index
,
86 Element
=> Perm_Tree_Access
,
88 Hash
=> Elaboration_Context_Hash
,
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, ...).
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
101 Is_Node_Deep
: Boolean;
102 -- Whether this node is of a deep type, to be used when moving the
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.
114 when Entire_Object
=>
115 Children_Permission
: Perm_Kind
;
117 -- Unfolded path of access type. The permission of the object
118 -- pointed to is given in Get_All.
121 Get_All
: Perm_Tree_Access
;
123 -- Unfolded path of array type. The permission of the elements is
124 -- given in Get_Elem.
126 when Array_Component
=>
127 Get_Elem
: Perm_Tree_Access
;
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
134 when Record_Component
=>
135 Component
: Perm_Tree_Maps
.Instance
;
136 Other_Components
: Perm_Tree_Access
;
140 type Perm_Tree_Wrapper
is record
143 -- We use this wrapper in order to have unconstrained discriminants
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.
150 type Perm_Env_Access
is access Perm_Env
;
151 -- Access to permission environments
153 package Env_Maps
is new Simple_HTable
154 (Header_Num
=> Elaboration_Context_Index
,
156 Element
=> Perm_Env_Access
,
158 Hash
=> Elaboration_Context_Hash
,
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.
164 type Env_Backups
is new Env_Maps
.Instance
;
165 -- The type defining the hash table saving the environments at the entry
168 package Boolean_Variables_Maps
is new Simple_HTable
169 (Header_Num
=> Elaboration_Context_Index
,
173 Hash
=> Elaboration_Context_Hash
,
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.
181 type Initialization_Map
is new Boolean_Variables_Maps
.Instance
;
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.
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
;
200 -----------------------
201 -- Memory Management --
202 -----------------------
206 To
: in out Perm_Env
);
207 -- Procedure to copy a permission environment
209 procedure Copy_Init_Map
210 (From
: Initialization_Map
;
211 To
: in out Initialization_Map
);
212 -- Procedure to copy an initialization map
215 (From
: Perm_Tree_Access
;
216 To
: Perm_Tree_Access
);
217 -- Procedure to copy a permission tree
220 (PE
: in out Perm_Env
);
221 -- Procedure to free a permission environment
223 procedure Free_Perm_Tree
224 (PT
: in out Perm_Tree_Access
);
225 -- Procedure to free a permission tree
231 procedure Perm_Mismatch
232 (Exp_Perm
, Act_Perm
: Perm_Kind
;
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.
240 package body Permissions
is
242 -------------------------
243 -- Children_Permission --
244 -------------------------
246 function Children_Permission
247 (T
: Perm_Tree_Access
)
251 return T
.all.Tree
.Children_Permission
;
252 end Children_Permission
;
259 (T
: Perm_Tree_Access
)
260 return Perm_Tree_Maps
.Instance
263 return T
.all.Tree
.Component
;
272 To
: in out Perm_Env
)
274 Comp_From
: Perm_Tree_Access
;
275 Key_From
: Perm_Tree_Maps
.Key_Option
;
276 Son
: Perm_Tree_Access
;
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);
285 Son
:= new Perm_Tree_Wrapper
;
286 Copy_Tree
(Comp_From
, Son
);
288 Set
(To
, Key_From
.K
, Son
);
289 Key_From
:= Get_Next_Key
(From
);
297 procedure Copy_Init_Map
298 (From
: Initialization_Map
;
299 To
: in out Initialization_Map
)
302 Key_From
: Boolean_Variables_Maps
.Key_Option
;
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
);
319 (From
: Perm_Tree_Access
;
320 To
: Perm_Tree_Access
)
326 when Entire_Object
=>
330 To
.all.Tree
.Get_All
:= new Perm_Tree_Wrapper
;
332 Copy_Tree
(Get_All
(From
), Get_All
(To
));
334 when Array_Component
=>
335 To
.all.Tree
.Get_Elem
:= new Perm_Tree_Wrapper
;
337 Copy_Tree
(Get_Elem
(From
), Get_Elem
(To
));
339 when Record_Component
=>
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
;
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
;
350 To
.all.Tree
.Other_Components
:=
351 new Perm_Tree_Wrapper
'(Other_Components (From).all);
353 Copy_Tree (Other_Components (From), Other_Components (To));
355 Key_From := Perm_Tree_Maps.Get_First_Key
357 while Key_From.Present loop
358 Comp_From := Perm_Tree_Maps.Get
359 (Component (From), Key_From.K);
361 pragma Assert (Comp_From /= null);
362 Son := new Perm_Tree_Wrapper;
364 Copy_Tree (Comp_From, Son);
367 (To.all.Tree.Component, Key_From.K, Son);
369 Key_From := Perm_Tree_Maps.Get_Next_Key
376 ------------------------------
377 -- Elaboration_Context_Hash --
378 ------------------------------
380 function Elaboration_Context_Hash
381 (Key : Entity_Id) return Elaboration_Context_Index
384 return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
385 end Elaboration_Context_Hash;
391 procedure Free_Env (PE : in out Perm_Env) is
392 CompO : Perm_Tree_Access;
394 CompO := Get_First (PE);
395 while CompO /= null loop
396 Free_Perm_Tree (CompO);
397 CompO := Get_Next (PE);
405 procedure Free_Perm_Tree
406 (PT : in out Perm_Tree_Access)
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
415 when Entire_Object =>
416 Free_Perm_Tree_Dealloc (PT);
419 Free_Perm_Tree (PT.all.Tree.Get_All);
420 Free_Perm_Tree_Dealloc (PT);
422 when Array_Component =>
423 Free_Perm_Tree (PT.all.Tree.Get_Elem);
425 when Record_Component =>
427 Comp : Perm_Tree_Access;
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
435 Free_Perm_Tree (Comp);
436 Comp := Perm_Tree_Maps.Get_Next (Component (PT));
439 Free_Perm_Tree_Dealloc (PT);
448 (T : Perm_Tree_Access)
449 return Perm_Tree_Access
452 return T.all.Tree.Get_All;
460 (T : Perm_Tree_Access)
461 return Perm_Tree_Access
464 return T.all.Tree.Get_Elem;
471 function Is_Node_Deep
472 (T : Perm_Tree_Access)
476 return T.all.Tree.Is_Node_Deep;
484 (T : Perm_Tree_Access)
488 return T.all.Tree.Kind;
491 ----------------------
492 -- Other_Components --
493 ----------------------
495 function Other_Components
496 (T : Perm_Tree_Access)
497 return Perm_Tree_Access
500 return T.all.Tree.Other_Components;
501 end Other_Components;
508 (T : Perm_Tree_Access)
512 return T.all.Tree.Permission;
519 procedure Perm_Mismatch
520 (Exp_Perm, Act_Perm : Perm_Kind;
524 Error_Msg_N ("\expected at least `"
525 & Perm_Kind'Image (Exp_Perm) & "`, got `"
526 & Perm_Kind'Image (Act_Perm) & "`", N);
533 --------------------------------------
534 -- Analysis modes for AST traversal --
535 --------------------------------------
537 -- The different modes for analysis. This allows to checking whether a path
538 -- found in the code should be moved, borrowed, or observed.
540 type Checking_Mode is
543 -- Default mode. Checks that paths have Read_Perm permission.
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.
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.
556 -- Enhanced moving semantics (under 'Access). Checks that paths have
557 -- Read_Write permission (shallow types may have only Write permission).
558 -- After moving a path, its permission is set to No_Access, as well as
559 -- the permission of its extensions and the permission of its prefixes
560 -- up to the first Reference node.
563 -- Used for actual OUT parameters. Checks that paths have Write_Perm
564 -- permission. After checking a path, its permission is set to Read_Only
565 -- when of a by-copy type, to No_Access otherwise. After the call, its
566 -- permission is set to Read_Write.
569 -- Used for actual IN parameters of a scalar type. Checks that paths
570 -- have Read_Perm permission. After checking a path, its permission
571 -- is set to Read_Only.
573 -- Also used for formal IN parameters
576 type Result_Kind
is (Folded
, Unfolded
, Function_Call
);
577 -- The type declaration to discriminate in the Perm_Or_Tree type
579 -- The result type of the function Get_Perm_Or_Tree. This returns either a
580 -- tree when it found the appropriate tree, or a permission when the search
581 -- finds a leaf and the subtree we are looking for is folded. In the last
582 -- case, we return instead the Children_Permission field of the leaf.
584 type Perm_Or_Tree
(R
: Result_Kind
) is record
586 when Folded
=> Found_Permission
: Perm_Kind
;
587 when Unfolded
=> Tree_Access
: Perm_Tree_Access
;
588 when Function_Call
=> null;
592 -----------------------
593 -- Local subprograms --
594 -----------------------
596 function "<=" (P1
, P2
: Perm_Kind
) return Boolean;
597 function ">=" (P1
, P2
: Perm_Kind
) return Boolean;
598 function Glb
(P1
, P2
: Perm_Kind
) return Perm_Kind
;
599 function Lub
(P1
, P2
: Perm_Kind
) return Perm_Kind
;
601 -- Checking proceduress for safe pointer usage. These procedures traverse
602 -- the AST, check nodes for correct permissions according to SPARK RM
603 -- 6.4.2, and update permissions depending on the node kind.
605 procedure Check_Call_Statement
(Call
: Node_Id
);
607 procedure Check_Callable_Body
(Body_N
: Node_Id
);
608 -- We are not in End_Of_Callee mode, hence we will save the environment
609 -- and start from a new one. We will add in the environment all formal
610 -- parameters as well as global used during the subprogram, with the
611 -- appropriate permissions (write-only for out, read-only for observed,
612 -- read-write for others).
614 -- After that we analyze the body of the function, and finaly, we check
615 -- that each borrowed parameter and global has read-write permission. We
616 -- then clean up the environment and put back the saved environment.
618 procedure Check_Declaration
(Decl
: Node_Id
);
620 procedure Check_Expression
(Expr
: Node_Id
);
622 procedure Check_Globals
(N
: Node_Id
; Check_Mode
: Checking_Mode
);
623 -- This procedure takes a global pragma and checks depending on mode:
624 -- Mode Read: every in global is readable
625 -- Mode Observe: same as Check_Param_Observes but on globals
626 -- Mode Borrow_Out: Check_Param_Outs for globals
627 -- Mode Move: Check_Param for globals with mode Read
628 -- Mode Assign: Check_Param for globals with mode Assign
630 procedure Check_List
(L
: List_Id
);
631 -- Calls Check_Node on each element of the list
633 procedure Check_Loop_Statement
(Loop_N
: Node_Id
);
635 procedure Check_Node
(N
: Node_Id
);
636 -- Main traversal procedure to check safe pointer usage. This procedure is
637 -- mutually recursive with the specialized procedures that follow.
639 procedure Check_Package_Body
(Pack
: Node_Id
);
641 procedure Check_Param
(Formal
: Entity_Id
; Actual
: Node_Id
);
642 -- This procedure takes a formal and an actual parameter and calls the
643 -- analyze node if the parameter is borrowed with mode in out, with the
644 -- appropriate Checking_Mode (Move).
646 procedure Check_Param_Observes
(Formal
: Entity_Id
; Actual
: Node_Id
);
647 -- This procedure takes a formal and an actual parameter and calls
648 -- the analyze node if the parameter is observed, with the appropriate
651 procedure Check_Param_Outs
(Formal
: Entity_Id
; Actual
: Node_Id
);
652 -- This procedure takes a formal and an actual parameter and calls the
653 -- analyze node if the parameter is of mode out, with the appropriate
656 procedure Check_Param_Read
(Formal
: Entity_Id
; Actual
: Node_Id
);
657 -- This procedure takes a formal and an actual parameter and checks the
658 -- readability of every in-mode parameter. This includes observed in, and
659 -- also borrowed in, that are then checked afterwards.
661 procedure Check_Statement
(Stmt
: Node_Id
);
663 function Get_Perm
(N
: Node_Id
) return Perm_Kind
;
664 -- The function that takes a name as input and returns a permission
667 function Get_Perm_Or_Tree
(N
: Node_Id
) return Perm_Or_Tree
;
668 -- This function gets a Node_Id and looks recursively to find the
669 -- appropriate subtree for that Node_Id. If the tree is folded on
670 -- that node, then it returns the permission given at the right level.
672 function Get_Perm_Tree
(N
: Node_Id
) return Perm_Tree_Access
;
673 -- This function gets a Node_Id and looks recursively to find the
674 -- appropriate subtree for that Node_Id. If the tree is folded, then
675 -- it unrolls the tree up to the appropriate level.
680 -- Function that returns whether the path given as parameter contains an
681 -- extension that is declared as aliased.
683 function Has_Array_Component
(N
: Node_Id
) return Boolean;
684 -- This function gets a Node_Id and looks recursively to find if the given
685 -- path has any array component.
687 function Has_Function_Component
(N
: Node_Id
) return Boolean;
688 -- This function gets a Node_Id and looks recursively to find if the given
689 -- path has any function component.
691 procedure Hp
(P
: Perm_Env
);
692 -- A procedure that outputs the hash table. This function is used only in
693 -- the debugger to look into a hash table.
694 pragma Unreferenced
(Hp
);
696 procedure Illegal_Global_Usage
(N
: Node_Or_Entity_Id
);
697 pragma No_Return
(Illegal_Global_Usage
);
698 -- A procedure that is called when deep globals or aliased globals are used
699 -- without any global aspect.
701 function Is_Borrowed_In
(E
: Entity_Id
) return Boolean;
702 -- Function that tells if the given entity is a borrowed in a formal
703 -- parameter, that is, if it is an access-to-variable type.
705 function Is_Deep
(E
: Entity_Id
) return Boolean;
706 -- A function that can tell if a type is deep or not. Returns true if the
707 -- type passed as argument is deep.
709 function Is_Shallow
(E
: Entity_Id
) return Boolean;
710 -- A function that can tell if a type is shallow or not. Returns true if
711 -- the type passed as argument is shallow.
713 function Loop_Of_Exit
(N
: Node_Id
) return Entity_Id
;
714 -- A function that takes an exit statement node and returns the entity of
715 -- the loop that this statement is exiting from.
717 procedure Merge_Envs
(Target
: in out Perm_Env
; Source
: in out Perm_Env
);
718 -- Merge Target and Source into Target, and then deallocate the Source
723 Found_Perm
: Perm_Kind
);
724 -- A procedure that is called when the permissions found contradict the
725 -- rules established by the RM. This function is called with the node, its
726 -- entity and the permission that was expected, and adds an error message
727 -- with the appropriate values.
729 procedure Perm_Error_Subprogram_End
733 Found_Perm
: Perm_Kind
);
734 -- A procedure that is called when the permissions found contradict the
735 -- rules established by the RM at the end of subprograms. This function
736 -- is called with the node, its entity, the node of the returning function
737 -- and the permission that was expected, and adds an error message with the
738 -- appropriate values.
740 procedure Process_Path
(N
: Node_Id
);
742 procedure Return_Declarations
(L
: List_Id
);
743 -- Check correct permissions on every declared object at the end of a
744 -- callee. Used at the end of the body of a callable entity. Checks that
745 -- paths of all borrowed formal parameters and global have Read_Write
748 procedure Return_Globals
(Subp
: Entity_Id
);
749 -- Takes a subprogram as input, and checks that all borrowed global items
750 -- of the subprogram indeed have RW permission at the end of the subprogram
753 procedure Return_Parameter_Or_Global
757 Global_Var
: Boolean);
758 -- Auxiliary procedure to Return_Parameters and Return_Globals
760 procedure Return_Parameters
(Subp
: Entity_Id
);
761 -- Takes a subprogram as input, and checks that all borrowed parameters of
762 -- the subprogram indeed have RW permission at the end of the subprogram
765 procedure Set_Perm_Extensions
(T
: Perm_Tree_Access
; P
: Perm_Kind
);
766 -- This procedure takes an access to a permission tree and modifies the
767 -- tree so that any strict extensions of the given tree become of the
768 -- access specified by parameter P.
770 procedure Set_Perm_Extensions_Move
(T
: Perm_Tree_Access
; E
: Entity_Id
);
771 -- Set permissions to
772 -- No for any extension with more .all
773 -- W for any deep extension with same number of .all
774 -- RW for any shallow extension with same number of .all
776 function Set_Perm_Prefixes_Assign
(N
: Node_Id
) return Perm_Tree_Access
;
777 -- This function takes a name as an input and sets in the permission
778 -- tree the given permission to the given name. The general rule here is
779 -- that everybody updates the permission of the subtree it is returning.
780 -- The permission of the assigned path has been set to RW by the caller.
782 -- Case where we have to normalize a tree after the correct permissions
783 -- have been assigned already. We look for the right subtree at the given
784 -- path, actualize its permissions, and then call the normalization on its
787 -- Example: We assign x.y and x.z then during Set_Perm_Prefixes_Move will
788 -- change the permission of x to RW because all of its components have
789 -- permission have permission RW.
791 function Set_Perm_Prefixes_Borrow_Out
(N
: Node_Id
) return Perm_Tree_Access
;
792 -- This function modifies the permissions of a given node_id in the
793 -- permission environment as well as in all the prefixes of the path,
794 -- given that the path is borrowed with mode out.
796 function Set_Perm_Prefixes_Move
797 (N
: Node_Id
; Mode
: Checking_Mode
)
798 return Perm_Tree_Access
;
799 pragma Precondition
(Mode
= Move
or Mode
= Super_Move
);
800 -- Given a node and a mode (that can be either Move or Super_Move), this
801 -- function modifies the permissions of a given node_id in the permission
802 -- environment as well as all the prefixes of the path, given that the path
803 -- is moved with or without 'Access. The general rule here is everybody
804 -- updates the permission of the subtree they are returning.
806 -- This case describes a move either under 'Access or without 'Access.
808 function Set_Perm_Prefixes_Observe
(N
: Node_Id
) return Perm_Tree_Access
;
809 -- This function modifies the permissions of a given node_id in the
810 -- permission environment as well as all the prefixes of the path,
811 -- given that the path is observed.
813 procedure Setup_Globals
(Subp
: Entity_Id
);
814 -- Takes a subprogram as input, and sets up the environment by adding
815 -- global items with appropriate permissions.
817 procedure Setup_Parameter_Or_Global
820 Global_Var
: Boolean);
821 -- Auxiliary procedure to Setup_Parameters and Setup_Globals
823 procedure Setup_Parameters
(Subp
: Entity_Id
);
824 -- Takes a subprogram as input, and sets up the environment by adding
825 -- formal parameters with appropriate permissions.
827 ----------------------
828 -- Global Variables --
829 ----------------------
831 Current_Perm_Env
: Perm_Env
;
832 -- The permission environment that is used for the analysis. This
833 -- environment can be saved, modified, reinitialized, but should be the
834 -- only one valid from which to extract the permissions of the paths in
835 -- scope. The analysis ensures at each point that this variables contains
836 -- a valid permission environment with all bindings in scope.
838 Current_Checking_Mode
: Checking_Mode
:= Read
;
839 -- The current analysis mode. This global variable indicates at each point
840 -- of the analysis whether the node being analyzed is moved, borrowed,
841 -- assigned, read, ... The full list of possible values can be found in
842 -- the declaration of type Checking_Mode.
844 Current_Loops_Envs
: Env_Backups
;
845 -- This variable contains saves of permission environments at each loop the
846 -- analysis entered. Each saved environment can be reached with the label
849 Current_Loops_Accumulators
: Env_Backups
;
850 -- This variable contains the environments used as accumulators for loops,
851 -- that consist of the merge of all environments at each exit point of
852 -- the loop (which can also be the entry point of the loop in the case of
853 -- non-infinite loops), each of them reachable from the label of the loop.
854 -- We require that the environment stored in the accumulator be less
855 -- restrictive than the saved environment at the beginning of the loop, and
856 -- the permission environment after the loop is equal to the accumulator.
858 Current_Initialization_Map
: Initialization_Map
;
859 -- This variable contains a map that binds each variable of the analyzed
860 -- source code to a boolean that becomes true whenever the variable is used
861 -- after declaration. Hence we can exclude from analysis variables that
862 -- are just declared and never accessed, typically at package declaration.
868 function "<=" (P1
, P2
: Perm_Kind
) return Boolean
878 function ">=" (P1
, P2
: Perm_Kind
) return Boolean
882 when No_Access
=> return True;
883 when Read_Only
=> return P1
in Read_Perm
;
884 when Write_Only
=> return P1
in Write_Perm
;
885 when Read_Write
=> return P1
= Read_Write
;
889 --------------------------
890 -- Check_Call_Statement --
891 --------------------------
893 procedure Check_Call_Statement
(Call
: Node_Id
) is
894 Saved_Env
: Perm_Env
;
896 procedure Iterate_Call
is new
897 Iterate_Call_Parameters
(Check_Param
);
898 procedure Iterate_Call_Observes
is new
899 Iterate_Call_Parameters
(Check_Param_Observes
);
900 procedure Iterate_Call_Outs
is new
901 Iterate_Call_Parameters
(Check_Param_Outs
);
902 procedure Iterate_Call_Read
is new
903 Iterate_Call_Parameters
(Check_Param_Read
);
906 -- Save environment, so that the modifications done by analyzing the
907 -- parameters are not kept at the end of the call.
908 Copy_Env
(Current_Perm_Env
,
911 -- We first check the Read access on every in parameter
913 Current_Checking_Mode
:= Read
;
914 Iterate_Call_Read
(Call
);
915 Check_Globals
(Get_Pragma
916 (Get_Called_Entity
(Call
), Pragma_Global
), Read
);
918 -- We first observe, then borrow with mode out, and then with other
919 -- modes. This ensures that we do not have to check for by-copy types
920 -- specially, because we read them before borrowing them.
922 Iterate_Call_Observes
(Call
);
923 Check_Globals
(Get_Pragma
924 (Get_Called_Entity
(Call
), Pragma_Global
),
927 Iterate_Call_Outs
(Call
);
928 Check_Globals
(Get_Pragma
929 (Get_Called_Entity
(Call
), Pragma_Global
),
933 Check_Globals
(Get_Pragma
934 (Get_Called_Entity
(Call
), Pragma_Global
), Move
);
936 -- Restore environment, because after borrowing/observing actual
937 -- parameters, they get their permission reverted to the ones before
940 Free_Env
(Current_Perm_Env
);
945 Free_Env
(Saved_Env
);
947 -- We assign the out parameters (necessarily borrowed per RM)
948 Current_Checking_Mode
:= Assign
;
950 Check_Globals
(Get_Pragma
951 (Get_Called_Entity
(Call
), Pragma_Global
),
954 end Check_Call_Statement
;
956 -------------------------
957 -- Check_Callable_Body --
958 -------------------------
960 procedure Check_Callable_Body
(Body_N
: Node_Id
) is
962 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
964 Saved_Env
: Perm_Env
;
965 Saved_Init_Map
: Initialization_Map
;
969 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_N
);
970 Spec_Id
: constant Entity_Id
:= Unique_Entity
(Body_Id
);
973 -- Check if SPARK pragma is not set to Off
975 if Present
(SPARK_Pragma
(Defining_Entity
(Body_N
))) then
976 if Get_SPARK_Mode_From_Annotation
977 (SPARK_Pragma
(Defining_Entity
(Body_N
, False))) /= Opt
.On
985 -- Save environment and put a new one in place
987 Copy_Env
(Current_Perm_Env
, Saved_Env
);
989 -- Save initialization map
991 Copy_Init_Map
(Current_Initialization_Map
, Saved_Init_Map
);
993 Current_Checking_Mode
:= Read
;
994 Current_Perm_Env
:= New_Env
;
996 -- Add formals and globals to the environment with adequate permissions
998 if Is_Subprogram_Or_Entry
(Spec_Id
) then
999 Setup_Parameters
(Spec_Id
);
1000 Setup_Globals
(Spec_Id
);
1003 -- Analyze the body of the function
1005 Check_List
(Declarations
(Body_N
));
1006 Check_Node
(Handled_Statement_Sequence
(Body_N
));
1008 -- Check the read-write permissions of borrowed parameters/globals
1010 if Ekind_In
(Spec_Id
, E_Procedure
, E_Entry
)
1011 and then not No_Return
(Spec_Id
)
1013 Return_Parameters
(Spec_Id
);
1014 Return_Globals
(Spec_Id
);
1017 -- Free the environments
1019 Free_Env
(Current_Perm_Env
);
1021 Copy_Env
(Saved_Env
,
1024 Free_Env
(Saved_Env
);
1026 -- Restore initialization map
1028 Copy_Init_Map
(Saved_Init_Map
, Current_Initialization_Map
);
1030 Reset
(Saved_Init_Map
);
1032 -- The assignment of all out parameters will be done by caller
1034 Current_Checking_Mode
:= Mode_Before
;
1035 end Check_Callable_Body
;
1037 -----------------------
1038 -- Check_Declaration --
1039 -----------------------
1041 procedure Check_Declaration
(Decl
: Node_Id
) is
1043 case N_Declaration
'(Nkind (Decl)) is
1044 when N_Full_Type_Declaration =>
1046 -- Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE
1050 when N_Object_Declaration =>
1052 -- First move the right-hand side
1054 Current_Checking_Mode := Move;
1055 Check_Node (Expression (Decl));
1058 Deep : constant Boolean :=
1059 Is_Deep (Etype (Defining_Identifier (Decl)));
1060 Elem : Perm_Tree_Access;
1063 Elem := new Perm_Tree_Wrapper'
1065 (Kind
=> Entire_Object
,
1066 Is_Node_Deep
=> Deep
,
1067 Permission
=> Read_Write
,
1068 Children_Permission
=> Read_Write
));
1070 -- If unitialized declaration, then set to Write_Only. If a
1071 -- pointer declaration, it has a null default initialization.
1073 if No
(Expression
(Decl
))
1074 and then not Has_Full_Default_Initialization
1075 (Etype
(Defining_Identifier
(Decl
)))
1076 and then not Is_Access_Type
1077 (Etype
(Defining_Identifier
(Decl
)))
1079 -- Objects of shallow types are considered as always
1080 -- initialized, leaving the checking of initialization to
1085 Elem
.all.Tree
.Permission
:= Write_Only
;
1086 Elem
.all.Tree
.Children_Permission
:= Write_Only
;
1089 -- Create new tree for defining identifier
1091 Set
(Current_Perm_Env
,
1092 Unique_Entity
(Defining_Identifier
(Decl
)),
1095 pragma Assert
(Get_First
(Current_Perm_Env
) /= null);
1098 when N_Subtype_Declaration
=>
1099 Check_Node
(Subtype_Indication
(Decl
));
1101 when N_Iterator_Specification
=>
1102 pragma Assert
(Is_Shallow
(Etype
(Defining_Identifier
(Decl
))));
1105 when N_Loop_Parameter_Specification
=>
1106 pragma Assert
(Is_Shallow
(Etype
(Defining_Identifier
(Decl
))));
1109 -- Checking should not be called directly on these nodes
1111 when N_Component_Declaration
1112 | N_Function_Specification
1113 | N_Entry_Declaration
1114 | N_Procedure_Specification
1116 raise Program_Error
;
1118 -- Ignored constructs for pointer checking
1120 when N_Formal_Object_Declaration
1121 | N_Formal_Type_Declaration
1122 | N_Incomplete_Type_Declaration
1123 | N_Private_Extension_Declaration
1124 | N_Private_Type_Declaration
1125 | N_Protected_Type_Declaration
1129 -- The following nodes are rewritten by semantic analysis
1131 when N_Expression_Function
=>
1132 raise Program_Error
;
1134 end Check_Declaration
;
1136 ----------------------
1137 -- Check_Expression --
1138 ----------------------
1140 procedure Check_Expression
(Expr
: Node_Id
) is
1141 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
1143 case N_Subexpr
'(Nkind (Expr)) is
1144 when N_Procedure_Call_Statement =>
1145 Check_Call_Statement (Expr);
1150 -- Check if identifier is pointing to nothing (On/Off/...)
1151 if not Present (Entity (Expr)) then
1155 -- Do not analyze things that are not of object Kind
1156 if Ekind (Entity (Expr)) not in Object_Kind then
1160 -- Consider as ident
1161 Process_Path (Expr);
1163 -- Switch to read mode and then check the readability of each operand
1167 Current_Checking_Mode := Read;
1168 Check_Node (Left_Opnd (Expr));
1169 Check_Node (Right_Opnd (Expr));
1171 -- Switch to read mode and then check the readability of each operand
1178 pragma Assert (Is_Shallow (Etype (Expr)));
1179 Current_Checking_Mode := Read;
1180 Check_Node (Right_Opnd (Expr));
1182 -- Forbid all deep expressions for Attribute ???
1184 when N_Attribute_Reference =>
1185 case Attribute_Name (Expr) is
1187 case Current_Checking_Mode is
1189 Check_Node (Prefix (Expr));
1192 Current_Checking_Mode := Super_Move;
1193 Check_Node (Prefix (Expr));
1195 -- Only assign names, not expressions
1198 raise Program_Error;
1200 -- Prefix in Super_Move should be a name, error here
1203 raise Program_Error;
1205 -- Could only borrow names of mode out, not n'Access
1208 raise Program_Error;
1211 Check_Node (Prefix (Expr));
1217 Current_Checking_Mode := Read;
1218 Check_Node (Prefix (Expr));
1221 Current_Checking_Mode := Read;
1222 Check_Node (Prefix (Expr));
1225 Check_List (Expressions (Expr));
1228 Check_Node (Prefix (Expr));
1230 when Name_SPARK_Mode =>
1234 Current_Checking_Mode := Read;
1235 Check_Node (Prefix (Expr));
1238 Check_List (Expressions (Expr));
1239 Check_Node (Prefix (Expr));
1244 Check_List (Expressions (Expr));
1245 Check_Node (Prefix (Expr));
1248 Current_Checking_Mode := Read;
1249 Check_Node (Prefix (Expr));
1251 -- Any Attribute referring to the underlying memory is ignored
1252 -- in the analysis. This means that taking the address of a
1253 -- variable makes a silent alias that is not rejected by the
1258 | Name_Component_Size
1266 -- Attributes referring to types (get values from types), hence
1267 -- no need to check either for borrows or any loans.
1274 -- Other attributes that fall out of the scope of the analysis
1281 Current_Checking_Mode := Read;
1282 Check_Node (Left_Opnd (Expr));
1283 Check_Node (Right_Opnd (Expr));
1286 Current_Checking_Mode := Read;
1287 Check_Node (Left_Opnd (Expr));
1288 Check_Node (Right_Opnd (Expr));
1290 -- Switch to read mode and then check the readability of each operand
1295 pragma Assert (Is_Shallow (Etype (Expr)));
1296 Current_Checking_Mode := Read;
1297 Check_Node (Left_Opnd (Expr));
1298 Check_Node (Right_Opnd (Expr));
1300 -- Check the arguments of the call
1302 when N_Function_Call =>
1303 Current_Checking_Mode := Read;
1304 Check_List (Parameter_Associations (Expr));
1306 when N_Explicit_Dereference =>
1307 Process_Path (Expr);
1309 -- Copy environment, run on each branch, and then merge
1311 when N_If_Expression =>
1313 Saved_Env : Perm_Env;
1315 -- Accumulator for the different branches
1319 Elmt : Node_Id := First (Expressions (Expr));
1322 Current_Checking_Mode := Read;
1326 Current_Checking_Mode := Mode_Before;
1330 Copy_Env (Current_Perm_Env,
1333 -- Here we have the original env in saved, current with a fresh
1334 -- copy, and new aliased.
1341 -- Here the new_environment contains curr env after then block
1345 -- Restore environment before if
1346 Copy_Env (Current_Perm_Env,
1349 Free_Env (Current_Perm_Env);
1351 Copy_Env (Saved_Env,
1354 -- Here new environment contains the environment after then and
1355 -- current the fresh copy of old one.
1360 Merge_Envs (New_Env,
1369 Free_Env (Saved_Env);
1372 when N_Indexed_Component =>
1373 Process_Path (Expr);
1375 -- Analyze the expression that is getting qualified
1377 when N_Qualified_Expression =>
1378 Check_Node (Expression (Expr));
1380 when N_Quantified_Expression =>
1382 Saved_Env : Perm_Env;
1384 Copy_Env (Current_Perm_Env, Saved_Env);
1385 Current_Checking_Mode := Read;
1386 Check_Node (Iterator_Specification (Expr));
1387 Check_Node (Loop_Parameter_Specification (Expr));
1389 Check_Node (Condition (Expr));
1390 Free_Env (Current_Perm_Env);
1391 Copy_Env (Saved_Env, Current_Perm_Env);
1392 Free_Env (Saved_Env);
1395 -- Analyze the list of associations in the aggregate
1398 Check_List (Expressions (Expr));
1399 Check_List (Component_Associations (Expr));
1402 Check_Node (Expression (Expr));
1404 when N_Case_Expression =>
1406 Saved_Env : Perm_Env;
1408 -- Accumulator for the different branches
1412 Elmt : Node_Id := First (Alternatives (Expr));
1415 Current_Checking_Mode := Read;
1416 Check_Node (Expression (Expr));
1418 Current_Checking_Mode := Mode_Before;
1422 Copy_Env (Current_Perm_Env,
1425 -- Here we have the original env in saved, current with a fresh
1426 -- copy, and new aliased.
1428 -- First alternative
1433 Copy_Env (Current_Perm_Env,
1436 Free_Env (Current_Perm_Env);
1438 -- Other alternatives
1440 while Present (Elmt) loop
1441 -- Restore environment
1443 Copy_Env (Saved_Env,
1448 -- Merge Current_Perm_Env into New_Env
1450 Merge_Envs (New_Env,
1461 Free_Env (Saved_Env);
1464 -- Analyze the list of associates in the aggregate as well as the
1467 when N_Extension_Aggregate =>
1469 Check_Node (Ancestor_Part (Expr));
1470 Check_List (Expressions (Expr));
1473 Check_Node (Low_Bound (Expr));
1474 Check_Node (High_Bound (Expr));
1476 -- We arrived at a path. Process it.
1478 when N_Selected_Component =>
1479 Process_Path (Expr);
1482 Process_Path (Expr);
1484 when N_Type_Conversion =>
1485 Check_Node (Expression (Expr));
1487 when N_Unchecked_Type_Conversion =>
1488 Check_Node (Expression (Expr));
1490 -- Checking should not be called directly on these nodes
1492 when N_Target_Name =>
1493 raise Program_Error;
1495 -- Unsupported constructs in SPARK
1497 when N_Delta_Aggregate =>
1498 Error_Msg_N ("unsupported construct in SPARK", Expr);
1500 -- Ignored constructs for pointer checking
1502 when N_Character_Literal
1504 | N_Numeric_Or_String_Literal
1506 | N_Raise_Expression
1511 -- The following nodes are never generated in GNATprove mode
1513 when N_Expression_With_Actions
1515 | N_Unchecked_Expression
1517 raise Program_Error;
1520 end Check_Expression;
1526 procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode) is
1528 if Nkind (N) = N_Empty then
1534 (List_Length (Pragma_Argument_Associations (N)) = 1);
1536 PAA : constant Node_Id :=
1537 First (Pragma_Argument_Associations (N));
1538 pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association);
1544 procedure Process (Mode : Name_Id;
1545 The_Global : Entity_Id);
1547 procedure Process (Mode : Name_Id;
1548 The_Global : Node_Id)
1550 Ident_Elt : constant Entity_Id :=
1551 Unique_Entity (Entity (The_Global));
1553 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1556 if Ekind (Ident_Elt) = E_Abstract_State then
1566 Check_Node (The_Global);
1574 raise Program_Error;
1583 if not Is_Borrowed_In (Ident_Elt) then
1586 Current_Checking_Mode := Observe;
1587 Check_Node (The_Global);
1600 Current_Checking_Mode := Borrow_Out;
1601 Check_Node (The_Global);
1613 if Is_Borrowed_In (Ident_Elt) then
1616 Current_Checking_Mode := Move;
1629 Current_Checking_Mode := Move;
1632 raise Program_Error;
1635 Check_Node (The_Global);
1646 -- Borrowed out or in out
1648 Process_Path (The_Global);
1651 raise Program_Error;
1655 raise Program_Error;
1658 Current_Checking_Mode := Mode_Before;
1662 if Nkind (Expression (PAA)) = N_Null then
1664 -- No globals, nothing to do
1667 elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
1670 Process (Name_Input, Expression (PAA));
1672 elsif Nkind (Expression (PAA)) = N_Aggregate
1673 and then Expressions (Expression (PAA)) /= No_List
1675 -- global => (foo, bar)
1677 RHS := First (Expressions (Expression (PAA)));
1678 while Present (RHS) loop
1683 Process (Name_Input, RHS);
1685 when N_Numeric_Or_String_Literal =>
1686 Process (Name_Input, Original_Node (RHS));
1689 raise Program_Error;
1695 elsif Nkind (Expression (PAA)) = N_Aggregate
1696 and then Component_Associations (Expression (PAA)) /= No_List
1698 -- global => (mode => foo,
1699 -- mode => (bar, baz))
1700 -- A mixture of things
1703 CA : constant List_Id :=
1704 Component_Associations (Expression (PAA));
1707 while Present (Row) loop
1708 pragma Assert (List_Length (Choices (Row)) = 1);
1709 The_Mode := Chars (First (Choices (Row)));
1711 RHS := Expression (Row);
1714 RHS := First (Expressions (RHS));
1715 while Present (RHS) loop
1717 when N_Numeric_Or_String_Literal =>
1718 Process (The_Mode, Original_Node (RHS));
1721 Process (The_Mode, RHS);
1730 Process (The_Mode, RHS);
1735 when N_Numeric_Or_String_Literal =>
1736 Process (The_Mode, Original_Node (RHS));
1739 raise Program_Error;
1748 raise Program_Error;
1757 procedure Check_List (L : List_Id) is
1761 while Present (N) loop
1767 --------------------------
1768 -- Check_Loop_Statement --
1769 --------------------------
1771 procedure Check_Loop_Statement (Loop_N : Node_Id) is
1773 -- Local Subprograms
1775 procedure Check_Is_Less_Restrictive_Env
1776 (Exiting_Env : Perm_Env;
1777 Entry_Env : Perm_Env);
1778 -- This procedure checks that the Exiting_Env environment is less
1779 -- restrictive than the Entry_Env environment.
1781 procedure Check_Is_Less_Restrictive_Tree
1782 (New_Tree : Perm_Tree_Access;
1783 Orig_Tree : Perm_Tree_Access;
1785 -- Auxiliary procedure to check that the tree New_Tree is less
1786 -- restrictive than the tree Orig_Tree for the entity E.
1788 procedure Perm_Error_Loop_Exit
1792 Found_Perm : Perm_Kind);
1793 -- A procedure that is called when the permissions found contradict
1794 -- the rules established by the RM at the exit of loops. This function
1795 -- is called with the entity, the node of the enclosing loop, the
1796 -- permission that was expected and the permission found, and issues
1797 -- an appropriate error message.
1799 -----------------------------------
1800 -- Check_Is_Less_Restrictive_Env --
1801 -----------------------------------
1803 procedure Check_Is_Less_Restrictive_Env
1804 (Exiting_Env : Perm_Env;
1805 Entry_Env : Perm_Env)
1807 Comp_Entry : Perm_Tree_Maps.Key_Option;
1808 Iter_Entry, Iter_Exit : Perm_Tree_Access;
1811 Comp_Entry := Get_First_Key (Entry_Env);
1812 while Comp_Entry.Present loop
1813 Iter_Entry := Get (Entry_Env, Comp_Entry.K);
1814 pragma Assert (Iter_Entry /= null);
1815 Iter_Exit := Get (Exiting_Env, Comp_Entry.K);
1816 pragma Assert (Iter_Exit /= null);
1817 Check_Is_Less_Restrictive_Tree
1818 (New_Tree => Iter_Exit,
1819 Orig_Tree => Iter_Entry,
1821 Comp_Entry := Get_Next_Key (Entry_Env);
1823 end Check_Is_Less_Restrictive_Env;
1825 ------------------------------------
1826 -- Check_Is_Less_Restrictive_Tree --
1827 ------------------------------------
1829 procedure Check_Is_Less_Restrictive_Tree
1830 (New_Tree : Perm_Tree_Access;
1831 Orig_Tree : Perm_Tree_Access;
1834 -----------------------
1835 -- Local Subprograms --
1836 -----------------------
1838 procedure Check_Is_Less_Restrictive_Tree_Than
1839 (Tree : Perm_Tree_Access;
1842 -- Auxiliary procedure to check that the tree N is less restrictive
1843 -- than the given permission P.
1845 procedure Check_Is_More_Restrictive_Tree_Than
1846 (Tree : Perm_Tree_Access;
1849 -- Auxiliary procedure to check that the tree N is more restrictive
1850 -- than the given permission P.
1852 -----------------------------------------
1853 -- Check_Is_Less_Restrictive_Tree_Than --
1854 -----------------------------------------
1856 procedure Check_Is_Less_Restrictive_Tree_Than
1857 (Tree : Perm_Tree_Access;
1862 if not (Permission (Tree) >= Perm) then
1863 Perm_Error_Loop_Exit
1864 (E, Loop_N, Permission (Tree), Perm);
1868 when Entire_Object =>
1869 if not (Children_Permission (Tree) >= Perm) then
1870 Perm_Error_Loop_Exit
1871 (E, Loop_N, Children_Permission (Tree), Perm);
1876 Check_Is_Less_Restrictive_Tree_Than
1877 (Get_All (Tree), Perm, E);
1879 when Array_Component =>
1880 Check_Is_Less_Restrictive_Tree_Than
1881 (Get_Elem (Tree), Perm, E);
1883 when Record_Component =>
1885 Comp : Perm_Tree_Access;
1887 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
1888 while Comp /= null loop
1889 Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E);
1891 Perm_Tree_Maps.Get_Next (Component (Tree));
1894 Check_Is_Less_Restrictive_Tree_Than
1895 (Other_Components (Tree), Perm, E);
1898 end Check_Is_Less_Restrictive_Tree_Than;
1900 -----------------------------------------
1901 -- Check_Is_More_Restrictive_Tree_Than --
1902 -----------------------------------------
1904 procedure Check_Is_More_Restrictive_Tree_Than
1905 (Tree : Perm_Tree_Access;
1910 if not (Perm >= Permission (Tree)) then
1911 Perm_Error_Loop_Exit
1912 (E, Loop_N, Permission (Tree), Perm);
1916 when Entire_Object =>
1917 if not (Perm >= Children_Permission (Tree)) then
1918 Perm_Error_Loop_Exit
1919 (E, Loop_N, Children_Permission (Tree), Perm);
1923 Check_Is_More_Restrictive_Tree_Than
1924 (Get_All (Tree), Perm, E);
1926 when Array_Component =>
1927 Check_Is_More_Restrictive_Tree_Than
1928 (Get_Elem (Tree), Perm, E);
1930 when Record_Component =>
1932 Comp : Perm_Tree_Access;
1934 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
1935 while Comp /= null loop
1936 Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E);
1938 Perm_Tree_Maps.Get_Next (Component (Tree));
1941 Check_Is_More_Restrictive_Tree_Than
1942 (Other_Components (Tree), Perm, E);
1945 end Check_Is_More_Restrictive_Tree_Than;
1947 -- Start of processing for Check_Is_Less_Restrictive_Tree
1950 if not (Permission (New_Tree) <= Permission (Orig_Tree)) then
1951 Perm_Error_Loop_Exit
1954 Perm => Permission (New_Tree),
1955 Found_Perm => Permission (Orig_Tree));
1958 case Kind (New_Tree) is
1960 -- Potentially folded tree. We check the other tree Orig_Tree to
1961 -- check whether it is folded or not. If folded we just compare
1962 -- their Permission and Children_Permission, if not, then we
1963 -- look at the Children_Permission of the folded tree against
1964 -- the unfolded tree Orig_Tree.
1966 when Entire_Object =>
1967 case Kind (Orig_Tree) is
1968 when Entire_Object =>
1969 if not (Children_Permission (New_Tree) <=
1970 Children_Permission (Orig_Tree))
1972 Perm_Error_Loop_Exit
1974 Children_Permission (New_Tree),
1975 Children_Permission (Orig_Tree));
1979 Check_Is_More_Restrictive_Tree_Than
1980 (Get_All (Orig_Tree), Children_Permission (New_Tree), E);
1982 when Array_Component =>
1983 Check_Is_More_Restrictive_Tree_Than
1984 (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E);
1986 when Record_Component =>
1988 Comp : Perm_Tree_Access;
1990 Comp := Perm_Tree_Maps.Get_First
1991 (Component (Orig_Tree));
1992 while Comp /= null loop
1993 Check_Is_More_Restrictive_Tree_Than
1994 (Comp, Children_Permission (New_Tree), E);
1995 Comp := Perm_Tree_Maps.Get_Next
1996 (Component (Orig_Tree));
1999 Check_Is_More_Restrictive_Tree_Than
2000 (Other_Components (Orig_Tree),
2001 Children_Permission (New_Tree), E);
2006 case Kind (Orig_Tree) is
2007 when Entire_Object =>
2008 Check_Is_Less_Restrictive_Tree_Than
2009 (Get_All (New_Tree), Children_Permission (Orig_Tree), E);
2012 Check_Is_Less_Restrictive_Tree
2013 (Get_All (New_Tree), Get_All (Orig_Tree), E);
2016 raise Program_Error;
2019 when Array_Component =>
2020 case Kind (Orig_Tree) is
2021 when Entire_Object =>
2022 Check_Is_Less_Restrictive_Tree_Than
2023 (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E);
2025 when Array_Component =>
2026 Check_Is_Less_Restrictive_Tree
2027 (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E);
2030 raise Program_Error;
2033 when Record_Component =>
2035 CompN : Perm_Tree_Access;
2038 Perm_Tree_Maps.Get_First (Component (New_Tree));
2039 case Kind (Orig_Tree) is
2040 when Entire_Object =>
2041 while CompN /= null loop
2042 Check_Is_Less_Restrictive_Tree_Than
2043 (CompN, Children_Permission (Orig_Tree), E);
2046 Perm_Tree_Maps.Get_Next (Component (New_Tree));
2049 Check_Is_Less_Restrictive_Tree_Than
2050 (Other_Components (New_Tree),
2051 Children_Permission (Orig_Tree),
2054 when Record_Component =>
2057 KeyO : Perm_Tree_Maps.Key_Option;
2058 CompO : Perm_Tree_Access;
2060 KeyO := Perm_Tree_Maps.Get_First_Key
2061 (Component (Orig_Tree));
2062 while KeyO.Present loop
2063 pragma Assert (CompO /= null);
2065 Check_Is_Less_Restrictive_Tree (CompN, CompO, E);
2067 KeyO := Perm_Tree_Maps.Get_Next_Key
2068 (Component (Orig_Tree));
2069 CompN := Perm_Tree_Maps.Get
2070 (Component (New_Tree), KeyO.K);
2071 CompO := Perm_Tree_Maps.Get
2072 (Component (Orig_Tree), KeyO.K);
2075 Check_Is_Less_Restrictive_Tree
2076 (Other_Components (New_Tree),
2077 Other_Components (Orig_Tree),
2082 raise Program_Error;
2086 end Check_Is_Less_Restrictive_Tree;
2088 --------------------------
2089 -- Perm_Error_Loop_Exit --
2090 --------------------------
2092 procedure Perm_Error_Loop_Exit
2096 Found_Perm : Perm_Kind)
2099 Error_Msg_Node_2 := Loop_Id;
2100 Error_Msg_N ("insufficient permission for & when exiting loop &", E);
2101 Perm_Mismatch (Exp_Perm => Perm,
2102 Act_Perm => Found_Perm,
2104 end Perm_Error_Loop_Exit;
2108 Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
2109 Loop_Env : constant Perm_Env_Access := new Perm_Env;
2112 -- Save environment prior to the loop
2114 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
2116 -- Add saved environment to loop environment
2118 Set (Current_Loops_Envs, Loop_Name, Loop_Env);
2120 -- If the loop is not a plain-loop, then it may either never be entered,
2121 -- or it may be exited after a number of iterations. Hence add the
2122 -- current permission environment as the initial loop exit environment.
2123 -- Otherwise, the loop exit environment remains empty until it is
2124 -- populated by analyzing exit statements.
2126 if Present (Iteration_Scheme (Loop_N)) then
2128 Exit_Env : constant Perm_Env_Access := new Perm_Env;
2130 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
2131 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
2137 Check_Node (Iteration_Scheme (Loop_N));
2138 Check_List (Statements (Loop_N));
2140 -- Check that environment gets less restrictive at end of loop
2142 Check_Is_Less_Restrictive_Env
2143 (Exiting_Env => Current_Perm_Env,
2144 Entry_Env => Loop_Env.all);
2146 -- Set environment to the one for exiting the loop
2149 Exit_Env : constant Perm_Env_Access :=
2150 Get (Current_Loops_Accumulators, Loop_Name);
2152 Free_Env (Current_Perm_Env);
2154 -- In the normal case, Exit_Env is not null and we use it. In the
2155 -- degraded case of a plain-loop without exit statements, Exit_Env is
2156 -- null, and we use the initial permission environment at the start
2157 -- of the loop to continue analysis. Any environment would be fine
2158 -- here, since the code after the loop is dead code, but this way we
2159 -- avoid spurious errors by having at least variables in scope inside
2162 if Exit_Env /= null then
2163 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
2165 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
2168 Free_Env (Loop_Env.all);
2169 Free_Env (Exit_Env.all);
2171 end Check_Loop_Statement;
2177 procedure Check_Node (N : Node_Id) is
2178 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2181 when N_Declaration =>
2182 Check_Declaration (N);
2185 Check_Expression (N);
2187 when N_Subtype_Indication =>
2188 Check_Node (Constraint (N));
2191 Check_Node (Get_Body_From_Stub (N));
2193 when N_Statement_Other_Than_Procedure_Call =>
2194 Check_Statement (N);
2196 when N_Package_Body =>
2197 Check_Package_Body (N);
2199 when N_Subprogram_Body
2203 Check_Callable_Body (N);
2205 when N_Protected_Body =>
2206 Check_List (Declarations (N));
2208 when N_Package_Declaration =>
2210 Spec : constant Node_Id := Specification (N);
2212 Current_Checking_Mode := Read;
2213 Check_List (Visible_Declarations (Spec));
2214 Check_List (Private_Declarations (Spec));
2216 Return_Declarations (Visible_Declarations (Spec));
2217 Return_Declarations (Private_Declarations (Spec));
2220 when N_Iteration_Scheme =>
2221 Current_Checking_Mode := Read;
2222 Check_Node (Condition (N));
2223 Check_Node (Iterator_Specification (N));
2224 Check_Node (Loop_Parameter_Specification (N));
2226 when N_Case_Expression_Alternative =>
2227 Current_Checking_Mode := Read;
2228 Check_List (Discrete_Choices (N));
2229 Current_Checking_Mode := Mode_Before;
2230 Check_Node (Expression (N));
2232 when N_Case_Statement_Alternative =>
2233 Current_Checking_Mode := Read;
2234 Check_List (Discrete_Choices (N));
2235 Current_Checking_Mode := Mode_Before;
2236 Check_List (Statements (N));
2238 when N_Component_Association =>
2239 Check_Node (Expression (N));
2241 when N_Handled_Sequence_Of_Statements =>
2242 Check_List (Statements (N));
2244 when N_Parameter_Association =>
2245 Check_Node (Explicit_Actual_Parameter (N));
2247 when N_Range_Constraint =>
2248 Check_Node (Range_Expression (N));
2250 when N_Index_Or_Discriminant_Constraint =>
2251 Check_List (Constraints (N));
2253 -- Checking should not be called directly on these nodes
2255 when N_Abortable_Part
2256 | N_Accept_Alternative
2257 | N_Access_Definition
2258 | N_Access_Function_Definition
2259 | N_Access_Procedure_Definition
2260 | N_Access_To_Object_Definition
2261 | N_Aspect_Specification
2262 | N_Compilation_Unit
2263 | N_Compilation_Unit_Aux
2264 | N_Component_Clause
2265 | N_Component_Definition
2267 | N_Constrained_Array_Definition
2269 | N_Decimal_Fixed_Point_Definition
2270 | N_Defining_Character_Literal
2271 | N_Defining_Identifier
2272 | N_Defining_Operator_Symbol
2273 | N_Defining_Program_Unit_Name
2274 | N_Delay_Alternative
2275 | N_Derived_Type_Definition
2277 | N_Discriminant_Association
2278 | N_Discriminant_Specification
2280 | N_Entry_Body_Formal_Part
2281 | N_Enumeration_Type_Definition
2282 | N_Entry_Call_Alternative
2283 | N_Entry_Index_Specification
2285 | N_Exception_Handler
2286 | N_Floating_Point_Definition
2287 | N_Formal_Decimal_Fixed_Point_Definition
2288 | N_Formal_Derived_Type_Definition
2289 | N_Formal_Discrete_Type_Definition
2290 | N_Formal_Floating_Point_Definition
2291 | N_Formal_Incomplete_Type_Definition
2292 | N_Formal_Modular_Type_Definition
2293 | N_Formal_Ordinary_Fixed_Point_Definition
2294 | N_Formal_Private_Type_Definition
2295 | N_Formal_Signed_Integer_Type_Definition
2296 | N_Generic_Association
2298 | N_Modular_Type_Definition
2299 | N_Ordinary_Fixed_Point_Definition
2300 | N_Package_Specification
2301 | N_Parameter_Specification
2302 | N_Pragma_Argument_Association
2303 | N_Protected_Definition
2304 | N_Push_Pop_xxx_Label
2305 | N_Real_Range_Specification
2306 | N_Record_Definition
2307 | N_SCIL_Dispatch_Table_Tag_Init
2308 | N_SCIL_Dispatching_Call
2309 | N_SCIL_Membership_Test
2310 | N_Signed_Integer_Type_Definition
2313 | N_Terminate_Alternative
2314 | N_Triggering_Alternative
2315 | N_Unconstrained_Array_Definition
2321 raise Program_Error;
2323 -- Unsupported constructs in SPARK
2325 when N_Iterated_Component_Association =>
2326 Error_Msg_N ("unsupported construct in SPARK", N);
2328 -- Ignored constructs for pointer checking
2330 when N_Abstract_Subprogram_Declaration
2332 | N_Attribute_Definition_Clause
2334 | N_Delta_Constraint
2335 | N_Digits_Constraint
2337 | N_Enumeration_Representation_Clause
2338 | N_Exception_Declaration
2339 | N_Exception_Renaming_Declaration
2340 | N_Formal_Package_Declaration
2341 | N_Formal_Subprogram_Declaration
2343 | N_Freeze_Generic_Entity
2344 | N_Function_Instantiation
2345 | N_Generic_Function_Renaming_Declaration
2346 | N_Generic_Package_Declaration
2347 | N_Generic_Package_Renaming_Declaration
2348 | N_Generic_Procedure_Renaming_Declaration
2349 | N_Generic_Subprogram_Declaration
2350 | N_Implicit_Label_Declaration
2353 | N_Number_Declaration
2354 | N_Object_Renaming_Declaration
2356 | N_Package_Instantiation
2357 | N_Package_Renaming_Declaration
2359 | N_Procedure_Instantiation
2360 | N_Record_Representation_Clause
2361 | N_Subprogram_Declaration
2362 | N_Subprogram_Renaming_Declaration
2363 | N_Task_Type_Declaration
2364 | N_Use_Package_Clause
2367 | N_Validate_Unchecked_Conversion
2368 | N_Variable_Reference_Marker
2372 -- The following nodes are rewritten by semantic analysis
2374 when N_Single_Protected_Declaration
2375 | N_Single_Task_Declaration
2377 raise Program_Error;
2380 Current_Checking_Mode := Mode_Before;
2383 ------------------------
2384 -- Check_Package_Body --
2385 ------------------------
2387 procedure Check_Package_Body (Pack : Node_Id) is
2388 Saved_Env : Perm_Env;
2392 if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
2393 if Get_SPARK_Mode_From_Annotation
2394 (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
2402 CorSp := Parent (Corresponding_Spec (Pack));
2403 while Nkind (CorSp) /= N_Package_Specification loop
2404 CorSp := Parent (CorSp);
2407 Check_List (Visible_Declarations (CorSp));
2411 Copy_Env (Current_Perm_Env,
2414 Check_List (Private_Declarations (CorSp));
2416 -- Set mode to Read, and then analyze declarations and statements
2418 Current_Checking_Mode := Read;
2420 Check_List (Declarations (Pack));
2421 Check_Node (Handled_Statement_Sequence (Pack));
2423 -- Check RW for every stateful variable (i.e. in declarations)
2425 Return_Declarations (Private_Declarations (CorSp));
2426 Return_Declarations (Visible_Declarations (CorSp));
2427 Return_Declarations (Declarations (Pack));
2429 -- Restore previous environment (i.e. delete every nonvisible
2430 -- declaration) from environment.
2432 Free_Env (Current_Perm_Env);
2433 Copy_Env (Saved_Env,
2435 end Check_Package_Body;
2441 procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
2442 Mode : constant Entity_Kind := Ekind (Formal);
2443 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2446 case Current_Checking_Mode is
2448 case Formal_Kind'(Mode
) is
2449 when E_In_Parameter
=>
2450 if Is_Borrowed_In
(Formal
) then
2453 Current_Checking_Mode
:= Move
;
2460 when E_Out_Parameter
=>
2463 when E_In_Out_Parameter
=>
2466 Current_Checking_Mode
:= Move
;
2470 Check_Node
(Actual
);
2473 case Formal_Kind
'(Mode) is
2474 when E_In_Parameter =>
2477 when E_Out_Parameter
2478 | E_In_Out_Parameter
2480 -- Borrowed out or in out
2482 Process_Path (Actual);
2487 raise Program_Error;
2490 Current_Checking_Mode := Mode_Before;
2493 --------------------------
2494 -- Check_Param_Observes --
2495 --------------------------
2497 procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is
2498 Mode : constant Entity_Kind := Ekind (Formal);
2499 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2503 when E_In_Parameter =>
2504 if not Is_Borrowed_In (Formal) then
2507 Current_Checking_Mode := Observe;
2508 Check_Node (Actual);
2516 Current_Checking_Mode := Mode_Before;
2517 end Check_Param_Observes;
2519 ----------------------
2520 -- Check_Param_Outs --
2521 ----------------------
2523 procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is
2524 Mode : constant Entity_Kind := Ekind (Formal);
2525 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2530 when E_Out_Parameter =>
2532 Current_Checking_Mode := Borrow_Out;
2533 Check_Node (Actual);
2540 Current_Checking_Mode := Mode_Before;
2541 end Check_Param_Outs;
2543 ----------------------
2544 -- Check_Param_Read --
2545 ----------------------
2547 procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is
2548 Mode : constant Entity_Kind := Ekind (Formal);
2551 pragma Assert (Current_Checking_Mode = Read);
2553 case Formal_Kind'(Mode
) is
2554 when E_In_Parameter
=>
2555 Check_Node
(Actual
);
2557 when E_Out_Parameter
2558 | E_In_Out_Parameter
2563 end Check_Param_Read
;
2565 -------------------------
2566 -- Check_Safe_Pointers --
2567 -------------------------
2569 procedure Check_Safe_Pointers
(N
: Node_Id
) is
2571 -- Local subprograms
2573 procedure Check_List
(L
: List_Id
);
2574 -- Call the main analysis procedure on each element of the list
2576 procedure Initialize
;
2577 -- Initialize global variables before starting the analysis of a body
2583 procedure Check_List
(L
: List_Id
) is
2587 while Present
(N
) loop
2588 Check_Safe_Pointers
(N
);
2597 procedure Initialize
is
2599 Reset
(Current_Loops_Envs
);
2600 Reset
(Current_Loops_Accumulators
);
2601 Reset
(Current_Perm_Env
);
2602 Reset
(Current_Initialization_Map
);
2608 -- SPARK_Mode pragma in application
2610 -- Start of processing for Check_Safe_Pointers
2616 when N_Compilation_Unit
=>
2617 Check_Safe_Pointers
(Unit
(N
));
2620 | N_Package_Declaration
2623 Prag
:= SPARK_Pragma
(Defining_Entity
(N
));
2624 if Present
(Prag
) then
2625 if Get_SPARK_Mode_From_Annotation
(Prag
) = Opt
.Off
then
2631 elsif Nkind
(N
) = N_Package_Body
then
2632 Check_List
(Declarations
(N
));
2634 elsif Nkind
(N
) = N_Package_Declaration
then
2635 Check_List
(Private_Declarations
(Specification
(N
)));
2636 Check_List
(Visible_Declarations
(Specification
(N
)));
2642 end Check_Safe_Pointers
;
2644 ---------------------
2645 -- Check_Statement --
2646 ---------------------
2648 procedure Check_Statement
(Stmt
: Node_Id
) is
2649 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
2651 case N_Statement_Other_Than_Procedure_Call
'(Nkind (Stmt)) is
2652 when N_Entry_Call_Statement =>
2653 Check_Call_Statement (Stmt);
2655 -- Move right-hand side first, and then assign left-hand side
2657 when N_Assignment_Statement =>
2658 if Is_Deep (Etype (Expression (Stmt))) then
2659 Current_Checking_Mode := Move;
2661 Current_Checking_Mode := Read;
2664 Check_Node (Expression (Stmt));
2665 Current_Checking_Mode := Assign;
2666 Check_Node (Name (Stmt));
2668 when N_Block_Statement =>
2670 Saved_Env : Perm_Env;
2675 Copy_Env (Current_Perm_Env,
2678 -- Analyze declarations and Handled_Statement_Sequences
2680 Current_Checking_Mode := Read;
2681 Check_List (Declarations (Stmt));
2682 Check_Node (Handled_Statement_Sequence (Stmt));
2684 -- Restore environment
2686 Free_Env (Current_Perm_Env);
2687 Copy_Env (Saved_Env,
2691 when N_Case_Statement =>
2693 Saved_Env : Perm_Env;
2695 -- Accumulator for the different branches
2699 Elmt : Node_Id := First (Alternatives (Stmt));
2702 Current_Checking_Mode := Read;
2703 Check_Node (Expression (Stmt));
2704 Current_Checking_Mode := Mode_Before;
2708 Copy_Env (Current_Perm_Env,
2711 -- Here we have the original env in saved, current with a fresh
2712 -- copy, and new aliased.
2714 -- First alternative
2719 Copy_Env (Current_Perm_Env,
2721 Free_Env (Current_Perm_Env);
2723 -- Other alternatives
2725 while Present (Elmt) loop
2726 -- Restore environment
2728 Copy_Env (Saved_Env,
2733 -- Merge Current_Perm_Env into New_Env
2735 Merge_Envs (New_Env,
2746 Free_Env (Saved_Env);
2749 when N_Delay_Relative_Statement =>
2750 Check_Node (Expression (Stmt));
2752 when N_Delay_Until_Statement =>
2753 Check_Node (Expression (Stmt));
2755 when N_Loop_Statement =>
2756 Check_Loop_Statement (Stmt);
2758 -- If deep type expression, then move, else read
2760 when N_Simple_Return_Statement =>
2761 case Nkind (Expression (Stmt)) is
2764 -- ??? This does not take into account the fact that
2765 -- a simple return inside an extended return statement
2766 -- applies to the extended return statement.
2767 Subp : constant Entity_Id :=
2768 Return_Applies_To (Return_Statement_Entity (Stmt));
2770 Return_Parameters (Subp);
2771 Return_Globals (Subp);
2775 if Is_Deep (Etype (Expression (Stmt))) then
2776 Current_Checking_Mode := Move;
2777 elsif Is_Shallow (Etype (Expression (Stmt))) then
2778 Current_Checking_Mode := Read;
2780 raise Program_Error;
2783 Check_Node (Expression (Stmt));
2786 when N_Extended_Return_Statement =>
2787 Check_List (Return_Object_Declarations (Stmt));
2788 Check_Node (Handled_Statement_Sequence (Stmt));
2790 Return_Declarations (Return_Object_Declarations (Stmt));
2793 -- ??? This does not take into account the fact that a simple
2794 -- return inside an extended return statement applies to the
2795 -- extended return statement.
2796 Subp : constant Entity_Id :=
2797 Return_Applies_To (Return_Statement_Entity (Stmt));
2799 Return_Parameters (Subp);
2800 Return_Globals (Subp);
2803 -- Merge the current_Perm_Env with the accumulator for the given loop
2805 when N_Exit_Statement =>
2807 Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
2809 Saved_Accumulator : constant Perm_Env_Access :=
2810 Get (Current_Loops_Accumulators, Loop_Name);
2812 Environment_Copy : constant Perm_Env_Access :=
2816 Copy_Env (Current_Perm_Env,
2817 Environment_Copy.all);
2819 if Saved_Accumulator = null then
2820 Set (Current_Loops_Accumulators,
2821 Loop_Name, Environment_Copy);
2823 Merge_Envs (Saved_Accumulator.all,
2824 Environment_Copy.all);
2828 -- Copy environment, run on each branch, and then merge
2830 when N_If_Statement =>
2832 Saved_Env : Perm_Env;
2834 -- Accumulator for the different branches
2840 Check_Node (Condition (Stmt));
2844 Copy_Env (Current_Perm_Env,
2847 -- Here we have the original env in saved, current with a fresh
2852 Check_List (Then_Statements (Stmt));
2854 Copy_Env (Current_Perm_Env,
2857 Free_Env (Current_Perm_Env);
2859 -- Here the new_environment contains curr env after then block
2866 Elmt := First (Elsif_Parts (Stmt));
2867 while Present (Elmt) loop
2868 -- Transfer into accumulator, and restore from save
2870 Copy_Env (Saved_Env,
2873 Check_Node (Condition (Elmt));
2874 Check_List (Then_Statements (Stmt));
2876 -- Merge Current_Perm_Env into New_Env
2878 Merge_Envs (New_Env,
2887 -- Restore environment before if
2889 Copy_Env (Saved_Env,
2892 -- Here new environment contains the environment after then and
2893 -- current the fresh copy of old one.
2895 Check_List (Else_Statements (Stmt));
2897 Merge_Envs (New_Env,
2906 Free_Env (Saved_Env);
2909 -- Unsupported constructs in SPARK
2911 when N_Abort_Statement
2912 | N_Accept_Statement
2913 | N_Asynchronous_Select
2915 | N_Conditional_Entry_Call
2917 | N_Requeue_Statement
2918 | N_Selective_Accept
2919 | N_Timed_Entry_Call
2921 Error_Msg_N ("unsupported construct in SPARK", Stmt);
2923 -- Ignored constructs for pointer checking
2925 when N_Null_Statement
2930 -- The following nodes are never generated in GNATprove mode
2932 when N_Compound_Statement
2935 raise Program_Error;
2937 end Check_Statement;
2943 function Get_Perm (N : Node_Id) return Perm_Kind is
2944 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
2947 case Tree_Or_Perm.R is
2949 return Tree_Or_Perm.Found_Permission;
2952 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
2953 return Permission (Tree_Or_Perm.Tree_Access);
2955 -- We encoutered a function call, hence the memory area is fresh,
2956 -- which means that the association permission is RW.
2958 when Function_Call =>
2964 ----------------------
2965 -- Get_Perm_Or_Tree --
2966 ----------------------
2968 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
2972 -- Base identifier. Normally those are the roots of the trees stored
2973 -- in the permission environment.
2975 when N_Defining_Identifier =>
2976 raise Program_Error;
2982 P : constant Entity_Id := Entity (N);
2984 C : constant Perm_Tree_Access :=
2985 Get (Current_Perm_Env, Unique_Entity (P));
2988 -- Setting the initialization map to True, so that this
2989 -- variable cannot be ignored anymore when looking at end
2990 -- of elaboration of package.
2992 Set (Current_Initialization_Map, Unique_Entity (P), True);
2995 -- No null possible here, there are no parents for the path.
2996 -- This means we are using a global variable without adding
2997 -- it in environment with a global aspect.
2999 Illegal_Global_Usage (N);
3001 return (R => Unfolded, Tree_Access => C);
3005 when N_Type_Conversion
3006 | N_Unchecked_Type_Conversion
3007 | N_Qualified_Expression
3009 return Get_Perm_Or_Tree (Expression (N));
3011 -- Happening when we try to get the permission of a variable that
3012 -- is a formal parameter. We get instead the defining identifier
3013 -- associated with the parameter (which is the one that has been
3014 -- stored for indexing).
3016 when N_Parameter_Specification =>
3017 return Get_Perm_Or_Tree (Defining_Identifier (N));
3019 -- We get the permission tree of its prefix, and then get either the
3020 -- subtree associated with that specific selection, or if we have a
3021 -- leaf that folds its children, we take the children's permission
3022 -- and return it using the discriminant Folded.
3024 when N_Selected_Component =>
3026 C : constant Perm_Or_Tree :=
3027 Get_Perm_Or_Tree (Prefix (N));
3037 pragma Assert (C.Tree_Access /= null);
3039 pragma Assert (Kind (C.Tree_Access) = Entire_Object
3041 Kind (C.Tree_Access) = Record_Component);
3043 if Kind (C.Tree_Access) = Record_Component then
3045 Selected_Component : constant Entity_Id :=
3046 Entity (Selector_Name (N));
3048 Selected_C : constant Perm_Tree_Access :=
3050 (Component (C.Tree_Access), Selected_Component);
3053 if Selected_C = null then
3054 return (R => Unfolded,
3056 Other_Components (C.Tree_Access));
3058 return (R => Unfolded,
3059 Tree_Access => Selected_C);
3062 elsif Kind (C.Tree_Access) = Entire_Object then
3063 return (R => Folded, Found_Permission =>
3064 Children_Permission (C.Tree_Access));
3066 raise Program_Error;
3071 -- We get the permission tree of its prefix, and then get either the
3072 -- subtree associated with that specific selection, or if we have a
3073 -- leaf that folds its children, we take the children's permission
3074 -- and return it using the discriminant Folded.
3076 when N_Indexed_Component
3080 C : constant Perm_Or_Tree :=
3081 Get_Perm_Or_Tree (Prefix (N));
3091 pragma Assert (C.Tree_Access /= null);
3093 pragma Assert (Kind (C.Tree_Access) = Entire_Object
3095 Kind (C.Tree_Access) = Array_Component);
3097 if Kind (C.Tree_Access) = Array_Component then
3098 pragma Assert (Get_Elem (C.Tree_Access) /= null);
3100 return (R => Unfolded,
3101 Tree_Access => Get_Elem (C.Tree_Access));
3102 elsif Kind (C.Tree_Access) = Entire_Object then
3103 return (R => Folded, Found_Permission =>
3104 Children_Permission (C.Tree_Access));
3106 raise Program_Error;
3111 -- We get the permission tree of its prefix, and then get either the
3112 -- subtree associated with that specific selection, or if we have a
3113 -- leaf that folds its children, we take the children's permission
3114 -- and return it using the discriminant Folded.
3116 when N_Explicit_Dereference =>
3118 C : constant Perm_Or_Tree :=
3119 Get_Perm_Or_Tree (Prefix (N));
3129 pragma Assert (C.Tree_Access /= null);
3131 pragma Assert (Kind (C.Tree_Access) = Entire_Object
3133 Kind (C.Tree_Access) = Reference);
3135 if Kind (C.Tree_Access) = Reference then
3136 if Get_All (C.Tree_Access) = null then
3138 raise Program_Error;
3142 Tree_Access => Get_All (C.Tree_Access));
3144 elsif Kind (C.Tree_Access) = Entire_Object then
3145 return (R => Folded, Found_Permission =>
3146 Children_Permission (C.Tree_Access));
3148 raise Program_Error;
3153 -- The name contains a function call, hence the given path is always
3154 -- new. We do not have to check for anything.
3156 when N_Function_Call =>
3157 return (R => Function_Call);
3160 raise Program_Error;
3162 end Get_Perm_Or_Tree;
3168 function Get_Perm_Tree
3170 return Perm_Tree_Access
3175 -- Base identifier. Normally those are the roots of the trees stored
3176 -- in the permission environment.
3178 when N_Defining_Identifier =>
3179 raise Program_Error;
3185 P : constant Node_Id := Entity (N);
3187 C : constant Perm_Tree_Access :=
3188 Get (Current_Perm_Env, Unique_Entity (P));
3191 -- Setting the initialization map to True, so that this
3192 -- variable cannot be ignored anymore when looking at end
3193 -- of elaboration of package.
3195 Set (Current_Initialization_Map, Unique_Entity (P), True);
3198 -- No null possible here, there are no parents for the path.
3199 -- This means we are using a global variable without adding
3200 -- it in environment with a global aspect.
3202 Illegal_Global_Usage (N);
3208 when N_Type_Conversion
3209 | N_Unchecked_Type_Conversion
3210 | N_Qualified_Expression
3212 return Get_Perm_Tree (Expression (N));
3214 when N_Parameter_Specification =>
3215 return Get_Perm_Tree (Defining_Identifier (N));
3217 -- We get the permission tree of its prefix, and then get either the
3218 -- subtree associated with that specific selection, or if we have a
3219 -- leaf that folds its children, we unroll it in one step.
3221 when N_Selected_Component =>
3223 C : constant Perm_Tree_Access :=
3224 Get_Perm_Tree (Prefix (N));
3228 -- If null then it means we went through a function call
3233 pragma Assert (Kind (C) = Entire_Object
3234 or else Kind (C) = Record_Component);
3236 if Kind (C) = Record_Component then
3237 -- The tree is unfolded. We just return the subtree.
3240 Selected_Component : constant Entity_Id :=
3241 Entity (Selector_Name (N));
3242 Selected_C : constant Perm_Tree_Access :=
3244 (Component (C), Selected_Component);
3247 if Selected_C = null then
3248 return Other_Components (C);
3253 elsif Kind (C) = Entire_Object then
3255 -- Expand the tree. Replace the node with
3256 -- Record_Component.
3260 -- Create the unrolled nodes
3262 Son : Perm_Tree_Access;
3264 Child_Perm : constant Perm_Kind :=
3265 Children_Permission (C);
3269 -- We change the current node from Entire_Object to
3270 -- Record_Component with same permission and an empty
3271 -- hash table as component list.
3274 (Kind => Record_Component,
3275 Is_Node_Deep => Is_Node_Deep (C),
3276 Permission => Permission (C),
3277 Component => Perm_Tree_Maps.Nil,
3279 new Perm_Tree_Wrapper'
3281 (Kind
=> Entire_Object
,
3282 -- Is_Node_Deep is true, to be conservative
3283 Is_Node_Deep
=> True,
3284 Permission
=> Child_Perm
,
3285 Children_Permission
=> Child_Perm
)
3289 -- We fill the hash table with all sons of the record,
3290 -- with basic Entire_Objects nodes.
3291 Elem
:= First_Component_Or_Discriminant
3292 (Etype
(Prefix
(N
)));
3294 while Present
(Elem
) loop
3295 Son
:= new Perm_Tree_Wrapper
'
3297 (Kind => Entire_Object,
3298 Is_Node_Deep => Is_Deep (Etype (Elem)),
3299 Permission => Child_Perm,
3300 Children_Permission => Child_Perm));
3303 (C.all.Tree.Component, Elem, Son);
3305 Next_Component_Or_Discriminant (Elem);
3308 -- we return the tree to the sons, so that the recursion
3312 Selected_Component : constant Entity_Id :=
3313 Entity (Selector_Name (N));
3315 Selected_C : constant Perm_Tree_Access :=
3317 (Component (C), Selected_Component);
3320 pragma Assert (Selected_C /= null);
3327 raise Program_Error;
3331 -- We set the permission tree of its prefix, and then we extract from
3332 -- the returned pointer the subtree. If folded, we unroll the tree at
3335 when N_Indexed_Component
3339 C : constant Perm_Tree_Access :=
3340 Get_Perm_Tree (Prefix (N));
3344 -- If null then we went through a function call
3349 pragma Assert (Kind (C) = Entire_Object
3350 or else Kind (C) = Array_Component);
3352 if Kind (C) = Array_Component then
3353 -- The tree is unfolded. We just return the elem subtree
3355 pragma Assert (Get_Elem (C) = null);
3357 return Get_Elem (C);
3358 elsif Kind (C) = Entire_Object then
3360 -- Expand the tree. Replace node with Array_Component.
3362 Son : Perm_Tree_Access;
3365 Son := new Perm_Tree_Wrapper'
3367 (Kind
=> Entire_Object
,
3368 Is_Node_Deep
=> Is_Node_Deep
(C
),
3369 Permission
=> Children_Permission
(C
),
3370 Children_Permission
=> Children_Permission
(C
)));
3372 -- We change the current node from Entire_Object
3373 -- to Array_Component with same permission and the
3374 -- previously defined son.
3376 C
.all.Tree
:= (Kind
=> Array_Component
,
3377 Is_Node_Deep
=> Is_Node_Deep
(C
),
3378 Permission
=> Permission
(C
),
3381 return Get_Elem
(C
);
3384 raise Program_Error
;
3388 -- We get the permission tree of its prefix, and then get either the
3389 -- subtree associated with that specific selection, or if we have a
3390 -- leaf that folds its children, we unroll the tree.
3392 when N_Explicit_Dereference
=>
3394 C
: Perm_Tree_Access
;
3397 C
:= Get_Perm_Tree
(Prefix
(N
));
3400 -- If null, we went through a function call
3405 pragma Assert
(Kind
(C
) = Entire_Object
3406 or else Kind
(C
) = Reference
);
3408 if Kind
(C
) = Reference
then
3409 -- The tree is unfolded. We return the elem subtree
3411 if Get_All
(C
) = null then
3413 raise Program_Error
;
3417 elsif Kind
(C
) = Entire_Object
then
3419 -- Expand the tree. Replace the node with Reference.
3421 Son
: Perm_Tree_Access
;
3424 Son
:= new Perm_Tree_Wrapper
'
3426 (Kind => Entire_Object,
3427 Is_Node_Deep => Is_Deep (Etype (N)),
3428 Permission => Children_Permission (C),
3429 Children_Permission => Children_Permission (C)));
3431 -- We change the current node from Entire_Object to
3432 -- Reference with same permission and the previous son.
3434 pragma Assert (Is_Node_Deep (C));
3436 C.all.Tree := (Kind => Reference,
3437 Is_Node_Deep => Is_Node_Deep (C),
3438 Permission => Permission (C),
3444 raise Program_Error;
3448 -- No permission tree for function calls
3450 when N_Function_Call =>
3454 raise Program_Error;
3462 function Glb (P1, P2 : Perm_Kind) return Perm_Kind
3504 function Has_Alias_Deep (Typ : Entity_Id) return Boolean;
3505 function Has_Alias_Deep (Typ : Entity_Id) return Boolean
3510 if Is_Array_Type (Typ)
3511 and then Has_Aliased_Components (Typ)
3515 -- Note: Has_Aliased_Components applies only to arrays
3517 elsif Is_Record_Type (Typ) then
3518 -- It is possible to have an aliased discriminant, so they must be
3519 -- checked along with normal components.
3521 Comp := First_Component_Or_Discriminant (Typ);
3522 while Present (Comp) loop
3523 if Is_Aliased (Comp)
3524 or else Is_Aliased (Etype (Comp))
3529 if Has_Alias_Deep (Etype (Comp)) then
3533 Next_Component_Or_Discriminant (Comp);
3537 return Is_Aliased (Typ);
3547 return Is_Aliased (Entity (N)) or else Has_Alias_Deep (Etype (N));
3549 when N_Defining_Identifier =>
3550 return Is_Aliased (N) or else Has_Alias_Deep (Etype (N));
3552 when N_Type_Conversion
3553 | N_Unchecked_Type_Conversion
3554 | N_Qualified_Expression
3556 return Has_Alias (Expression (N));
3558 when N_Parameter_Specification =>
3559 return Has_Alias (Defining_Identifier (N));
3561 when N_Selected_Component =>
3562 case Nkind (Selector_Name (N)) is
3563 when N_Identifier =>
3564 if Is_Aliased (Entity (Selector_Name (N))) then
3568 when others => null;
3572 return Has_Alias (Prefix (N));
3574 when N_Indexed_Component
3577 return Has_Alias (Prefix (N));
3579 when N_Explicit_Dereference =>
3582 when N_Function_Call =>
3585 when N_Attribute_Reference =>
3586 if Is_Deep (Etype (Prefix (N))) then
3587 raise Program_Error;
3596 -------------------------
3597 -- Has_Array_Component --
3598 -------------------------
3600 function Has_Array_Component (N : Node_Id) return Boolean is
3603 -- Base identifier. There is no array component here.
3607 | N_Defining_Identifier
3611 -- We check if the expression inside the conversion has an array
3614 when N_Type_Conversion
3615 | N_Unchecked_Type_Conversion
3616 | N_Qualified_Expression
3618 return Has_Array_Component (Expression (N));
3620 -- We check if the prefix has an array component
3622 when N_Selected_Component =>
3623 return Has_Array_Component (Prefix (N));
3625 -- We found the array component, return True
3627 when N_Indexed_Component
3632 -- We check if the prefix has an array component
3634 when N_Explicit_Dereference =>
3635 return Has_Array_Component (Prefix (N));
3637 when N_Function_Call =>
3641 raise Program_Error;
3643 end Has_Array_Component;
3645 ----------------------------
3646 -- Has_Function_Component --
3647 ----------------------------
3649 function Has_Function_Component (N : Node_Id) return Boolean is
3652 -- Base identifier. There is no function component here.
3656 | N_Defining_Identifier
3660 -- We check if the expression inside the conversion has a function
3663 when N_Type_Conversion
3664 | N_Unchecked_Type_Conversion
3665 | N_Qualified_Expression
3667 return Has_Function_Component (Expression (N));
3669 -- We check if the prefix has a function component
3671 when N_Selected_Component =>
3672 return Has_Function_Component (Prefix (N));
3674 -- We check if the prefix has a function component
3676 when N_Indexed_Component
3679 return Has_Function_Component (Prefix (N));
3681 -- We check if the prefix has a function component
3683 when N_Explicit_Dereference =>
3684 return Has_Function_Component (Prefix (N));
3686 -- We found the function component, return True
3688 when N_Function_Call =>
3692 raise Program_Error;
3695 end Has_Function_Component;
3701 procedure Hp (P : Perm_Env) is
3702 Elem : Perm_Tree_Maps.Key_Option;
3705 Elem := Get_First_Key (P);
3706 while Elem.Present loop
3707 Print_Node_Briefly (Elem.K);
3708 Elem := Get_Next_Key (P);
3712 --------------------------
3713 -- Illegal_Global_Usage --
3714 --------------------------
3716 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is
3718 Error_Msg_NE ("cannot use global variable & of deep type", N, N);
3719 Error_Msg_N ("\without prior declaration in a Global aspect", N);
3721 Errout.Finalize (Last_Call => True);
3722 Errout.Output_Messages;
3723 Exit_Program (E_Errors);
3724 end Illegal_Global_Usage;
3726 --------------------
3727 -- Is_Borrowed_In --
3728 --------------------
3730 function Is_Borrowed_In (E : Entity_Id) return Boolean is
3732 return Is_Access_Type (Etype (E))
3733 and then not Is_Access_Constant (Etype (E));
3740 function Is_Deep (E : Entity_Id) return Boolean is
3741 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean;
3743 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is
3745 Pack_Decl : Node_Id;
3748 if Is_Itype (E) then
3749 Decl := Associated_Node_For_Itype (E);
3754 Pack_Decl := Parent (Parent (Decl));
3756 if Nkind (Pack_Decl) /= N_Package_Declaration then
3761 Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl)))
3762 and then Get_SPARK_Mode_From_Annotation
3763 (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off;
3764 end Is_Private_Entity_Mode_Off;
3766 pragma Assert (Is_Type (E));
3775 -- Just check the depth of its component type
3780 return Is_Deep (Component_Type (E));
3782 when E_String_Literal_Subtype =>
3785 -- Per RM 8.11 for class-wide types
3787 when E_Class_Wide_Subtype
3792 -- ??? What about hidden components
3801 Elmt := First_Component_Or_Discriminant (E);
3802 while Present (Elmt) loop
3803 if Is_Deep (Etype (Elmt)) then
3806 Next_Component_Or_Discriminant (Elmt);
3813 when Private_Kind =>
3814 if Is_Private_Entity_Mode_Off (E) then
3817 if Present (Full_View (E)) then
3818 return Is_Deep (Full_View (E));
3824 when E_Incomplete_Type =>
3827 when E_Incomplete_Subtype =>
3830 -- No problem with synchronized types
3832 when E_Protected_Type
3833 | E_Protected_Subtype
3839 when E_Exception_Type =>
3843 raise Program_Error;
3851 function Is_Shallow (E : Entity_Id) return Boolean is
3853 pragma Assert (Is_Type (E));
3854 return not Is_Deep (E);
3861 function Loop_Of_Exit (N : Node_Id) return Entity_Id is
3862 Nam : Node_Id := Name (N);
3863 Stmt : Node_Id := N;
3866 while Present (Stmt) loop
3867 Stmt := Parent (Stmt);
3868 if Nkind (Stmt) = N_Loop_Statement then
3869 Nam := Identifier (Stmt);
3874 return Entity (Nam);
3880 function Lub (P1, P2 : Perm_Kind) return Perm_Kind
3918 procedure Merge_Envs
3919 (Target : in out Perm_Env;
3920 Source : in out Perm_Env)
3922 procedure Merge_Trees
3923 (Target : Perm_Tree_Access;
3924 Source : Perm_Tree_Access);
3926 procedure Merge_Trees
3927 (Target : Perm_Tree_Access;
3928 Source : Perm_Tree_Access)
3930 procedure Apply_Glb_Tree
3931 (A : Perm_Tree_Access;
3934 procedure Apply_Glb_Tree
3935 (A : Perm_Tree_Access;
3939 A.all.Tree.Permission := Glb (Permission (A), P);
3942 when Entire_Object =>
3943 A.all.Tree.Children_Permission :=
3944 Glb (Children_Permission (A), P);
3947 Apply_Glb_Tree (Get_All (A), P);
3949 when Array_Component =>
3950 Apply_Glb_Tree (Get_Elem (A), P);
3952 when Record_Component =>
3954 Comp : Perm_Tree_Access;
3956 Comp := Perm_Tree_Maps.Get_First (Component (A));
3957 while Comp /= null loop
3958 Apply_Glb_Tree (Comp, P);
3959 Comp := Perm_Tree_Maps.Get_Next (Component (A));
3962 Apply_Glb_Tree (Other_Components (A), P);
3967 Perm : constant Perm_Kind :=
3968 Glb (Permission (Target), Permission (Source));
3971 pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
3972 Target.all.Tree.Permission := Perm;
3974 case Kind (Target) is
3975 when Entire_Object =>
3977 Child_Perm : constant Perm_Kind :=
3978 Children_Permission (Target);
3981 case Kind (Source) is
3982 when Entire_Object =>
3983 Target.all.Tree.Children_Permission :=
3984 Glb (Child_Perm, Children_Permission (Source));
3987 Copy_Tree (Source, Target);
3988 Target.all.Tree.Permission := Perm;
3989 Apply_Glb_Tree (Get_All (Target), Child_Perm);
3991 when Array_Component =>
3992 Copy_Tree (Source, Target);
3993 Target.all.Tree.Permission := Perm;
3994 Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
3996 when Record_Component =>
3997 Copy_Tree (Source, Target);
3998 Target.all.Tree.Permission := Perm;
4000 Comp : Perm_Tree_Access;
4004 Perm_Tree_Maps.Get_First (Component (Target));
4005 while Comp /= null loop
4006 -- Apply glb tree on every component subtree
4008 Apply_Glb_Tree (Comp, Child_Perm);
4009 Comp := Perm_Tree_Maps.Get_Next
4010 (Component (Target));
4013 Apply_Glb_Tree (Other_Components (Target), Child_Perm);
4018 case Kind (Source) is
4019 when Entire_Object =>
4020 Apply_Glb_Tree (Get_All (Target),
4021 Children_Permission (Source));
4024 Merge_Trees (Get_All (Target), Get_All (Source));
4027 raise Program_Error;
4031 when Array_Component =>
4032 case Kind (Source) is
4033 when Entire_Object =>
4034 Apply_Glb_Tree (Get_Elem (Target),
4035 Children_Permission (Source));
4037 when Array_Component =>
4038 Merge_Trees (Get_Elem (Target), Get_Elem (Source));
4041 raise Program_Error;
4045 when Record_Component =>
4046 case Kind (Source) is
4047 when Entire_Object =>
4049 Child_Perm : constant Perm_Kind :=
4050 Children_Permission (Source);
4052 Comp : Perm_Tree_Access;
4055 Comp := Perm_Tree_Maps.Get_First
4056 (Component (Target));
4057 while Comp /= null loop
4058 -- Apply glb tree on every component subtree
4060 Apply_Glb_Tree (Comp, Child_Perm);
4062 Perm_Tree_Maps.Get_Next (Component (Target));
4064 Apply_Glb_Tree (Other_Components (Target), Child_Perm);
4067 when Record_Component =>
4069 Key_Source : Perm_Tree_Maps.Key_Option;
4070 CompTarget : Perm_Tree_Access;
4071 CompSource : Perm_Tree_Access;
4074 Key_Source := Perm_Tree_Maps.Get_First_Key
4075 (Component (Source));
4077 while Key_Source.Present loop
4078 CompSource := Perm_Tree_Maps.Get
4079 (Component (Source), Key_Source.K);
4080 CompTarget := Perm_Tree_Maps.Get
4081 (Component (Target), Key_Source.K);
4083 pragma Assert (CompSource /= null);
4084 Merge_Trees (CompTarget, CompSource);
4086 Key_Source := Perm_Tree_Maps.Get_Next_Key
4087 (Component (Source));
4090 Merge_Trees (Other_Components (Target),
4091 Other_Components (Source));
4095 raise Program_Error;
4101 CompTarget : Perm_Tree_Access;
4102 CompSource : Perm_Tree_Access;
4103 KeyTarget : Perm_Tree_Maps.Key_Option;
4106 KeyTarget := Get_First_Key (Target);
4107 -- Iterate over every tree of the environment in the target, and merge
4108 -- it with the source if there is such a similar one that exists. If
4109 -- there is none, then skip.
4110 while KeyTarget.Present loop
4112 CompSource := Get (Source, KeyTarget.K);
4113 CompTarget := Get (Target, KeyTarget.K);
4115 pragma Assert (CompTarget /= null);
4117 if CompSource /= null then
4118 Merge_Trees (CompTarget, CompSource);
4119 Remove (Source, KeyTarget.K);
4122 KeyTarget := Get_Next_Key (Target);
4125 -- Iterate over every tree of the environment of the source. And merge
4126 -- again. If there is not any tree of the target then just copy the tree
4127 -- from source to target.
4129 KeySource : Perm_Tree_Maps.Key_Option;
4131 KeySource := Get_First_Key (Source);
4132 while KeySource.Present loop
4134 CompSource := Get (Source, KeySource.K);
4135 CompTarget := Get (Target, KeySource.K);
4137 if CompTarget = null then
4138 CompTarget := new Perm_Tree_Wrapper'(CompSource
.all);
4139 Copy_Tree
(CompSource
, CompTarget
);
4140 Set
(Target
, KeySource
.K
, CompTarget
);
4142 Merge_Trees
(CompTarget
, CompSource
);
4145 KeySource
:= Get_Next_Key
(Source
);
4156 procedure Perm_Error
4159 Found_Perm
: Perm_Kind
)
4161 procedure Set_Root_Object
4163 Obj
: out Entity_Id
;
4164 Deref
: out Boolean);
4165 -- Set the root object Obj, and whether the path contains a dereference,
4166 -- from a path Path.
4168 ---------------------
4169 -- Set_Root_Object --
4170 ---------------------
4172 procedure Set_Root_Object
4174 Obj
: out Entity_Id
;
4175 Deref
: out Boolean)
4178 case Nkind
(Path
) is
4182 Obj
:= Entity
(Path
);
4185 when N_Type_Conversion
4186 | N_Unchecked_Type_Conversion
4187 | N_Qualified_Expression
4189 Set_Root_Object
(Expression
(Path
), Obj
, Deref
);
4191 when N_Indexed_Component
4192 | N_Selected_Component
4195 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
4197 when N_Explicit_Dereference
=>
4198 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
4202 raise Program_Error
;
4204 end Set_Root_Object
;
4211 -- Start of processing for Perm_Error
4214 Set_Root_Object
(N
, Root
, Is_Deref
);
4218 ("insufficient permission on dereference from &", N
, Root
);
4220 Error_Msg_NE
("insufficient permission for &", N
, Root
);
4223 Perm_Mismatch
(Perm
, Found_Perm
, N
);
4226 -------------------------------
4227 -- Perm_Error_Subprogram_End --
4228 -------------------------------
4230 procedure Perm_Error_Subprogram_End
4234 Found_Perm
: Perm_Kind
)
4237 Error_Msg_Node_2
:= Subp
;
4238 Error_Msg_NE
("insufficient permission for & when returning from &",
4240 Perm_Mismatch
(Perm
, Found_Perm
, Subp
);
4241 end Perm_Error_Subprogram_End
;
4247 procedure Process_Path
(N
: Node_Id
) is
4248 Root
: constant Entity_Id
:= Get_Enclosing_Object
(N
);
4251 -- We ignore if yielding to synchronized
4254 and then Is_Synchronized_Object
(Root
)
4259 -- We ignore shallow unaliased. They are checked in flow analysis,
4260 -- allowing backward compatibility.
4262 if Current_Checking_Mode
/= Super_Move
4263 and then not Has_Alias
(N
)
4264 and then Is_Shallow
(Etype
(N
))
4270 Perm_N
: constant Perm_Kind
:= Get_Perm
(N
);
4274 case Current_Checking_Mode
is
4275 -- Check permission R, do nothing
4278 if Perm_N
not in Read_Perm
then
4279 Perm_Error
(N
, Read_Only
, Perm_N
);
4283 -- If shallow type no need for RW, only R
4286 if Is_Shallow
(Etype
(N
)) then
4287 if Perm_N
not in Read_Perm
then
4288 Perm_Error
(N
, Read_Only
, Perm_N
);
4292 -- Check permission RW if deep
4294 if Perm_N
/= Read_Write
then
4295 Perm_Error
(N
, Read_Write
, Perm_N
);
4300 -- Set permission to W to the path and any of its prefix
4302 Tree
: constant Perm_Tree_Access
:=
4303 Set_Perm_Prefixes_Move
(N
, Move
);
4307 -- We went through a function call, no permission to
4313 -- Set permissions to
4314 -- No for any extension with more .all
4315 -- W for any deep extension with same number of .all
4316 -- RW for any shallow extension with same number of .all
4318 Set_Perm_Extensions_Move
(Tree
, Etype
(N
));
4322 -- Check permission RW
4325 if Perm_N
/= Read_Write
then
4326 Perm_Error
(N
, Read_Write
, Perm_N
);
4331 -- Set permission to No to the path and any of its prefix up
4332 -- to the first .all and then W.
4334 Tree
: constant Perm_Tree_Access
:=
4335 Set_Perm_Prefixes_Move
(N
, Super_Move
);
4339 -- We went through a function call, no permission to
4345 -- Set permissions to No on any strict extension of the path
4347 Set_Perm_Extensions
(Tree
, No_Access
);
4350 -- Check permission W
4353 if Perm_N
not in Write_Perm
then
4354 Perm_Error
(N
, Write_Only
, Perm_N
);
4358 -- If the tree has an array component, then the permissions do
4359 -- not get modified by the assignment.
4361 if Has_Array_Component
(N
) then
4365 -- Same if has function component
4367 if Has_Function_Component
(N
) then -- Dead code?
4372 -- Get the permission tree for the path
4374 Tree
: constant Perm_Tree_Access
:=
4377 Dummy
: Perm_Tree_Access
;
4381 -- We went through a function call, no permission to
4387 -- Set permission RW for it and all of its extensions
4389 Tree
.all.Tree
.Permission
:= Read_Write
;
4391 Set_Perm_Extensions
(Tree
, Read_Write
);
4393 -- Normalize the permission tree
4395 Dummy
:= Set_Perm_Prefixes_Assign
(N
);
4398 -- Check permission W
4401 if Perm_N
not in Write_Perm
then
4402 Perm_Error
(N
, Write_Only
, Perm_N
);
4406 -- Set permission to No to the path and any of its prefixes
4408 Tree
: constant Perm_Tree_Access
:=
4409 Set_Perm_Prefixes_Borrow_Out
(N
);
4413 -- We went through a function call, no permission to
4419 -- Set permissions to No on any strict extension of the path
4421 Set_Perm_Extensions
(Tree
, No_Access
);
4425 if Perm_N
not in Read_Perm
then
4426 Perm_Error
(N
, Read_Only
, Perm_N
);
4429 if Is_By_Copy_Type
(Etype
(N
)) then
4434 -- Set permission to No on the path and any of its prefixes
4436 Tree
: constant Perm_Tree_Access
:=
4437 Set_Perm_Prefixes_Observe
(N
);
4441 -- We went through a function call, no permission to
4447 -- Set permissions to No on any strict extension of the path
4449 Set_Perm_Extensions
(Tree
, Read_Only
);
4455 -------------------------
4456 -- Return_Declarations --
4457 -------------------------
4459 procedure Return_Declarations
(L
: List_Id
) is
4461 procedure Return_Declaration
(Decl
: Node_Id
);
4462 -- Check correct permissions for every declared object
4464 ------------------------
4465 -- Return_Declaration --
4466 ------------------------
4468 procedure Return_Declaration
(Decl
: Node_Id
) is
4470 if Nkind
(Decl
) = N_Object_Declaration
then
4471 -- Check RW for object declared, unless the object has never been
4474 if Get
(Current_Initialization_Map
,
4475 Unique_Entity
(Defining_Identifier
(Decl
))) = False
4480 -- We ignore shallow unaliased. They are checked in flow analysis,
4481 -- allowing backward compatibility.
4483 if not Has_Alias
(Defining_Identifier
(Decl
))
4484 and then Is_Shallow
(Etype
(Defining_Identifier
(Decl
)))
4490 Elem
: constant Perm_Tree_Access
:=
4491 Get
(Current_Perm_Env
,
4492 Unique_Entity
(Defining_Identifier
(Decl
)));
4496 -- Here we are on a declaration. Hence it should have been
4497 -- added in the environment when analyzing this node with
4498 -- mode Read. Hence it is not possible to find a null
4502 raise Program_Error
;
4505 if Permission
(Elem
) /= Read_Write
then
4506 Perm_Error
(Decl
, Read_Write
, Permission
(Elem
));
4510 end Return_Declaration
;
4516 -- Start of processing for Return_Declarations
4520 while Present
(N
) loop
4521 Return_Declaration
(N
);
4524 end Return_Declarations
;
4526 --------------------
4527 -- Return_Globals --
4528 --------------------
4530 procedure Return_Globals
(Subp
: Entity_Id
) is
4532 procedure Return_Globals_From_List
4533 (First_Item
: Node_Id
;
4534 Kind
: Formal_Kind
);
4535 -- Return global items from the list starting at Item
4537 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
);
4538 -- Return global items for the mode Global_Mode
4540 ------------------------------
4541 -- Return_Globals_From_List --
4542 ------------------------------
4544 procedure Return_Globals_From_List
4545 (First_Item
: Node_Id
;
4548 Item
: Node_Id
:= First_Item
;
4552 while Present
(Item
) loop
4555 -- Ignore abstract states, which play no role in pointer aliasing
4557 if Ekind
(E
) = E_Abstract_State
then
4560 Return_Parameter_Or_Global
(E
, Kind
, Subp
, Global_Var
=> True);
4564 end Return_Globals_From_List
;
4566 ----------------------------
4567 -- Return_Globals_Of_Mode --
4568 ----------------------------
4570 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
) is
4575 when Name_Input | Name_Proof_In
=>
4576 Kind
:= E_In_Parameter
;
4578 Kind
:= E_Out_Parameter
;
4580 Kind
:= E_In_Out_Parameter
;
4582 raise Program_Error
;
4585 -- Return both global items from Global and Refined_Global pragmas
4587 Return_Globals_From_List
(First_Global
(Subp
, Global_Mode
), Kind
);
4588 Return_Globals_From_List
4589 (First_Global
(Subp
, Global_Mode
, Refined
=> True), Kind
);
4590 end Return_Globals_Of_Mode
;
4592 -- Start of processing for Return_Globals
4595 Return_Globals_Of_Mode
(Name_Proof_In
);
4596 Return_Globals_Of_Mode
(Name_Input
);
4597 Return_Globals_Of_Mode
(Name_Output
);
4598 Return_Globals_Of_Mode
(Name_In_Out
);
4601 --------------------------------
4602 -- Return_Parameter_Or_Global --
4603 --------------------------------
4605 procedure Return_Parameter_Or_Global
4609 Global_Var
: Boolean)
4611 Elem
: constant Perm_Tree_Access
:= Get
(Current_Perm_Env
, Id
);
4612 pragma Assert
(Elem
/= null);
4615 -- Shallow unaliased parameters and globals cannot introduce pointer
4618 if not Has_Alias
(Id
) and then Is_Shallow
(Etype
(Id
)) then
4621 -- Observed IN parameters and globals need not return a permission to
4624 elsif Mode
= E_In_Parameter
4625 and then (not Is_Borrowed_In
(Id
) or else Global_Var
)
4629 -- All other parameters and globals should return with mode RW to the
4633 if Permission
(Elem
) /= Read_Write
then
4634 Perm_Error_Subprogram_End
4638 Found_Perm
=> Permission
(Elem
));
4641 end Return_Parameter_Or_Global
;
4643 -----------------------
4644 -- Return_Parameters --
4645 -----------------------
4647 procedure Return_Parameters
(Subp
: Entity_Id
) is
4651 Formal
:= First_Formal
(Subp
);
4652 while Present
(Formal
) loop
4653 Return_Parameter_Or_Global
(Formal
, Ekind
(Formal
), Subp
, False);
4654 Next_Formal
(Formal
);
4656 end Return_Parameters
;
4658 -------------------------
4659 -- Set_Perm_Extensions --
4660 -------------------------
4662 procedure Set_Perm_Extensions
4663 (T
: Perm_Tree_Access
;
4666 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
);
4668 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
)
4672 when Entire_Object
=>
4676 Free_Perm_Tree
(T
.all.Tree
.Get_All
);
4678 when Array_Component
=>
4679 Free_Perm_Tree
(T
.all.Tree
.Get_Elem
);
4681 -- Free every Component subtree
4683 when Record_Component
=>
4685 Comp
: Perm_Tree_Access
;
4688 Comp
:= Perm_Tree_Maps
.Get_First
(Component
(T
));
4689 while Comp
/= null loop
4690 Free_Perm_Tree
(Comp
);
4691 Comp
:= Perm_Tree_Maps
.Get_Next
(Component
(T
));
4694 Free_Perm_Tree
(T
.all.Tree
.Other_Components
);
4697 end Free_Perm_Tree_Children
;
4699 Son
: constant Perm_Tree
:=
4701 (Kind => Entire_Object,
4702 Is_Node_Deep => Is_Node_Deep (T),
4703 Permission => Permission (T),
4704 Children_Permission => P);
4707 Free_Perm_Tree_Children (T);
4709 end Set_Perm_Extensions;
4711 ------------------------------
4712 -- Set_Perm_Extensions_Move --
4713 ------------------------------
4715 procedure Set_Perm_Extensions_Move
4716 (T : Perm_Tree_Access;
4720 if not Is_Node_Deep (T) then
4721 -- We are a shallow extension with same number of .all
4723 Set_Perm_Extensions (T, Read_Write);
4727 -- We are a deep extension here (or the moved deep path)
4729 T.all.Tree.Permission := Write_Only;
4731 case T.all.Tree.Kind is
4732 -- Unroll the tree depending on the type
4734 when Entire_Object =>
4737 | E_String_Literal_Subtype
4739 Set_Perm_Extensions (T, No_Access);
4741 -- No need to unroll here, directly put sons to No_Access
4744 if Ekind (E) in Access_Subprogram_Kind then
4747 Set_Perm_Extensions (T, No_Access);
4750 -- No unrolling done, too complicated
4752 when E_Class_Wide_Subtype
4755 | E_Incomplete_Subtype
4760 Set_Perm_Extensions (T, No_Access);
4762 -- Expand the tree. Replace the node with Array component.
4765 | E_Array_Subtype =>
4767 Son : Perm_Tree_Access;
4770 Son := new Perm_Tree_Wrapper'
4772 (Kind
=> Entire_Object
,
4773 Is_Node_Deep
=> Is_Node_Deep
(T
),
4774 Permission
=> Read_Write
,
4775 Children_Permission
=> Read_Write
));
4777 Set_Perm_Extensions_Move
(Son
, Component_Type
(E
));
4779 -- We change the current node from Entire_Object to
4780 -- Reference with Write_Only and the previous son.
4782 pragma Assert
(Is_Node_Deep
(T
));
4784 T
.all.Tree
:= (Kind
=> Array_Component
,
4785 Is_Node_Deep
=> Is_Node_Deep
(T
),
4786 Permission
=> Write_Only
,
4790 -- Unroll, and set permission extensions with component type
4794 | E_Record_Type_With_Private
4795 | E_Record_Subtype_With_Private
4797 | E_Protected_Subtype
4800 -- Expand the tree. Replace the node with
4801 -- Record_Component.
4805 Son
: Perm_Tree_Access
;
4808 -- We change the current node from Entire_Object to
4809 -- Record_Component with same permission and an empty
4810 -- hash table as component list.
4812 pragma Assert
(Is_Node_Deep
(T
));
4815 (Kind
=> Record_Component
,
4816 Is_Node_Deep
=> Is_Node_Deep
(T
),
4817 Permission
=> Write_Only
,
4818 Component
=> Perm_Tree_Maps
.Nil
,
4820 new Perm_Tree_Wrapper
'
4822 (Kind => Entire_Object,
4823 Is_Node_Deep => True,
4824 Permission => Read_Write,
4825 Children_Permission => Read_Write)
4829 -- We fill the hash table with all sons of the record,
4830 -- with basic Entire_Objects nodes.
4831 Elem := First_Component_Or_Discriminant (E);
4832 while Present (Elem) loop
4833 Son := new Perm_Tree_Wrapper'
4835 (Kind
=> Entire_Object
,
4836 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
4837 Permission
=> Read_Write
,
4838 Children_Permission
=> Read_Write
));
4840 Set_Perm_Extensions_Move
(Son
, Etype
(Elem
));
4843 (T
.all.Tree
.Component
, Elem
, Son
);
4845 Next_Component_Or_Discriminant
(Elem
);
4851 | E_Limited_Private_Type
4852 | E_Limited_Private_Subtype
4854 Set_Perm_Extensions_Move
(T
, Underlying_Type
(E
));
4857 raise Program_Error
;
4861 -- Now the son does not have the same number of .all
4862 Set_Perm_Extensions
(T
, No_Access
);
4864 when Array_Component
=>
4865 Set_Perm_Extensions_Move
(Get_Elem
(T
), Component_Type
(E
));
4867 when Record_Component
=>
4869 Comp
: Perm_Tree_Access
;
4873 It
:= First_Component_Or_Discriminant
(E
);
4874 while It
/= Empty
loop
4875 Comp
:= Perm_Tree_Maps
.Get
(Component
(T
), It
);
4876 pragma Assert
(Comp
/= null);
4877 Set_Perm_Extensions_Move
(Comp
, It
);
4878 It
:= Next_Component_Or_Discriminant
(E
);
4881 Set_Perm_Extensions
(Other_Components
(T
), No_Access
);
4884 end Set_Perm_Extensions_Move
;
4886 ------------------------------
4887 -- Set_Perm_Prefixes_Assign --
4888 ------------------------------
4890 function Set_Perm_Prefixes_Assign
(N
: Node_Id
) return Perm_Tree_Access
is
4891 C
: constant Perm_Tree_Access
:= Get_Perm_Tree
(N
);
4894 pragma Assert
(Current_Checking_Mode
= Assign
);
4896 -- The function should not be called if has_function_component
4898 pragma Assert
(C
/= null);
4901 when Entire_Object
=>
4902 pragma Assert
(Children_Permission
(C
) = Read_Write
);
4904 -- Maroua: Children could have read_only perm. Why Read_Write?
4906 C
.all.Tree
.Permission
:= Read_Write
;
4909 pragma Assert
(Get_All
(C
) /= null);
4911 C
.all.Tree
.Permission
:=
4912 Lub
(Permission
(C
), Permission
(Get_All
(C
)));
4914 when Array_Component
=>
4915 pragma Assert
(C
.all.Tree
.Get_Elem
/= null);
4917 -- Given that it is not possible to know which element has been
4918 -- assigned, then the permissions do not get changed in case of
4923 when Record_Component
=>
4925 Comp
: Perm_Tree_Access
;
4926 Perm
: Perm_Kind
:= Read_Write
;
4929 -- We take the Glb of all the descendants, and then update the
4930 -- permission of the node with it.
4932 Comp
:= Perm_Tree_Maps
.Get_First
(Component
(C
));
4933 while Comp
/= null loop
4934 Perm
:= Glb
(Perm
, Permission
(Comp
));
4935 Comp
:= Perm_Tree_Maps
.Get_Next
(Component
(C
));
4938 Perm
:= Glb
(Perm
, Permission
(Other_Components
(C
)));
4940 C
.all.Tree
.Permission
:= Lub
(Permission
(C
), Perm
);
4946 -- Base identifier. End recursion here.
4950 | N_Defining_Identifier
4954 when N_Type_Conversion
4955 | N_Unchecked_Type_Conversion
4956 | N_Qualified_Expression
4958 return Set_Perm_Prefixes_Assign
(Expression
(N
));
4960 when N_Parameter_Specification
=>
4961 raise Program_Error
;
4963 -- Continue recursion on prefix
4965 when N_Selected_Component
=>
4966 return Set_Perm_Prefixes_Assign
(Prefix
(N
));
4968 -- Continue recursion on prefix
4970 when N_Indexed_Component
4973 return Set_Perm_Prefixes_Assign
(Prefix
(N
));
4975 -- Continue recursion on prefix
4977 when N_Explicit_Dereference
=>
4978 return Set_Perm_Prefixes_Assign
(Prefix
(N
));
4980 when N_Function_Call
=>
4981 raise Program_Error
;
4984 raise Program_Error
;
4987 end Set_Perm_Prefixes_Assign
;
4989 ----------------------------------
4990 -- Set_Perm_Prefixes_Borrow_Out --
4991 ----------------------------------
4993 function Set_Perm_Prefixes_Borrow_Out
4995 return Perm_Tree_Access
4998 pragma Assert
(Current_Checking_Mode
= Borrow_Out
);
5001 -- Base identifier. Set permission to No.
5007 P
: constant Node_Id
:= Entity
(N
);
5009 C
: constant Perm_Tree_Access
:=
5010 Get
(Current_Perm_Env
, Unique_Entity
(P
));
5012 pragma Assert
(C
/= null);
5015 -- Setting the initialization map to True, so that this
5016 -- variable cannot be ignored anymore when looking at end
5017 -- of elaboration of package.
5019 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
5021 C
.all.Tree
.Permission
:= No_Access
;
5025 when N_Type_Conversion
5026 | N_Unchecked_Type_Conversion
5027 | N_Qualified_Expression
5029 return Set_Perm_Prefixes_Borrow_Out
(Expression
(N
));
5031 when N_Parameter_Specification
5032 | N_Defining_Identifier
5034 raise Program_Error
;
5036 -- We set the permission tree of its prefix, and then we extract
5037 -- our subtree from the returned pointer and assign an adequate
5038 -- permission to it, if unfolded. If folded, we unroll the tree
5041 when N_Selected_Component
=>
5043 C
: constant Perm_Tree_Access
:=
5044 Set_Perm_Prefixes_Borrow_Out
(Prefix
(N
));
5048 -- We went through a function call, do nothing
5053 -- The permission of the returned node should be No
5055 pragma Assert
(Permission
(C
) = No_Access
);
5057 pragma Assert
(Kind
(C
) = Entire_Object
5058 or else Kind
(C
) = Record_Component
);
5060 if Kind
(C
) = Record_Component
then
5061 -- The tree is unfolded. We just modify the permission and
5062 -- return the record subtree.
5065 Selected_Component
: constant Entity_Id
:=
5066 Entity
(Selector_Name
(N
));
5068 Selected_C
: Perm_Tree_Access
:=
5070 (Component
(C
), Selected_Component
);
5073 if Selected_C
= null then
5074 Selected_C
:= Other_Components
(C
);
5077 pragma Assert
(Selected_C
/= null);
5079 Selected_C
.all.Tree
.Permission
:= No_Access
;
5083 elsif Kind
(C
) = Entire_Object
then
5085 -- Expand the tree. Replace the node with
5086 -- Record_Component.
5090 -- Create an empty hash table
5092 Hashtbl
: Perm_Tree_Maps
.Instance
;
5094 -- We create the unrolled nodes, that will all have same
5095 -- permission than parent.
5097 Son
: Perm_Tree_Access
;
5099 ChildrenPerm
: constant Perm_Kind
:=
5100 Children_Permission
(C
);
5103 -- We change the current node from Entire_Object to
5104 -- Record_Component with same permission and an empty
5105 -- hash table as component list.
5108 (Kind
=> Record_Component
,
5109 Is_Node_Deep
=> Is_Node_Deep
(C
),
5110 Permission
=> Permission
(C
),
5111 Component
=> Hashtbl
,
5113 new Perm_Tree_Wrapper
'
5115 (Kind => Entire_Object,
5116 Is_Node_Deep => True,
5117 Permission => ChildrenPerm,
5118 Children_Permission => ChildrenPerm)
5121 -- We fill the hash table with all sons of the record,
5122 -- with basic Entire_Objects nodes.
5123 Elem := First_Component_Or_Discriminant
5124 (Etype (Prefix (N)));
5126 while Present (Elem) loop
5127 Son := new Perm_Tree_Wrapper'
5129 (Kind
=> Entire_Object
,
5130 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
5131 Permission
=> ChildrenPerm
,
5132 Children_Permission
=> ChildrenPerm
));
5135 (C
.all.Tree
.Component
, Elem
, Son
);
5137 Next_Component_Or_Discriminant
(Elem
);
5140 -- Now we set the right field to No_Access, and then we
5141 -- return the tree to the sons, so that the recursion can
5145 Selected_Component
: constant Entity_Id
:=
5146 Entity
(Selector_Name
(N
));
5148 Selected_C
: Perm_Tree_Access
:=
5150 (Component
(C
), Selected_Component
);
5153 if Selected_C
= null then
5154 Selected_C
:= Other_Components
(C
);
5157 pragma Assert
(Selected_C
/= null);
5159 Selected_C
.all.Tree
.Permission
:= No_Access
;
5165 raise Program_Error
;
5169 -- We set the permission tree of its prefix, and then we extract
5170 -- from the returned pointer the subtree and assign an adequate
5171 -- permission to it, if unfolded. If folded, we unroll the tree in
5174 when N_Indexed_Component
5178 C
: constant Perm_Tree_Access
:=
5179 Set_Perm_Prefixes_Borrow_Out
(Prefix
(N
));
5183 -- We went through a function call, do nothing
5188 -- The permission of the returned node should be either W
5189 -- (because the recursive call sets <= Write_Only) or No
5190 -- (if another path has been moved with 'Access).
5192 pragma Assert
(Permission
(C
) = No_Access
);
5194 pragma Assert
(Kind
(C
) = Entire_Object
5195 or else Kind
(C
) = Array_Component
);
5197 if Kind
(C
) = Array_Component
then
5198 -- The tree is unfolded. We just modify the permission and
5199 -- return the elem subtree.
5201 pragma Assert
(Get_Elem
(C
) /= null);
5203 C
.all.Tree
.Get_Elem
.all.Tree
.Permission
:= No_Access
;
5205 return Get_Elem
(C
);
5206 elsif Kind
(C
) = Entire_Object
then
5208 -- Expand the tree. Replace node with Array_Component.
5210 Son
: Perm_Tree_Access
;
5213 Son
:= new Perm_Tree_Wrapper
'
5215 (Kind => Entire_Object,
5216 Is_Node_Deep => Is_Node_Deep (C),
5217 Permission => No_Access,
5218 Children_Permission => Children_Permission (C)));
5220 -- We change the current node from Entire_Object
5221 -- to Array_Component with same permission and the
5222 -- previously defined son.
5224 C.all.Tree := (Kind => Array_Component,
5225 Is_Node_Deep => Is_Node_Deep (C),
5226 Permission => No_Access,
5229 return Get_Elem (C);
5232 raise Program_Error;
5236 -- We set the permission tree of its prefix, and then we extract
5237 -- from the returned pointer the subtree and assign an adequate
5238 -- permission to it, if unfolded. If folded, we unroll the tree
5241 when N_Explicit_Dereference =>
5243 C : constant Perm_Tree_Access :=
5244 Set_Perm_Prefixes_Borrow_Out (Prefix (N));
5248 -- We went through a function call. Do nothing.
5253 -- The permission of the returned node should be No
5255 pragma Assert (Permission (C) = No_Access);
5256 pragma Assert (Kind (C) = Entire_Object
5257 or else Kind (C) = Reference);
5259 if Kind (C) = Reference then
5260 -- The tree is unfolded. We just modify the permission and
5261 -- return the elem subtree.
5263 pragma Assert (Get_All (C) /= null);
5265 C.all.Tree.Get_All.all.Tree.Permission := No_Access;
5268 elsif Kind (C) = Entire_Object then
5270 -- Expand the tree. Replace the node with Reference.
5272 Son : Perm_Tree_Access;
5275 Son := new Perm_Tree_Wrapper'
5277 (Kind
=> Entire_Object
,
5278 Is_Node_Deep
=> Is_Deep
(Etype
(N
)),
5279 Permission
=> No_Access
,
5280 Children_Permission
=> Children_Permission
(C
)));
5282 -- We change the current node from Entire_Object to
5283 -- Reference with No_Access and the previous son.
5285 pragma Assert
(Is_Node_Deep
(C
));
5287 C
.all.Tree
:= (Kind
=> Reference
,
5288 Is_Node_Deep
=> Is_Node_Deep
(C
),
5289 Permission
=> No_Access
,
5295 raise Program_Error
;
5299 when N_Function_Call
=>
5303 raise Program_Error
;
5305 end Set_Perm_Prefixes_Borrow_Out
;
5307 ----------------------------
5308 -- Set_Perm_Prefixes_Move --
5309 ----------------------------
5311 function Set_Perm_Prefixes_Move
5312 (N
: Node_Id
; Mode
: Checking_Mode
)
5313 return Perm_Tree_Access
5318 -- Base identifier. Set permission to W or No depending on Mode.
5324 P
: constant Node_Id
:= Entity
(N
);
5325 C
: constant Perm_Tree_Access
:=
5326 Get
(Current_Perm_Env
, Unique_Entity
(P
));
5329 -- The base tree can be RW (first move from this base path) or
5330 -- W (already some extensions values moved), or even No_Access
5331 -- (extensions moved with 'Access). But it cannot be Read_Only
5332 -- (we get an error).
5334 if Permission
(C
) = Read_Only
then
5335 raise Unrecoverable_Error
;
5338 -- Setting the initialization map to True, so that this
5339 -- variable cannot be ignored anymore when looking at end
5340 -- of elaboration of package.
5342 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
5345 -- No null possible here, there are no parents for the path.
5346 -- This means we are using a global variable without adding
5347 -- it in environment with a global aspect.
5349 Illegal_Global_Usage
(N
);
5352 if Mode
= Super_Move
then
5353 C
.all.Tree
.Permission
:= No_Access
;
5355 C
.all.Tree
.Permission
:= Glb
(Write_Only
, Permission
(C
));
5361 when N_Type_Conversion
5362 | N_Unchecked_Type_Conversion
5363 | N_Qualified_Expression
5365 return Set_Perm_Prefixes_Move
(Expression
(N
), Mode
);
5367 when N_Parameter_Specification
5368 | N_Defining_Identifier
5370 raise Program_Error
;
5372 -- We set the permission tree of its prefix, and then we extract
5373 -- from the returned pointer our subtree and assign an adequate
5374 -- permission to it, if unfolded. If folded, we unroll the tree
5377 when N_Selected_Component
=>
5379 C
: constant Perm_Tree_Access
:=
5380 Set_Perm_Prefixes_Move
(Prefix
(N
), Mode
);
5384 -- We went through a function call, do nothing
5389 -- The permission of the returned node should be either W
5390 -- (because the recursive call sets <= Write_Only) or No
5391 -- (if another path has been moved with 'Access).
5393 pragma Assert
(Permission
(C
) = No_Access
5394 or else Permission
(C
) = Write_Only
);
5396 if Mode
= Super_Move
then
5397 -- The permission of the returned node should be No (thanks
5398 -- to the recursion).
5400 pragma Assert
(Permission
(C
) = No_Access
);
5404 pragma Assert
(Kind
(C
) = Entire_Object
5405 or else Kind
(C
) = Record_Component
);
5407 if Kind
(C
) = Record_Component
then
5408 -- The tree is unfolded. We just modify the permission and
5409 -- return the record subtree.
5412 Selected_Component
: constant Entity_Id
:=
5413 Entity
(Selector_Name
(N
));
5415 Selected_C
: Perm_Tree_Access
:=
5417 (Component
(C
), Selected_Component
);
5420 if Selected_C
= null then
5421 -- If the hash table returns no element, then we fall
5422 -- into the part of Other_Components.
5423 pragma Assert
(Is_Tagged_Type
(Etype
(Prefix
(N
))));
5425 Selected_C
:= Other_Components
(C
);
5428 pragma Assert
(Selected_C
/= null);
5430 -- The Selected_C can have permissions:
5431 -- RW : first move in this path
5432 -- W : Already other moves in this path
5433 -- No : Already other moves with 'Access
5435 pragma Assert
(Permission
(Selected_C
) /= Read_Only
);
5436 if Mode
= Super_Move
then
5437 Selected_C
.all.Tree
.Permission
:= No_Access
;
5439 Selected_C
.all.Tree
.Permission
:=
5440 Glb
(Write_Only
, Permission
(Selected_C
));
5446 elsif Kind
(C
) = Entire_Object
then
5448 -- Expand the tree. Replace the node with
5449 -- Record_Component.
5453 -- Create an empty hash table
5455 Hashtbl
: Perm_Tree_Maps
.Instance
;
5457 -- We are in Move or Super_Move mode, hence we can assume
5458 -- that the Children_permission is RW, given that there
5459 -- are no other paths that could have been moved.
5461 pragma Assert
(Children_Permission
(C
) = Read_Write
);
5463 -- We create the unrolled nodes, that will all have RW
5464 -- permission given that we are in move mode. We will
5465 -- then set the right node to W.
5467 Son
: Perm_Tree_Access
;
5470 -- We change the current node from Entire_Object to
5471 -- Record_Component with same permission and an empty
5472 -- hash table as component list.
5475 (Kind
=> Record_Component
,
5476 Is_Node_Deep
=> Is_Node_Deep
(C
),
5477 Permission
=> Permission
(C
),
5478 Component
=> Hashtbl
,
5480 new Perm_Tree_Wrapper
'
5482 (Kind => Entire_Object,
5483 Is_Node_Deep => True,
5484 Permission => Read_Write,
5485 Children_Permission => Read_Write)
5488 -- We fill the hash table with all sons of the record,
5489 -- with basic Entire_Objects nodes.
5490 Elem := First_Component_Or_Discriminant
5491 (Etype (Prefix (N)));
5493 while Present (Elem) loop
5494 Son := new Perm_Tree_Wrapper'
5496 (Kind
=> Entire_Object
,
5497 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
5498 Permission
=> Read_Write
,
5499 Children_Permission
=> Read_Write
));
5502 (C
.all.Tree
.Component
, Elem
, Son
);
5504 Next_Component_Or_Discriminant
(Elem
);
5507 -- Now we set the right field to Write_Only or No_Access
5508 -- depending on mode, and then we return the tree to the
5509 -- sons, so that the recursion can continue.
5512 Selected_Component
: constant Entity_Id
:=
5513 Entity
(Selector_Name
(N
));
5515 Selected_C
: Perm_Tree_Access
:=
5517 (Component
(C
), Selected_Component
);
5520 if Selected_C
= null then
5521 Selected_C
:= Other_Components
(C
);
5524 pragma Assert
(Selected_C
/= null);
5526 -- Given that this is a newly created Select_C, we can
5527 -- safely assume that its permission is Read_Write.
5529 pragma Assert
(Permission
(Selected_C
) =
5532 if Mode
= Super_Move
then
5533 Selected_C
.all.Tree
.Permission
:= No_Access
;
5535 Selected_C
.all.Tree
.Permission
:= Write_Only
;
5542 raise Program_Error
;
5546 -- We set the permission tree of its prefix, and then we extract
5547 -- from the returned pointer the subtree and assign an adequate
5548 -- permission to it, if unfolded. If folded, we unroll the tree
5551 when N_Indexed_Component
5555 C
: constant Perm_Tree_Access
:=
5556 Set_Perm_Prefixes_Move
(Prefix
(N
), Mode
);
5560 -- We went through a function call, do nothing
5565 -- The permission of the returned node should be either
5566 -- W (because the recursive call sets <= Write_Only)
5567 -- or No (if another path has been moved with 'Access)
5569 if Mode
= Super_Move
then
5570 pragma Assert
(Permission
(C
) = No_Access
);
5573 pragma Assert
(Permission
(C
) = Write_Only
5574 or else Permission
(C
) = No_Access
);
5578 pragma Assert
(Kind
(C
) = Entire_Object
5579 or else Kind
(C
) = Array_Component
);
5581 if Kind
(C
) = Array_Component
then
5582 -- The tree is unfolded. We just modify the permission and
5583 -- return the elem subtree.
5585 if Get_Elem
(C
) = null then
5587 raise Program_Error
;
5590 -- The Get_Elem can have permissions :
5591 -- RW : first move in this path
5592 -- W : Already other moves in this path
5593 -- No : Already other moves with 'Access
5595 pragma Assert
(Permission
(Get_Elem
(C
)) /= Read_Only
);
5597 if Mode
= Super_Move
then
5598 C
.all.Tree
.Get_Elem
.all.Tree
.Permission
:= No_Access
;
5600 C
.all.Tree
.Get_Elem
.all.Tree
.Permission
:=
5601 Glb
(Write_Only
, Permission
(Get_Elem
(C
)));
5604 return Get_Elem
(C
);
5605 elsif Kind
(C
) = Entire_Object
then
5607 -- Expand the tree. Replace node with Array_Component.
5609 -- We are in move mode, hence we can assume that the
5610 -- Children_permission is RW.
5612 pragma Assert
(Children_Permission
(C
) = Read_Write
);
5614 Son
: Perm_Tree_Access
;
5617 Son
:= new Perm_Tree_Wrapper
'
5619 (Kind => Entire_Object,
5620 Is_Node_Deep => Is_Node_Deep (C),
5621 Permission => Read_Write,
5622 Children_Permission => Read_Write));
5624 if Mode = Super_Move then
5625 Son.all.Tree.Permission := No_Access;
5627 Son.all.Tree.Permission := Write_Only;
5630 -- We change the current node from Entire_Object
5631 -- to Array_Component with same permission and the
5632 -- previously defined son.
5634 C.all.Tree := (Kind => Array_Component,
5635 Is_Node_Deep => Is_Node_Deep (C),
5636 Permission => Permission (C),
5639 return Get_Elem (C);
5642 raise Program_Error;
5646 -- We set the permission tree of its prefix, and then we extract
5647 -- from the returned pointer the subtree and assign an adequate
5648 -- permission to it, if unfolded. If folded, we unroll the tree
5651 when N_Explicit_Dereference =>
5653 C : constant Perm_Tree_Access :=
5654 Set_Perm_Prefixes_Move (Prefix (N), Move);
5658 -- We went through a function call: do nothing
5663 -- The permission of the returned node should be only
5664 -- W (because the recursive call sets <= Write_Only)
5665 -- No is NOT POSSIBLE here
5667 pragma Assert (Permission (C) = Write_Only);
5669 pragma Assert (Kind (C) = Entire_Object
5670 or else Kind (C) = Reference);
5672 if Kind (C) = Reference then
5673 -- The tree is unfolded. We just modify the permission and
5674 -- return the elem subtree.
5676 if Get_All (C) = null then
5678 raise Program_Error;
5681 -- The Get_All can have permissions :
5682 -- RW : first move in this path
5683 -- W : Already other moves in this path
5684 -- No : Already other moves with 'Access
5686 pragma Assert
(Permission
(Get_All
(C
)) /= Read_Only
);
5688 if Mode
= Super_Move
then
5689 C
.all.Tree
.Get_All
.all.Tree
.Permission
:= No_Access
;
5691 Get_All
(C
).all.Tree
.Permission
:=
5692 Glb
(Write_Only
, Permission
(Get_All
(C
)));
5695 elsif Kind
(C
) = Entire_Object
then
5697 -- Expand the tree. Replace the node with Reference.
5699 -- We are in Move or Super_Move mode, hence we can assume
5700 -- that the Children_permission is RW.
5702 pragma Assert
(Children_Permission
(C
) = Read_Write
);
5704 Son
: Perm_Tree_Access
;
5707 Son
:= new Perm_Tree_Wrapper
'
5709 (Kind => Entire_Object,
5710 Is_Node_Deep => Is_Deep (Etype (N)),
5711 Permission => Read_Write,
5712 Children_Permission => Read_Write));
5714 if Mode = Super_Move then
5715 Son.all.Tree.Permission := No_Access;
5717 Son.all.Tree.Permission := Write_Only;
5720 -- We change the current node from Entire_Object to
5721 -- Reference with Write_Only and the previous son.
5723 pragma Assert (Is_Node_Deep (C));
5725 C.all.Tree := (Kind => Reference,
5726 Is_Node_Deep => Is_Node_Deep (C),
5727 Permission => Write_Only,
5728 -- Write_only is equal to C.Permission
5734 raise Program_Error;
5738 when N_Function_Call =>
5742 raise Program_Error;
5745 end Set_Perm_Prefixes_Move;
5747 -------------------------------
5748 -- Set_Perm_Prefixes_Observe --
5749 -------------------------------
5751 function Set_Perm_Prefixes_Observe
5753 return Perm_Tree_Access
5756 pragma Assert (Current_Checking_Mode = Observe);
5759 -- Base identifier. Set permission to R.
5763 | N_Defining_Identifier
5767 C : Perm_Tree_Access;
5770 if Nkind (N) = N_Defining_Identifier then
5776 C := Get (Current_Perm_Env, Unique_Entity (P));
5777 -- Setting the initialization map to True, so that this
5778 -- variable cannot be ignored anymore when looking at end
5779 -- of elaboration of package.
5781 Set (Current_Initialization_Map, Unique_Entity (P), True);
5784 -- No null possible here, there are no parents for the path.
5785 -- This means we are using a global variable without adding
5786 -- it in environment with a global aspect.
5788 Illegal_Global_Usage (N);
5791 C.all.Tree.Permission := Glb (Read_Only, Permission (C));
5796 when N_Type_Conversion
5797 | N_Unchecked_Type_Conversion
5798 | N_Qualified_Expression
5800 return Set_Perm_Prefixes_Observe (Expression (N));
5802 when N_Parameter_Specification =>
5803 raise Program_Error;
5805 -- We set the permission tree of its prefix, and then we extract
5806 -- from the returned pointer our subtree and assign an adequate
5807 -- permission to it, if unfolded. If folded, we unroll the tree
5810 when N_Selected_Component =>
5812 C : constant Perm_Tree_Access :=
5813 Set_Perm_Prefixes_Observe (Prefix (N));
5817 -- We went through a function call, do nothing
5822 pragma Assert (Kind (C) = Entire_Object
5823 or else Kind (C) = Record_Component);
5825 if Kind (C) = Record_Component then
5826 -- The tree is unfolded. We just modify the permission and
5827 -- return the record subtree. We put the permission to the
5828 -- glb of read_only and its current permission, to consider
5829 -- the case of observing x.y while x.z has been moved. Then
5830 -- x should be No_Access.
5833 Selected_Component : constant Entity_Id :=
5834 Entity (Selector_Name (N));
5836 Selected_C : Perm_Tree_Access :=
5838 (Component (C), Selected_Component);
5841 if Selected_C = null then
5842 Selected_C := Other_Components (C);
5845 pragma Assert (Selected_C /= null);
5847 Selected_C.all.Tree.Permission :=
5848 Glb (Read_Only, Permission (Selected_C));
5852 elsif Kind (C) = Entire_Object then
5854 -- Expand the tree. Replace the node with
5855 -- Record_Component.
5859 -- Create an empty hash table
5861 Hashtbl : Perm_Tree_Maps.Instance;
5863 -- We create the unrolled nodes, that will all have RW
5864 -- permission given that we are in move mode. We will
5865 -- then set the right node to W.
5867 Son : Perm_Tree_Access;
5869 Child_Perm : constant Perm_Kind :=
5870 Children_Permission (C);
5873 -- We change the current node from Entire_Object to
5874 -- Record_Component with same permission and an empty
5875 -- hash table as component list.
5878 (Kind => Record_Component,
5879 Is_Node_Deep => Is_Node_Deep (C),
5880 Permission => Permission (C),
5881 Component => Hashtbl,
5883 new Perm_Tree_Wrapper'
5885 (Kind
=> Entire_Object
,
5886 Is_Node_Deep
=> True,
5887 Permission
=> Child_Perm
,
5888 Children_Permission
=> Child_Perm
)
5891 -- We fill the hash table with all sons of the record,
5892 -- with basic Entire_Objects nodes.
5893 Elem
:= First_Component_Or_Discriminant
5894 (Etype
(Prefix
(N
)));
5896 while Present
(Elem
) loop
5897 Son
:= new Perm_Tree_Wrapper
'
5899 (Kind => Entire_Object,
5900 Is_Node_Deep => Is_Deep (Etype (Elem)),
5901 Permission => Child_Perm,
5902 Children_Permission => Child_Perm));
5905 (C.all.Tree.Component, Elem, Son);
5907 Next_Component_Or_Discriminant (Elem);
5910 -- Now we set the right field to Read_Only. and then we
5911 -- return the tree to the sons, so that the recursion can
5915 Selected_Component : constant Entity_Id :=
5916 Entity (Selector_Name (N));
5918 Selected_C : Perm_Tree_Access :=
5920 (Component (C), Selected_Component);
5923 if Selected_C = null then
5924 Selected_C := Other_Components (C);
5927 pragma Assert (Selected_C /= null);
5929 Selected_C.all.Tree.Permission :=
5930 Glb (Read_Only, Child_Perm);
5936 raise Program_Error;
5940 -- We set the permission tree of its prefix, and then we extract from
5941 -- the returned pointer the subtree and assign an adequate permission
5942 -- to it, if unfolded. If folded, we unroll the tree at one step.
5944 when N_Indexed_Component
5948 C : constant Perm_Tree_Access :=
5949 Set_Perm_Prefixes_Observe (Prefix (N));
5953 -- We went through a function call, do nothing
5958 pragma Assert (Kind (C) = Entire_Object
5959 or else Kind (C) = Array_Component);
5961 if Kind (C) = Array_Component then
5962 -- The tree is unfolded. We just modify the permission and
5963 -- return the elem subtree.
5965 pragma Assert (Get_Elem (C) /= null);
5967 C.all.Tree.Get_Elem.all.Tree.Permission :=
5968 Glb (Read_Only, Permission (Get_Elem (C)));
5970 return Get_Elem (C);
5971 elsif Kind (C) = Entire_Object then
5973 -- Expand the tree. Replace node with Array_Component.
5975 Son : Perm_Tree_Access;
5977 Child_Perm : constant Perm_Kind :=
5978 Glb (Read_Only, Children_Permission (C));
5981 Son := new Perm_Tree_Wrapper'
5983 (Kind
=> Entire_Object
,
5984 Is_Node_Deep
=> Is_Node_Deep
(C
),
5985 Permission
=> Child_Perm
,
5986 Children_Permission
=> Child_Perm
));
5988 -- We change the current node from Entire_Object
5989 -- to Array_Component with same permission and the
5990 -- previously defined son.
5992 C
.all.Tree
:= (Kind
=> Array_Component
,
5993 Is_Node_Deep
=> Is_Node_Deep
(C
),
5994 Permission
=> Child_Perm
,
5997 return Get_Elem
(C
);
6001 raise Program_Error
;
6005 -- We set the permission tree of its prefix, and then we extract from
6006 -- the returned pointer the subtree and assign an adequate permission
6007 -- to it, if unfolded. If folded, we unroll the tree at one step.
6009 when N_Explicit_Dereference
=>
6011 C
: constant Perm_Tree_Access
:=
6012 Set_Perm_Prefixes_Observe
(Prefix
(N
));
6016 -- We went through a function call, do nothing
6021 pragma Assert
(Kind
(C
) = Entire_Object
6022 or else Kind
(C
) = Reference
);
6024 if Kind
(C
) = Reference
then
6025 -- The tree is unfolded. We just modify the permission and
6026 -- return the elem subtree.
6028 pragma Assert
(Get_All
(C
) /= null);
6030 C
.all.Tree
.Get_All
.all.Tree
.Permission
:=
6031 Glb
(Read_Only
, Permission
(Get_All
(C
)));
6034 elsif Kind
(C
) = Entire_Object
then
6036 -- Expand the tree. Replace the node with Reference.
6038 Son
: Perm_Tree_Access
;
6040 Child_Perm
: constant Perm_Kind
:=
6041 Glb
(Read_Only
, Children_Permission
(C
));
6044 Son
:= new Perm_Tree_Wrapper
'
6046 (Kind => Entire_Object,
6047 Is_Node_Deep => Is_Deep (Etype (N)),
6048 Permission => Child_Perm,
6049 Children_Permission => Child_Perm));
6051 -- We change the current node from Entire_Object to
6052 -- Reference with Write_Only and the previous son.
6054 pragma Assert (Is_Node_Deep (C));
6056 C.all.Tree := (Kind => Reference,
6057 Is_Node_Deep => Is_Node_Deep (C),
6058 Permission => Child_Perm,
6064 raise Program_Error;
6068 when N_Function_Call =>
6072 raise Program_Error;
6075 end Set_Perm_Prefixes_Observe;
6081 procedure Setup_Globals (Subp : Entity_Id) is
6083 procedure Setup_Globals_From_List
6084 (First_Item : Node_Id;
6085 Kind : Formal_Kind);
6086 -- Set up global items from the list starting at Item
6088 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
6089 -- Set up global items for the mode Global_Mode
6091 -----------------------------
6092 -- Setup_Globals_From_List --
6093 -----------------------------
6095 procedure Setup_Globals_From_List
6096 (First_Item : Node_Id;
6099 Item : Node_Id := First_Item;
6103 while Present (Item) loop
6106 -- Ignore abstract states, which play no role in pointer aliasing
6108 if Ekind (E) = E_Abstract_State then
6111 Setup_Parameter_Or_Global (E, Kind, Global_Var => True);
6115 end Setup_Globals_From_List;
6117 ---------------------------
6118 -- Setup_Globals_Of_Mode --
6119 ---------------------------
6121 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
6126 when Name_Input | Name_Proof_In =>
6127 Kind := E_In_Parameter;
6129 Kind := E_Out_Parameter;
6131 Kind := E_In_Out_Parameter;
6133 raise Program_Error;
6136 -- Set up both global items from Global and Refined_Global pragmas
6138 Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
6139 Setup_Globals_From_List
6140 (First_Global (Subp, Global_Mode, Refined => True), Kind);
6141 end Setup_Globals_Of_Mode;
6143 -- Start of processing for Setup_Globals
6146 Setup_Globals_Of_Mode (Name_Proof_In);
6147 Setup_Globals_Of_Mode (Name_Input);
6148 Setup_Globals_Of_Mode (Name_Output);
6149 Setup_Globals_Of_Mode (Name_In_Out);
6152 -------------------------------
6153 -- Setup_Parameter_Or_Global --
6154 -------------------------------
6156 procedure Setup_Parameter_Or_Global
6159 Global_Var : Boolean)
6161 Elem : Perm_Tree_Access;
6164 Elem := new Perm_Tree_Wrapper'
6166 (Kind
=> Entire_Object
,
6167 Is_Node_Deep
=> Is_Deep
(Etype
(Id
)),
6168 Permission
=> Read_Write
,
6169 Children_Permission
=> Read_Write
));
6172 when E_In_Parameter
=>
6174 -- Borrowed IN: RW for everybody
6176 if Is_Borrowed_In
(Id
) and not Global_Var
then
6177 Elem
.all.Tree
.Permission
:= Read_Write
;
6178 Elem
.all.Tree
.Children_Permission
:= Read_Write
;
6180 -- Observed IN: R for everybody
6183 Elem
.all.Tree
.Permission
:= Read_Only
;
6184 Elem
.all.Tree
.Children_Permission
:= Read_Only
;
6187 -- OUT: borrow, but callee has W only
6189 when E_Out_Parameter
=>
6190 Elem
.all.Tree
.Permission
:= Write_Only
;
6191 Elem
.all.Tree
.Children_Permission
:= Write_Only
;
6193 -- IN OUT: borrow and callee has RW
6195 when E_In_Out_Parameter
=>
6196 Elem
.all.Tree
.Permission
:= Read_Write
;
6197 Elem
.all.Tree
.Children_Permission
:= Read_Write
;
6200 Set
(Current_Perm_Env
, Id
, Elem
);
6201 end Setup_Parameter_Or_Global
;
6203 ----------------------
6204 -- Setup_Parameters --
6205 ----------------------
6207 procedure Setup_Parameters
(Subp
: Entity_Id
) is
6211 Formal
:= First_Formal
(Subp
);
6212 while Present
(Formal
) loop
6213 Setup_Parameter_Or_Global
6214 (Formal
, Ekind
(Formal
), Global_Var
=> False);
6215 Next_Formal
(Formal
);
6217 end Setup_Parameters
;