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