[Ada] Missing return statement is illegal in GNATprove mode

[Arnaud Charlet]

This patch makes the missing return statement illegal in GNATprove
mode as required by official SPARK 2014 syntax/semantics. The
following program is compiled with -gnatd.F

     1. package Various is
     2.    subtype Index_Type is
     3.      Positive range 1 .. 10;
     4.    type Integer_Array is
     5.      array (Index_Type) of Integer;
     6.    function Search_For_Zero
     7.      (Values : Integer_Array) return Index_Type;
     8. end Various;

     1. package body Various is
     2.    function Search_For_Zero
     3.      (Values : Integer_Array) return Index_Type
     4.    is
     5.    begin
     6.       for J in Values'Range loop
                                    |
        >>> "return" statement missing following this statement

     7.          if Values(J) = 0 then
     8.             return J;
     9.          end if;
    10.       end loop;
    11.    end Search_For_Zero;

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-01-20  Robert Dewar  <dewar@adacore.com>

	* errout.ads, errout.adb: Implement >? >x? >X? sequences in error
	messages.
	* sem_ch6.adb (Check_Statement_Sequence): Missing return is an
	error in GNATprove mode.

-------------- next part --------------
Index: errout.adb
===================================================================
--- errout.adb	(revision 206837)
+++ errout.adb	(working copy)
@@ -2713,7 +2713,8 @@
       P : Natural;     -- Current index;
 
       procedure Set_Msg_Insertion_Warning;
-      --  Deal with ? ?? ?x? ?X? insertion sequences
+      --  Deal with ? ?? ?x? ?X? insertion sequences (also < <? <x? <X?). The
+      --  caller has already bumped the pointer past the initial ? or <.
 
       -------------------------------
       -- Set_Msg_Insertion_Warning --
@@ -2819,14 +2820,12 @@
 
             when '<' =>
 
-               --  If tagging of messages is enabled, and this is a warning,
-               --  then it is treated as being [enabled by default].
+               --  Note: the prescan already set Is_Warning_Msg True if and
+               --  only if Error_Msg_Warn is set to True. If Error_Msg_Warn
+               --  is False, the call to Set_Msg_Insertion_Warning here does
+               --  no harm, since Warning_Msg_Char is ignored in that case.
 
-               if Error_Msg_Warn
-                 and Warning_Doc_Switch
-               then
-                  Warning_Msg_Char := '?';
-               end if;
+               Set_Msg_Insertion_Warning;
 
             when '|' =>
                null; -- already dealt with
Index: errout.ads
===================================================================
--- errout.ads	(revision 206809)
+++ errout.ads	(working copy)
@@ -64,7 +64,6 @@
    --  are active (see errout.ads for details). If this switch is False, then
    --  these sequences are ignored (i.e. simply equivalent to a single ?). The
    --  -gnatw.d switch sets this flag True, -gnatw.D sets this flag False.
-   --  Note: always ignored in VMS mode where we do not provide this feature.
 
    -----------------------------------
    -- Suppression of Error Messages --
@@ -305,8 +304,10 @@
    --    Insertion character < (Less Than: conditional warning message)
    --      The character < appearing anywhere in a message is used for a
    --      conditional error message. If Error_Msg_Warn is True, then the
-   --      effect is the same as ? described above. If Error_Msg_Warn is
-   --      False, then there is no effect.
+   --      effect is the same as ? described above, and in particular <? and
+   --      <X? have the effect of ?? and ?X? respectively. If Error_Msg_Warn
+   --      is False, then the < <? or <X? sequence is ignored and the message
+   --      is treated as a error rather than a warning.
 
    --    Insertion character A-Z (Upper case letter: Ada reserved word)
    --      If two or more upper case letters appear in the message, they are
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 206827)
+++ sem_ch6.adb	(working copy)
@@ -7222,12 +7222,24 @@
 
          if Mode = 'F' then
             if not Raise_Exception_Call then
-               Error_Msg_N
-                 ("RETURN statement missing following this statement??!",
-                  Last_Stm);
-               Error_Msg_N
-                 ("\Program_Error may be raised at run time??!",
-                  Last_Stm);
+
+               --  In GNATprove mode, it is an error to have a missing return
+
+               if GNATprove_Mode then
+                  Error_Msg_N
+                    ("RETURN statement missing following this statement!",
+                     Last_Stm);
+
+               --  Otherwise normal case of warning (RM insists this is legal)
+
+               else
+                  Error_Msg_N
+                    ("RETURN statement missing following this statement??!",
+                     Last_Stm);
+                  Error_Msg_N
+                    ("\Program_Error may be raised at run time??!",
+                     Last_Stm);
+               end if;
             end if;
 
             --  Note: we set Err even though we have not issued a warning