[Ada] Test SPARK_Mode instead of GNATProve_Mode for warnings

[Arnaud Charlet <charlet at adacore dot com>]

This changes the handling of cases in which warnings are normally given
for constructs that are bound to raise run time exceptions if executed.
Previously we converted these to errors unconditionally in GNATProve
mode, but that caused trouble with non-SPARK code, notably s-scaval
from the run-time library.

With this patch, we now properly handle the setting of SPARK_Mode in
the front end, and these warnings are converted to errors only if we
have SPARK_Mode (On), as shown by the following test program:

     1. package SPMode is
     2.    pragma SPARK_Mode (ON);
     3.    X : Positive := 0; -- ERROR
                           |
        >>> value not in range of type "Standard.Positive"
        >>> "Constraint_Error" would have been raised at run time

     4.    procedure P1;
     5.    pragma SPARK_Mode (ON);
     6.    procedure P2;
     7.    procedure P3;
     8. private
     9.    pragma SPARK_Mode (OFF);
    10.    X1 : Positive := 0; -- WARNING
                            |
        >>> warning: value not in range of type "Standard.Positive"
        >>> warning: "Constraint_Error" will be raised at run time

    11. end;

     1. package body SPMode is
     2.    pragma SPARK_Mode (off);
     3.    Y : Positive := 0; -- WARNING
                           |
        >>> warning: value not in range of type "Standard.Positive"
        >>> warning: "Constraint_Error" will be raised at run time

     4.    procedure P1 is
     5.       P1P : Positive := 0; -- ERROR
                                |
        >>> value not in range of type "Standard.Positive"
        >>> "Constraint_Error" would have been raised at run time

     6.    begin
     7.       null;
     8.    end;
     9.    procedure P2 is
    10.       pragma SPARK_Mode (ON);
    11.       P2P : Positive := 0; -- ERROR
                                |
        >>> value not in range of type "Standard.Positive"
        >>> "Constraint_Error" would have been raised at run time

    12.    begin
    13.       null;
    14.    end;
    15.    procedure P3 is
    16.       P3P : Positive := 0; -- WARNING
                                |
        >>> warning: value not in range of type "Standard.Positive"
        >>> warning: "Constraint_Error" will be raised at run time

    17.    begin
    18.       null;
    19.    end;
    20. end;

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

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

	* checks.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* exp_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* opt.adb (SPARK_Mode_Config): Handled like other config flags
	* opt.ads (SPARK_Mode_Type): Moved here from types (renamed from
	SPARK_Mode_Id) (SPARK_Mode_Type): Add pragma Ordered, remove
	SPARK_ from names (SPARK_Mode): New flag (SPARK_Mode_Config):
	New flag (Config_Switches_Type): Add SPARK_Mode field
	* sem.adb: Minor code reorganization (remove unnecessary with)
	* sem.ads (Scope_Stack_Entry): Add Save_SPARK_Mode field
	* sem_aggr.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_attr.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_ch3.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Reset SPARK_Mode
	from spec if needed
	* sem_ch7.adb (Analyze_Package_Body_Helper): Reset SPARK_Mode
	from spec if needed
	* sem_ch8.adb (Push_Scope): Save SPARK_Mode (Pop_Scope):
	Restore SPARK_Mode
	* sem_elab.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_prag.adb (Get_SPARK_Mode_From_Pragma): New function
	(Get_SPARK_Mode_Id): Removed (Get_SPARK_Mode_Type): New name
	of Get_SPARK_Mode_Id
	* sem_prag.ads (Get_SPARK_Mode_From_Pragma): New function
	* sem_res.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_util.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* types.ads (SPARK_Mode_Id): Moved to opt.ads and renamed
	SPARK_Mode_Type

Attachment: difs
Description: Text document