Skip to content

Commit

Permalink
ada: Fix SPARK context not restored when Load_Unit is failing
Browse files Browse the repository at this point in the history
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.

Tested on x86_64-pc-linux-gnu, committed on master.
  • Loading branch information
dkm authored and ouuleilei-bot committed May 25, 2023
1 parent c2d62cd commit 200de0b
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 12 deletions.
41 changes: 30 additions & 11 deletions gcc/ada/rtsfind.adb
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 --
--------------------------------
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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;

--------------------
Expand Down
2 changes: 1 addition & 1 deletion gcc/ada/sem_ch6.adb
Original file line number Diff line number Diff line change
Expand Up @@ -2262,7 +2262,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
Expand Down

0 comments on commit 200de0b

Please sign in to comment.