par-endh.adb (Check_End): issue a syntax error in SPARK mode for missing label at...

2011-08-01  Yannick Moy  <moy@adacore.com>

	* par-endh.adb (Check_End): issue a syntax error in SPARK mode for
	missing label at end of declaration (subprogram or package)
	* par-ch4.adb (P_Name): issue a syntax error in SPARK mode for mixing
	of positional and named parameter association
	* par.adb, par-util.adb (Formal_Error_Msg_SP): new wrapper on
	Error_Msg_SP which adds a prefix to the error message giving the name
	of the formal language analyzed
	* sem_ch6.adb (Analyze_Return_Type): issue an error in formal mode for
	access result type in subprogram, unconstrained array as result type,.
	(Analyze_Subprogram_Declaration): issue an error in formal mode for null
	procedure
	* sem_ch8.adb: Code clean up.

From-SVN: r177048

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 0c0b22f7e1f61c8d4a88e82d469d8c5cabf4f19b..868af9bb1df649b7329119cfdded0f1eb1543a22 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,18 @@
+2011-08-01  Yannick Moy  <moy@adacore.com>
+
+       * par-endh.adb (Check_End): issue a syntax error in SPARK mode for
+       missing label at end of declaration (subprogram or package)
+       * par-ch4.adb (P_Name): issue a syntax error in SPARK mode for mixing
+       of positional and named parameter association
+       * par.adb, par-util.adb (Formal_Error_Msg_SP): new wrapper on
+       Error_Msg_SP which adds a prefix to the error message giving the name
+       of the formal language analyzed
+       * sem_ch6.adb (Analyze_Return_Type): issue an error in formal mode for
+       access result type in subprogram, unconstrained array as result type,.
+       (Analyze_Subprogram_Declaration): issue an error in formal mode for null
+       procedure
+       * sem_ch8.adb: Code clean up.
+
 2011-08-01  Javier Miranda  <miranda@adacore.com>
 
        * sem_ch7.adb (Uninstall_Declarations): Remove useless code.

diff --git a/gcc/ada/par-ch4.adb b/gcc/ada/par-ch4.adb
index 4c25c3ca649dbdb9fb51815f37e4af621def8f2b..a351446841f2087d8b3ca62944193addfc5afc7c 100644 (file)
--- a/gcc/ada/par-ch4.adb
+++ b/gcc/ada/par-ch4.adb
@@ -669,6 +669,10 @@ package body Ch4 is
             --  Test for => (allow := as error substitute)
 
             if Token = Tok_Arrow or else Token = Tok_Colon_Equal then
+               if SPARK_Mode then
+                  Formal_Error_Msg_SP ("no mixing of positional and named "
+                                       & "parameter association");
+               end if;
                Restore_Scan_State (Scan_State); -- to Id
                goto LP_State_Call;
 

diff --git a/gcc/ada/par-endh.adb b/gcc/ada/par-endh.adb
index ca3506dd94d625ed803c08abd39557b1d916f984..ae18703e8ed967939982735c70787a31b89d6868 100644 (file)
--- a/gcc/ada/par-endh.adb
+++ b/gcc/ada/par-endh.adb
@@ -371,6 +371,17 @@ package body Endh is
                   Set_Comes_From_Source (End_Labl, False);
                   End_Labl_Present := False;
 
+                  --  In SPARK mode, no missing label is allowed
+
+                  if SPARK_Mode
+                    and then End_Type = E_Name
+                    and then Explicit_Start_Label (Scope.Last)
+                  then
+                     Error_Msg_Node_1 := Scope.Table (Scope.Last).Labl;
+                     Formal_Error_Msg_SP -- CODEFIX
+                       ("`END &` required");
+                  end if;
+
                   --  Do style check for missing label
 
                   if Style_Check

diff --git a/gcc/ada/par-util.adb b/gcc/ada/par-util.adb
index 6a0e8efc6cbdd156c5b7a7daad4deeb1ca75f0c9..eeb93af639a2a4a0ef7720eb3ebfeead8794072f 100644 (file)
--- a/gcc/ada/par-util.adb
+++ b/gcc/ada/par-util.adb
@@ -377,6 +377,16 @@ package body Util is
       null;
    end Discard_Junk_Node;
 
+   -------------------------
+   -- Formal_Error_Msg_SP --
+   -------------------------
+
+   procedure Formal_Error_Msg_SP (Msg : String) is
+   begin
+      pragma Assert (Formal_Verification_Mode);
+      Error_Msg_SP ("(" & Formal_Language & ") " & Msg);
+   end Formal_Error_Msg_SP;
+
    ------------
    -- Ignore --
    ------------

diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb
index 99f6806057d7ad1ee5f7a1ffe3ea01595343c3dc..da84343b53a29e5f5096307e56e05b259999d5fb 100644 (file)
--- a/gcc/ada/par.adb
+++ b/gcc/ada/par.adb
@@ -1158,6 +1158,10 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is
       --  the argument. A typical use is to skip by some junk that is not
       --  expected in the current context.
 
+      procedure Formal_Error_Msg_SP (Msg : String);
+      --  Wrapper on Errout.Error_Msg_SP which adds a prefix to Msg giving
+      --  the name of the formal language analyzed (spark or alfa)
+
       procedure Ignore (T : Token_Type);
       --  If current token matches T, then give an error message and skip
       --  past it, otherwise the call has no effect at all. T may be any

diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 338eae56149279dbad787e275788732610bcbec6..8e2e2793ffc3ebc15d19d94919a6126c17e5f894 100644 (file)
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1398,6 +1398,13 @@ package body Sem_Ch6 is
       if Result_Definition (N) /= Error then
          if Nkind (Result_Definition (N)) = N_Access_Definition then
 
+            --  Access result is not allowed in SPARK or ALFA
+
+            if Formal_Verification_Mode then
+               Formal_Error_Msg_N
+                 ("access result is not allowed", Result_Definition (N));
+            end if;
+
             --  Ada 2005 (AI-254): Handle anonymous access to subprograms
 
             declare
@@ -1426,6 +1433,17 @@ package body Sem_Ch6 is
             Typ := Entity (Result_Definition (N));
             Set_Etype (Designator, Typ);
 
+            --  Unconstrained array as result is not allowed in SPARK or ALFA
+
+            if Formal_Verification_Mode
+              and then Is_Array_Type (Typ)
+              and then not Is_Constrained (Typ)
+            then
+               Formal_Error_Msg_N
+                 ("returning an unconstrained array is not allowed",
+                 Result_Definition (N));
+            end if;
+
             --  Ada 2005 (AI-231): Ensure proper usage of null exclusion
 
             Null_Exclusion_Static_Checks (N);
@@ -2806,6 +2824,15 @@ package body Sem_Ch6 is
    --  Start of processing for Analyze_Subprogram_Declaration
 
    begin
+      --  Null procedures are not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode
+        and then Nkind (Specification (N)) = N_Procedure_Specification
+        and then Null_Present (Specification (N))
+      then
+         Formal_Error_Msg_N ("null procedure not allowed", N);
+      end if;
+
       --  For a null procedure, capture the profile before analysis, for
       --  expansion at the freeze point and at each point of call. The body
       --  will only be used if the procedure has preconditions. In that case

diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 5380401939244afca3662e8b4f967422b4779d19..56f57d177a5b02c25f03b1d50d52b8c65f965e81 100644 (file)
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -6300,6 +6300,7 @@ package body Sem_Ch8 is
       end loop;
 
       pragma Assert (False);  --  unreachable
+      raise Program_Error;
    end Has_Loop_In_Inner_Open_Scopes;
 
    --------------------