diff options
| author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2014-01-20 16:10:53 +0000 |
|---|---|---|
| committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2014-01-20 16:10:53 +0000 |
| commit | c4968aa29cbc07d8d8135459bd628af4144d8adb (patch) | |
| tree | de2038d9772868c26e4ecc32ab0ca7550e3d1447 /gcc/ada/opt.adb | |
| parent | 99971aaa7d0882f454a54e8c73ec50e8e69aee63 (diff) | |
| download | gcc-c4968aa29cbc07d8d8135459bd628af4144d8adb.tar.gz | |
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
2014-01-20 Ed Schonberg <schonberg@adacore.com>
* sem_ch13.adb: Add semantic information to rewritten type
reference.
2014-01-20 Ed Schonberg <schonberg@adacore.com>
* exp_ch5.adb (Expand_N_Assignment_Statement): If both sides
are of a type with unknown discriminants, convert both to the
underlying view of the type, so that the proper constraint check
can be applied to the right-hand side.
2014-01-20 Robert Dewar <dewar@adacore.com>
* atree.adb (Copy_Node): Fix failure to copy last component
(Exchange_Entities): Fix failure to exchange last entity
2014-01-20 Ed Schonberg <schonberg@adacore.com>
* sem_ch12.adb: Code clean up.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@206844 138bc75d-0d04-0410-961f-82ee72b054a4
Diffstat (limited to 'gcc/ada/opt.adb')
| -rw-r--r-- | gcc/ada/opt.adb | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb index 0f65614811b..ce23faacaab 100644 --- a/gcc/ada/opt.adb +++ b/gcc/ada/opt.adb @@ -63,6 +63,7 @@ package body Opt is Persistent_BSS_Mode_Config := Persistent_BSS_Mode; Polling_Required_Config := Polling_Required; Short_Descriptors_Config := Short_Descriptors; + SPARK_Mode_Config := SPARK_Mode; Use_VADS_Size_Config := Use_VADS_Size; -- Reset the indication that Optimize_Alignment was set locally, since @@ -98,6 +99,7 @@ package body Opt is Persistent_BSS_Mode := Save.Persistent_BSS_Mode; Polling_Required := Save.Polling_Required; Short_Descriptors := Save.Short_Descriptors; + SPARK_Mode := Save.SPARK_Mode; Use_VADS_Size := Save.Use_VADS_Size; -- Update consistently the value of Init_Or_Norm_Scalars. The value of @@ -134,6 +136,7 @@ package body Opt is Save.Persistent_BSS_Mode := Persistent_BSS_Mode; Save.Polling_Required := Polling_Required; Save.Short_Descriptors := Short_Descriptors; + Save.SPARK_Mode := SPARK_Mode; Save.Use_VADS_Size := Use_VADS_Size; end Save_Opt_Config_Switches; @@ -164,6 +167,7 @@ package body Opt is Persistent_BSS_Mode := False; Use_VADS_Size := False; Optimize_Alignment_Local := True; + SPARK_Mode := Auto; -- For an internal unit, assertions/debug pragmas are off unless this -- is the main unit and they were explicitly enabled. We also make @@ -198,6 +202,7 @@ package body Opt is Optimize_Alignment := Optimize_Alignment_Config; Optimize_Alignment_Local := False; Persistent_BSS_Mode := Persistent_BSS_Mode_Config; + SPARK_Mode := SPARK_Mode_Config; Use_VADS_Size := Use_VADS_Size_Config; -- Update consistently the value of Init_Or_Norm_Scalars. The value |