1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- S E M _ S P A R K --
9 -- Copyright (C) 2017-2019, 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 with 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;
59 -- Permission type associated with paths. These are related to but not
60 -- the same as the states associated with names used in SPARK RM 3.10:
61 -- Unrestricted, Observed, Borrowed, Moved. When ownership rules lead to
62 -- a state change for a name, this may correspond to multiple permission
63 -- changes for the paths corresponding to the name, its prefixes, and
64 -- its extensions. For example, when an object is assigned to, the
65 -- corresponding name gets into state Moved, while the path for the name
66 -- gets permission Write_Only as well as every prefix of the name, and
67 -- every suffix gets permission No_Access.
69 type Perm_Kind_Option is
71 -- Special value used when no permission is passed around
74 -- The path cannot be accessed for reading or writing. This is the
75 -- case for the path of a name in the Borrowed state.
78 -- The path can only be accessed for reading. This is the case for
79 -- the path of a name in the Observed state.
82 -- The path can be accessed for both reading and writing. This is the
83 -- case for the path of a name in the Unrestricted state.
86 -- The path can only be accessed for writing. This is the case for
87 -- the path of a name in the Moved state.
90 subtype Perm_Kind is Perm_Kind_Option range No_Access .. Write_Only;
91 subtype Read_Perm is Perm_Kind range Read_Only .. Read_Write;
92 subtype Write_Perm is Perm_Kind range Read_Write .. Write_Only;
94 type Perm_Tree_Wrapper;
96 type Perm_Tree_Access is access Perm_Tree_Wrapper;
97 -- A tree of permissions is defined, where the root is a whole object
98 -- and tree branches follow access paths in memory. As Perm_Tree is a
99 -- discriminated record, a wrapper type is used for the access type
100 -- designating a subtree, to make it unconstrained so that it can be
103 -- Nodes in the permission tree are of different kinds
106 (Entire_Object, -- Scalar object, or folded object of any type
107 Reference, -- Unfolded object of access type
108 Array_Component, -- Unfolded object of array type
109 Record_Component -- Unfolded object of record type
112 package Perm_Tree_Maps is new Simple_HTable
113 (Header_Num => Elaboration_Context_Index,
115 Element => Perm_Tree_Access,
117 Hash => Elaboration_Context_Hash,
119 -- The instantation of a hash table, with keys being entities and values
120 -- being pointers to permission trees. This is used to define global
121 -- environment permissions (entities in that case are stand-alone
122 -- objects or formal parameters), as well as the permissions for the
123 -- extensions of a Record_Component node (entities in that case are
124 -- record components).
126 -- The definition of permission trees. This is a tree, which has a
127 -- permission at each node, and depending on the type of the node, can
128 -- have zero, one, or more children reached through an access to tree.
130 type Perm_Tree (Kind : Path_Kind := Entire_Object) is record
131 Permission : Perm_Kind;
132 -- Permission at this level in the path
134 Is_Node_Deep : Boolean;
135 -- Whether this node is of a "deep" type, i.e. an access type or a
136 -- composite type containing access type subcomponents. This
137 -- corresponds to both "observing" and "owning" types in SPARK RM
138 -- 3.10. To be used when moving the path.
140 Explanation : Node_Id;
141 -- Node that can be used in an explanation for a permission mismatch
144 -- An entire object is either a leaf (an object which cannot be
145 -- extended further in a path) or a subtree in folded form (which
146 -- could later be unfolded further in another kind of node). The
147 -- field Children_Permission specifies a permission for every
148 -- extension of that node if that permission is different from the
149 -- node's permission.
151 when Entire_Object =>
152 Children_Permission : Perm_Kind;
154 -- Unfolded path of access type. The permission of the object
155 -- pointed to is given in Get_All.
158 Get_All : Perm_Tree_Access;
160 -- Unfolded path of array type. The permission of elements is
161 -- given in Get_Elem.
163 when Array_Component =>
164 Get_Elem : Perm_Tree_Access;
166 -- Unfolded path of record type. The permission of the components
167 -- is given in Component.
169 when Record_Component =>
170 Component : Perm_Tree_Maps.Instance;
174 type Perm_Tree_Wrapper is record
177 -- We use this wrapper in order to have unconstrained discriminants
179 type Perm_Env is new Perm_Tree_Maps.Instance;
180 -- The definition of a permission environment for the analysis. This is
181 -- just a hash table from entities to permission trees.
183 type Perm_Env_Access is access Perm_Env;
184 -- Access to permission environments
186 package Env_Maps is new Simple_HTable
187 (Header_Num => Elaboration_Context_Index,
189 Element => Perm_Env_Access,
191 Hash => Elaboration_Context_Hash,
193 -- The instantiation of a hash table whose elements are permission
194 -- environments. This hash table is used to save the environments at
195 -- the entry of each loop, with the key being the loop label.
197 type Env_Backups is new Env_Maps.Instance;
198 -- The type defining the hash table saving the environments at the entry
201 package Variable_Maps is new Simple_HTable
202 (Header_Num => Elaboration_Context_Index,
206 Hash => Elaboration_Context_Hash,
209 type Variable_Mapping is new Variable_Maps.Instance;
210 -- Mapping from variables to nodes denoting paths that are observed or
211 -- borrowed by the variable.
217 -- Simple getters to avoid having .all.Tree.Field everywhere. Of course,
218 -- that's only for the top access, as otherwise this reverses the order
219 -- in accesses visually.
221 function Children_Permission (T : Perm_Tree_Access) return Perm_Kind;
222 function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance;
223 function Explanation (T : Perm_Tree_Access) return Node_Id;
224 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access;
225 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access;
226 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean;
227 function Kind (T : Perm_Tree_Access) return Path_Kind;
228 function Permission (T : Perm_Tree_Access) return Perm_Kind;
230 -----------------------
231 -- Memory Management --
232 -----------------------
236 To : in out Perm_Env);
237 -- Procedure to copy a permission environment
239 procedure Move_Env (From, To : in out Perm_Env);
240 -- Procedure to move a permission environment. It frees To, moves From
241 -- in To and sets From to Nil.
243 procedure Move_Variable_Mapping (From, To : in out Variable_Mapping);
244 -- Move a variable mapping, freeing memory as needed and resetting the
247 procedure Copy_Tree (From, To : Perm_Tree_Access);
248 -- Procedure to copy a permission tree
250 procedure Free_Env (PE : in out Perm_Env);
251 -- Procedure to free a permission environment
253 procedure Free_Tree (PT : in out Perm_Tree_Access);
254 -- Procedure to free a permission tree
260 procedure Perm_Mismatch
262 Exp_Perm : Perm_Kind;
263 Act_Perm : Perm_Kind;
265 Forbidden_Perm : Boolean := False);
266 -- Issues a continuation error message about a mismatch between a
267 -- desired permission Exp_Perm and a permission obtained Act_Perm. N
268 -- is the node on which the error is reported.
272 package body Permissions is
274 -------------------------
275 -- Children_Permission --
276 -------------------------
278 function Children_Permission (T : Perm_Tree_Access) return Perm_Kind is
280 return T.all.Tree.Children_Permission;
281 end Children_Permission;
287 function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance
290 return T.all.Tree.Component;
297 procedure Copy_Env (From : Perm_Env; To : in out Perm_Env) is
298 Comp_From : Perm_Tree_Access;
299 Key_From : Perm_Tree_Maps.Key_Option;
300 Son : Perm_Tree_Access;
304 Key_From := Get_First_Key (From);
305 while Key_From.Present loop
306 Comp_From := Get (From, Key_From.K);
307 pragma Assert (Comp_From /= null);
309 Son := new Perm_Tree_Wrapper;
310 Copy_Tree (Comp_From, Son);
312 Set (To, Key_From.K, Son);
313 Key_From := Get_Next_Key (From);
321 procedure Copy_Tree (From, To : Perm_Tree_Access) is
323 -- Copy the direct components of the tree
327 -- Now reallocate access components for a deep copy of the tree
330 when Entire_Object =>
334 To.all.Tree.Get_All := new Perm_Tree_Wrapper;
335 Copy_Tree (Get_All (From), Get_All (To));
337 when Array_Component =>
338 To.all.Tree.Get_Elem := new Perm_Tree_Wrapper;
339 Copy_Tree (Get_Elem (From), Get_Elem (To));
341 when Record_Component =>
343 Comp_From : Perm_Tree_Access;
344 Key_From : Perm_Tree_Maps.Key_Option;
345 Son : Perm_Tree_Access;
346 Hash_Table : Perm_Tree_Maps.Instance;
348 -- We put a new hash table, so that it gets dealiased from
349 -- the Component (From) hash table.
350 To.all.Tree.Component := Hash_Table;
351 Key_From := Perm_Tree_Maps.Get_First_Key
354 while Key_From.Present loop
355 Comp_From := Perm_Tree_Maps.Get
356 (Component (From), Key_From.K);
357 pragma Assert (Comp_From /= null);
358 Son := new Perm_Tree_Wrapper;
359 Copy_Tree (Comp_From, Son);
361 (To.all.Tree.Component, Key_From.K, Son);
362 Key_From := Perm_Tree_Maps.Get_Next_Key
369 ------------------------------
370 -- Elaboration_Context_Hash --
371 ------------------------------
373 function Elaboration_Context_Hash
374 (Key : Entity_Id) return Elaboration_Context_Index
377 return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
378 end Elaboration_Context_Hash;
384 procedure Free_Env (PE : in out Perm_Env) is
385 CompO : Perm_Tree_Access;
387 CompO := Get_First (PE);
388 while CompO /= null loop
390 CompO := Get_Next (PE);
400 procedure Free_Tree (PT : in out Perm_Tree_Access) is
401 procedure Free_Perm_Tree_Dealloc is
402 new Ada.Unchecked_Deallocation
403 (Perm_Tree_Wrapper, Perm_Tree_Access);
404 -- The deallocator for permission_trees
408 when Entire_Object =>
412 Free_Tree (PT.all.Tree.Get_All);
414 when Array_Component =>
415 Free_Tree (PT.all.Tree.Get_Elem);
417 when Record_Component =>
419 Comp : Perm_Tree_Access;
422 Comp := Perm_Tree_Maps.Get_First (Component (PT));
423 while Comp /= null loop
425 -- Free every Component subtree
428 Comp := Perm_Tree_Maps.Get_Next (Component (PT));
433 Free_Perm_Tree_Dealloc (PT);
440 function Explanation (T : Perm_Tree_Access) return Node_Id is
442 return T.all.Tree.Explanation;
449 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access is
451 return T.all.Tree.Get_All;
458 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access is
460 return T.all.Tree.Get_Elem;
467 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean is
469 return T.all.Tree.Is_Node_Deep;
476 function Kind (T : Perm_Tree_Access) return Path_Kind is
478 return T.all.Tree.Kind;
485 procedure Move_Env (From, To : in out Perm_Env) is
489 From := Perm_Env (Perm_Tree_Maps.Nil);
492 ---------------------------
493 -- Move_Variable_Mapping --
494 ---------------------------
496 procedure Move_Variable_Mapping (From, To : in out Variable_Mapping) is
500 From := Variable_Mapping (Variable_Maps.Nil);
501 end Move_Variable_Mapping;
507 function Permission (T : Perm_Tree_Access) return Perm_Kind is
509 return T.all.Tree.Permission;
516 procedure Perm_Mismatch
518 Exp_Perm : Perm_Kind;
519 Act_Perm : Perm_Kind;
521 Forbidden_Perm : Boolean := False)
524 Error_Msg_Sloc := Sloc (Expl);
526 if Forbidden_Perm then
527 if Exp_Perm = No_Access then
528 Error_Msg_N ("\object was moved #", N);
535 if Act_Perm = Read_Only then
537 ("\object was declared as not writeable #", N);
539 Error_Msg_N ("\object was moved #", N);
543 Error_Msg_N ("\object was moved #", N);
555 --------------------------------------
556 -- Analysis modes for AST traversal --
557 --------------------------------------
559 -- The different modes for analysis. This allows checking whether a path
560 -- has the right permission, and also updating permissions when a path is
561 -- moved, borrowed, or observed.
563 type Extended_Checking_Mode is
566 -- Special value used for assignment, to check that subexpressions of
567 -- the assigned path are readable.
573 -- Move semantics. Checks that paths have Read_Write permission. After
574 -- moving a path, its permission and the permission of its prefixes are
575 -- set to Write_Only, while the permission of its extensions is set to
579 -- Used for the target of an assignment, or an actual parameter with
580 -- mode OUT. Checks that paths have Write_Perm permission. After
581 -- assigning to a path, its permission and the permission of its
582 -- extensions are set to Read_Write. The permission of its prefixes may
583 -- be normalized from Write_Only to Read_Write depending on other
584 -- permissions in the tree (a prefix gets permission Read_Write when all
585 -- its extensions become Read_Write).
588 -- Borrow semantics. Checks that paths have Read_Write permission. After
589 -- borrowing a path, its permission and the permission of its prefixes
590 -- and extensions are set to No_Access.
593 -- Observe semantics. Checks that paths have Read_Perm permission. After
594 -- observing a path, its permission and the permission of its prefixes
595 -- and extensions are set to Read_Only.
598 subtype Checking_Mode is Extended_Checking_Mode range Read .. Observe;
600 type Result_Kind is (Folded, Unfolded);
601 -- The type declaration to discriminate in the Perm_Or_Tree type
603 -- The result type of the function Get_Perm_Or_Tree. This returns either a
604 -- tree when it found the appropriate tree, or a permission when the search
605 -- finds a leaf and the subtree we are looking for is folded. In the last
606 -- case, we return instead the Children_Permission field of the leaf.
608 type Perm_Or_Tree (R : Result_Kind) is record
611 Found_Permission : Perm_Kind;
612 Explanation : Node_Id;
614 Tree_Access : Perm_Tree_Access;
618 type Error_Status is (OK, Error);
620 -----------------------
621 -- Local subprograms --
622 -----------------------
624 function "<=" (P1, P2 : Perm_Kind) return Boolean;
625 function ">=" (P1, P2 : Perm_Kind) return Boolean;
626 function Glb (P1, P2 : Perm_Kind) return Perm_Kind;
627 function Lub (P1, P2 : Perm_Kind) return Perm_Kind;
629 procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id);
630 -- Handle assignment as part of an assignment statement or an object
633 procedure Check_Call_Statement (Call : Node_Id);
635 procedure Check_Callable_Body (Body_N : Node_Id);
636 -- Entry point for the analysis of a subprogram or entry body
638 procedure Check_Declaration (Decl : Node_Id);
640 procedure Check_Declaration_Legality
643 Legal : in out Boolean);
644 -- Check the legality of declaration Decl regarding rules not related to
645 -- permissions. Update Legal to False if a rule is violated. Issue an
646 -- error message if Force is True and Emit_Messages returns True.
648 procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode);
649 pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint,
651 N_Subtype_Indication,
654 or else Nkind (Expr) in N_Subexpr);
656 procedure Check_Globals (Subp : Entity_Id);
657 -- This procedure takes a subprogram called and checks the permission of
660 -- Checking proceduress for safe pointer usage. These procedures traverse
661 -- the AST, check nodes for correct permissions according to SPARK RM 3.10,
662 -- and update permissions depending on the node kind. The main procedure
663 -- Check_Node is mutually recursive with the specialized procedures that
666 procedure Check_List (L : List_Id);
667 -- Calls Check_Node on each element of the list
669 procedure Check_Loop_Statement (Stmt : Node_Id);
671 procedure Check_Node (N : Node_Id);
672 -- Main traversal procedure to check safe pointer usage
674 procedure Check_Old_Loop_Entry (N : Node_Id);
675 -- Check SPARK RM 3.10(14) regarding 'Old and 'Loop_Entry
677 procedure Check_Package_Body (Pack : Node_Id);
679 procedure Check_Package_Spec (Pack : Node_Id);
681 procedure Check_Parameter_Or_Global
686 Global_Var : Boolean);
687 -- Check the permission of every actual parameter or global
689 procedure Check_Pragma (Prag : Node_Id);
691 procedure Check_Source_Of_Borrow_Or_Observe
693 Status : out Error_Status);
695 procedure Check_Statement (Stmt : Node_Id);
697 procedure Check_Type_Legality
700 Legal : in out Boolean);
701 -- Check that type Typ is either not deep, or that it is an observing or
702 -- owning type according to SPARK RM 3.10
704 function Get_Expl (N : Node_Or_Entity_Id) return Node_Id;
705 -- The function that takes a name as input and returns an explanation node
706 -- for the permission associated with it.
708 function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id;
709 pragma Precondition (Is_Path_Expression (Expr));
710 -- Return the expression being borrowed/observed when borrowing or
711 -- observing Expr. If Expr is a call to a traversal function, this is
712 -- the first actual, otherwise it is Expr.
714 function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind;
715 -- The function that takes a name as input and returns a permission
716 -- associated with it.
718 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
719 pragma Precondition (Is_Path_Expression (N));
720 -- This function gets a node and looks recursively to find the appropriate
721 -- subtree for that node. If the tree is folded on that node, then it
722 -- returns the permission given at the right level.
724 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
725 pragma Precondition (Is_Path_Expression (N));
726 -- This function gets a node and looks recursively to find the appropriate
727 -- subtree for that node. If the tree is folded, then it unrolls the tree
728 -- up to the appropriate level.
730 function Get_Root_Object
732 Through_Traversal : Boolean := True;
733 Is_Traversal : Boolean := False) return Entity_Id;
734 -- Return the root of the path expression Expr, or Empty for an allocator,
735 -- NULL, or a function call. Through_Traversal is True if it should follow
736 -- through calls to traversal functions. Is_Traversal is True if this
737 -- corresponds to a value returned from a traversal function, which should
738 -- allow if-expressions and case-expressions that refer to the same root,
739 -- even if the paths are not the same in all branches.
742 with procedure Handle_Parameter_Or_Global
744 Formal_Typ : Entity_Id;
745 Param_Mode : Formal_Kind;
747 Global_Var : Boolean);
748 procedure Handle_Globals (Subp : Entity_Id);
749 -- Handling of globals is factored in a generic instantiated below
751 function Has_Array_Component (Expr : Node_Id) return Boolean;
752 pragma Precondition (Is_Path_Expression (Expr));
753 -- This function gets a node and looks recursively to determine whether the
754 -- given path has any array component.
756 procedure Hp (P : Perm_Env);
757 -- A procedure that outputs the hash table. This function is used only in
758 -- the debugger to look into a hash table.
759 pragma Unreferenced (Hp);
761 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id);
762 pragma No_Return (Illegal_Global_Usage);
763 -- A procedure that is called when deep globals or aliased globals are used
764 -- without any global aspect.
766 function Is_Path_Expression
768 Is_Traversal : Boolean := False) return Boolean;
769 -- Return whether Expr corresponds to a path. Is_Traversal is True if this
770 -- corresponds to a value returned from a traversal function, which should
771 -- allow if-expressions and case-expressions.
773 function Is_Subpath_Expression
775 Is_Traversal : Boolean := False) return Boolean;
776 -- Return True if Expr can be part of a path expression. Is_Traversal is
777 -- True if this corresponds to a value returned from a traversal function,
778 -- which should allow if-expressions and case-expressions.
780 function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean;
781 -- Determine if the candidate Prefix is indeed a prefix of Expr, or almost
782 -- a prefix, in the sense that they could still refer to overlapping memory
785 function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean;
787 function Loop_Of_Exit (N : Node_Id) return Entity_Id;
788 -- A function that takes an exit statement node and returns the entity of
789 -- the loop that this statement is exiting from.
791 procedure Merge_Env (Source : in out Perm_Env; Target : in out Perm_Env);
792 -- Merge Target and Source into Target, and then deallocate the Source
797 Found_Perm : Perm_Kind;
799 Forbidden_Perm : Boolean := False);
800 -- A procedure that is called when the permissions found contradict the
801 -- rules established by the RM. This function is called with the node and
802 -- the permission that was expected, and issues an error message with the
803 -- appropriate values.
805 procedure Perm_Error_Subprogram_End
809 Found_Perm : Perm_Kind;
811 -- A procedure that is called when the permissions found contradict the
812 -- rules established by the RM at the end of subprograms. This function is
813 -- called with the node, the node of the returning function, and the
814 -- permission that was expected, and adds an error message with the
815 -- appropriate values.
817 procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode);
818 pragma Precondition (Is_Path_Expression (Expr));
819 -- Check correct permission for the path in the checking mode Mode, and
820 -- update permissions of the path and its prefixes/extensions.
822 procedure Return_Globals (Subp : Entity_Id);
823 -- Takes a subprogram as input, and checks that all borrowed global items
824 -- of the subprogram indeed have Read_Write permission at the end of the
825 -- subprogram execution.
827 procedure Return_Parameter_Or_Global
832 Global_Var : Boolean);
833 -- Auxiliary procedure to Return_Parameters and Return_Globals
835 procedure Return_Parameters (Subp : Entity_Id);
836 -- Takes a subprogram as input, and checks that all out parameters of the
837 -- subprogram indeed have Read_Write permission at the end of the
838 -- subprogram execution.
840 procedure Set_Perm_Extensions
841 (T : Perm_Tree_Access;
844 -- This procedure takes an access to a permission tree and modifies the
845 -- tree so that any strict extensions of the given tree become of the
846 -- access specified by parameter P.
848 procedure Set_Perm_Extensions_Move
849 (T : Perm_Tree_Access;
852 -- Set permissions to
853 -- No for any extension with more .all
854 -- W for any deep extension with same number of .all
855 -- RW for any shallow extension with same number of .all
857 function Set_Perm_Prefixes
859 Perm : Perm_Kind_Option;
860 Expl : Node_Id) return Perm_Tree_Access;
861 pragma Precondition (Is_Path_Expression (N));
862 -- This function modifies the permissions of a given node in the permission
863 -- environment as well as all the prefixes of the path, to the new
864 -- permission Perm. The general rule here is that everybody updates the
865 -- permission of the subtree they are returning.
867 procedure Set_Perm_Prefixes_Assign (N : Node_Id);
868 pragma Precondition (Is_Path_Expression (N));
869 -- This procedure takes a name as an input and sets in the permission
870 -- tree the given permission to the given name. The general rule here is
871 -- that everybody updates the permission of the subtree it is returning.
872 -- The permission of the assigned path has been set to RW by the caller.
874 -- Case where we have to normalize a tree after the correct permissions
875 -- have been assigned already. We look for the right subtree at the given
876 -- path, actualize its permissions, and then call the normalization on its
879 -- Example: We assign x.y and x.z, and then Set_Perm_Prefixes_Assign will
880 -- change the permission of x to RW because all of its components have
883 procedure Setup_Globals (Subp : Entity_Id);
884 -- Takes a subprogram as input, and sets up the environment by adding
885 -- global items with appropriate permissions.
887 procedure Setup_Parameter_Or_Global
892 Global_Var : Boolean;
894 -- Auxiliary procedure to Setup_Parameters and Setup_Globals
896 procedure Setup_Parameters (Subp : Entity_Id);
897 -- Takes a subprogram as input, and sets up the environment by adding
898 -- formal parameters with appropriate permissions.
900 procedure Setup_Protected_Components (Subp : Entity_Id);
901 -- Takes a protected operation as input, and sets up the environment by
902 -- adding protected components with appropriate permissions.
904 ----------------------
905 -- Global Variables --
906 ----------------------
908 Current_Perm_Env : Perm_Env;
909 -- The permission environment that is used for the analysis. This
910 -- environment can be saved, modified, reinitialized, but should be the
911 -- only one valid from which to extract the permissions of the paths in
912 -- scope. The analysis ensures at each point that this variables contains
913 -- a valid permission environment with all bindings in scope.
915 Inside_Procedure_Call : Boolean := False;
916 -- Set while checking the actual parameters of a procedure or entry call
918 Inside_Elaboration : Boolean := False;
919 -- Set during package spec/body elaboration, during which move and local
920 -- observe/borrow are not allowed. As a result, no other checking is needed
921 -- during elaboration.
923 Current_Loops_Envs : Env_Backups;
924 -- This variable contains saves of permission environments at each loop the
925 -- analysis entered. Each saved environment can be reached with the label
928 Current_Loops_Accumulators : Env_Backups;
929 -- This variable contains the environments used as accumulators for loops,
930 -- that consist of the merge of all environments at each exit point of
931 -- the loop (which can also be the entry point of the loop in the case of
932 -- non-infinite loops), each of them reachable from the label of the loop.
933 -- We require that the environment stored in the accumulator be less
934 -- restrictive than the saved environment at the beginning of the loop, and
935 -- the permission environment after the loop is equal to the accumulator.
937 Current_Borrowers : Variable_Mapping;
938 -- Mapping from borrowers to the path borrowed
940 Current_Observers : Variable_Mapping;
941 -- Mapping from observers to the path observed
947 -- Generic procedure is defined first so that instantiations can be defined
948 -- anywhere afterwards.
950 procedure Handle_Globals (Subp : Entity_Id) is
954 procedure Handle_Globals_From_List
955 (First_Item : Node_Id;
957 -- Handle global items from the list starting at Item
959 procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id);
960 -- Handle global items for the mode Global_Mode
962 ------------------------------
963 -- Handle_Globals_From_List --
964 ------------------------------
966 procedure Handle_Globals_From_List
967 (First_Item : Node_Id;
970 Item : Node_Id := First_Item;
974 while Present (Item) loop
977 -- Ignore abstract states, which play no role in pointer aliasing
979 if Ekind (E) = E_Abstract_State then
982 Handle_Parameter_Or_Global (Expr => Item,
983 Formal_Typ => Retysp (Etype (Item)),
991 end Handle_Globals_From_List;
993 ----------------------------
994 -- Handle_Globals_Of_Mode --
995 ----------------------------
997 procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id) is
1005 Kind := E_In_Parameter;
1008 Kind := E_Out_Parameter;
1011 Kind := E_In_Out_Parameter;
1014 raise Program_Error;
1017 -- Check both global items from Global and Refined_Global pragmas
1019 Handle_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
1020 Handle_Globals_From_List
1021 (First_Global (Subp, Global_Mode, Refined => True), Kind);
1022 end Handle_Globals_Of_Mode;
1024 -- Start of processing for Handle_Globals
1027 Handle_Globals_Of_Mode (Name_Proof_In);
1028 Handle_Globals_Of_Mode (Name_Input);
1029 Handle_Globals_Of_Mode (Name_Output);
1030 Handle_Globals_Of_Mode (Name_In_Out);
1037 function "<=" (P1, P2 : Perm_Kind) return Boolean is
1046 function ">=" (P1, P2 : Perm_Kind) return Boolean is
1049 when No_Access => return True;
1050 when Read_Only => return P1 in Read_Perm;
1051 when Write_Only => return P1 in Write_Perm;
1052 when Read_Write => return P1 = Read_Write;
1056 ----------------------
1057 -- Check_Assignment --
1058 ----------------------
1060 procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id) is
1062 -- Local subprograms
1064 procedure Handle_Borrow
1068 -- Update map of current borrowers
1070 procedure Handle_Observe
1074 -- Update map of current observers
1080 procedure Handle_Borrow
1085 Borrowed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
1088 -- SPARK RM 3.10(8): If the type of the target is an anonymous
1089 -- access-to-variable type (an owning access type), the source shall
1090 -- be an owning access object [..] whose root object is the target
1093 -- ??? In fact we could be slightly more permissive in allowing even
1094 -- a call to a traversal function of the right form.
1097 and then (Is_Traversal_Function_Call (Expr)
1098 or else Get_Root_Object (Borrowed) /= Var)
1100 if Emit_Messages then
1102 ("source of assignment must have & as root" &
1103 " (SPARK RM 3.10(8)))",
1109 Set (Current_Borrowers, Var, Borrowed);
1112 --------------------
1113 -- Handle_Observe --
1114 --------------------
1116 procedure Handle_Observe
1121 Observed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
1124 -- ??? We are currently using the same restriction for observers
1125 -- as for borrowers. To be seen if the SPARK RM current rule really
1126 -- allows more uses.
1129 and then (Is_Traversal_Function_Call (Expr)
1130 or else Get_Root_Object (Observed) /= Var)
1132 if Emit_Messages then
1134 ("source of assignment must have & as root" &
1135 " (SPARK RM 3.10(8)))",
1141 Set (Current_Observers, Var, Observed);
1146 Target_Typ : constant Node_Id := Etype (Target);
1147 Is_Decl : constant Boolean := Nkind (Target) = N_Defining_Identifier;
1148 Target_Root : Entity_Id;
1149 Expr_Root : Entity_Id;
1151 Status : Error_Status;
1152 Dummy : Boolean := True;
1154 -- Start of processing for Check_Assignment
1157 Check_Type_Legality (Target_Typ, Force => True, Legal => Dummy);
1159 if Is_Anonymous_Access_Type (Target_Typ) then
1160 Check_Source_Of_Borrow_Or_Observe (Expr, Status);
1162 if Status /= OK then
1167 Target_Root := Target;
1169 Target_Root := Get_Root_Object (Target);
1172 Expr_Root := Get_Root_Object (Expr);
1174 -- SPARK RM 3.10(7): For an assignment statement where the target is
1175 -- a stand-alone object of an anonymous access-to-object type.
1177 pragma Assert (Present (Target_Root));
1179 -- If the type of the target is an anonymous access-to-constant type
1180 -- (an observing access type), the source shall be an owning access
1181 -- object denoted by a name that is not in the Moved state, and whose
1182 -- root object is not in the Moved state and is not declared at a
1183 -- statically deeper accessibility level than that of the target
1186 if Is_Access_Constant (Target_Typ) then
1187 Perm := Get_Perm (Expr);
1189 if Perm = No_Access then
1190 Perm_Error (Expr, No_Access, No_Access,
1191 Expl => Get_Expl (Expr),
1192 Forbidden_Perm => True);
1196 Perm := Get_Perm (Expr_Root);
1198 if Perm = No_Access then
1199 Perm_Error (Expr, No_Access, No_Access,
1200 Expl => Get_Expl (Expr_Root),
1201 Forbidden_Perm => True);
1205 -- ??? check accessibility level
1207 -- If the type of the target is an anonymous access-to-variable
1208 -- type (an owning access type), the source shall be an owning
1209 -- access object denoted by a name that is in the Unrestricted
1210 -- state, and whose root object is the target object itself.
1212 Check_Expression (Expr, Observe);
1213 Handle_Observe (Target_Root, Expr, Is_Decl);
1216 Perm := Get_Perm (Expr);
1218 if Perm /= Read_Write then
1219 Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
1224 if not Is_Entity_Name (Target) then
1225 if Emit_Messages then
1227 ("target of borrow must be stand-alone variable",
1232 elsif Target_Root /= Expr_Root then
1233 if Emit_Messages then
1235 ("source of borrow must be variable &",
1242 Check_Expression (Expr, Borrow);
1243 Handle_Borrow (Target_Root, Expr, Is_Decl);
1246 elsif Is_Deep (Target_Typ) then
1248 if Is_Path_Expression (Expr) then
1249 Check_Expression (Expr, Move);
1252 if Emit_Messages then
1253 Error_Msg_N ("expression not allowed as source of move", Expr);
1259 Check_Expression (Expr, Read);
1261 end Check_Assignment;
1263 --------------------------
1264 -- Check_Call_Statement --
1265 --------------------------
1267 procedure Check_Call_Statement (Call : Node_Id) is
1269 Subp : constant Entity_Id := Get_Called_Entity (Call);
1271 -- Local subprograms
1273 procedure Check_Param (Formal : Entity_Id; Actual : Node_Id);
1274 -- Check the permission of every actual parameter
1276 procedure Update_Param (Formal : Entity_Id; Actual : Node_Id);
1277 -- Update the permission of OUT actual parameters
1283 procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
1285 Check_Parameter_Or_Global
1287 Typ => Retysp (Etype (Formal)),
1288 Kind => Ekind (Formal),
1290 Global_Var => False);
1297 procedure Update_Param (Formal : Entity_Id; Actual : Node_Id) is
1298 Mode : constant Entity_Kind := Ekind (Formal);
1301 case Formal_Kind'(Mode) is
1302 when E_Out_Parameter =>
1303 Check_Expression (Actual, Assign);
1310 procedure Check_Params is new
1311 Iterate_Call_Parameters (Check_Param);
1313 procedure Update_Params is new
1314 Iterate_Call_Parameters (Update_Param);
1316 -- Start of processing for Check_Call_Statement
1319 Inside_Procedure_Call := True;
1320 Check_Params (Call);
1321 if Ekind (Get_Called_Entity (Call)) = E_Subprogram_Type then
1322 if Emit_Messages then
1324 ("call through access to subprogram is not allowed in SPARK",
1328 Check_Globals (Get_Called_Entity (Call));
1331 Inside_Procedure_Call := False;
1332 Update_Params (Call);
1333 end Check_Call_Statement;
1335 -------------------------
1336 -- Check_Callable_Body --
1337 -------------------------
1339 procedure Check_Callable_Body (Body_N : Node_Id) is
1340 Save_In_Elab : constant Boolean := Inside_Elaboration;
1341 Body_Id : constant Entity_Id := Defining_Entity (Body_N);
1342 Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
1343 Prag : constant Node_Id := SPARK_Pragma (Body_Id);
1345 Saved_Env : Perm_Env;
1346 Saved_Borrowers : Variable_Mapping;
1347 Saved_Observers : Variable_Mapping;
1350 -- Only SPARK bodies are analyzed
1353 or else Get_SPARK_Mode_From_Annotation (Prag) /= Opt.On
1358 Inside_Elaboration := False;
1360 if Ekind (Spec_Id) = E_Function
1361 and then Is_Anonymous_Access_Type (Etype (Spec_Id))
1362 and then not Is_Traversal_Function (Spec_Id)
1364 if Emit_Messages then
1365 Error_Msg_N ("anonymous access type for result only allowed for "
1366 & "traversal functions", Spec_Id);
1371 -- Save environment and put a new one in place
1373 Move_Env (Current_Perm_Env, Saved_Env);
1374 Move_Variable_Mapping (Current_Borrowers, Saved_Borrowers);
1375 Move_Variable_Mapping (Current_Observers, Saved_Observers);
1377 -- Add formals and globals to the environment with adequate permissions
1379 if Is_Subprogram_Or_Entry (Spec_Id) then
1380 Setup_Parameters (Spec_Id);
1381 Setup_Globals (Spec_Id);
1384 -- For protected operations, add protected components to the environment
1385 -- with adequate permissions.
1387 if Is_Protected_Operation (Spec_Id) then
1388 Setup_Protected_Components (Spec_Id);
1391 -- Analyze the body of the subprogram
1393 Check_List (Declarations (Body_N));
1394 Check_Node (Handled_Statement_Sequence (Body_N));
1396 -- Check the read-write permissions of borrowed parameters/globals
1398 if Ekind_In (Spec_Id, E_Procedure, E_Entry)
1399 and then not No_Return (Spec_Id)
1401 Return_Parameters (Spec_Id);
1402 Return_Globals (Spec_Id);
1405 -- Restore the saved environment and free the current one
1407 Move_Env (Saved_Env, Current_Perm_Env);
1408 Move_Variable_Mapping (Saved_Borrowers, Current_Borrowers);
1409 Move_Variable_Mapping (Saved_Observers, Current_Observers);
1411 Inside_Elaboration := Save_In_Elab;
1412 end Check_Callable_Body;
1414 -----------------------
1415 -- Check_Declaration --
1416 -----------------------
1418 procedure Check_Declaration (Decl : Node_Id) is
1419 Target : constant Entity_Id := Defining_Identifier (Decl);
1420 Target_Typ : constant Node_Id := Etype (Target);
1422 Dummy : Boolean := True;
1425 -- Start with legality rules not related to permissions
1427 Check_Declaration_Legality (Decl, Force => True, Legal => Dummy);
1429 -- Now check permission-related legality rules
1431 case N_Declaration'(Nkind (Decl)) is
1432 when N_Full_Type_Declaration =>
1435 -- ??? What about component declarations with defaults.
1437 when N_Subtype_Declaration =>
1438 Check_Expression (Subtype_Indication (Decl), Read);
1440 when N_Object_Declaration =>
1441 Expr := Expression (Decl);
1443 if Present (Expr) then
1444 Check_Assignment (Target => Target,
1448 if Is_Deep (Target_Typ) then
1450 Tree : constant Perm_Tree_Access :=
1451 new Perm_Tree_Wrapper'
1453 (Kind => Entire_Object,
1454 Is_Node_Deep => True,
1455 Explanation => Decl,
1456 Permission => Read_Write,
1457 Children_Permission => Read_Write));
1459 Set (Current_Perm_Env, Target, Tree);
1463 when N_Iterator_Specification =>
1466 when N_Loop_Parameter_Specification =>
1469 -- Checking should not be called directly on these nodes
1471 when N_Function_Specification
1472 | N_Entry_Declaration
1473 | N_Procedure_Specification
1474 | N_Component_Declaration
1476 raise Program_Error;
1478 -- Ignored constructs for pointer checking
1480 when N_Formal_Object_Declaration
1481 | N_Formal_Type_Declaration
1482 | N_Incomplete_Type_Declaration
1483 | N_Private_Extension_Declaration
1484 | N_Private_Type_Declaration
1485 | N_Protected_Type_Declaration
1489 -- The following nodes are rewritten by semantic analysis
1491 when N_Expression_Function =>
1492 raise Program_Error;
1494 end Check_Declaration;
1496 --------------------------------
1497 -- Check_Declaration_Legality --
1498 --------------------------------
1500 procedure Check_Declaration_Legality
1503 Legal : in out Boolean)
1505 function Original_Emit_Messages return Boolean renames Emit_Messages;
1507 function Emit_Messages return Boolean;
1508 -- Local wrapper around generic formal parameter Emit_Messages, to
1509 -- check the value of parameter Force before calling the original
1510 -- Emit_Messages, and setting Legal to False.
1516 function Emit_Messages return Boolean is
1519 return Force and then Original_Emit_Messages;
1524 Target : constant Entity_Id := Defining_Identifier (Decl);
1525 Target_Typ : constant Node_Id := Etype (Target);
1528 -- Start of processing for Check_Declaration_Legality
1531 case N_Declaration'(Nkind (Decl)) is
1532 when N_Full_Type_Declaration =>
1533 Check_Type_Legality (Target, Force, Legal);
1535 when N_Subtype_Declaration =>
1538 when N_Object_Declaration =>
1539 Expr := Expression (Decl);
1541 Check_Type_Legality (Target_Typ, Force, Legal);
1543 -- A declaration of a stand-alone object of an anonymous access
1544 -- type shall have an explicit initial value and shall occur
1545 -- immediately within a subprogram body, an entry body, or a
1546 -- block statement (SPARK RM 3.10(4)).
1548 if Is_Anonymous_Access_Type (Target_Typ) then
1550 Scop : constant Entity_Id := Scope (Target);
1552 if not Is_Local_Context (Scop) then
1553 if Emit_Messages then
1555 ("object of anonymous access type must be declared "
1556 & "immediately within a subprogram, entry or block "
1557 & "(SPARK RM 3.10(4))", Decl);
1563 if Emit_Messages then
1564 Error_Msg_N ("object of anonymous access type must be "
1565 & "initialized (SPARK RM 3.10(4))", Decl);
1570 when N_Iterator_Specification =>
1573 when N_Loop_Parameter_Specification =>
1576 -- Checking should not be called directly on these nodes
1578 when N_Function_Specification
1579 | N_Entry_Declaration
1580 | N_Procedure_Specification
1581 | N_Component_Declaration
1583 raise Program_Error;
1585 -- Ignored constructs for pointer checking
1587 when N_Formal_Object_Declaration
1588 | N_Formal_Type_Declaration
1589 | N_Incomplete_Type_Declaration
1590 | N_Private_Extension_Declaration
1591 | N_Private_Type_Declaration
1592 | N_Protected_Type_Declaration
1596 -- The following nodes are rewritten by semantic analysis
1598 when N_Expression_Function =>
1599 raise Program_Error;
1601 end Check_Declaration_Legality;
1603 ----------------------
1604 -- Check_Expression --
1605 ----------------------
1607 procedure Check_Expression
1609 Mode : Extended_Checking_Mode)
1611 -- Local subprograms
1613 function Is_Type_Name (Expr : Node_Id) return Boolean;
1614 -- Detect when a path expression is in fact a type name
1616 procedure Move_Expression (Expr : Node_Id);
1617 -- Some subexpressions are only analyzed in Move mode. This is a
1618 -- specialized version of Check_Expression for that case.
1620 procedure Move_Expression_List (L : List_Id);
1621 -- Call Move_Expression on every expression in the list L
1623 procedure Read_Expression (Expr : Node_Id);
1624 -- Most subexpressions are only analyzed in Read mode. This is a
1625 -- specialized version of Check_Expression for that case.
1627 procedure Read_Expression_List (L : List_Id);
1628 -- Call Read_Expression on every expression in the list L
1630 procedure Read_Indexes (Expr : Node_Id);
1631 -- When processing a path, the index expressions and function call
1632 -- arguments occurring on the path should be analyzed in Read mode.
1638 function Is_Type_Name (Expr : Node_Id) return Boolean is
1640 return Nkind_In (Expr, N_Expanded_Name, N_Identifier)
1641 and then Is_Type (Entity (Expr));
1644 ---------------------
1645 -- Move_Expression --
1646 ---------------------
1648 -- Distinguish the case where the argument is a path expression that
1649 -- needs explicit moving.
1651 procedure Move_Expression (Expr : Node_Id) is
1653 if Is_Path_Expression (Expr) then
1654 Check_Expression (Expr, Move);
1656 Read_Expression (Expr);
1658 end Move_Expression;
1660 --------------------------
1661 -- Move_Expression_List --
1662 --------------------------
1664 procedure Move_Expression_List (L : List_Id) is
1668 while Present (N) loop
1669 Move_Expression (N);
1672 end Move_Expression_List;
1674 ---------------------
1675 -- Read_Expression --
1676 ---------------------
1678 procedure Read_Expression (Expr : Node_Id) is
1680 Check_Expression (Expr, Read);
1681 end Read_Expression;
1683 --------------------------
1684 -- Read_Expression_List --
1685 --------------------------
1687 procedure Read_Expression_List (L : List_Id) is
1691 while Present (N) loop
1692 Read_Expression (N);
1695 end Read_Expression_List;
1701 procedure Read_Indexes (Expr : Node_Id) is
1703 -- Local subprograms
1705 function Is_Singleton_Choice (Choices : List_Id) return Boolean;
1706 -- Return whether Choices is a singleton choice
1708 procedure Read_Param (Formal : Entity_Id; Actual : Node_Id);
1709 -- Call Read_Expression on the actual
1711 -------------------------
1712 -- Is_Singleton_Choice --
1713 -------------------------
1715 function Is_Singleton_Choice (Choices : List_Id) return Boolean is
1716 Choice : constant Node_Id := First (Choices);
1718 return List_Length (Choices) = 1
1719 and then Nkind (Choice) /= N_Others_Choice
1720 and then not Nkind_In (Choice, N_Subtype_Indication, N_Range)
1722 (Nkind_In (Choice, N_Identifier, N_Expanded_Name)
1723 and then Is_Type (Entity (Choice)));
1724 end Is_Singleton_Choice;
1730 procedure Read_Param (Formal : Entity_Id; Actual : Node_Id) is
1731 pragma Unreferenced (Formal);
1733 Read_Expression (Actual);
1736 procedure Read_Params is new Iterate_Call_Parameters (Read_Param);
1738 -- Start of processing for Read_Indexes
1741 if not Is_Subpath_Expression (Expr) then
1742 if Emit_Messages then
1744 ("name expected here for move/borrow/observe", Expr);
1749 case N_Subexpr'(Nkind (Expr)) is
1756 when N_Explicit_Dereference
1757 | N_Selected_Component
1759 Read_Indexes (Prefix (Expr));
1761 when N_Indexed_Component =>
1762 Read_Indexes (Prefix (Expr));
1763 Read_Expression_List (Expressions (Expr));
1766 Read_Indexes (Prefix (Expr));
1767 Read_Expression (Discrete_Range (Expr));
1769 -- The argument of an allocator is moved as part of the implicit
1773 Move_Expression (Expression (Expr));
1775 when N_Function_Call =>
1777 if Ekind (Get_Called_Entity (Expr)) = E_Subprogram_Type then
1778 if Emit_Messages then
1780 ("call through access to subprogram is not allowed in "
1784 Check_Globals (Get_Called_Entity (Expr));
1788 Read_Expression (Left_Opnd (Expr));
1789 Read_Expression (Right_Opnd (Expr));
1791 when N_Qualified_Expression
1793 | N_Unchecked_Type_Conversion
1795 Read_Indexes (Expression (Expr));
1799 Assocs : constant List_Id := Component_Associations (Expr);
1801 Assoc : Node_Id := Nlists.First (Assocs);
1805 -- The subexpressions of an aggregate are moved as part
1806 -- of the implicit assignments. Handle the positional
1807 -- components first.
1809 Move_Expression_List (Expressions (Expr));
1811 -- Handle the named components next
1813 while Present (Assoc) loop
1814 CL := Choices (Assoc);
1816 -- For an array aggregate, we should also check that the
1817 -- expressions used in choices are readable.
1819 if Is_Array_Type (Etype (Expr)) then
1820 Choice := Nlists.First (CL);
1821 while Present (Choice) loop
1822 if Nkind (Choice) /= N_Others_Choice then
1823 Read_Expression (Choice);
1829 -- There can be only one element for a value of deep type
1830 -- in order to avoid aliasing.
1832 if not Box_Present (Assoc)
1833 and then Is_Deep (Etype (Expression (Assoc)))
1834 and then not Is_Singleton_Choice (CL)
1835 and then Emit_Messages
1838 ("singleton choice required to prevent aliasing",
1842 -- The subexpressions of an aggregate are moved as part
1843 -- of the implicit assignments.
1845 if not Box_Present (Assoc) then
1846 Move_Expression (Expression (Assoc));
1853 when N_Extension_Aggregate =>
1855 Exprs : constant List_Id := Expressions (Expr);
1856 Assocs : constant List_Id := Component_Associations (Expr);
1858 Assoc : Node_Id := Nlists.First (Assocs);
1861 Move_Expression (Ancestor_Part (Expr));
1863 -- No positional components allowed at this stage
1865 if Present (Exprs) then
1866 raise Program_Error;
1869 while Present (Assoc) loop
1870 CL := Choices (Assoc);
1872 -- Only singleton components allowed at this stage
1874 if not Is_Singleton_Choice (CL) then
1875 raise Program_Error;
1878 -- The subexpressions of an aggregate are moved as part
1879 -- of the implicit assignments.
1881 if not Box_Present (Assoc) then
1882 Move_Expression (Expression (Assoc));
1889 when N_If_Expression =>
1891 Cond : constant Node_Id := First (Expressions (Expr));
1892 Then_Part : constant Node_Id := Next (Cond);
1893 Else_Part : constant Node_Id := Next (Then_Part);
1895 Read_Expression (Cond);
1896 Read_Indexes (Then_Part);
1897 Read_Indexes (Else_Part);
1900 when N_Case_Expression =>
1902 Cases : constant List_Id := Alternatives (Expr);
1903 Cur_Case : Node_Id := First (Cases);
1906 Read_Expression (Expression (Expr));
1908 while Present (Cur_Case) loop
1909 Read_Indexes (Expression (Cur_Case));
1914 when N_Attribute_Reference =>
1916 (Get_Attribute_Id (Attribute_Name (Expr)) =
1917 Attribute_Loop_Entry
1919 Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
1921 Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Image);
1923 Read_Expression (Prefix (Expr));
1925 if Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
1926 or else (Get_Attribute_Id (Attribute_Name (Expr)) =
1928 and then Is_Type_Name (Prefix (Expr)))
1930 Read_Expression_List (Expressions (Expr));
1934 raise Program_Error;
1938 -- Start of processing for Check_Expression
1941 if Is_Type_Name (Expr) then
1944 elsif Is_Path_Expression (Expr) then
1945 if Mode /= Assign then
1946 Read_Indexes (Expr);
1949 if Mode /= Read_Subexpr then
1950 Process_Path (Expr, Mode);
1956 -- Expressions that are not path expressions should only be analyzed in
1959 if Mode /= Read then
1960 if Emit_Messages then
1961 Error_Msg_N ("name expected here for move/borrow/observe", Expr);
1966 -- Special handling for nodes that may contain evaluated expressions in
1967 -- the form of constraints.
1969 case Nkind (Expr) is
1970 when N_Index_Or_Discriminant_Constraint =>
1972 Assn : Node_Id := First (Constraints (Expr));
1974 while Present (Assn) loop
1975 case Nkind (Assn) is
1976 when N_Discriminant_Association =>
1977 Read_Expression (Expression (Assn));
1980 Read_Expression (Assn);
1988 when N_Range_Constraint =>
1989 Read_Expression (Range_Expression (Expr));
1992 when N_Subtype_Indication =>
1993 if Present (Constraint (Expr)) then
1994 Read_Expression (Constraint (Expr));
1998 when N_Digits_Constraint =>
1999 Read_Expression (Digits_Expression (Expr));
2000 if Present (Range_Constraint (Expr)) then
2001 Read_Expression (Range_Constraint (Expr));
2005 when N_Delta_Constraint =>
2006 Read_Expression (Delta_Expression (Expr));
2007 if Present (Range_Constraint (Expr)) then
2008 Read_Expression (Range_Constraint (Expr));
2016 -- At this point Expr can only be a subexpression
2018 case N_Subexpr'(Nkind (Expr)) is
2023 Read_Expression (Left_Opnd (Expr));
2024 Read_Expression (Right_Opnd (Expr));
2026 when N_Membership_Test =>
2027 Read_Expression (Left_Opnd (Expr));
2028 if Present (Right_Opnd (Expr)) then
2029 Read_Expression (Right_Opnd (Expr));
2032 Cases : constant List_Id := Alternatives (Expr);
2033 Cur_Case : Node_Id := First (Cases);
2036 while Present (Cur_Case) loop
2037 Read_Expression (Cur_Case);
2044 Read_Expression (Right_Opnd (Expr));
2046 when N_Attribute_Reference =>
2048 Aname : constant Name_Id := Attribute_Name (Expr);
2049 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
2050 Pref : constant Node_Id := Prefix (Expr);
2051 Args : constant List_Id := Expressions (Expr);
2056 -- The following attributes take either no arguments, or
2057 -- arguments that do not refer to evaluated expressions
2058 -- (like Length or Loop_Entry), hence only the prefix
2059 -- needs to be read.
2061 when Attribute_Address
2062 | Attribute_Alignment
2063 | Attribute_Callable
2064 | Attribute_Component_Size
2065 | Attribute_Constrained
2067 | Attribute_First_Bit
2069 | Attribute_Last_Bit
2071 | Attribute_Loop_Entry
2072 | Attribute_Object_Size
2073 | Attribute_Position
2075 | Attribute_Terminated
2077 | Attribute_Value_Size
2079 Read_Expression (Pref);
2081 -- The following attributes take a type name as prefix,
2082 -- hence only the arguments need to be read.
2084 when Attribute_Ceiling
2091 | Attribute_Remainder
2092 | Attribute_Rounding
2094 | Attribute_Truncation
2098 Read_Expression_List (Args);
2100 -- Attributes Image and Img either take a type name as
2101 -- prefix with an expression in argument, or the expression
2102 -- directly as prefix. Adapt to each case.
2104 when Attribute_Image
2108 Read_Expression (Pref);
2110 Read_Expression_List (Args);
2113 -- Attribute Update takes expressions as both prefix and
2114 -- arguments, so both need to be read.
2116 when Attribute_Update =>
2117 Read_Expression (Pref);
2118 Read_Expression_List (Args);
2120 -- Attribute Modulus does not reference the evaluated
2121 -- expression, so it can be ignored for this analysis.
2123 when Attribute_Modulus =>
2126 -- The following attributes apply to types; there are no
2127 -- expressions to read.
2129 when Attribute_Class
2130 | Attribute_Storage_Size
2134 -- Postconditions should not be analyzed
2139 raise Program_Error;
2147 Read_Expression (Low_Bound (Expr));
2148 Read_Expression (High_Bound (Expr));
2150 when N_If_Expression =>
2151 Read_Expression_List (Expressions (Expr));
2153 when N_Case_Expression =>
2155 Cases : constant List_Id := Alternatives (Expr);
2156 Cur_Case : Node_Id := First (Cases);
2159 while Present (Cur_Case) loop
2160 Read_Expression (Expression (Cur_Case));
2164 Read_Expression (Expression (Expr));
2167 when N_Qualified_Expression
2169 | N_Unchecked_Type_Conversion
2171 Read_Expression (Expression (Expr));
2173 when N_Quantified_Expression =>
2175 For_In_Spec : constant Node_Id :=
2176 Loop_Parameter_Specification (Expr);
2177 For_Of_Spec : constant Node_Id :=
2178 Iterator_Specification (Expr);
2179 For_Of_Spec_Typ : Node_Id;
2182 if Present (For_In_Spec) then
2183 Read_Expression (Discrete_Subtype_Definition (For_In_Spec));
2185 Read_Expression (Name (For_Of_Spec));
2186 For_Of_Spec_Typ := Subtype_Indication (For_Of_Spec);
2187 if Present (For_Of_Spec_Typ) then
2188 Read_Expression (For_Of_Spec_Typ);
2192 Read_Expression (Condition (Expr));
2195 when N_Character_Literal
2196 | N_Numeric_Or_String_Literal
2198 | N_Raise_Expression
2203 when N_Delta_Aggregate
2208 -- Procedure calls are handled in Check_Node
2210 when N_Procedure_Call_Statement =>
2211 raise Program_Error;
2213 -- Path expressions are handled before this point
2218 | N_Explicit_Dereference
2219 | N_Extension_Aggregate
2222 | N_Indexed_Component
2224 | N_Selected_Component
2227 raise Program_Error;
2229 -- The following nodes are never generated in GNATprove mode
2231 when N_Expression_With_Actions
2233 | N_Unchecked_Expression
2235 raise Program_Error;
2237 end Check_Expression;
2243 procedure Check_List (L : List_Id) is
2247 while Present (N) loop
2253 --------------------------
2254 -- Check_Loop_Statement --
2255 --------------------------
2257 procedure Check_Loop_Statement (Stmt : Node_Id) is
2259 -- Local Subprograms
2261 procedure Check_Is_Less_Restrictive_Env
2262 (Exiting_Env : Perm_Env;
2263 Entry_Env : Perm_Env);
2264 -- This procedure checks that the Exiting_Env environment is less
2265 -- restrictive than the Entry_Env environment.
2267 procedure Check_Is_Less_Restrictive_Tree
2268 (New_Tree : Perm_Tree_Access;
2269 Orig_Tree : Perm_Tree_Access;
2271 -- Auxiliary procedure to check that the tree New_Tree is less
2272 -- restrictive than the tree Orig_Tree for the entity E.
2274 procedure Perm_Error_Loop_Exit
2278 Found_Perm : Perm_Kind;
2280 -- A procedure that is called when the permissions found contradict
2281 -- the rules established by the RM at the exit of loops. This function
2282 -- is called with the entity, the node of the enclosing loop, the
2283 -- permission that was expected, and the permission found, and issues
2284 -- an appropriate error message.
2286 -----------------------------------
2287 -- Check_Is_Less_Restrictive_Env --
2288 -----------------------------------
2290 procedure Check_Is_Less_Restrictive_Env
2291 (Exiting_Env : Perm_Env;
2292 Entry_Env : Perm_Env)
2294 Comp_Entry : Perm_Tree_Maps.Key_Option;
2295 Iter_Entry, Iter_Exit : Perm_Tree_Access;
2298 Comp_Entry := Get_First_Key (Entry_Env);
2299 while Comp_Entry.Present loop
2300 Iter_Entry := Get (Entry_Env, Comp_Entry.K);
2301 pragma Assert (Iter_Entry /= null);
2302 Iter_Exit := Get (Exiting_Env, Comp_Entry.K);
2303 pragma Assert (Iter_Exit /= null);
2304 Check_Is_Less_Restrictive_Tree
2305 (New_Tree => Iter_Exit,
2306 Orig_Tree => Iter_Entry,
2308 Comp_Entry := Get_Next_Key (Entry_Env);
2310 end Check_Is_Less_Restrictive_Env;
2312 ------------------------------------
2313 -- Check_Is_Less_Restrictive_Tree --
2314 ------------------------------------
2316 procedure Check_Is_Less_Restrictive_Tree
2317 (New_Tree : Perm_Tree_Access;
2318 Orig_Tree : Perm_Tree_Access;
2321 -- Local subprograms
2323 procedure Check_Is_Less_Restrictive_Tree_Than
2324 (Tree : Perm_Tree_Access;
2327 -- Auxiliary procedure to check that the tree N is less restrictive
2328 -- than the given permission P.
2330 procedure Check_Is_More_Restrictive_Tree_Than
2331 (Tree : Perm_Tree_Access;
2334 -- Auxiliary procedure to check that the tree N is more restrictive
2335 -- than the given permission P.
2337 -----------------------------------------
2338 -- Check_Is_Less_Restrictive_Tree_Than --
2339 -----------------------------------------
2341 procedure Check_Is_Less_Restrictive_Tree_Than
2342 (Tree : Perm_Tree_Access;
2347 if not (Permission (Tree) >= Perm) then
2348 Perm_Error_Loop_Exit
2349 (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
2353 when Entire_Object =>
2354 if not (Children_Permission (Tree) >= Perm) then
2355 Perm_Error_Loop_Exit
2356 (E, Stmt, Children_Permission (Tree), Perm,
2357 Explanation (Tree));
2362 Check_Is_Less_Restrictive_Tree_Than
2363 (Get_All (Tree), Perm, E);
2365 when Array_Component =>
2366 Check_Is_Less_Restrictive_Tree_Than
2367 (Get_Elem (Tree), Perm, E);
2369 when Record_Component =>
2371 Comp : Perm_Tree_Access;
2373 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
2374 while Comp /= null loop
2375 Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E);
2377 Perm_Tree_Maps.Get_Next (Component (Tree));
2381 end Check_Is_Less_Restrictive_Tree_Than;
2383 -----------------------------------------
2384 -- Check_Is_More_Restrictive_Tree_Than --
2385 -----------------------------------------
2387 procedure Check_Is_More_Restrictive_Tree_Than
2388 (Tree : Perm_Tree_Access;
2393 if not (Perm >= Permission (Tree)) then
2394 Perm_Error_Loop_Exit
2395 (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
2399 when Entire_Object =>
2400 if not (Perm >= Children_Permission (Tree)) then
2401 Perm_Error_Loop_Exit
2402 (E, Stmt, Children_Permission (Tree), Perm,
2403 Explanation (Tree));
2407 Check_Is_More_Restrictive_Tree_Than
2408 (Get_All (Tree), Perm, E);
2410 when Array_Component =>
2411 Check_Is_More_Restrictive_Tree_Than
2412 (Get_Elem (Tree), Perm, E);
2414 when Record_Component =>
2416 Comp : Perm_Tree_Access;
2418 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
2419 while Comp /= null loop
2420 Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E);
2422 Perm_Tree_Maps.Get_Next (Component (Tree));
2426 end Check_Is_More_Restrictive_Tree_Than;
2428 -- Start of processing for Check_Is_Less_Restrictive_Tree
2431 if not (Permission (New_Tree) <= Permission (Orig_Tree)) then
2432 Perm_Error_Loop_Exit
2435 Perm => Permission (New_Tree),
2436 Found_Perm => Permission (Orig_Tree),
2437 Expl => Explanation (New_Tree));
2440 case Kind (New_Tree) is
2442 -- Potentially folded tree. We check the other tree Orig_Tree to
2443 -- check whether it is folded or not. If folded we just compare
2444 -- their Permission and Children_Permission, if not, then we
2445 -- look at the Children_Permission of the folded tree against
2446 -- the unfolded tree Orig_Tree.
2448 when Entire_Object =>
2449 case Kind (Orig_Tree) is
2450 when Entire_Object =>
2451 if not (Children_Permission (New_Tree) <=
2452 Children_Permission (Orig_Tree))
2454 Perm_Error_Loop_Exit
2456 Children_Permission (New_Tree),
2457 Children_Permission (Orig_Tree),
2458 Explanation (New_Tree));
2462 Check_Is_More_Restrictive_Tree_Than
2463 (Get_All (Orig_Tree), Children_Permission (New_Tree), E);
2465 when Array_Component =>
2466 Check_Is_More_Restrictive_Tree_Than
2467 (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E);
2469 when Record_Component =>
2471 Comp : Perm_Tree_Access;
2473 Comp := Perm_Tree_Maps.Get_First
2474 (Component (Orig_Tree));
2475 while Comp /= null loop
2476 Check_Is_More_Restrictive_Tree_Than
2477 (Comp, Children_Permission (New_Tree), E);
2478 Comp := Perm_Tree_Maps.Get_Next
2479 (Component (Orig_Tree));
2485 case Kind (Orig_Tree) is
2486 when Entire_Object =>
2487 Check_Is_Less_Restrictive_Tree_Than
2488 (Get_All (New_Tree), Children_Permission (Orig_Tree), E);
2491 Check_Is_Less_Restrictive_Tree
2492 (Get_All (New_Tree), Get_All (Orig_Tree), E);
2495 raise Program_Error;
2498 when Array_Component =>
2499 case Kind (Orig_Tree) is
2500 when Entire_Object =>
2501 Check_Is_Less_Restrictive_Tree_Than
2502 (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E);
2504 when Array_Component =>
2505 Check_Is_Less_Restrictive_Tree
2506 (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E);
2509 raise Program_Error;
2512 when Record_Component =>
2514 CompN : Perm_Tree_Access;
2517 Perm_Tree_Maps.Get_First (Component (New_Tree));
2518 case Kind (Orig_Tree) is
2519 when Entire_Object =>
2520 while CompN /= null loop
2521 Check_Is_Less_Restrictive_Tree_Than
2522 (CompN, Children_Permission (Orig_Tree), E);
2525 Perm_Tree_Maps.Get_Next (Component (New_Tree));
2528 when Record_Component =>
2531 KeyO : Perm_Tree_Maps.Key_Option;
2532 CompO : Perm_Tree_Access;
2534 KeyO := Perm_Tree_Maps.Get_First_Key
2535 (Component (Orig_Tree));
2536 while KeyO.Present loop
2537 CompN := Perm_Tree_Maps.Get
2538 (Component (New_Tree), KeyO.K);
2539 CompO := Perm_Tree_Maps.Get
2540 (Component (Orig_Tree), KeyO.K);
2541 pragma Assert (CompO /= null);
2543 Check_Is_Less_Restrictive_Tree (CompN, CompO, E);
2545 KeyO := Perm_Tree_Maps.Get_Next_Key
2546 (Component (Orig_Tree));
2551 raise Program_Error;
2555 end Check_Is_Less_Restrictive_Tree;
2557 --------------------------
2558 -- Perm_Error_Loop_Exit --
2559 --------------------------
2561 procedure Perm_Error_Loop_Exit
2565 Found_Perm : Perm_Kind;
2569 if Emit_Messages then
2570 Error_Msg_Node_2 := Loop_Id;
2572 ("insufficient permission for & when exiting loop &", E);
2573 Perm_Mismatch (Exp_Perm => Perm,
2574 Act_Perm => Found_Perm,
2578 end Perm_Error_Loop_Exit;
2582 Loop_Name : constant Entity_Id := Entity (Identifier (Stmt));
2583 Loop_Env : constant Perm_Env_Access := new Perm_Env;
2584 Scheme : constant Node_Id := Iteration_Scheme (Stmt);
2586 -- Start of processing for Check_Loop_Statement
2589 -- Save environment prior to the loop
2591 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
2593 -- Add saved environment to loop environment
2595 Set (Current_Loops_Envs, Loop_Name, Loop_Env);
2597 -- If the loop is not a plain-loop, then it may either never be entered,
2598 -- or it may be exited after a number of iterations. Hence add the
2599 -- current permission environment as the initial loop exit environment.
2600 -- Otherwise, the loop exit environment remains empty until it is
2601 -- populated by analyzing exit statements.
2603 if Present (Iteration_Scheme (Stmt)) then
2605 Exit_Env : constant Perm_Env_Access := new Perm_Env;
2608 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
2609 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
2615 if Present (Scheme) then
2617 -- Case of a WHILE loop
2619 if Present (Condition (Scheme)) then
2620 Check_Expression (Condition (Scheme), Read);
2622 -- Case of a FOR loop
2626 Param_Spec : constant Node_Id :=
2627 Loop_Parameter_Specification (Scheme);
2628 Iter_Spec : constant Node_Id := Iterator_Specification (Scheme);
2630 if Present (Param_Spec) then
2632 (Discrete_Subtype_Definition (Param_Spec), Read);
2634 Check_Expression (Name (Iter_Spec), Read);
2635 if Present (Subtype_Indication (Iter_Spec)) then
2636 Check_Expression (Subtype_Indication (Iter_Spec), Read);
2643 Check_List (Statements (Stmt));
2645 -- Check that environment gets less restrictive at end of loop
2647 Check_Is_Less_Restrictive_Env
2648 (Exiting_Env => Current_Perm_Env,
2649 Entry_Env => Loop_Env.all);
2651 -- Set environment to the one for exiting the loop
2654 Exit_Env : constant Perm_Env_Access :=
2655 Get (Current_Loops_Accumulators, Loop_Name);
2657 Free_Env (Current_Perm_Env);
2659 -- In the normal case, Exit_Env is not null and we use it. In the
2660 -- degraded case of a plain-loop without exit statements, Exit_Env is
2661 -- null, and we use the initial permission environment at the start
2662 -- of the loop to continue analysis. Any environment would be fine
2663 -- here, since the code after the loop is dead code, but this way we
2664 -- avoid spurious errors by having at least variables in scope inside
2667 if Exit_Env /= null then
2668 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
2669 Free_Env (Loop_Env.all);
2670 Free_Env (Exit_Env.all);
2672 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
2673 Free_Env (Loop_Env.all);
2676 end Check_Loop_Statement;
2682 procedure Check_Node (N : Node_Id) is
2684 procedure Check_Subprogram_Contract (N : Node_Id);
2685 -- Check the postcondition-like contracts for use of 'Old
2687 -------------------------------
2688 -- Check_Subprogram_Contract --
2689 -------------------------------
2691 procedure Check_Subprogram_Contract (N : Node_Id) is
2693 if Nkind (N) = N_Subprogram_Declaration
2694 or else Acts_As_Spec (N)
2697 E : constant Entity_Id := Unique_Defining_Entity (N);
2698 Post : constant Node_Id :=
2699 Get_Pragma (E, Pragma_Postcondition);
2700 Cases : constant Node_Id :=
2701 Get_Pragma (E, Pragma_Contract_Cases);
2703 Check_Old_Loop_Entry (Post);
2704 Check_Old_Loop_Entry (Cases);
2707 elsif Nkind (N) = N_Subprogram_Body then
2709 E : constant Entity_Id := Defining_Entity (N);
2710 Ref_Post : constant Node_Id :=
2711 Get_Pragma (E, Pragma_Refined_Post);
2713 Check_Old_Loop_Entry (Ref_Post);
2716 end Check_Subprogram_Contract;
2718 -- Start of processing for Check_Node
2722 when N_Declaration =>
2723 Check_Declaration (N);
2726 Check_Node (Get_Body_From_Stub (N));
2728 when N_Statement_Other_Than_Procedure_Call =>
2729 Check_Statement (N);
2731 when N_Procedure_Call_Statement =>
2732 Check_Call_Statement (N);
2734 when N_Package_Body =>
2735 if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
2736 Check_Package_Body (N);
2739 when N_Subprogram_Body =>
2740 if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
2741 Check_Subprogram_Contract (N);
2742 Check_Callable_Body (N);
2748 Check_Callable_Body (N);
2750 when N_Protected_Body =>
2751 Check_List (Declarations (N));
2753 when N_Package_Declaration =>
2754 Check_Package_Spec (N);
2756 when N_Handled_Sequence_Of_Statements =>
2757 Check_List (Statements (N));
2762 when N_Subprogram_Declaration =>
2763 Check_Subprogram_Contract (N);
2765 -- Attribute references in statement position are not supported in
2766 -- SPARK and will be rejected by GNATprove.
2768 when N_Attribute_Reference =>
2771 -- Ignored constructs for pointer checking
2773 when N_Abstract_Subprogram_Declaration
2775 | N_Attribute_Definition_Clause
2777 | N_Delta_Constraint
2778 | N_Digits_Constraint
2780 | N_Enumeration_Representation_Clause
2781 | N_Exception_Declaration
2782 | N_Exception_Renaming_Declaration
2783 | N_Formal_Package_Declaration
2784 | N_Formal_Subprogram_Declaration
2786 | N_Freeze_Generic_Entity
2787 | N_Function_Instantiation
2788 | N_Generic_Function_Renaming_Declaration
2789 | N_Generic_Package_Declaration
2790 | N_Generic_Package_Renaming_Declaration
2791 | N_Generic_Procedure_Renaming_Declaration
2792 | N_Generic_Subprogram_Declaration
2793 | N_Implicit_Label_Declaration
2796 | N_Number_Declaration
2797 | N_Object_Renaming_Declaration
2799 | N_Package_Instantiation
2800 | N_Package_Renaming_Declaration
2801 | N_Procedure_Instantiation
2803 | N_Record_Representation_Clause
2804 | N_Subprogram_Renaming_Declaration
2805 | N_Task_Type_Declaration
2806 | N_Use_Package_Clause
2809 | N_Validate_Unchecked_Conversion
2810 | N_Variable_Reference_Marker
2811 | N_Discriminant_Association
2813 -- ??? check whether we should do something special for
2814 -- N_Discriminant_Association, or maybe raise Program_Error.
2818 -- Checking should not be called directly on these nodes
2821 raise Program_Error;
2825 --------------------------
2826 -- Check_Old_Loop_Entry --
2827 --------------------------
2829 procedure Check_Old_Loop_Entry (N : Node_Id) is
2831 function Check_Attribute (N : Node_Id) return Traverse_Result;
2833 ---------------------
2834 -- Check_Attribute --
2835 ---------------------
2837 function Check_Attribute (N : Node_Id) return Traverse_Result is
2838 Attr_Id : Attribute_Id;
2843 if Nkind (N) = N_Attribute_Reference then
2844 Attr_Id := Get_Attribute_Id (Attribute_Name (N));
2845 Aname := Attribute_Name (N);
2847 if Attr_Id = Attribute_Old
2848 or else Attr_Id = Attribute_Loop_Entry
2852 if Is_Deep (Etype (Pref)) then
2853 if Nkind (Pref) /= N_Function_Call then
2854 if Emit_Messages then
2855 Error_Msg_Name_1 := Aname;
2857 ("prefix of % attribute must be a function call "
2858 & "(SPARK RM 3.10(14))", Pref);
2861 elsif Is_Traversal_Function_Call (Pref) then
2862 if Emit_Messages then
2863 Error_Msg_Name_1 := Aname;
2865 ("prefix of % attribute should not call a traversal "
2866 & "function (SPARK RM 3.10(14))", Pref);
2874 end Check_Attribute;
2876 procedure Check_All is new Traverse_Proc (Check_Attribute);
2878 -- Start of processing for Check_Old_Loop_Entry
2882 end Check_Old_Loop_Entry;
2884 ------------------------
2885 -- Check_Package_Body --
2886 ------------------------
2888 procedure Check_Package_Body (Pack : Node_Id) is
2889 Save_In_Elab : constant Boolean := Inside_Elaboration;
2890 Spec : constant Node_Id :=
2891 Package_Specification (Corresponding_Spec (Pack));
2892 Id : constant Entity_Id := Defining_Entity (Pack);
2893 Prag : constant Node_Id := SPARK_Pragma (Id);
2894 Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id);
2895 Saved_Env : Perm_Env;
2899 and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
2901 Inside_Elaboration := True;
2903 -- Save environment and put a new one in place
2905 Move_Env (Current_Perm_Env, Saved_Env);
2907 -- Reanalyze package spec to have its variables in the environment
2909 Check_List (Visible_Declarations (Spec));
2910 Check_List (Private_Declarations (Spec));
2912 -- Check declarations and statements in the special mode for
2915 Check_List (Declarations (Pack));
2917 if Present (Aux_Prag)
2918 and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
2920 Check_Node (Handled_Statement_Sequence (Pack));
2923 -- Restore the saved environment and free the current one
2925 Move_Env (Saved_Env, Current_Perm_Env);
2927 Inside_Elaboration := Save_In_Elab;
2929 end Check_Package_Body;
2931 ------------------------
2932 -- Check_Package_Spec --
2933 ------------------------
2935 procedure Check_Package_Spec (Pack : Node_Id) is
2936 Save_In_Elab : constant Boolean := Inside_Elaboration;
2937 Spec : constant Node_Id := Specification (Pack);
2938 Id : constant Entity_Id := Defining_Entity (Pack);
2939 Prag : constant Node_Id := SPARK_Pragma (Id);
2940 Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id);
2941 Saved_Env : Perm_Env;
2945 and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
2947 Inside_Elaboration := True;
2949 -- Save environment and put a new one in place
2951 Move_Env (Current_Perm_Env, Saved_Env);
2953 -- Check declarations in the special mode for elaboration
2955 Check_List (Visible_Declarations (Spec));
2957 if Present (Aux_Prag)
2958 and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
2960 Check_List (Private_Declarations (Spec));
2963 -- Restore the saved environment and free the current one. As part of
2964 -- the restoration, the environment of the package spec is merged in
2965 -- the enclosing environment, which may be an enclosing
2966 -- package/subprogram spec or body which has access to the variables
2967 -- of the package spec.
2969 Merge_Env (Saved_Env, Current_Perm_Env);
2971 Inside_Elaboration := Save_In_Elab;
2973 end Check_Package_Spec;
2975 -------------------------------
2976 -- Check_Parameter_Or_Global --
2977 -------------------------------
2979 procedure Check_Parameter_Or_Global
2984 Global_Var : Boolean)
2986 Mode : Checking_Mode;
2987 Status : Error_Status;
2991 and then Is_Anonymous_Access_Type (Typ)
2993 Check_Source_Of_Borrow_Or_Observe (Expr, Status);
2995 if Status /= OK then
3001 when E_In_Parameter =>
3003 -- Inputs of functions have R permission only
3005 if Ekind (Subp) = E_Function then
3008 -- Input global variables have R permission only
3010 elsif Global_Var then
3013 -- Anonymous access to constant is an observe
3015 elsif Is_Anonymous_Access_Type (Typ)
3016 and then Is_Access_Constant (Typ)
3020 -- Other access types are a borrow
3022 elsif Is_Access_Type (Typ) then
3025 -- Deep types other than access types define an observe
3027 elsif Is_Deep (Typ) then
3030 -- Otherwise the variable is read
3036 when E_Out_Parameter =>
3039 when E_In_Out_Parameter =>
3043 if Mode = Assign then
3044 Check_Expression (Expr, Read_Subexpr);
3047 Check_Expression (Expr, Mode);
3048 end Check_Parameter_Or_Global;
3050 procedure Check_Globals_Inst is
3051 new Handle_Globals (Check_Parameter_Or_Global);
3053 procedure Check_Globals (Subp : Entity_Id) renames Check_Globals_Inst;
3059 procedure Check_Pragma (Prag : Node_Id) is
3060 Prag_Id : constant Pragma_Id := Get_Pragma_Id (Prag);
3061 Arg1 : constant Node_Id :=
3062 First (Pragma_Argument_Associations (Prag));
3063 Arg2 : Node_Id := Empty;
3066 if Present (Arg1) then
3067 Arg2 := Next (Arg1);
3071 when Pragma_Check =>
3073 Expr : constant Node_Id := Expression (Arg2);
3075 Check_Expression (Expr, Read);
3077 -- Prefix of Loop_Entry should be checked inside any assertion
3078 -- where it may appear.
3080 Check_Old_Loop_Entry (Expr);
3083 -- Prefix of Loop_Entry should be checked inside a Loop_Variant
3085 when Pragma_Loop_Variant =>
3086 Check_Old_Loop_Entry (Prag);
3088 -- There is no need to check contracts, as these can only access
3089 -- inputs and outputs of the subprogram. Inputs are checked
3090 -- independently for R permission. Outputs are checked
3091 -- independently to have RW permission on exit.
3093 -- Postconditions are checked for correct use of 'Old, but starting
3094 -- from the corresponding declaration, in order to avoid dealing with
3095 -- with contracts on generic subprograms, which are not handled in
3098 when Pragma_Precondition
3099 | Pragma_Postcondition
3100 | Pragma_Contract_Cases
3101 | Pragma_Refined_Post
3105 -- The same holds for the initial condition after package
3106 -- elaboration, for the different reason that library-level
3107 -- variables can only be left in RW state after elaboration.
3109 when Pragma_Initial_Condition =>
3112 -- These pragmas should have been rewritten and/or removed in
3116 | Pragma_Assert_And_Cut
3118 | Pragma_Compile_Time_Error
3119 | Pragma_Compile_Time_Warning
3121 | Pragma_Loop_Invariant
3123 raise Program_Error;
3130 -------------------------
3131 -- Check_Safe_Pointers --
3132 -------------------------
3134 procedure Check_Safe_Pointers (N : Node_Id) is
3136 -- Local subprograms
3138 procedure Check_List (L : List_Id);
3139 -- Call the main analysis procedure on each element of the list
3141 procedure Initialize;
3142 -- Initialize global variables before starting the analysis of a body
3148 procedure Check_List (L : List_Id) is
3152 while Present (N) loop
3153 Check_Safe_Pointers (N);
3162 procedure Initialize is
3164 Reset (Current_Loops_Envs);
3165 Reset (Current_Loops_Accumulators);
3166 Reset (Current_Perm_Env);
3169 -- Start of processing for Check_Safe_Pointers
3175 when N_Compilation_Unit =>
3176 Check_Safe_Pointers (Unit (N));
3179 | N_Package_Declaration
3180 | N_Subprogram_Declaration
3184 E : constant Entity_Id := Defining_Entity (N);
3185 Prag : constant Node_Id := SPARK_Pragma (E);
3186 -- SPARK_Mode pragma in application
3189 if Ekind (Unique_Entity (E)) in Generic_Unit_Kind then
3192 elsif Present (Prag) then
3193 if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then
3197 elsif Nkind (N) = N_Package_Body then
3198 Check_List (Declarations (N));
3200 elsif Nkind (N) = N_Package_Declaration then
3201 Check_List (Private_Declarations (Specification (N)));
3202 Check_List (Visible_Declarations (Specification (N)));
3209 end Check_Safe_Pointers;
3211 ---------------------------------------
3212 -- Check_Source_Of_Borrow_Or_Observe --
3213 ---------------------------------------
3215 procedure Check_Source_Of_Borrow_Or_Observe
3217 Status : out Error_Status)
3222 if Is_Path_Expression (Expr) then
3223 Root := Get_Root_Object (Expr);
3230 -- SPARK RM 3.10(3): If the target of an assignment operation is an
3231 -- object of an anonymous access-to-object type (including copy-in for
3232 -- a parameter), then the source shall be a name denoting a part of a
3233 -- stand-alone object, a part of a parameter, or a call to a traversal
3237 if Emit_Messages then
3238 if Nkind (Expr) = N_Function_Call then
3240 ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
3242 ("\function called must be a traversal function", Expr);
3245 ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
3247 ("\expression must be part of stand-alone object or " &
3255 end Check_Source_Of_Borrow_Or_Observe;
3257 ---------------------
3258 -- Check_Statement --
3259 ---------------------
3261 procedure Check_Statement (Stmt : Node_Id) is
3263 case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is
3265 -- An entry call is handled like other calls
3267 when N_Entry_Call_Statement =>
3268 Check_Call_Statement (Stmt);
3270 -- An assignment may correspond to a move, a borrow, or an observe
3272 when N_Assignment_Statement =>
3274 Target : constant Node_Id := Name (Stmt);
3277 -- Start with checking that the subexpressions of the target
3278 -- path are readable, before possibly updating the permission
3279 -- of these subexpressions in Check_Assignment.
3281 Check_Expression (Target, Read_Subexpr);
3283 Check_Assignment (Target => Target,
3284 Expr => Expression (Stmt));
3286 -- ??? We need a rule that forbids targets of assignment for
3287 -- which the path is not known, for example when there is a
3288 -- function call involved (which includes calls to traversal
3289 -- functions). Otherwise there is no way to update the
3290 -- corresponding path permission.
3292 if No (Get_Root_Object
3293 (Target, Through_Traversal => False))
3295 if Emit_Messages then
3296 Error_Msg_N ("illegal target for assignment", Target);
3301 Check_Expression (Target, Assign);
3304 when N_Block_Statement =>
3305 Check_List (Declarations (Stmt));
3306 Check_Node (Handled_Statement_Sequence (Stmt));
3308 -- Remove local borrowers and observers
3311 Decl : Node_Id := First (Declarations (Stmt));
3314 while Present (Decl) loop
3315 if Nkind (Decl) = N_Object_Declaration then
3316 Var := Defining_Identifier (Decl);
3317 Remove (Current_Borrowers, Var);
3318 Remove (Current_Observers, Var);
3325 when N_Case_Statement =>
3328 Saved_Env : Perm_Env;
3329 -- Copy of environment for analysis of the different cases
3331 -- Accumulator for the different cases
3334 Check_Expression (Expression (Stmt), Read);
3338 Copy_Env (Current_Perm_Env, Saved_Env);
3340 -- First alternative
3342 Alt := First (Alternatives (Stmt));
3343 Check_List (Statements (Alt));
3348 Move_Env (Current_Perm_Env, New_Env);
3350 -- Other alternatives
3352 while Present (Alt) loop
3354 -- Restore environment
3356 Copy_Env (Saved_Env, Current_Perm_Env);
3360 Check_List (Statements (Alt));
3363 -- Merge Current_Perm_Env into New_Env
3365 Merge_Env (Source => Current_Perm_Env, Target => New_Env);
3368 Move_Env (New_Env, Current_Perm_Env);
3369 Free_Env (Saved_Env);
3372 when N_Delay_Relative_Statement
3373 | N_Delay_Until_Statement
3375 Check_Expression (Expression (Stmt), Read);
3377 when N_Loop_Statement =>
3378 Check_Loop_Statement (Stmt);
3380 when N_Simple_Return_Statement =>
3382 Subp : constant Entity_Id :=
3383 Return_Applies_To (Return_Statement_Entity (Stmt));
3384 Expr : constant Node_Id := Expression (Stmt);
3386 if Present (Expression (Stmt)) then
3388 Return_Typ : constant Entity_Id :=
3389 Etype (Expression (Stmt));
3392 -- SPARK RM 3.10(5): A return statement that applies
3393 -- to a traversal function that has an anonymous
3394 -- access-to-constant (respectively, access-to-variable)
3395 -- result type, shall return either the literal null
3396 -- or an access object denoted by a direct or indirect
3397 -- observer (respectively, borrower) of the traversed
3400 if Is_Anonymous_Access_Type (Return_Typ) then
3401 pragma Assert (Is_Traversal_Function (Subp));
3403 if Nkind (Expr) /= N_Null then
3405 Expr_Root : constant Entity_Id :=
3406 Get_Root_Object (Expr, Is_Traversal => True);
3407 Param : constant Entity_Id :=
3408 First_Formal (Subp);
3410 if Param /= Expr_Root and then Emit_Messages then
3412 ("returned value must be rooted in "
3413 & "traversed parameter & "
3414 & "(SPARK RM 3.10(5))",
3420 -- Move expression to caller
3422 elsif Is_Deep (Return_Typ) then
3424 if Is_Path_Expression (Expr) then
3425 Check_Expression (Expr, Move);
3428 if Emit_Messages then
3430 ("expression not allowed as source of move",
3437 Check_Expression (Expr, Read);
3440 if Ekind_In (Subp, E_Procedure, E_Entry)
3441 and then not No_Return (Subp)
3443 Return_Parameters (Subp);
3444 Return_Globals (Subp);
3450 when N_Extended_Return_Statement =>
3452 Subp : constant Entity_Id :=
3453 Return_Applies_To (Return_Statement_Entity (Stmt));
3454 Decls : constant List_Id := Return_Object_Declarations (Stmt);
3455 Decl : constant Node_Id := Last_Non_Pragma (Decls);
3456 Obj : constant Entity_Id := Defining_Identifier (Decl);
3460 -- SPARK RM 3.10(5): return statement of traversal function
3462 if Is_Traversal_Function (Subp) and then Emit_Messages then
3464 ("extended return cannot apply to a traversal function",
3468 Check_List (Return_Object_Declarations (Stmt));
3469 Check_Node (Handled_Statement_Sequence (Stmt));
3471 if Is_Deep (Etype (Obj)) then
3472 Perm := Get_Perm (Obj);
3474 if Perm /= Read_Write then
3475 Perm_Error (Decl, Read_Write, Perm,
3476 Expl => Get_Expl (Obj));
3480 if Ekind_In (Subp, E_Procedure, E_Entry)
3481 and then not No_Return (Subp)
3483 Return_Parameters (Subp);
3484 Return_Globals (Subp);
3488 -- On loop exit, merge the current permission environment with the
3489 -- accumulator for the given loop.
3491 when N_Exit_Statement =>
3493 Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
3494 Saved_Accumulator : constant Perm_Env_Access :=
3495 Get (Current_Loops_Accumulators, Loop_Name);
3496 Environment_Copy : constant Perm_Env_Access :=
3499 Copy_Env (Current_Perm_Env, Environment_Copy.all);
3501 if Saved_Accumulator = null then
3502 Set (Current_Loops_Accumulators,
3503 Loop_Name, Environment_Copy);
3505 Merge_Env (Source => Environment_Copy.all,
3506 Target => Saved_Accumulator.all);
3507 -- ??? Either free Environment_Copy, or change the type
3508 -- of loop accumulators to directly store permission
3513 -- On branches, analyze each branch independently on a fresh copy of
3514 -- the permission environment, then merge the resulting permission
3517 when N_If_Statement =>
3519 Saved_Env : Perm_Env;
3521 -- Accumulator for the different branches
3524 Check_Expression (Condition (Stmt), Read);
3528 Copy_Env (Current_Perm_Env, Saved_Env);
3532 Check_List (Then_Statements (Stmt));
3533 Move_Env (Current_Perm_Env, New_Env);
3540 Branch := First (Elsif_Parts (Stmt));
3541 while Present (Branch) loop
3543 -- Restore current permission environment
3545 Copy_Env (Saved_Env, Current_Perm_Env);
3546 Check_Expression (Condition (Branch), Read);
3547 Check_List (Then_Statements (Branch));
3549 -- Merge current permission environment
3551 Merge_Env (Source => Current_Perm_Env, Target => New_Env);
3558 -- Restore current permission environment
3560 Copy_Env (Saved_Env, Current_Perm_Env);
3561 Check_List (Else_Statements (Stmt));
3563 -- Merge current permission environment
3565 Merge_Env (Source => Current_Perm_Env, Target => New_Env);
3569 Move_Env (New_Env, Current_Perm_Env);
3570 Free_Env (Saved_Env);
3573 -- We should ideally ignore the branch after raising an exception,
3574 -- so that it is not taken into account in merges. For now, just
3575 -- propagate the current environment.
3577 when N_Raise_Statement =>
3580 when N_Null_Statement =>
3583 -- Unsupported constructs in SPARK
3585 when N_Abort_Statement
3586 | N_Accept_Statement
3587 | N_Asynchronous_Select
3589 | N_Conditional_Entry_Call
3591 | N_Requeue_Statement
3592 | N_Selective_Accept
3593 | N_Timed_Entry_Call
3597 -- The following nodes are never generated in GNATprove mode
3599 when N_Compound_Statement
3602 raise Program_Error;
3604 end Check_Statement;
3606 -------------------------
3607 -- Check_Type_Legality --
3608 -------------------------
3610 procedure Check_Type_Legality
3613 Legal : in out Boolean)
3615 function Original_Emit_Messages return Boolean renames Emit_Messages;
3617 function Emit_Messages return Boolean;
3618 -- Local wrapper around generic formal parameter Emit_Messages, to
3619 -- check the value of parameter Force before calling the original
3620 -- Emit_Messages, and setting Legal to False.
3626 function Emit_Messages return Boolean is
3629 return Force and then Original_Emit_Messages;
3634 Check_Typ : constant Entity_Id := Retysp (Typ);
3636 -- Start of processing for Check_Type_Legality
3639 case Type_Kind'(Ekind (Check_Typ)) is
3641 case Access_Kind'(Ekind (Check_Typ)) is
3643 | E_Anonymous_Access_Type
3646 when E_Access_Subtype =>
3647 Check_Type_Legality (Base_Type (Check_Typ), Force, Legal);
3648 when E_Access_Attribute_Type =>
3649 if Emit_Messages then
3650 Error_Msg_N ("access attribute not allowed in SPARK",
3653 when E_Allocator_Type =>
3654 if Emit_Messages then
3655 Error_Msg_N ("missing type resolution", Check_Typ);
3657 when E_General_Access_Type =>
3658 if Emit_Messages then
3660 ("general access type & not allowed in SPARK",
3661 Check_Typ, Check_Typ);
3663 when Access_Subprogram_Kind =>
3664 if Emit_Messages then
3666 ("access to subprogram type & not allowed in SPARK",
3667 Check_Typ, Check_Typ);
3674 Check_Type_Legality (Component_Type (Check_Typ), Force, Legal);
3677 if Is_Deep (Check_Typ)
3678 and then (Is_Tagged_Type (Check_Typ)
3679 or else Is_Class_Wide_Type (Check_Typ))
3681 if Emit_Messages then
3683 ("tagged type & cannot be owning in SPARK",
3684 Check_Typ, Check_Typ);
3691 Comp := First_Component_Or_Discriminant (Check_Typ);
3692 while Present (Comp) loop
3694 -- Ignore components which are not visible in SPARK
3696 if Component_Is_Visible_In_SPARK (Comp) then
3697 Check_Type_Legality (Etype (Comp), Force, Legal);
3699 Next_Component_Or_Discriminant (Comp);
3705 | E_String_Literal_Subtype
3714 -- Do not check type whose full view is not SPARK
3718 | E_Limited_Private_Type
3719 | E_Limited_Private_Subtype
3723 end Check_Type_Legality;
3729 function Get_Expl (N : Node_Or_Entity_Id) return Node_Id is
3731 -- Special case for the object declared in an extended return statement
3733 if Nkind (N) = N_Defining_Identifier then
3735 C : constant Perm_Tree_Access :=
3736 Get (Current_Perm_Env, Unique_Entity (N));
3738 pragma Assert (C /= null);
3739 return Explanation (C);
3742 -- The expression is a call to a traversal function
3744 elsif Is_Traversal_Function_Call (N) then
3747 -- The expression is directly rooted in an object
3749 elsif Present (Get_Root_Object (N, Through_Traversal => False)) then
3751 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
3753 case Tree_Or_Perm.R is
3755 return Tree_Or_Perm.Explanation;
3758 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
3759 return Explanation (Tree_Or_Perm.Tree_Access);
3763 -- The expression is a function call, an allocation, or null
3770 -----------------------------------
3771 -- Get_Observed_Or_Borrowed_Expr --
3772 -----------------------------------
3774 function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id is
3776 if Is_Traversal_Function_Call (Expr) then
3777 return First_Actual (Expr);
3781 end Get_Observed_Or_Borrowed_Expr;
3787 function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind is
3789 -- Special case for the object declared in an extended return statement
3791 if Nkind (N) = N_Defining_Identifier then
3793 C : constant Perm_Tree_Access :=
3794 Get (Current_Perm_Env, Unique_Entity (N));
3796 pragma Assert (C /= null);
3797 return Permission (C);
3800 -- The expression is a call to a traversal function
3802 elsif Is_Traversal_Function_Call (N) then
3804 Callee : constant Entity_Id := Get_Called_Entity (N);
3806 if Is_Access_Constant (Etype (Callee)) then
3813 -- The expression is directly rooted in an object
3815 elsif Present (Get_Root_Object (N, Through_Traversal => False)) then
3817 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
3819 case Tree_Or_Perm.R is
3821 return Tree_Or_Perm.Found_Permission;
3824 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
3825 return Permission (Tree_Or_Perm.Tree_Access);
3829 -- The expression is a function call, an allocation, or null
3836 ----------------------
3837 -- Get_Perm_Or_Tree --
3838 ----------------------
3840 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
3844 when N_Expanded_Name
3848 C : constant Perm_Tree_Access :=
3849 Get (Current_Perm_Env, Unique_Entity (Entity (N)));
3851 -- Except during elaboration, the root object should have been
3852 -- declared and entered into the current permission
3855 if not Inside_Elaboration
3858 Illegal_Global_Usage (N, N);
3861 return (R => Unfolded, Tree_Access => C);
3864 -- For a nonterminal path, we get the permission tree of its
3865 -- prefix, and then get the subtree associated with the extension,
3866 -- if unfolded. If folded, we return the permission associated with
3869 when N_Explicit_Dereference
3870 | N_Indexed_Component
3871 | N_Selected_Component
3875 C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
3879 -- Some earlier prefix was already folded, return the
3880 -- permission found.
3886 case Kind (C.Tree_Access) is
3888 -- If the prefix tree is already folded, return the
3889 -- children permission.
3891 when Entire_Object =>
3892 return (R => Folded,
3894 Children_Permission (C.Tree_Access),
3896 Explanation (C.Tree_Access));
3899 pragma Assert (Nkind (N) = N_Explicit_Dereference);
3900 return (R => Unfolded,
3901 Tree_Access => Get_All (C.Tree_Access));
3903 when Record_Component =>
3904 pragma Assert (Nkind (N) = N_Selected_Component);
3906 Comp : constant Entity_Id :=
3907 Original_Record_Component
3908 (Entity (Selector_Name (N)));
3909 D : constant Perm_Tree_Access :=
3911 (Component (C.Tree_Access), Comp);
3913 pragma Assert (D /= null);
3914 return (R => Unfolded,
3918 when Array_Component =>
3919 pragma Assert (Nkind (N) = N_Indexed_Component
3921 Nkind (N) = N_Slice);
3922 pragma Assert (Get_Elem (C.Tree_Access) /= null);
3923 return (R => Unfolded,
3924 Tree_Access => Get_Elem (C.Tree_Access));
3929 when N_Qualified_Expression
3931 | N_Unchecked_Type_Conversion
3933 return Get_Perm_Or_Tree (Expression (N));
3936 raise Program_Error;
3938 end Get_Perm_Or_Tree;
3944 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is
3946 return Set_Perm_Prefixes (N, None, Empty);
3949 ---------------------
3950 -- Get_Root_Object --
3951 ---------------------
3953 function Get_Root_Object
3955 Through_Traversal : Boolean := True;
3956 Is_Traversal : Boolean := False) return Entity_Id
3958 function GRO (Expr : Node_Id) return Entity_Id;
3959 -- Local wrapper on the actual function, to propagate the values of
3960 -- optional parameters.
3966 function GRO (Expr : Node_Id) return Entity_Id is
3968 return Get_Root_Object (Expr, Through_Traversal, Is_Traversal);
3971 Get_Root_Object : Boolean;
3972 pragma Unmodified (Get_Root_Object);
3973 -- Local variable to mask the name of function Get_Root_Object, to
3974 -- prevent direct call. Instead GRO wrapper should be called.
3976 -- Start of processing for Get_Root_Object
3979 if not Is_Subpath_Expression (Expr, Is_Traversal) then
3980 if Emit_Messages then
3981 Error_Msg_N ("name expected here for path", Expr);
3986 case Nkind (Expr) is
3987 when N_Expanded_Name
3990 return Entity (Expr);
3992 when N_Explicit_Dereference
3993 | N_Indexed_Component
3994 | N_Selected_Component
3997 return GRO (Prefix (Expr));
3999 -- There is no root object for an (extension) aggregate, allocator,
4004 | N_Extension_Aggregate
4010 -- In the case of a call to a traversal function, the root object is
4011 -- the root of the traversed parameter. Otherwise there is no root
4014 when N_Function_Call =>
4015 if Through_Traversal
4016 and then Is_Traversal_Function_Call (Expr)
4018 return GRO (First_Actual (Expr));
4023 when N_Qualified_Expression
4025 | N_Unchecked_Type_Conversion
4027 return GRO (Expression (Expr));
4029 when N_Attribute_Reference =>
4031 (Get_Attribute_Id (Attribute_Name (Expr)) =
4032 Attribute_Loop_Entry
4034 Get_Attribute_Id (Attribute_Name (Expr)) =
4036 or else Get_Attribute_Id (Attribute_Name (Expr)) =
4040 when N_If_Expression =>
4041 if Is_Traversal then
4043 Cond : constant Node_Id := First (Expressions (Expr));
4044 Then_Part : constant Node_Id := Next (Cond);
4045 Else_Part : constant Node_Id := Next (Then_Part);
4046 Then_Root : constant Entity_Id := GRO (Then_Part);
4047 Else_Root : constant Entity_Id := GRO (Else_Part);
4049 if Nkind (Then_Part) = N_Null then
4051 elsif Nkind (Else_Part) = N_Null then
4053 elsif Then_Root = Else_Root then
4056 if Emit_Messages then
4058 ("same name expected here in each branch", Expr);
4064 if Emit_Messages then
4065 Error_Msg_N ("name expected here for path", Expr);
4070 when N_Case_Expression =>
4071 if Is_Traversal then
4073 Cases : constant List_Id := Alternatives (Expr);
4074 Cur_Case : Node_Id := First (Cases);
4075 Cur_Root : Entity_Id;
4076 Common_Root : Entity_Id := Empty;
4079 while Present (Cur_Case) loop
4080 Cur_Root := GRO (Expression (Cur_Case));
4082 if Common_Root = Empty then
4083 Common_Root := Cur_Root;
4084 elsif Common_Root /= Cur_Root then
4085 if Emit_Messages then
4087 ("same name expected here in each branch", Expr);
4097 if Emit_Messages then
4098 Error_Msg_N ("name expected here for path", Expr);
4104 raise Program_Error;
4106 end Get_Root_Object;
4112 function Glb (P1, P2 : Perm_Kind) return Perm_Kind
4146 -------------------------
4147 -- Has_Array_Component --
4148 -------------------------
4150 function Has_Array_Component (Expr : Node_Id) return Boolean is
4152 case Nkind (Expr) is
4153 when N_Expanded_Name
4158 when N_Explicit_Dereference
4159 | N_Selected_Component
4161 return Has_Array_Component (Prefix (Expr));
4163 when N_Indexed_Component
4174 when N_Qualified_Expression
4176 | N_Unchecked_Type_Conversion
4178 return Has_Array_Component (Expression (Expr));
4181 raise Program_Error;
4183 end Has_Array_Component;
4189 procedure Hp (P : Perm_Env) is
4190 Elem : Perm_Tree_Maps.Key_Option;
4193 Elem := Get_First_Key (P);
4194 while Elem.Present loop
4195 Print_Node_Briefly (Elem.K);
4196 Elem := Get_Next_Key (P);
4200 --------------------------
4201 -- Illegal_Global_Usage --
4202 --------------------------
4204 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id)
4207 Error_Msg_NE ("cannot use global variable & of deep type", N, E);
4208 Error_Msg_N ("\without prior declaration in a Global aspect", N);
4209 Errout.Finalize (Last_Call => True);
4210 Errout.Output_Messages;
4211 Exit_Program (E_Errors);
4212 end Illegal_Global_Usage;
4218 function Is_Deep (Typ : Entity_Id) return Boolean is
4220 case Type_Kind'(Ekind (Retysp (Typ))) is
4227 return Is_Deep (Component_Type (Retysp (Typ)));
4233 Comp := First_Component_Or_Discriminant (Retysp (Typ));
4234 while Present (Comp) loop
4236 -- Ignore components not visible in SPARK
4238 if Component_Is_Visible_In_SPARK (Comp)
4239 and then Is_Deep (Etype (Comp))
4243 Next_Component_Or_Discriminant (Comp);
4249 | E_String_Literal_Subtype
4258 -- Ignore full view of types if it is not in SPARK
4262 | E_Limited_Private_Type
4263 | E_Limited_Private_Subtype
4273 function Is_Legal (N : Node_Id) return Boolean is
4274 Legal : Boolean := True;
4278 when N_Declaration =>
4279 Check_Declaration_Legality (N, Force => False, Legal => Legal);
4287 ----------------------
4288 -- Is_Local_Context --
4289 ----------------------
4291 function Is_Local_Context (Scop : Entity_Id) return Boolean is
4293 return Is_Subprogram_Or_Entry (Scop)
4294 or else Ekind (Scop) = E_Block;
4295 end Is_Local_Context;
4297 ------------------------
4298 -- Is_Path_Expression --
4299 ------------------------
4301 function Is_Path_Expression
4303 Is_Traversal : Boolean := False) return Boolean
4305 function IPE (Expr : Node_Id) return Boolean;
4306 -- Local wrapper on the actual function, to propagate the values of
4307 -- optional parameter Is_Traversal.
4313 function IPE (Expr : Node_Id) return Boolean is
4315 return Is_Path_Expression (Expr, Is_Traversal);
4318 Is_Path_Expression : Boolean;
4319 pragma Unmodified (Is_Path_Expression);
4320 -- Local variable to mask the name of function Is_Path_Expression, to
4321 -- prevent direct call. Instead IPE wrapper should be called.
4323 -- Start of processing for Is_Path_Expression
4326 case Nkind (Expr) is
4327 when N_Expanded_Name
4328 | N_Explicit_Dereference
4330 | N_Indexed_Component
4331 | N_Selected_Component
4336 -- Special value NULL corresponds to an empty path
4341 -- Object returned by an (extension) aggregate, an allocator, or
4342 -- a function call corresponds to a path.
4346 | N_Extension_Aggregate
4351 when N_Qualified_Expression
4353 | N_Unchecked_Type_Conversion
4355 return IPE (Expression (Expr));
4357 -- When returning from a traversal function, consider an
4358 -- if-expression as a possible path expression.
4360 when N_If_Expression =>
4361 if Is_Traversal then
4363 Cond : constant Node_Id := First (Expressions (Expr));
4364 Then_Part : constant Node_Id := Next (Cond);
4365 Else_Part : constant Node_Id := Next (Then_Part);
4367 return IPE (Then_Part)
4368 and then IPE (Else_Part);
4374 -- When returning from a traversal function, consider
4375 -- a case-expression as a possible path expression.
4377 when N_Case_Expression =>
4378 if Is_Traversal then
4380 Cases : constant List_Id := Alternatives (Expr);
4381 Cur_Case : Node_Id := First (Cases);
4384 while Present (Cur_Case) loop
4385 if not IPE (Expression (Cur_Case)) then
4400 end Is_Path_Expression;
4402 -------------------------
4403 -- Is_Prefix_Or_Almost --
4404 -------------------------
4406 function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean is
4408 type Expr_Array is array (Positive range <>) of Node_Id;
4409 -- Sequence of expressions that make up a path
4411 function Get_Expr_Array (Expr : Node_Id) return Expr_Array;
4412 pragma Precondition (Is_Path_Expression (Expr));
4413 -- Return the sequence of expressions that make up a path
4415 --------------------
4416 -- Get_Expr_Array --
4417 --------------------
4419 function Get_Expr_Array (Expr : Node_Id) return Expr_Array is
4421 case Nkind (Expr) is
4422 when N_Expanded_Name
4425 return Expr_Array'(1 => Expr);
4427 when N_Explicit_Dereference
4428 | N_Indexed_Component
4429 | N_Selected_Component
4432 return Get_Expr_Array (Prefix (Expr)) & Expr;
4434 when N_Qualified_Expression
4436 | N_Unchecked_Type_Conversion
4438 return Get_Expr_Array (Expression (Expr));
4441 raise Program_Error;
4447 Prefix_Path : constant Expr_Array := Get_Expr_Array (Pref);
4448 Expr_Path : constant Expr_Array := Get_Expr_Array (Expr);
4450 Prefix_Root : constant Node_Id := Prefix_Path (1);
4451 Expr_Root : constant Node_Id := Expr_Path (1);
4453 Common_Len : constant Positive :=
4454 Positive'Min (Prefix_Path'Length, Expr_Path'Length);
4456 -- Start of processing for Is_Prefix_Or_Almost
4459 if Entity (Prefix_Root) /= Entity (Expr_Root) then
4463 for J in 2 .. Common_Len loop
4465 Prefix_Elt : constant Node_Id := Prefix_Path (J);
4466 Expr_Elt : constant Node_Id := Expr_Path (J);
4468 case Nkind (Prefix_Elt) is
4469 when N_Explicit_Dereference =>
4470 if Nkind (Expr_Elt) /= N_Explicit_Dereference then
4474 when N_Selected_Component =>
4475 if Nkind (Expr_Elt) /= N_Selected_Component
4476 or else Original_Record_Component
4477 (Entity (Selector_Name (Prefix_Elt)))
4478 /= Original_Record_Component
4479 (Entity (Selector_Name (Expr_Elt)))
4484 when N_Indexed_Component
4487 if not Nkind_In (Expr_Elt, N_Indexed_Component, N_Slice) then
4492 raise Program_Error;
4497 -- If the expression path is longer than the prefix one, then at this
4498 -- point the prefix property holds.
4500 if Expr_Path'Length > Prefix_Path'Length then
4503 -- Otherwise check if none of the remaining path elements in the
4504 -- candidate prefix involve a dereference.
4507 for J in Common_Len + 1 .. Prefix_Path'Length loop
4508 if Nkind (Prefix_Path (J)) = N_Explicit_Dereference then
4515 end Is_Prefix_Or_Almost;
4517 ---------------------------
4518 -- Is_Subpath_Expression --
4519 ---------------------------
4521 function Is_Subpath_Expression
4523 Is_Traversal : Boolean := False) return Boolean
4526 return Is_Path_Expression (Expr, Is_Traversal)
4528 or else (Nkind_In (Expr, N_Qualified_Expression,
4530 N_Unchecked_Type_Conversion)
4531 and then Is_Subpath_Expression (Expression (Expr)))
4533 or else (Nkind (Expr) = N_Attribute_Reference
4535 (Get_Attribute_Id (Attribute_Name (Expr)) =
4538 Get_Attribute_Id (Attribute_Name (Expr)) =
4539 Attribute_Loop_Entry
4541 Get_Attribute_Id (Attribute_Name (Expr)) =
4544 or else Nkind (Expr) = N_Op_Concat;
4545 end Is_Subpath_Expression;
4547 ---------------------------
4548 -- Is_Traversal_Function --
4549 ---------------------------
4551 function Is_Traversal_Function (E : Entity_Id) return Boolean is
4553 return Ekind (E) = E_Function
4555 -- A function is said to be a traversal function if the result type of
4556 -- the function is an anonymous access-to-object type,
4558 and then Is_Anonymous_Access_Type (Etype (E))
4560 -- the function has at least one formal parameter,
4562 and then Present (First_Formal (E))
4564 -- and the function's first parameter is of an access type.
4566 and then Is_Access_Type (Retysp (Etype (First_Formal (E))));
4567 end Is_Traversal_Function;
4569 --------------------------------
4570 -- Is_Traversal_Function_Call --
4571 --------------------------------
4573 function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean is
4575 return Nkind (Expr) = N_Function_Call
4576 and then Present (Get_Called_Entity (Expr))
4577 and then Is_Traversal_Function (Get_Called_Entity (Expr));
4578 end Is_Traversal_Function_Call;
4584 function Loop_Of_Exit (N : Node_Id) return Entity_Id is
4585 Nam : Node_Id := Name (N);
4586 Stmt : Node_Id := N;
4589 while Present (Stmt) loop
4590 Stmt := Parent (Stmt);
4591 if Nkind (Stmt) = N_Loop_Statement then
4592 Nam := Identifier (Stmt);
4597 return Entity (Nam);
4604 function Lub (P1, P2 : Perm_Kind) return Perm_Kind is
4641 procedure Merge_Env (Source : in out Perm_Env; Target : in out Perm_Env) is
4643 -- Local subprograms
4645 procedure Apply_Glb_Tree
4646 (A : Perm_Tree_Access;
4649 procedure Merge_Trees
4650 (Target : Perm_Tree_Access;
4651 Source : Perm_Tree_Access);
4653 --------------------
4654 -- Apply_Glb_Tree --
4655 --------------------
4657 procedure Apply_Glb_Tree
4658 (A : Perm_Tree_Access;
4662 A.all.Tree.Permission := Glb (Permission (A), P);
4665 when Entire_Object =>
4666 A.all.Tree.Children_Permission :=
4667 Glb (Children_Permission (A), P);
4670 Apply_Glb_Tree (Get_All (A), P);
4672 when Array_Component =>
4673 Apply_Glb_Tree (Get_Elem (A), P);
4675 when Record_Component =>
4677 Comp : Perm_Tree_Access;
4679 Comp := Perm_Tree_Maps.Get_First (Component (A));
4680 while Comp /= null loop
4681 Apply_Glb_Tree (Comp, P);
4682 Comp := Perm_Tree_Maps.Get_Next (Component (A));
4692 procedure Merge_Trees
4693 (Target : Perm_Tree_Access;
4694 Source : Perm_Tree_Access)
4696 Perm : constant Perm_Kind :=
4697 Glb (Permission (Target), Permission (Source));
4700 pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
4701 Target.all.Tree.Permission := Perm;
4703 case Kind (Target) is
4704 when Entire_Object =>
4706 Child_Perm : constant Perm_Kind :=
4707 Children_Permission (Target);
4710 case Kind (Source) is
4711 when Entire_Object =>
4712 Target.all.Tree.Children_Permission :=
4713 Glb (Child_Perm, Children_Permission (Source));
4716 Copy_Tree (Source, Target);
4717 Target.all.Tree.Permission := Perm;
4718 Apply_Glb_Tree (Get_All (Target), Child_Perm);
4720 when Array_Component =>
4721 Copy_Tree (Source, Target);
4722 Target.all.Tree.Permission := Perm;
4723 Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
4725 when Record_Component =>
4726 Copy_Tree (Source, Target);
4727 Target.all.Tree.Permission := Perm;
4729 Comp : Perm_Tree_Access;
4733 Perm_Tree_Maps.Get_First (Component (Target));
4734 while Comp /= null loop
4735 -- Apply glb tree on every component subtree
4737 Apply_Glb_Tree (Comp, Child_Perm);
4738 Comp := Perm_Tree_Maps.Get_Next
4739 (Component (Target));
4746 case Kind (Source) is
4747 when Entire_Object =>
4748 Apply_Glb_Tree (Get_All (Target),
4749 Children_Permission (Source));
4752 Merge_Trees (Get_All (Target), Get_All (Source));
4755 raise Program_Error;
4759 when Array_Component =>
4760 case Kind (Source) is
4761 when Entire_Object =>
4762 Apply_Glb_Tree (Get_Elem (Target),
4763 Children_Permission (Source));
4765 when Array_Component =>
4766 Merge_Trees (Get_Elem (Target), Get_Elem (Source));
4769 raise Program_Error;
4773 when Record_Component =>
4774 case Kind (Source) is
4775 when Entire_Object =>
4777 Child_Perm : constant Perm_Kind :=
4778 Children_Permission (Source);
4780 Comp : Perm_Tree_Access;
4783 Comp := Perm_Tree_Maps.Get_First
4784 (Component (Target));
4785 while Comp /= null loop
4786 -- Apply glb tree on every component subtree
4788 Apply_Glb_Tree (Comp, Child_Perm);
4790 Perm_Tree_Maps.Get_Next (Component (Target));
4794 when Record_Component =>
4796 Key_Source : Perm_Tree_Maps.Key_Option;
4797 CompTarget : Perm_Tree_Access;
4798 CompSource : Perm_Tree_Access;
4801 Key_Source := Perm_Tree_Maps.Get_First_Key
4802 (Component (Source));
4804 while Key_Source.Present loop
4805 CompSource := Perm_Tree_Maps.Get
4806 (Component (Source), Key_Source.K);
4807 CompTarget := Perm_Tree_Maps.Get
4808 (Component (Target), Key_Source.K);
4810 pragma Assert (CompSource /= null);
4811 Merge_Trees (CompTarget, CompSource);
4813 Key_Source := Perm_Tree_Maps.Get_Next_Key
4814 (Component (Source));
4819 raise Program_Error;
4826 CompTarget : Perm_Tree_Access;
4827 CompSource : Perm_Tree_Access;
4828 KeyTarget : Perm_Tree_Maps.Key_Option;
4830 -- Start of processing for Merge_Env
4833 KeyTarget := Get_First_Key (Target);
4834 -- Iterate over every tree of the environment in the target, and merge
4835 -- it with the source if there is such a similar one that exists. If
4836 -- there is none, then skip.
4837 while KeyTarget.Present loop
4839 CompSource := Get (Source, KeyTarget.K);
4840 CompTarget := Get (Target, KeyTarget.K);
4842 pragma Assert (CompTarget /= null);
4844 if CompSource /= null then
4845 Merge_Trees (CompTarget, CompSource);
4846 Remove (Source, KeyTarget.K);
4849 KeyTarget := Get_Next_Key (Target);
4852 -- Iterate over every tree of the environment of the source. And merge
4853 -- again. If there is not any tree of the target then just copy the tree
4854 -- from source to target.
4856 KeySource : Perm_Tree_Maps.Key_Option;
4858 KeySource := Get_First_Key (Source);
4859 while KeySource.Present loop
4861 CompSource := Get (Source, KeySource.K);
4862 CompTarget := Get (Target, KeySource.K);
4864 if CompTarget = null then
4865 CompTarget := new Perm_Tree_Wrapper'(CompSource.all);
4866 Copy_Tree (CompSource, CompTarget);
4867 Set (Target, KeySource.K, CompTarget);
4869 Merge_Trees (CompTarget, CompSource);
4872 KeySource := Get_Next_Key (Source);
4883 procedure Perm_Error
4886 Found_Perm : Perm_Kind;
4888 Forbidden_Perm : Boolean := False)
4890 procedure Set_Root_Object
4892 Obj : out Entity_Id;
4893 Deref : out Boolean);
4894 -- Set the root object Obj, and whether the path contains a dereference,
4895 -- from a path Path.
4897 ---------------------
4898 -- Set_Root_Object --
4899 ---------------------
4901 procedure Set_Root_Object
4903 Obj : out Entity_Id;
4904 Deref : out Boolean)
4907 case Nkind (Path) is
4911 Obj := Entity (Path);
4914 when N_Type_Conversion
4915 | N_Unchecked_Type_Conversion
4916 | N_Qualified_Expression
4918 Set_Root_Object (Expression (Path), Obj, Deref);
4920 when N_Indexed_Component
4921 | N_Selected_Component
4924 Set_Root_Object (Prefix (Path), Obj, Deref);
4926 when N_Explicit_Dereference =>
4927 Set_Root_Object (Prefix (Path), Obj, Deref);
4931 raise Program_Error;
4933 end Set_Root_Object;
4939 -- Start of processing for Perm_Error
4942 Set_Root_Object (N, Root, Is_Deref);
4944 if Emit_Messages then
4947 ("insufficient permission on dereference from &", N, Root);
4949 Error_Msg_NE ("insufficient permission for &", N, Root);
4952 Perm_Mismatch (N, Perm, Found_Perm, Expl, Forbidden_Perm);
4956 -------------------------------
4957 -- Perm_Error_Subprogram_End --
4958 -------------------------------
4960 procedure Perm_Error_Subprogram_End
4964 Found_Perm : Perm_Kind;
4968 if Emit_Messages then
4969 Error_Msg_Node_2 := Subp;
4970 Error_Msg_NE ("insufficient permission for & when returning from &",
4972 Perm_Mismatch (Subp, Perm, Found_Perm, Expl);
4974 end Perm_Error_Subprogram_End;
4980 procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode) is
4982 procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id);
4983 -- Check expression Expr originating in Root was not borrowed
4985 procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id);
4986 -- Check expression Expr originating in Root was not observed
4988 ------------------------
4989 -- Check_Not_Borrowed --
4990 ------------------------
4992 procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id) is
4994 -- An expression without root object cannot be borrowed
5000 -- Otherwise, try to match the expression with one of the borrowed
5004 Key : Variable_Maps.Key_Option :=
5005 Get_First_Key (Current_Borrowers);
5008 B_Pledge : Entity_Id := Empty;
5011 -- Search for a call to a pledge function or a global pragma in
5012 -- the parents of Expr.
5015 Call : Node_Id := Expr;
5017 while Present (Call)
5019 (Nkind (Call) /= N_Function_Call
5020 or else not Is_Pledge_Function (Get_Called_Entity (Call)))
5022 -- Do not check for borrowed objects in global contracts
5023 -- ??? However we should keep these objects in the borrowed
5024 -- state when verifying the subprogram so that we can make
5025 -- sure that they are only read inside pledges.
5026 -- ??? There is probably a better way to disable checking of
5027 -- borrows inside global contracts.
5029 if Nkind (Call) = N_Pragma
5030 and then Get_Pragma_Id (Pragma_Name (Call)) = Pragma_Global
5035 Call := Parent (Call);
5039 and then Nkind (First_Actual (Call)) in N_Has_Entity
5041 B_Pledge := Entity (First_Actual (Call));
5045 while Key.Present loop
5047 Borrowed := Get (Current_Borrowers, Var);
5049 if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr)
5050 and then Var /= B_Pledge
5051 and then Emit_Messages
5053 Error_Msg_Sloc := Sloc (Borrowed);
5054 Error_Msg_N ("object was borrowed #", Expr);
5057 Key := Get_Next_Key (Current_Borrowers);
5060 end Check_Not_Borrowed;
5062 ------------------------
5063 -- Check_Not_Observed --
5064 ------------------------
5066 procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id) is
5068 -- An expression without root object cannot be observed
5074 -- Otherwise, try to match the expression with one of the observed
5078 Key : Variable_Maps.Key_Option :=
5079 Get_First_Key (Current_Observers);
5084 while Key.Present loop
5086 Observed := Get (Current_Observers, Var);
5088 if Is_Prefix_Or_Almost (Pref => Observed, Expr => Expr)
5089 and then Emit_Messages
5091 Error_Msg_Sloc := Sloc (Observed);
5092 Error_Msg_N ("object was observed #", Expr);
5095 Key := Get_Next_Key (Current_Observers);
5098 end Check_Not_Observed;
5102 Expr_Type : constant Entity_Id := Etype (Expr);
5103 Root : Entity_Id := Get_Root_Object (Expr);
5104 Perm : Perm_Kind_Option;
5106 -- Start of processing for Process_Path
5109 -- Nothing to do if the root type is not deep, or the path is not rooted
5112 if not Present (Root)
5113 or else not Is_Deep (Etype (Root))
5118 -- Identify the root type for the path
5120 Root := Unique_Entity (Root);
5122 -- Except during elaboration, the root object should have been declared
5123 -- and entered into the current permission environment.
5125 if not Inside_Elaboration
5126 and then Get (Current_Perm_Env, Root) = null
5128 Illegal_Global_Usage (Expr, Root);
5131 -- During elaboration, only the validity of operations is checked, no
5132 -- need to compute the permission of Expr.
5134 if Inside_Elaboration then
5137 Perm := Get_Perm (Expr);
5140 -- Check permissions
5146 -- No checking needed during elaboration
5148 if Inside_Elaboration then
5152 -- Check path is readable
5154 if Perm not in Read_Perm then
5155 Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
5161 -- Forbidden on deep path during elaboration, otherwise no
5164 if Inside_Elaboration then
5165 if Is_Deep (Expr_Type)
5166 and then not Inside_Procedure_Call
5167 and then Present (Get_Root_Object (Expr))
5168 and then Emit_Messages
5170 Error_Msg_N ("illegal move during elaboration", Expr);
5176 -- For deep path, check RW permission, otherwise R permission
5178 if not Is_Deep (Expr_Type) then
5179 if Perm not in Read_Perm then
5180 Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
5185 -- SPARK RM 3.10(1): At the point of a move operation the state of
5186 -- the source object (if any) shall be Unrestricted.
5188 if Perm /= Read_Write then
5189 Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
5195 -- No checking needed during elaboration
5197 if Inside_Elaboration then
5201 -- For assignment, check W permission
5203 if Perm not in Write_Perm then
5204 Perm_Error (Expr, Write_Only, Perm, Expl => Get_Expl (Expr));
5210 -- Forbidden during elaboration, an error is already issued in
5211 -- Check_Declaration, just return.
5213 if Inside_Elaboration then
5217 -- For borrowing, check RW permission
5219 if Perm /= Read_Write then
5220 Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
5226 -- Forbidden during elaboration, an error is already issued in
5227 -- Check_Declaration, just return.
5229 if Inside_Elaboration then
5233 -- For borrowing, check R permission
5235 if Perm not in Read_Perm then
5236 Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
5241 -- Check path was not borrowed
5243 Check_Not_Borrowed (Expr, Root);
5245 -- For modes that require W permission, check path was not observed
5248 when Read | Observe =>
5250 when Assign | Move | Borrow =>
5251 Check_Not_Observed (Expr, Root);
5254 -- Do not update permission environment when handling calls
5256 if Inside_Procedure_Call then
5260 -- Update the permissions
5269 -- SPARK RM 3.10(1): After a move operation, the state of the
5270 -- source object (if any) becomes Moved.
5272 if Present (Get_Root_Object (Expr)) then
5274 Tree : constant Perm_Tree_Access :=
5275 Set_Perm_Prefixes (Expr, Write_Only, Expl => Expr);
5277 pragma Assert (Tree /= null);
5278 Set_Perm_Extensions_Move (Tree, Etype (Expr), Expl => Expr);
5284 -- If there is no root object, or the tree has an array component,
5285 -- then the permissions do not get modified by the assignment.
5287 if No (Get_Root_Object (Expr))
5288 or else Has_Array_Component (Expr)
5293 -- Set permission RW for the path and its extensions
5296 Tree : constant Perm_Tree_Access := Get_Perm_Tree (Expr);
5298 Tree.all.Tree.Permission := Read_Write;
5299 Set_Perm_Extensions (Tree, Read_Write, Expl => Expr);
5301 -- Normalize the permission tree
5303 Set_Perm_Prefixes_Assign (Expr);
5306 -- Borrowing and observing of paths is handled by the variables
5307 -- Current_Borrowers and Current_Observers.
5309 when Borrow | Observe =>
5314 --------------------
5315 -- Return_Globals --
5316 --------------------
5318 procedure Return_Globals (Subp : Entity_Id) is
5320 procedure Return_Global
5325 Global_Var : Boolean);
5326 -- Proxy procedure to return globals, to adjust for the type of first
5327 -- parameter expected by Return_Parameter_Or_Global.
5333 procedure Return_Global
5338 Global_Var : Boolean)
5341 Return_Parameter_Or_Global
5342 (Id => Entity (Expr),
5346 Global_Var => Global_Var);
5349 procedure Return_Globals_Inst is new Handle_Globals (Return_Global);
5351 -- Start of processing for Return_Globals
5354 Return_Globals_Inst (Subp);
5357 --------------------------------
5358 -- Return_Parameter_Or_Global --
5359 --------------------------------
5361 procedure Return_Parameter_Or_Global
5366 Global_Var : Boolean)
5369 -- Shallow parameters and globals need not be considered
5371 if not Is_Deep (Typ) then
5374 elsif Kind = E_In_Parameter then
5376 -- Input global variables are observed only
5381 -- Anonymous access to constant is an observe
5383 elsif Is_Anonymous_Access_Type (Typ)
5384 and then Is_Access_Constant (Typ)
5388 -- Deep types other than access types define an observe
5390 elsif not Is_Access_Type (Typ) then
5395 -- All other parameters and globals should return with mode RW to the
5399 Tree : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
5401 if Permission (Tree) /= Read_Write then
5402 Perm_Error_Subprogram_End
5406 Found_Perm => Permission (Tree),
5407 Expl => Explanation (Tree));
5410 end Return_Parameter_Or_Global;
5412 -----------------------
5413 -- Return_Parameters --
5414 -----------------------
5416 procedure Return_Parameters (Subp : Entity_Id) is
5419 Formal := First_Formal (Subp);
5420 while Present (Formal) loop
5421 Return_Parameter_Or_Global
5423 Typ => Retysp (Etype (Formal)),
5424 Kind => Ekind (Formal),
5426 Global_Var => False);
5427 Next_Formal (Formal);
5429 end Return_Parameters;
5431 -------------------------
5432 -- Set_Perm_Extensions --
5433 -------------------------
5435 procedure Set_Perm_Extensions
5436 (T : Perm_Tree_Access;
5440 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access);
5441 -- Free the permission tree of children if any, prio to replacing T
5443 -----------------------------
5444 -- Free_Perm_Tree_Children --
5445 -----------------------------
5447 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is
5450 when Entire_Object =>
5454 Free_Tree (T.all.Tree.Get_All);
5456 when Array_Component =>
5457 Free_Tree (T.all.Tree.Get_Elem);
5459 when Record_Component =>
5461 Hashtbl : Perm_Tree_Maps.Instance := Component (T);
5462 Comp : Perm_Tree_Access;
5465 Comp := Perm_Tree_Maps.Get_First (Hashtbl);
5466 while Comp /= null loop
5468 Comp := Perm_Tree_Maps.Get_Next (Hashtbl);
5471 Perm_Tree_Maps.Reset (Hashtbl);
5474 end Free_Perm_Tree_Children;
5476 -- Start of processing for Set_Perm_Extensions
5479 Free_Perm_Tree_Children (T);
5480 T.all.Tree := Perm_Tree'(Kind => Entire_Object,
5481 Is_Node_Deep => Is_Node_Deep (T),
5482 Explanation => Expl,
5483 Permission => Permission (T),
5484 Children_Permission => P);
5485 end Set_Perm_Extensions;
5487 ------------------------------
5488 -- Set_Perm_Extensions_Move --
5489 ------------------------------
5491 procedure Set_Perm_Extensions_Move
5492 (T : Perm_Tree_Access;
5496 Check_Ty : constant Entity_Id := Retysp (E);
5498 -- Shallow extensions are set to RW
5500 if not Is_Node_Deep (T) then
5501 Set_Perm_Extensions (T, Read_Write, Expl => Expl);
5505 -- Deep extensions are set to W before .all and NO afterwards
5507 T.all.Tree.Permission := Write_Only;
5509 case T.all.Tree.Kind is
5511 -- For a folded tree of composite type, unfold the tree for better
5514 when Entire_Object =>
5515 case Ekind (Check_Ty) is
5520 C : constant Perm_Tree_Access :=
5521 new Perm_Tree_Wrapper'
5523 (Kind => Entire_Object,
5524 Is_Node_Deep => Is_Node_Deep (T),
5525 Explanation => Expl,
5526 Permission => Read_Write,
5527 Children_Permission => Read_Write));
5529 Set_Perm_Extensions_Move
5530 (C, Component_Type (Check_Ty), Expl);
5531 T.all.Tree := (Kind => Array_Component,
5532 Is_Node_Deep => Is_Node_Deep (T),
5533 Explanation => Expl,
5534 Permission => Write_Only,
5540 C : Perm_Tree_Access;
5542 Hashtbl : Perm_Tree_Maps.Instance;
5545 Comp := First_Component_Or_Discriminant (Check_Ty);
5546 while Present (Comp) loop
5548 -- Unfold components which are visible in SPARK
5550 if Component_Is_Visible_In_SPARK (Comp) then
5551 C := new Perm_Tree_Wrapper'
5553 (Kind => Entire_Object,
5554 Is_Node_Deep => Is_Deep (Etype (Comp)),
5555 Explanation => Expl,
5556 Permission => Read_Write,
5557 Children_Permission => Read_Write));
5558 Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
5560 -- Hidden components are never deep
5563 C := new Perm_Tree_Wrapper'
5565 (Kind => Entire_Object,
5566 Is_Node_Deep => False,
5567 Explanation => Expl,
5568 Permission => Read_Write,
5569 Children_Permission => Read_Write));
5570 Set_Perm_Extensions (C, Read_Write, Expl => Expl);
5574 (Hashtbl, Original_Record_Component (Comp), C);
5575 Next_Component_Or_Discriminant (Comp);
5579 (Kind => Record_Component,
5580 Is_Node_Deep => Is_Node_Deep (T),
5581 Explanation => Expl,
5582 Permission => Write_Only,
5583 Component => Hashtbl);
5586 -- Otherwise, extensions are set to NO
5589 Set_Perm_Extensions (T, No_Access, Expl);
5593 Set_Perm_Extensions (T, No_Access, Expl);
5595 when Array_Component =>
5596 Set_Perm_Extensions_Move
5597 (Get_Elem (T), Component_Type (Check_Ty), Expl);
5599 when Record_Component =>
5601 C : Perm_Tree_Access;
5605 Comp := First_Component_Or_Discriminant (Check_Ty);
5606 while Present (Comp) loop
5607 C := Perm_Tree_Maps.Get
5608 (Component (T), Original_Record_Component (Comp));
5609 pragma Assert (C /= null);
5611 -- Move visible components
5613 if Component_Is_Visible_In_SPARK (Comp) then
5614 Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
5616 -- Hidden components are never deep
5619 Set_Perm_Extensions (C, Read_Write, Expl => Expl);
5622 Next_Component_Or_Discriminant (Comp);
5626 end Set_Perm_Extensions_Move;
5628 -----------------------
5629 -- Set_Perm_Prefixes --
5630 -----------------------
5632 function Set_Perm_Prefixes
5634 Perm : Perm_Kind_Option;
5635 Expl : Node_Id) return Perm_Tree_Access
5639 when N_Expanded_Name
5643 E : constant Entity_Id := Unique_Entity (Entity (N));
5644 C : constant Perm_Tree_Access := Get (Current_Perm_Env, E);
5645 pragma Assert (C /= null);
5648 if Perm /= None then
5649 C.all.Tree.Permission := Glb (Perm, Permission (C));
5655 -- For a nonterminal path, we set the permission tree of its prefix,
5656 -- and then we extract from the returned pointer the subtree and
5657 -- assign an adequate permission to it, if unfolded. If folded,
5658 -- we unroll the tree one level.
5660 when N_Explicit_Dereference =>
5662 C : constant Perm_Tree_Access :=
5663 Set_Perm_Prefixes (Prefix (N), Perm, Expl);
5664 pragma Assert (C /= null);
5665 pragma Assert (Kind (C) = Entire_Object
5666 or else Kind (C) = Reference);
5668 -- The tree is already unfolded. Replace the permission of the
5671 if Kind (C) = Reference then
5673 D : constant Perm_Tree_Access := Get_All (C);
5674 pragma Assert (D /= null);
5677 if Perm /= None then
5678 D.all.Tree.Permission := Glb (Perm, Permission (D));
5684 -- The tree is folded. Expand it.
5688 pragma Assert (Kind (C) = Entire_Object);
5690 Child_P : constant Perm_Kind := Children_Permission (C);
5691 D : constant Perm_Tree_Access :=
5692 new Perm_Tree_Wrapper'
5694 (Kind => Entire_Object,
5695 Is_Node_Deep => Is_Deep (Etype (N)),
5696 Explanation => Expl,
5697 Permission => Child_P,
5698 Children_Permission => Child_P));
5700 if Perm /= None then
5701 D.all.Tree.Permission := Perm;
5704 C.all.Tree := (Kind => Reference,
5705 Is_Node_Deep => Is_Node_Deep (C),
5706 Explanation => Expl,
5707 Permission => Permission (C),
5714 when N_Selected_Component =>
5716 C : constant Perm_Tree_Access :=
5717 Set_Perm_Prefixes (Prefix (N), Perm, Expl);
5718 pragma Assert (C /= null);
5719 pragma Assert (Kind (C) = Entire_Object
5720 or else Kind (C) = Record_Component);
5722 -- The tree is already unfolded. Replace the permission of the
5725 if Kind (C) = Record_Component then
5727 Comp : constant Entity_Id :=
5728 Original_Record_Component
5729 (Entity (Selector_Name (N)));
5730 D : constant Perm_Tree_Access :=
5731 Perm_Tree_Maps.Get (Component (C), Comp);
5732 pragma Assert (D /= null);
5735 if Perm /= None then
5736 D.all.Tree.Permission := Glb (Perm, Permission (D));
5742 -- The tree is folded. Expand it.
5746 pragma Assert (Kind (C) = Entire_Object);
5748 D : Perm_Tree_Access;
5749 D_This : Perm_Tree_Access;
5752 Child_P : constant Perm_Kind := Children_Permission (C);
5753 Hashtbl : Perm_Tree_Maps.Instance;
5754 -- Create an empty hash table
5758 First_Component_Or_Discriminant
5759 (Retysp (Etype (Prefix (N))));
5761 while Present (Comp) loop
5763 and then Original_Record_Component (Comp) =
5764 Original_Record_Component
5765 (Entity (Selector_Name (N)))
5772 D := new Perm_Tree_Wrapper'
5774 (Kind => Entire_Object,
5776 -- Hidden components are never deep
5777 Component_Is_Visible_In_SPARK (Comp)
5778 and then Is_Deep (Etype (Comp)),
5779 Explanation => Expl,
5781 Children_Permission => Child_P));
5783 (Hashtbl, Original_Record_Component (Comp), D);
5785 -- Store the tree to return for this component
5787 if Original_Record_Component (Comp) =
5788 Original_Record_Component
5789 (Entity (Selector_Name (N)))
5794 Next_Component_Or_Discriminant (Comp);
5797 C.all.Tree := (Kind => Record_Component,
5798 Is_Node_Deep => Is_Node_Deep (C),
5799 Explanation => Expl,
5800 Permission => Permission (C),
5801 Component => Hashtbl);
5807 when N_Indexed_Component
5811 C : constant Perm_Tree_Access :=
5812 Set_Perm_Prefixes (Prefix (N), Perm, Expl);
5813 pragma Assert (C /= null);
5814 pragma Assert (Kind (C) = Entire_Object
5815 or else Kind (C) = Array_Component);
5817 -- The tree is already unfolded. Replace the permission of the
5820 if Kind (C) = Array_Component then
5822 D : constant Perm_Tree_Access := Get_Elem (C);
5823 pragma Assert (D /= null);
5826 if Perm /= None then
5827 D.all.Tree.Permission := Glb (Perm, Permission (D));
5833 -- The tree is folded. Expand it.
5837 pragma Assert (Kind (C) = Entire_Object);
5839 Child_P : constant Perm_Kind := Children_Permission (C);
5840 D : constant Perm_Tree_Access :=
5841 new Perm_Tree_Wrapper'
5843 (Kind => Entire_Object,
5844 Is_Node_Deep => Is_Node_Deep (C),
5845 Explanation => Expl,
5846 Permission => Child_P,
5847 Children_Permission => Child_P));
5849 if Perm /= None then
5850 D.all.Tree.Permission := Perm;
5853 C.all.Tree := (Kind => Array_Component,
5854 Is_Node_Deep => Is_Node_Deep (C),
5855 Explanation => Expl,
5856 Permission => Permission (C),
5863 when N_Qualified_Expression
5865 | N_Unchecked_Type_Conversion
5867 return Set_Perm_Prefixes (Expression (N), Perm, Expl);
5870 raise Program_Error;
5872 end Set_Perm_Prefixes;
5874 ------------------------------
5875 -- Set_Perm_Prefixes_Assign --
5876 ------------------------------
5878 procedure Set_Perm_Prefixes_Assign (N : Node_Id) is
5879 C : constant Perm_Tree_Access := Get_Perm_Tree (N);
5883 when Entire_Object =>
5884 pragma Assert (Children_Permission (C) = Read_Write);
5885 C.all.Tree.Permission := Read_Write;
5888 C.all.Tree.Permission :=
5889 Lub (Permission (C), Permission (Get_All (C)));
5891 when Array_Component =>
5894 when Record_Component =>
5896 Comp : Perm_Tree_Access;
5897 Perm : Perm_Kind := Read_Write;
5900 -- We take the Glb of all the descendants, and then update the
5901 -- permission of the node with it.
5903 Comp := Perm_Tree_Maps.Get_First (Component (C));
5904 while Comp /= null loop
5905 Perm := Glb (Perm, Permission (Comp));
5906 Comp := Perm_Tree_Maps.Get_Next (Component (C));
5909 C.all.Tree.Permission := Lub (Permission (C), Perm);
5915 -- Base identifier end recursion
5917 when N_Expanded_Name
5922 when N_Explicit_Dereference
5923 | N_Indexed_Component
5924 | N_Selected_Component
5927 Set_Perm_Prefixes_Assign (Prefix (N));
5929 when N_Qualified_Expression
5931 | N_Unchecked_Type_Conversion
5933 Set_Perm_Prefixes_Assign (Expression (N));
5936 raise Program_Error;
5938 end Set_Perm_Prefixes_Assign;
5944 procedure Setup_Globals (Subp : Entity_Id) is
5946 procedure Setup_Global
5951 Global_Var : Boolean);
5952 -- Proxy procedure to set up globals, to adjust for the type of first
5953 -- parameter expected by Setup_Parameter_Or_Global.
5959 procedure Setup_Global
5964 Global_Var : Boolean)
5967 Setup_Parameter_Or_Global
5968 (Id => Entity (Expr),
5972 Global_Var => Global_Var,
5976 procedure Setup_Globals_Inst is new Handle_Globals (Setup_Global);
5978 -- Start of processing for Setup_Globals
5981 Setup_Globals_Inst (Subp);
5984 -------------------------------
5985 -- Setup_Parameter_Or_Global --
5986 -------------------------------
5988 procedure Setup_Parameter_Or_Global
5993 Global_Var : Boolean;
5996 Perm : Perm_Kind_Option;
6000 when E_In_Parameter =>
6002 -- Shallow parameters and globals need not be considered
6004 if not Is_Deep (Typ) then
6007 -- Inputs of functions have R permission only
6009 elsif Ekind (Subp) = E_Function then
6012 -- Input global variables have R permission only
6014 elsif Global_Var then
6017 -- Anonymous access to constant is an observe
6019 elsif Is_Anonymous_Access_Type (Typ)
6020 and then Is_Access_Constant (Typ)
6024 -- Other access types are a borrow
6026 elsif Is_Access_Type (Typ) then
6029 -- Deep types other than access types define an observe
6035 when E_Out_Parameter
6036 | E_In_Out_Parameter
6038 -- Shallow parameters and globals need not be considered
6040 if not Is_Deep (Typ) then
6043 -- Functions cannot have outputs in SPARK
6045 elsif Ekind (Subp) = E_Function then
6048 -- Deep types define a borrow or a move
6055 if Perm /= None then
6057 Tree : constant Perm_Tree_Access :=
6058 new Perm_Tree_Wrapper'
6060 (Kind => Entire_Object,
6061 Is_Node_Deep => Is_Deep (Etype (Id)),
6062 Explanation => Expl,
6064 Children_Permission => Perm));
6066 Set (Current_Perm_Env, Id, Tree);
6069 end Setup_Parameter_Or_Global;
6071 ----------------------
6072 -- Setup_Parameters --
6073 ----------------------
6075 procedure Setup_Parameters (Subp : Entity_Id) is
6078 Formal := First_Formal (Subp);
6079 while Present (Formal) loop
6080 Setup_Parameter_Or_Global
6082 Typ => Retysp (Etype (Formal)),
6083 Kind => Ekind (Formal),
6085 Global_Var => False,
6087 Next_Formal (Formal);
6089 end Setup_Parameters;
6091 --------------------------------
6092 -- Setup_Protected_Components --
6093 --------------------------------
6095 procedure Setup_Protected_Components (Subp : Entity_Id) is
6096 Typ : constant Entity_Id := Scope (Subp);
6101 Comp := First_Component_Or_Discriminant (Typ);
6103 -- The protected object is an implicit input of protected functions, and
6104 -- an implicit input-output of protected procedures and entries.
6106 if Ekind (Subp) = E_Function then
6107 Kind := E_In_Parameter;
6109 Kind := E_In_Out_Parameter;
6112 while Present (Comp) loop
6113 Setup_Parameter_Or_Global
6115 Typ => Retysp (Etype (Comp)),
6118 Global_Var => False,
6121 Next_Component_Or_Discriminant (Comp);
6123 end Setup_Protected_Components;