diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-04-27 15:22:35 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-04-27 15:22:35 +0200 |
| commit | bfc37f375f608454f7ee960b40ee7d6eefb14f3d (patch) | |
| tree | 210ef3038dbcebc06fa981634abf2c43db15e559 | |
| parent | 9dd8f36f2310db400fde9ca4b55ebb7791f50ec0 (diff) | |
| download | gcc-bfc37f375f608454f7ee960b40ee7d6eefb14f3d.zip gcc-bfc37f375f608454f7ee960b40ee7d6eefb14f3d.tar.gz gcc-bfc37f375f608454f7ee960b40ee7d6eefb14f3d.tar.bz2 | |
[multiple changes]
2017-04-27 Yannick Moy <moy@adacore.com>
* gnat1drv.adb (Adjust_Global_Switches): Issue
a warning in GNATprove mode if the runtime library does not
support IEEE-754 floats.
2017-04-27 Ed Schonberg <schonberg@adacore.com>
* sem_prag.adb (Inherit_Class_Wide_Pre): If the parent operation
is itself inherited it does not carry any contract information,
so examine its parent operation which is its Alias.
From-SVN: r247332
| -rw-r--r-- | gcc/ada/ChangeLog | 12 | ||||
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 24 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 7 |
3 files changed, 41 insertions, 2 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6a32381..7c4293d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,15 @@ +2017-04-27 Yannick Moy <moy@adacore.com> + + * gnat1drv.adb (Adjust_Global_Switches): Issue + a warning in GNATprove mode if the runtime library does not + support IEEE-754 floats. + +2017-04-27 Ed Schonberg <schonberg@adacore.com> + + * sem_prag.adb (Inherit_Class_Wide_Pre): If the parent operation + is itself inherited it does not carry any contract information, + so examine its parent operation which is its Alias. + 2017-04-27 Ed Schonberg <schonberg@adacore.com> * sem_attr.adb (Analyze_Attribute, case 'Image): In Ada2012 the diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 14bf6e3..863f227 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -496,6 +496,30 @@ procedure Gnat1drv is -- which is more complex to formally verify than the original source. Tagged_Type_Expansion := False; + + -- Detect that the runtime library support for floating-point numbers + -- may not be compatible with SPARK analysis of IEEE-754 floats. + + if Denorm_On_Target = False then + Write_Line + ("warning: Run-time library may be configured incorrectly"); + Write_Line + ("warning: " + & "(SPARK analysis requires support for float subnormals)"); + + elsif Machine_Rounds_On_Target = False then + Write_Line + ("warning: Run-time library may be configured incorrectly"); + Write_Line + ("warning: " + & "(SPARK analysis requires support for float rounding)"); + + elsif Signed_Zeros_On_Target = False then + Write_Line + ("warning: Run-time library may be configured incorrectly"); + Write_Line + ("warning: (SPARK analysis requires support for signed zeros)"); + end if; end if; -- Set Configurable_Run_Time mode if system.ads flag set or if the diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index e4efaab..5e90f7b 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -4232,9 +4232,12 @@ package body Sem_Prag is -- For a type derived from a generic formal type, the operation -- inheriting the condition is a renaming, not an overriding of - -- the operation of the formal. + -- the operation of the formal. Ditto for an inherited + -- operation which has no explicit contracts. - if Is_Generic_Type (Find_Dispatching_Type (Prev)) then + if Is_Generic_Type (Find_Dispatching_Type (Prev)) + or else not Comes_From_Source (Prev) + then Prev := Alias (Prev); else Prev := Overridden_Operation (Prev); |