diff options
| author | Yannick Moy <moy@adacore.com> | 2023-10-20 09:39:10 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-11-30 11:12:49 +0100 |
| commit | 1029b95079a073bba17d5e39029287e1e9600021 (patch) | |
| tree | 30c4b6a1c206b49fd5c0391a7c8a5366ba3ec53f /gcc/ada/sem_disp.adb | |
| parent | dab7e3430e76c7f23839e112f1c9676383263256 (diff) | |
| download | gcc-1029b95079a073bba17d5e39029287e1e9600021.zip gcc-1029b95079a073bba17d5e39029287e1e9600021.tar.gz gcc-1029b95079a073bba17d5e39029287e1e9600021.tar.bz2 | |
ada: Remove SPARK legality checks
SPARK legality checks apply only to code with SPARK_Mode On, and are
performed again in GNATprove for detecting SPARK-compatible declarations
in code with SPARK_Mode Auto. Remove this duplication, to only perform
SPARK legality checking in GNATprove. After this patch, only a few
special SPARK legality checks are performed in the frontend, which could
be moved to GNATprove later.
gcc/ada/
* contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract):
Remove checking on volatility. Remove handling of SPARK_Mode, not
needed anymore.
(Analyze_Entry_Or_Subprogram_Contract): Remove checking on
volatility.
(Check_Type_Or_Object_External_Properties): Same.
(Analyze_Object_Contract): Same.
* freeze.adb (Freeze_Record_Type): Same. Also remove checking on
synchronized types and ghost types.
* sem_ch12.adb (Instantiate_Object): Remove checking on
volatility.
(Instantiate_Type): Same.
* sem_ch3.adb (Access_Type_Declaration): Same.
(Derived_Type_Declaration): Remove checking related to untagged
partial view.
(Process_Discriminants): Remove checking on volatility.
* sem_ch5.adb (Analyze_Loop_Parameter_Specification): Same.
* sem_ch6.adb (Analyze_Procedure_Call): Fix use of SPARK_Mode
where GNATprove_Mode was intended.
* sem_disp.adb (Inherited_Subprograms): Protect against Empty
node.
* sem_prag.adb (Analyze_Global_In_Decl_Part): Remove checking on
volatility.
(Analyze_Pragma): Same.
* sem_res.adb (Flag_Effectively_Volatile_Objects): Remove.
(Resolve_Actuals): Remove checking on volatility.
(Resolve_Entity_Name): Same.
* sem_util.adb (Check_Nonvolatile_Function_Profile): Remove.
(Check_Volatility_Compatibility): Remove.
* sem_util.ads: Same.
Diffstat (limited to 'gcc/ada/sem_disp.adb')
| -rw-r--r-- | gcc/ada/sem_disp.adb | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index ab7bc40..6975f4a 100644 --- a/gcc/ada/sem_disp.adb +++ b/gcc/ada/sem_disp.adb @@ -2581,6 +2581,7 @@ package body Sem_Disp is loop Parent_Op := Overridden_Operation (Parent_Op); exit when No (Parent_Op) + or else No (Find_DT (Parent_Op)) or else (No_Interfaces and then Is_Interface (Find_DT (Parent_Op))); |