ada: Cleanup SPARK legality checking

Move one SPARK legality check from GNAT to GNATprove, and cleanup
other uses of SPARK_Mode for legality checking.

gcc/ada/

	* sem_ch4.adb (Analyze_Selected_Component): Check correct mode
	variable for GNATprove.
	* sem_prag.adb (Refined_State): Call SPARK_Msg_NE which checks
	value of SPARK_Mode before issuing a message.
	* sem_res.adb (Resolve_Entity_Name): Remove legality check for
	SPARK RM 6.1.9(1), moved to GNATprove.

diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index d506944bc8dd54393f061c7278787063b375cf55..64aa9a84e605540bb867b3812e5f16d73096c22f 100644 (file)
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -6025,17 +6025,17 @@ package body Sem_Ch4 is
                      --  Emit appropriate message. The node will be replaced
                      --  by an appropriate raise statement.
 
-                     --  Note that in SPARK mode, as with all calls to apply a
-                     --  compile time constraint error, this will be made into
-                     --  an error to simplify the processing of the formal
-                     --  verification backend.
+                     --  Note that in GNATprove mode, as with all calls to
+                     --  apply a compile time constraint error, this will be
+                     --  made into an error to simplify the processing of the
+                     --  formal verification backend.
 
                      Apply_Compile_Time_Constraint_Error
                        (N, "component not present in }??",
                         CE_Discriminant_Check_Failed,
                         Ent          => Prefix_Type,
                         Emit_Message =>
-                          SPARK_Mode = On or not In_Instance_Not_Visible);
+                          GNATprove_Mode or not In_Instance_Not_Visible);
                      return;
                   end if;
 

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 9d66fb71a0606b8d205907a8200ce27f0c0401d1..db20f20b9f10f2878989654e9faf89ead2617aa4 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -23375,15 +23375,13 @@ package body Sem_Prag is
             Analyze_If_Present (Pragma_SPARK_Mode);
 
             --  State refinement is allowed only when the corresponding package
-            --  declaration has non-null pragma Abstract_State. Refinement not
-            --  enforced when SPARK checks are suppressed (SPARK RM 7.2.2(3)).
+            --  declaration has non-null pragma Abstract_State (SPARK RM
+            --  7.2.2(3)).
 
-            if SPARK_Mode /= Off
-              and then
-                (No (Abstract_States (Spec_Id))
-                  or else Has_Null_Abstract_State (Spec_Id))
+            if No (Abstract_States (Spec_Id))
+              or else Has_Null_Abstract_State (Spec_Id)
             then
-               Error_Msg_NE
+               SPARK_Msg_NE
                  ("useless refinement, package & does not define abstract "
                   & "states", N, Spec_Id);
                return;

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index c684075219b14a4fee7a3bd2f3e9ca6e0bf787b7..d81a5af9032e95f4137f8c14c32e01acc2cb8edb 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7787,14 +7787,6 @@ package body Sem_Res is
       --  Determine whether Expr is part of an N_Attribute_Reference
       --  expression.
 
-      function In_Attribute_Old (Expr : Node_Id) return Boolean;
-      --  Determine whether Expr is in attribute Old
-
-      function Within_Exceptional_Cases_Consequence
-        (Expr : Node_Id)
-         return Boolean;
-      --  Determine whether Expr is part of an Exceptional_Cases consequence
-
       ----------------------------------------
       -- Is_Assignment_Or_Object_Expression --
       ----------------------------------------
@@ -7836,31 +7828,6 @@ package body Sem_Res is
          end if;
       end Is_Assignment_Or_Object_Expression;
 
-      ----------------------
-      -- In_Attribute_Old --
-      ----------------------
-
-      function In_Attribute_Old (Expr : Node_Id) return Boolean is
-         N : Node_Id := Expr;
-      begin
-         while Present (N) loop
-            if Nkind (N) = N_Attribute_Reference
-              and then Attribute_Name (N) = Name_Old
-            then
-               return True;
-
-            --  Prevent the search from going too far
-
-            elsif Is_Body_Or_Package_Declaration (N) then
-               return False;
-            end if;
-
-            N := Parent (N);
-         end loop;
-
-         return False;
-      end In_Attribute_Old;
-
       -----------------------------
       -- Is_Attribute_Expression --
       -----------------------------
@@ -7884,39 +7851,6 @@ package body Sem_Res is
          return False;
       end Is_Attribute_Expression;
 
-      ------------------------------------------
-      -- Within_Exceptional_Cases_Consequence --
-      ------------------------------------------
-
-      function Within_Exceptional_Cases_Consequence
-        (Expr : Node_Id)
-         return Boolean
-      is
-         Context : Node_Id := Parent (Expr);
-      begin
-         while Present (Context) loop
-            if Nkind (Context) = N_Pragma then
-
-               --  In Exceptional_Cases references to formal parameters are
-               --  only allowed within consequences, so it is enough to
-               --  recognize the pragma itself.
-
-               if Get_Pragma_Id (Context) = Pragma_Exceptional_Cases then
-                  return True;
-               end if;
-
-            --  Prevent the search from going too far
-
-            elsif Is_Body_Or_Package_Declaration (Context) then
-               return False;
-            end if;
-
-            Context := Parent (Context);
-         end loop;
-
-         return False;
-      end Within_Exceptional_Cases_Consequence;
-
       --  Local variables
 
       E   : constant Entity_Id := Entity (N);
@@ -8048,40 +7982,6 @@ package body Sem_Res is
 
          if SPARK_Mode = On then
 
-            --  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
-            --  of a reference to the 'Old attribute. For convenience, we also
-            --  allow them as prefixes of attributes that do not actually read
-            --  data from the object.
-
-            if Ekind (E) in E_Out_Parameter | E_In_Out_Parameter
-              and then Scope (E) = Current_Scope_No_Loops
-              and then Within_Exceptional_Cases_Consequence (N)
-              and then not In_Attribute_Old (N)
-              and then not (Nkind (Parent (N)) = N_Attribute_Reference
-                              and then
-                            Attribute_Name (Parent (N)) in Name_Constrained
-                                                         | Name_First
-                                                         | Name_Last
-                                                         | Name_Length
-                                                         | Name_Range)
-              and then not Is_By_Reference_Type (Etype (E))
-              and then not Is_Aliased (E)
-            then
-               if Ekind (E) = E_Out_Parameter then
-                  Error_Msg_N
-                    ("formal parameter of mode `OUT` cannot appear " &
-                       "in consequence of Exceptional_Cases", N);
-               else
-                  Error_Msg_N
-                    ("formal parameter of mode `IN OUT` cannot appear " &
-                       "in consequence of Exceptional_Cases", N);
-               end if;
-               Error_Msg_N
-                 ("\only parameters passed by reference are allowed", N);
-            end if;
-
             --  Check for possible elaboration issues with respect to reads of
             --  variables. The act of renaming the variable is not considered a
             --  read as it simply establishes an alias.