mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-04-05 10:30:55 +08:00
Code Issues Packages Projects Releases Wiki Activity

[multiple changes]

Browse Source 
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
This commit is contained in:
Arnaud Charlet 2017-04-27 15:22:35 +02:00
parent 9dd8f36f23
commit bfc37f375f
3 changed files with 41 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
gcc/ada/ChangeLog
View File

@ -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

24
gcc/ada/gnat1drv.adb
View File

@ -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

7
gcc/ada/sem_prag.adb
View File

@ -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);