From 52a59c8266404bfa57926834031613686088260f Mon Sep 17 00:00:00 2001 From: charlet Date: Thu, 27 Apr 2017 13:22:35 +0000 Subject: [PATCH] 2017-04-27 Yannick Moy * 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 * 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. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@247332 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/ChangeLog | 12 ++++++++++++ gcc/ada/gnat1drv.adb | 24 ++++++++++++++++++++++++ gcc/ada/sem_prag.adb | 7 +++++-- 3 files changed, 41 insertions(+), 2 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6a32381ed3b..7c4293d27c6 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,15 @@ +2017-04-27 Yannick Moy + + * 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 + + * 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 * sem_attr.adb (Analyze_Attribute, case 'Image): In Ada2012 the diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 14bf6e37fe0..863f227bb08 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 e4efaabeb44..5e90f7b15a0 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); -- 2.11.4.GIT