diff options
Diffstat (limited to 'gcc/ada/lib-xref-spark_specific.adb')
| -rw-r--r-- | gcc/ada/lib-xref-spark_specific.adb | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 43a0237..b570725 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -40,6 +40,7 @@ package body SPARK_Specific is SPARK_Entities : constant array (Entity_Kind) of Boolean := (E_Constant => True, + E_Entry => True, E_Function => True, E_In_Out_Parameter => True, E_In_Parameter => True, @@ -268,7 +269,7 @@ package body SPARK_Specific is => Typ := Xref_Entity_Letters (Ekind (E)); - when E_Package_Body | E_Subprogram_Body => + when E_Package_Body | E_Subprogram_Body | E_Task_Body => Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E))); when E_Void => @@ -1006,14 +1007,19 @@ package body SPARK_Specific is procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is begin - if Nkind_In (N, N_Entry_Body, - N_Entry_Declaration, - N_Package_Body, + if Nkind_In (N, N_Entry_Body, -- entries + N_Entry_Declaration) + or else + Nkind_In (N, N_Package_Body, -- packages N_Package_Body_Stub, - N_Package_Declaration, - N_Subprogram_Body, + N_Package_Declaration) + or else + Nkind_In (N, N_Subprogram_Body, -- subprograms N_Subprogram_Body_Stub, N_Subprogram_Declaration) + or else + Nkind_In (N, N_Task_Body, -- tasks + N_Task_Body_Stub) then Add_SPARK_Scope (N); end if; @@ -1105,6 +1111,10 @@ package body SPARK_Specific is Result := Defining_Identifier (Result); exit; + when N_Task_Body => + Result := Defining_Identifier (Result); + exit; + when others => Result := Parent (Result); end case; |