aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMarc Poulhiès <poulhies@adacore.com>2023-02-28 11:01:47 +0100
committerMarc Poulhiès <poulhies@adacore.com>2023-05-25 09:44:15 +0200
commitf6156f454f2d88166cdc18e4281e084c31066f8f (patch)
treeccab0eaf4702af641f3a52d21db89129d0ecaaff
parent7b67bfab289d7f50beed51ca72717be5a8154f3b (diff)
downloadgcc-f6156f454f2d88166cdc18e4281e084c31066f8f.zip
gcc-f6156f454f2d88166cdc18e4281e084c31066f8f.tar.gz
gcc-f6156f454f2d88166cdc18e4281e084c31066f8f.tar.bz2
ada: Fix SPARK context not restored when Load_Unit is failing
When Load_Unit fails to find the unit or encounters an error, the Load_Fail procedure is called and an exception is raised, skipping the restoration of the SPARK/Ghost context stored on procedure entry. gcc/ada/ * rtsfind.adb (Load_RTU.Restore_SPARK_Context): New. (Load_RTU): Use Restore_SPARK_Context on all exit paths. * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Initialize local variable to Empty.
-rw-r--r--gcc/ada/rtsfind.adb41
-rw-r--r--gcc/ada/sem_ch6.adb2
2 files changed, 31 insertions, 12 deletions
diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb
index 4b8e89e..278797f 100644
--- a/gcc/ada/rtsfind.adb
+++ b/gcc/ada/rtsfind.adb
@@ -1023,6 +1023,13 @@ package body Rtsfind is
U : RT_Unit_Table_Record renames RT_Unit_Table (U_Id);
Priv_Par : constant Elist_Id := New_Elmt_List;
Lib_Unit : Node_Id;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ Saved_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save Ghost and SPARK mode-related data to restore on exit
procedure Save_Private_Visibility;
-- If the current unit is the body of child unit or the spec of a
@@ -1034,6 +1041,9 @@ package body Rtsfind is
procedure Restore_Private_Visibility;
-- Restore the visibility of ancestors after compiling RTU
+ procedure Restore_SPARK_Context;
+ -- Restore Ghost and SPARK mode-related data saved on procedure entry
+
--------------------------------
-- Restore_Private_Visibility --
--------------------------------
@@ -1075,15 +1085,16 @@ package body Rtsfind is
end loop;
end Save_Private_Visibility;
- -- Local variables
+ ---------------------------
+ -- Restore_SPARK_Context --
+ ---------------------------
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
- Saved_ISMP : constant Boolean :=
- Ignore_SPARK_Mode_Pragmas_In_Instance;
- Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
- Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
- -- Save Ghost and SPARK mode-related data to restore on exit
+ procedure Restore_SPARK_Context is
+ begin
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ end Restore_SPARK_Context;
-- Start of processing for Load_RTU
@@ -1195,9 +1206,17 @@ package body Rtsfind is
Set_Is_Potentially_Use_Visible (U.Entity, True);
end if;
- Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
- Restore_Ghost_Region (Saved_GM, Saved_IGR);
- Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Restore_SPARK_Context;
+
+ exception
+ -- The Load_Fail procedure that is called when the result of Load_Unit
+ -- is not satisfactory raises an exception. As the compiler is able to
+ -- recover in some cases (i.e. when RE_Not_Available is raised), we need
+ -- to restore the SPARK/Ghost context correctly.
+
+ when others =>
+ Restore_SPARK_Context;
+ raise;
end Load_RTU;
--------------------
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 992688c..48b363e 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2277,7 +2277,7 @@ package body Sem_Ch6 is
Mask_Types : Elist_Id := No_Elist;
Prot_Typ : Entity_Id := Empty;
Spec_Decl : Node_Id := Empty;
- Spec_Id : Entity_Id;
+ Spec_Id : Entity_Id := Empty;
Last_Real_Spec_Entity : Entity_Id := Empty;
-- When we analyze a separate spec, the entity chain ends up containing