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

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

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.

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;
 

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

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 --
    ------------

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

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

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;
 
    --------------------