This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
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.
Attachment:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |