From: Yannick Moy Date: Thu, 4 Jul 2019 08:05:36 +0000 (+0000) Subject: [Ada] Better error messages for ownership errors in SPARK X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b04fe972e31570bfb09ae398576c1c79847a9f28;p=gcc.git [Ada] Better error messages for ownership errors in SPARK When SPARK code does not follow the ownership rules of SPARK RM 3.10, the error message now points to a location explaining why the object has a more restricted permission than the expected one. There is no impact on compilation. 2019-07-04 Yannick Moy gcc/ada/ * sem_spark.adb (Explanation, Get_Expl): New functions to get the explanation for a permission mismatch. (Perm_Error, Perm_Mismatch, Perm_Error_Loop_Exit): Take explanation into account for issuing a more precise error message. (Set_Perm_Prefixes, Set_Perm_Extensions, Set_Perm_Extensions_Move): Pass suitable argument for the explanation node. From-SVN: r273050 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 46f30aa87fe..127c24346c6 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,14 @@ +2019-07-04 Yannick Moy + + * sem_spark.adb (Explanation, Get_Expl): New functions to get + the explanation for a permission mismatch. + (Perm_Error, Perm_Mismatch, Perm_Error_Loop_Exit): Take + explanation into account for issuing a more precise error + message. + (Set_Perm_Prefixes, Set_Perm_Extensions, + Set_Perm_Extensions_Move): Pass suitable argument for the + explanation node. + 2019-07-04 Arnaud Charlet * exp_aggr.adb (In_Place_Assign_OK): Moved to top level and add diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index b4e816ef297..82ddb161b8e 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -137,6 +137,9 @@ package body Sem_SPARK is -- corresponds to both "observing" and "owning" types in SPARK RM -- 3.10. To be used when moving the path. + Explanation : Node_Id; + -- Node that can be used in an explanation for a permission mismatch + case Kind is -- An entire object is either a leaf (an object which cannot be -- extended further in a path) or a subtree in folded form (which @@ -217,6 +220,7 @@ package body Sem_SPARK is function Children_Permission (T : Perm_Tree_Access) return Perm_Kind; function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance; + function Explanation (T : Perm_Tree_Access) return Node_Id; function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access; function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access; function Is_Node_Deep (T : Perm_Tree_Access) return Boolean; @@ -257,6 +261,7 @@ package body Sem_SPARK is (N : Node_Id; Exp_Perm : Perm_Kind; Act_Perm : Perm_Kind; + Expl : Node_Id; Forbidden_Perm : Boolean := False); -- Issues a continuation error message about a mismatch between a -- desired permission Exp_Perm and a permission obtained Act_Perm. N @@ -428,6 +433,15 @@ package body Sem_SPARK is Free_Perm_Tree_Dealloc (PT); end Free_Tree; + ----------------- + -- Explanation -- + ----------------- + + function Explanation (T : Perm_Tree_Access) return Node_Id is + begin + return T.all.Tree.Explanation; + end Explanation; + ------------- -- Get_All -- ------------- @@ -503,22 +517,34 @@ package body Sem_SPARK is (N : Node_Id; Exp_Perm : Perm_Kind; Act_Perm : Perm_Kind; + Expl : Node_Id; Forbidden_Perm : Boolean := False) is begin + Error_Msg_Sloc := Sloc (Expl); + if Forbidden_Perm then - if Exp_Perm = Act_Perm then - Error_Msg_N ("\got forbidden state `" - & Perm_Kind'Image (Exp_Perm), N); + if Exp_Perm = No_Access then + Error_Msg_N ("\object was moved #", N); else - Error_Msg_N ("\forbidden state `" - & Perm_Kind'Image (Exp_Perm) & "`, got `" - & Perm_Kind'Image (Act_Perm) & "`", N); + raise Program_Error; end if; else - Error_Msg_N ("\expected state `" - & Perm_Kind'Image (Exp_Perm) & "` at least, got `" - & Perm_Kind'Image (Act_Perm) & "`", N); + case Exp_Perm is + when Write_Perm => + if Act_Perm = Read_Only then + Error_Msg_N + ("\object was declared as not writeable #", N); + else + Error_Msg_N ("\object was moved #", N); + end if; + + when Read_Only => + Error_Msg_N ("\object was moved #", N); + + when No_Access => + raise Program_Error; + end case; end if; end Perm_Mismatch; @@ -575,8 +601,11 @@ package body Sem_SPARK is type Perm_Or_Tree (R : Result_Kind) is record case R is - when Folded => Found_Permission : Perm_Kind; - when Unfolded => Tree_Access : Perm_Tree_Access; + when Folded => + Found_Permission : Perm_Kind; + Explanation : Node_Id; + when Unfolded => + Tree_Access : Perm_Tree_Access; end case; end record; @@ -650,6 +679,10 @@ package body Sem_SPARK is -- Check that type Typ is either not deep, or that it is an observing or -- owning type according to SPARK RM 3.10 + function Get_Expl (N : Node_Or_Entity_Id) return Node_Id; + -- The function that takes a name as input and returns an explanation node + -- for the permission associated with it. + function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id; pragma Precondition (Is_Path_Expression (Expr)); -- Return the expression being borrowed/observed when borrowing or @@ -732,6 +765,7 @@ package body Sem_SPARK is (N : Node_Id; Perm : Perm_Kind; Found_Perm : Perm_Kind; + Expl : Node_Id; Forbidden_Perm : Boolean := False); -- A procedure that is called when the permissions found contradict the -- rules established by the RM. This function is called with the node and @@ -742,7 +776,8 @@ package body Sem_SPARK is (E : Entity_Id; Subp : Entity_Id; Perm : Perm_Kind; - Found_Perm : Perm_Kind); + Found_Perm : Perm_Kind; + Expl : Node_Id); -- A procedure that is called when the permissions found contradict the -- rules established by the RM at the end of subprograms. This function is -- called with the node, the node of the returning function, and the @@ -772,12 +807,18 @@ package body Sem_SPARK is -- subprogram indeed have Read_Write permission at the end of the -- subprogram execution. - procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind); + procedure Set_Perm_Extensions + (T : Perm_Tree_Access; + P : Perm_Kind; + Expl : Node_Id); -- This procedure takes an access to a permission tree and modifies the -- tree so that any strict extensions of the given tree become of the -- access specified by parameter P. - procedure Set_Perm_Extensions_Move (T : Perm_Tree_Access; E : Entity_Id); + procedure Set_Perm_Extensions_Move + (T : Perm_Tree_Access; + E : Entity_Id; + Expl : Node_Id); -- Set permissions to -- No for any extension with more .all -- W for any deep extension with same number of .all @@ -785,7 +826,8 @@ package body Sem_SPARK is function Set_Perm_Prefixes (N : Node_Id; - Perm : Perm_Kind_Option) return Perm_Tree_Access; + Perm : Perm_Kind_Option; + Expl : Node_Id) return Perm_Tree_Access; pragma Precondition (Is_Path_Expression (N)); -- This function modifies the permissions of a given node in the permission -- environment as well as all the prefixes of the path, to the new @@ -817,7 +859,8 @@ package body Sem_SPARK is Typ : Entity_Id; Kind : Formal_Kind; Subp : Entity_Id; - Global_Var : Boolean); + Global_Var : Boolean; + Expl : Node_Id); -- Auxiliary procedure to Setup_Parameters and Setup_Globals procedure Setup_Parameters (Subp : Entity_Id); @@ -1106,6 +1149,7 @@ package body Sem_SPARK is if Perm = No_Access then Perm_Error (Expr, No_Access, No_Access, + Expl => Get_Expl (Expr), Forbidden_Perm => True); return; end if; @@ -1114,6 +1158,7 @@ package body Sem_SPARK is if Perm = No_Access then Perm_Error (Expr, No_Access, No_Access, + Expl => Get_Expl (Expr_Root), Forbidden_Perm => True); return; end if; @@ -1133,7 +1178,7 @@ package body Sem_SPARK is Perm := Get_Perm (Expr); if Perm /= Read_Write then - Perm_Error (Expr, Read_Write, Perm); + Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr)); return; end if; @@ -1331,6 +1376,7 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => True, + Explanation => Decl, Permission => Read_Write, Children_Permission => Read_Write)); begin @@ -1819,7 +1865,8 @@ package body Sem_SPARK is (E : Entity_Id; Loop_Id : Node_Id; Perm : Perm_Kind; - Found_Perm : Perm_Kind); + Found_Perm : Perm_Kind; + Expl : Node_Id); -- A procedure that is called when the permissions found contradict -- the rules established by the RM at the exit of loops. This function -- is called with the entity, the node of the enclosing loop, the @@ -1889,14 +1936,15 @@ package body Sem_SPARK is begin if not (Permission (Tree) >= Perm) then Perm_Error_Loop_Exit - (E, Stmt, Permission (Tree), Perm); + (E, Stmt, Permission (Tree), Perm, Explanation (Tree)); end if; case Kind (Tree) is when Entire_Object => if not (Children_Permission (Tree) >= Perm) then Perm_Error_Loop_Exit - (E, Stmt, Children_Permission (Tree), Perm); + (E, Stmt, Children_Permission (Tree), Perm, + Explanation (Tree)); end if; @@ -1934,14 +1982,15 @@ package body Sem_SPARK is begin if not (Perm >= Permission (Tree)) then Perm_Error_Loop_Exit - (E, Stmt, Permission (Tree), Perm); + (E, Stmt, Permission (Tree), Perm, Explanation (Tree)); end if; case Kind (Tree) is when Entire_Object => if not (Perm >= Children_Permission (Tree)) then Perm_Error_Loop_Exit - (E, Stmt, Children_Permission (Tree), Perm); + (E, Stmt, Children_Permission (Tree), Perm, + Explanation (Tree)); end if; when Reference => @@ -1974,7 +2023,8 @@ package body Sem_SPARK is (E => E, Loop_Id => Stmt, Perm => Permission (New_Tree), - Found_Perm => Permission (Orig_Tree)); + Found_Perm => Permission (Orig_Tree), + Expl => Explanation (New_Tree)); end if; case Kind (New_Tree) is @@ -1994,7 +2044,8 @@ package body Sem_SPARK is Perm_Error_Loop_Exit (E, Stmt, Children_Permission (New_Tree), - Children_Permission (Orig_Tree)); + Children_Permission (Orig_Tree), + Explanation (New_Tree)); end if; when Reference => @@ -2101,14 +2152,16 @@ package body Sem_SPARK is (E : Entity_Id; Loop_Id : Node_Id; Perm : Perm_Kind; - Found_Perm : Perm_Kind) + Found_Perm : Perm_Kind; + Expl : Node_Id) is begin Error_Msg_Node_2 := Loop_Id; Error_Msg_N ("insufficient permission for & when exiting loop &", E); Perm_Mismatch (Exp_Perm => Perm, Act_Perm => Found_Perm, - N => Loop_Id); + N => Loop_Id, + Expl => Expl); end Perm_Error_Loop_Exit; -- Local variables @@ -2836,7 +2889,7 @@ package body Sem_SPARK is Perm := Get_Perm (Obj); if Perm /= Read_Write then - Perm_Error (Decl, Read_Write, Perm); + Perm_Error (Decl, Read_Write, Perm, Expl => Get_Expl (Obj)); end if; if Ekind_In (Subp, E_Procedure, E_Entry) @@ -3044,6 +3097,51 @@ package body Sem_SPARK is end case; end Check_Type; + -------------- + -- Get_Expl -- + -------------- + + function Get_Expl (N : Node_Or_Entity_Id) return Node_Id is + begin + -- Special case for the object declared in an extended return statement + + if Nkind (N) = N_Defining_Identifier then + declare + C : constant Perm_Tree_Access := + Get (Current_Perm_Env, Unique_Entity (N)); + begin + pragma Assert (C /= null); + return Explanation (C); + end; + + -- The expression is a call to a traversal function + + elsif Is_Traversal_Function_Call (N) then + return N; + + -- The expression is directly rooted in an object + + elsif Present (Get_Root_Object (N, Through_Traversal => False)) then + declare + Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N); + begin + case Tree_Or_Perm.R is + when Folded => + return Tree_Or_Perm.Explanation; + + when Unfolded => + pragma Assert (Tree_Or_Perm.Tree_Access /= null); + return Explanation (Tree_Or_Perm.Tree_Access); + end case; + end; + + -- The expression is a function call, an allocation, or null + + else + return N; + end if; + end Get_Expl; + ----------------------------------- -- Get_Observed_Or_Borrowed_Expr -- ----------------------------------- @@ -3159,7 +3257,9 @@ package body Sem_SPARK is when Entire_Object => return (R => Folded, Found_Permission => - Children_Permission (C.Tree_Access)); + Children_Permission (C.Tree_Access), + Explanation => + Explanation (C.Tree_Access)); when Reference => pragma Assert (Nkind (N) = N_Explicit_Dereference); @@ -3208,7 +3308,7 @@ package body Sem_SPARK is function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is begin - return Set_Perm_Prefixes (N, None); + return Set_Perm_Prefixes (N, None, Empty); end Get_Perm_Tree; --------------------- @@ -3912,6 +4012,7 @@ package body Sem_SPARK is (N : Node_Id; Perm : Perm_Kind; Found_Perm : Perm_Kind; + Expl : Node_Id; Forbidden_Perm : Boolean := False) is procedure Set_Root_Object @@ -3975,7 +4076,7 @@ package body Sem_SPARK is Error_Msg_NE ("insufficient permission for &", N, Root); end if; - Perm_Mismatch (N, Perm, Found_Perm, Forbidden_Perm); + Perm_Mismatch (N, Perm, Found_Perm, Expl, Forbidden_Perm); end Perm_Error; ------------------------------- @@ -3986,13 +4087,14 @@ package body Sem_SPARK is (E : Entity_Id; Subp : Entity_Id; Perm : Perm_Kind; - Found_Perm : Perm_Kind) + Found_Perm : Perm_Kind; + Expl : Node_Id) is begin Error_Msg_Node_2 := Subp; Error_Msg_NE ("insufficient permission for & when returning from &", Subp, E); - Perm_Mismatch (Subp, Perm, Found_Perm); + Perm_Mismatch (Subp, Perm, Found_Perm, Expl); end Perm_Error_Subprogram_End; ------------------ @@ -4035,7 +4137,7 @@ package body Sem_SPARK is if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr) then Error_Msg_Sloc := Sloc (Borrowed); - Error_Msg_N ("expression was borrowed #", Expr); + Error_Msg_N ("object was borrowed #", Expr); end if; Key := Get_Next_Key (Current_Borrowers); @@ -4071,7 +4173,7 @@ package body Sem_SPARK is if Is_Prefix_Or_Almost (Pref => Observed, Expr => Expr) then Error_Msg_Sloc := Sloc (Observed); - Error_Msg_N ("expression was observed #", Expr); + Error_Msg_N ("object was observed #", Expr); end if; Key := Get_Next_Key (Current_Observers); @@ -4134,7 +4236,7 @@ package body Sem_SPARK is -- Check path is readable if Perm not in Read_Perm then - Perm_Error (Expr, Read_Only, Perm); + Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr)); return; end if; @@ -4158,7 +4260,7 @@ package body Sem_SPARK is if not Is_Deep (Expr_Type) then if Perm not in Read_Perm then - Perm_Error (Expr, Read_Only, Perm); + Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr)); end if; return; end if; @@ -4167,7 +4269,7 @@ package body Sem_SPARK is -- the source object (if any) shall be Unrestricted. if Perm /= Read_Write then - Perm_Error (Expr, Read_Write, Perm); + Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr)); return; end if; @@ -4182,7 +4284,7 @@ package body Sem_SPARK is -- For assignment, check W permission if Perm not in Write_Perm then - Perm_Error (Expr, Write_Only, Perm); + Perm_Error (Expr, Write_Only, Perm, Expl => Get_Expl (Expr)); return; end if; @@ -4201,7 +4303,7 @@ package body Sem_SPARK is -- For borrowing, check RW permission if Perm /= Read_Write then - Perm_Error (Expr, Read_Write, Perm); + Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr)); return; end if; @@ -4220,7 +4322,7 @@ package body Sem_SPARK is -- For borrowing, check R permission if Perm not in Read_Perm then - Perm_Error (Expr, Read_Only, Perm); + Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr)); return; end if; end case; @@ -4259,10 +4361,10 @@ package body Sem_SPARK is if Present (Get_Root_Object (Expr)) then declare Tree : constant Perm_Tree_Access := - Set_Perm_Prefixes (Expr, Write_Only); + Set_Perm_Prefixes (Expr, Write_Only, Expl => Expr); begin pragma Assert (Tree /= null); - Set_Perm_Extensions_Move (Tree, Etype (Expr)); + Set_Perm_Extensions_Move (Tree, Etype (Expr), Expl => Expr); end; end if; @@ -4283,7 +4385,7 @@ package body Sem_SPARK is Tree : constant Perm_Tree_Access := Get_Perm_Tree (Expr); begin Tree.all.Tree.Permission := Read_Write; - Set_Perm_Extensions (Tree, Read_Write); + Set_Perm_Extensions (Tree, Read_Write, Expl => Expr); -- Normalize the permission tree @@ -4390,7 +4492,8 @@ package body Sem_SPARK is (E => Id, Subp => Subp, Perm => Read_Write, - Found_Perm => Permission (Tree)); + Found_Perm => Permission (Tree), + Expl => Explanation (Tree)); end if; end; end Return_Parameter_Or_Global; @@ -4418,7 +4521,10 @@ package body Sem_SPARK is -- Set_Perm_Extensions -- ------------------------- - procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind) is + procedure Set_Perm_Extensions + (T : Perm_Tree_Access; + P : Perm_Kind; + Expl : Node_Id) is procedure Free_Perm_Tree_Children (T : Perm_Tree_Access); -- Free the permission tree of children if any, prio to replacing T @@ -4462,6 +4568,7 @@ package body Sem_SPARK is Free_Perm_Tree_Children (T); T.all.Tree := Perm_Tree'(Kind => Entire_Object, Is_Node_Deep => Is_Node_Deep (T), + Explanation => Expl, Permission => Permission (T), Children_Permission => P); end Set_Perm_Extensions; @@ -4471,14 +4578,15 @@ package body Sem_SPARK is ------------------------------ procedure Set_Perm_Extensions_Move - (T : Perm_Tree_Access; - E : Entity_Id) + (T : Perm_Tree_Access; + E : Entity_Id; + Expl : Node_Id) is begin -- Shallow extensions are set to RW if not Is_Node_Deep (T) then - Set_Perm_Extensions (T, Read_Write); + Set_Perm_Extensions (T, Read_Write, Expl => Expl); return; end if; @@ -4502,12 +4610,14 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Node_Deep (T), + Explanation => Expl, Permission => Read_Write, Children_Permission => Read_Write)); begin - Set_Perm_Extensions_Move (C, Component_Type (E)); + Set_Perm_Extensions_Move (C, Component_Type (E), Expl); T.all.Tree := (Kind => Array_Component, Is_Node_Deep => Is_Node_Deep (T), + Explanation => Expl, Permission => Write_Only, Get_Elem => C); end; @@ -4525,9 +4635,10 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (Comp)), + Explanation => Expl, Permission => Read_Write, Children_Permission => Read_Write)); - Set_Perm_Extensions_Move (C, Etype (Comp)); + Set_Perm_Extensions_Move (C, Etype (Comp), Expl); Perm_Tree_Maps.Set (Hashtbl, Comp, C); Next_Component_Or_Discriminant (Comp); end loop; @@ -4535,6 +4646,7 @@ package body Sem_SPARK is T.all.Tree := (Kind => Record_Component, Is_Node_Deep => Is_Node_Deep (T), + Explanation => Expl, Permission => Write_Only, Component => Hashtbl); end; @@ -4542,14 +4654,14 @@ package body Sem_SPARK is -- Otherwise, extensions are set to NO when others => - Set_Perm_Extensions (T, No_Access); + Set_Perm_Extensions (T, No_Access, Expl); end case; when Reference => - Set_Perm_Extensions (T, No_Access); + Set_Perm_Extensions (T, No_Access, Expl); when Array_Component => - Set_Perm_Extensions_Move (Get_Elem (T), Component_Type (E)); + Set_Perm_Extensions_Move (Get_Elem (T), Component_Type (E), Expl); when Record_Component => declare @@ -4561,7 +4673,7 @@ package body Sem_SPARK is while Present (Comp) loop C := Perm_Tree_Maps.Get (Component (T), Comp); pragma Assert (C /= null); - Set_Perm_Extensions_Move (C, Etype (Comp)); + Set_Perm_Extensions_Move (C, Etype (Comp), Expl); Next_Component_Or_Discriminant (Comp); end loop; end; @@ -4574,7 +4686,8 @@ package body Sem_SPARK is function Set_Perm_Prefixes (N : Node_Id; - Perm : Perm_Kind_Option) return Perm_Tree_Access + Perm : Perm_Kind_Option; + Expl : Node_Id) return Perm_Tree_Access is begin case Nkind (N) is @@ -4602,7 +4715,7 @@ package body Sem_SPARK is when N_Explicit_Dereference => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes (Prefix (N), Perm); + Set_Perm_Prefixes (Prefix (N), Perm, Expl); pragma Assert (C /= null); pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Reference); @@ -4635,6 +4748,7 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (N)), + Explanation => Expl, Permission => Child_P, Children_Permission => Child_P)); begin @@ -4644,6 +4758,7 @@ package body Sem_SPARK is C.all.Tree := (Kind => Reference, Is_Node_Deep => Is_Node_Deep (C), + Explanation => Expl, Permission => Permission (C), Get_All => D); return D; @@ -4654,7 +4769,7 @@ package body Sem_SPARK is when N_Selected_Component => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes (Prefix (N), Perm); + Set_Perm_Prefixes (Prefix (N), Perm, Expl); pragma Assert (C /= null); pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Record_Component); @@ -4708,6 +4823,7 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (Comp)), + Explanation => Expl, Permission => P, Children_Permission => Child_P)); Perm_Tree_Maps.Set (Hashtbl, Comp, D); @@ -4723,6 +4839,7 @@ package body Sem_SPARK is C.all.Tree := (Kind => Record_Component, Is_Node_Deep => Is_Node_Deep (C), + Explanation => Expl, Permission => Permission (C), Component => Hashtbl); return D_This; @@ -4735,7 +4852,7 @@ package body Sem_SPARK is => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes (Prefix (N), Perm); + Set_Perm_Prefixes (Prefix (N), Perm, Expl); pragma Assert (C /= null); pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Array_Component); @@ -4768,6 +4885,7 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Node_Deep (C), + Explanation => Expl, Permission => Child_P, Children_Permission => Child_P)); begin @@ -4777,6 +4895,7 @@ package body Sem_SPARK is C.all.Tree := (Kind => Array_Component, Is_Node_Deep => Is_Node_Deep (C), + Explanation => Expl, Permission => Permission (C), Get_Elem => D); return D; @@ -4788,7 +4907,7 @@ package body Sem_SPARK is | N_Type_Conversion | N_Unchecked_Type_Conversion => - return Set_Perm_Prefixes (Expression (N), Perm); + return Set_Perm_Prefixes (Expression (N), Perm, Expl); when others => raise Program_Error; @@ -4893,7 +5012,8 @@ package body Sem_SPARK is Typ => Typ, Kind => Kind, Subp => Subp, - Global_Var => Global_Var); + Global_Var => Global_Var, + Expl => Expr); end Setup_Global; procedure Setup_Globals_Inst is new Handle_Globals (Setup_Global); @@ -4913,7 +5033,8 @@ package body Sem_SPARK is Typ : Entity_Id; Kind : Formal_Kind; Subp : Entity_Id; - Global_Var : Boolean) + Global_Var : Boolean; + Expl : Node_Id) is Perm : Perm_Kind_Option; @@ -4989,6 +5110,7 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (Id)), + Explanation => Expl, Permission => Perm, Children_Permission => Perm)); begin @@ -5011,7 +5133,8 @@ package body Sem_SPARK is Typ => Underlying_Type (Etype (Formal)), Kind => Ekind (Formal), Subp => Subp, - Global_Var => False); + Global_Var => False, + Expl => Formal); Next_Formal (Formal); end loop; end Setup_Parameters;