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 <de...@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.
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
