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.

1 files changed, 0 insertions, 95 deletions

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 70a8417..8e5d351 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -3620,10 +3620,6 @@ package body Sem_Res is
       --  interpretation, but the form of the actual can only be determined
       --  once the primitive operation is identified.
 
-      procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id);
-      --  Emit an error concerning the illegal usage of an effectively volatile
-      --  object for reading in interfering context (SPARK RM 7.1.3(10)).
-
       procedure Insert_Default;
       --  If the actual is missing in a call, insert in the actuals list
       --  an instance of the default expression. The insertion is always
@@ -3874,68 +3870,6 @@ package body Sem_Res is
          end if;
       end Check_Prefixed_Call;
 
-      ---------------------------------------
-      -- Flag_Effectively_Volatile_Objects --
-      ---------------------------------------
-
-      procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id) is
-         function Flag_Object (N : Node_Id) return Traverse_Result;
-         --  Determine whether arbitrary node N denotes an effectively volatile
-         --  object for reading and if it does, emit an error.
-
-         -----------------
-         -- Flag_Object --
-         -----------------
-
-         function Flag_Object (N : Node_Id) return Traverse_Result is
-            Id : Entity_Id;
-
-         begin
-            case Nkind (N) is
-               --  Do not consider nested function calls because they have
-               --  already been processed during their own resolution.
-
-               when N_Function_Call =>
-                  return Skip;
-
-               when N_Identifier | N_Expanded_Name =>
-                  Id := Entity (N);
-
-                  --  Identifiers of components and discriminants are not names
-                  --  in the sense of Ada RM 4.1. They can only occur as a
-                  --  selector_name in selected_component or as a choice in
-                  --  component_association.
-
-                  if Present (Id)
-                    and then Is_Object (Id)
-                    and then Ekind (Id) not in E_Component | E_Discriminant
-                    and then Is_Effectively_Volatile_For_Reading (Id)
-                    and then
-                      not Is_OK_Volatile_Context (Context       => Parent (N),
-                                                  Obj_Ref       => N,
-                                                  Check_Actuals => True)
-                  then
-                     Error_Msg_Code := GEC_Volatile_Non_Interfering_Context;
-                     Error_Msg_N
-                       ("volatile object cannot appear in this context '[[]']",
-                        N);
-                  end if;
-
-                  return Skip;
-
-               when others =>
-                  return OK;
-            end case;
-         end Flag_Object;
-
-         procedure Flag_Objects is new Traverse_Proc (Flag_Object);
-
-      --  Start of processing for Flag_Effectively_Volatile_Objects
-
-      begin
-         Flag_Objects (Expr);
-      end Flag_Effectively_Volatile_Objects;
-
       --------------------
       -- Insert_Default --
       --------------------
@@ -5128,22 +5062,6 @@ package body Sem_Res is
                Check_Unset_Reference (A);
             end if;
 
-            --  The following checks are only relevant when SPARK_Mode is on as
-            --  they are not standard Ada legality rule. Internally generated
-            --  temporaries are ignored.
-
-            if SPARK_Mode = On and then Comes_From_Source (A) then
-
-               --  Inspect the expression and flag each effectively volatile
-               --  object for reading as illegal because it appears within
-               --  an interfering context. Note that this is usually done
-               --  in Resolve_Entity_Name, but when the effectively volatile
-               --  object for reading appears as an actual in a call, the call
-               --  must be resolved first.
-
-               Flag_Effectively_Volatile_Objects (A);
-            end if;
-
             --  A formal parameter of a specific tagged type whose related
             --  subprogram is subject to pragma Extensions_Visible with value
             --  "False" cannot act as an actual in a subprogram with value
@@ -8130,19 +8048,6 @@ package body Sem_Res is
 
          if SPARK_Mode = On then
 
-            --  An effectively volatile object for reading must appear in
-            --  non-interfering context (SPARK RM 7.1.3(10)).
-
-            if Is_Object (E)
-              and then Is_Effectively_Volatile_For_Reading (E)
-              and then
-                not Is_OK_Volatile_Context (Par, N, Check_Actuals => False)
-            then
-               Error_Msg_Code := GEC_Volatile_Non_Interfering_Context;
-               SPARK_Msg_N
-                 ("volatile object cannot appear in this context '[[]']", N);
-            end if;
-
             --  Parameters of modes OUT or IN OUT of the subprogram shall not
             --  occur in the consequences of an exceptional contract unless
             --  they are either passed by reference or occur in the prefix