[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6a32381ed3b11d7452b1ba4cccaaccf7a6407795..7c4293d27c605db0be3b6e75d3f4386c34b4b622 100644 (file)
--- 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 14bf6e37fe09c282e6d113e9bb0a7f017eea68bf..863f227bb0834ff4a3885f2dd80d0b33ee73492d 100644 (file)
--- 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 e4efaabeb44e587b1a8d32dc862f715124be32bc..5e90f7b15a0cd9f8cab4ad2b1df6cf2d1489618e 100644 (file)
--- 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);