From: Arnaud Charlet <charlet@gcc.gnu.org>
Date: Thu, 27 Apr 2017 13:22:35 +0000 (+0200)
Subject: [multiple changes]
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bfc37f375f608454f7ee960b40ee7d6eefb14f3d;p=gcc.git

[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 6a32381ed3b..7c4293d27c6 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 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);