[multiple changes]

2015-01-30  Robert Dewar  <dewar@adacore.com>

	* einfo.ads: Minor comment fix.
	* freeze.adb (Freeze_Profile): Add test for suspicious import
	in pure unit.
	* sem_prag.adb (Process_Import_Or_Interface): Test for suspicious
	use in Pure unit is now moved to Freeze (to properly catch
	Pure_Function exemption).

2015-01-30  Bob Duff  <duff@adacore.com>

	* sem_res.ads: Minor comment fix.
	* sem_type.adb: sem_type.adb (Remove_Conversions): Need to
	check both operands of an operator.

2015-01-30  Yannick Moy  <moy@adacore.com>

	* a-assert.ads, a-assert.adb: Mark package spec in SPARK. Set assertion
	policy for Pre to Ignore.
	(Assert): Add precondition.

From-SVN: r220288

7 files changed, 106 insertions, 13 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f9cbac4..f748f63 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,26 @@
 2015-01-30  Robert Dewar  <dewar@adacore.com>
 
+	* einfo.ads: Minor comment fix.
+	* freeze.adb (Freeze_Profile): Add test for suspicious import
+	in pure unit.
+	* sem_prag.adb (Process_Import_Or_Interface): Test for suspicious
+	use in Pure unit is now moved to Freeze (to properly catch
+	Pure_Function exemption).
+
+2015-01-30  Bob Duff  <duff@adacore.com>
+
+	* sem_res.ads: Minor comment fix.
+	* sem_type.adb: sem_type.adb (Remove_Conversions): Need to
+	check both operands of an operator.
+
+2015-01-30  Yannick Moy  <moy@adacore.com>
+
+	* a-assert.ads, a-assert.adb: Mark package spec in SPARK. Set assertion
+	policy for Pre to Ignore.
+	(Assert): Add precondition.
+
+2015-01-30  Robert Dewar  <dewar@adacore.com>
+
 	* sem_prag.adb (Process_Import_Or_Interface): Warn if used in
 	Pure unit.
 	* s-valllu.ads (Scan_Raw_Long_Long_Unsigned): Clarify
diff --git a/gcc/ada/a-assert.adb b/gcc/ada/a-assert.adb
index 9a03c81..54b84b4 100644
--- a/gcc/ada/a-assert.adb
+++ b/gcc/ada/a-assert.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---         Copyright (C) 2007-2012  Free Software Foundation, Inc.          --
+--         Copyright (C) 2007-2015, Free Software Foundation, Inc.          --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -29,7 +29,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package body Ada.Assertions is
+package body Ada.Assertions with
+  SPARK_Mode
+is
 
    ------------
    -- Assert --
diff --git a/gcc/ada/a-assert.ads b/gcc/ada/a-assert.ads
index 232201b..d0ce6f0 100644
--- a/gcc/ada/a-assert.ads
+++ b/gcc/ada/a-assert.ads
@@ -4,15 +4,41 @@
 --                                                                          --
 --                       A D A . A S S E R T I O N S                        --
 --                                                                          --
+--            Copyright (C) 2015, Free Software Foundation, Inc.            --
+--                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
--- GNAT.  In accordance with the copyright of that document, you can freely --
--- copy and modify this specification,  provided that if you redistribute a --
--- modified version,  any changes that you have made are clearly indicated. --
+-- GNAT. The copyright notice above, and the license provisions that follow --
+-- apply solely to the contracts that have been added.                      --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  Preconditions in this unit are meant for analysis only, not for run-time
+--  checking, so that the expected exceptions are raised when calling Assert.
+--  This is enforced by setting the corresponding assertion policy to Ignore.
+
+pragma Assertion_Policy (Pre => Ignore);
+
 --  We do a with of System.Assertions to get hold of the exception (following
 --  the specific RM permission that lets' Assertion_Error being a renaming).
 --  The suppression of Warnings stops the warning about bad categorization.
@@ -21,7 +47,9 @@ pragma Warnings (Off);
 with System.Assertions;
 pragma Warnings (On);
 
-package Ada.Assertions is
+package Ada.Assertions with
+  SPARK_Mode
+is
    pragma Pure (Assertions);
 
    Assertion_Error : exception renames System.Assertions.Assert_Failure;
@@ -29,8 +57,10 @@ package Ada.Assertions is
    --  Exception_Name will refer to the one in System.Assertions (see
    --  AARM-11.4.1(12.b)).
 
-   procedure Assert (Check : Boolean);
+   procedure Assert (Check : Boolean) with
+     Pre => Check;
 
-   procedure Assert (Check : Boolean; Message : String);
+   procedure Assert (Check : Boolean; Message : String) with
+     Pre => Check;
 
 end Ada.Assertions;
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 0c9fb61..ae714da5 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -2040,10 +2040,10 @@ package Einfo is
 
 --    Import_Pragma (Node35)
 --       Defined in subprogram entities. Set if a valid pragma Import or pragma
---       Import_Function or pragma Import_Procedure aplies to the subprogram,
+--       Import_Function or pragma Import_Procedure applies to the subprogram,
 --       in which case this field points to the pragma (we can't use the normal
 --       Rep_Item chain mechanism, because a single pragma Import can apply
---       to multiple subprogram entities.
+--       to multiple subprogram entities).
 
 --    In_Package_Body (Flag48)
 --       Defined in package entities. Set on the entity that denotes the
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 3c88297..2864fb1 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -3081,6 +3081,44 @@ package body Freeze is
             end if;
          end if;
 
+         --  Check suspicious use of Import in pure unit
+
+         if Is_Imported (E) and then Is_Pure (Cunit_Entity (Current_Sem_Unit))
+
+           --  Ignore internally generated entity. This happens in some cases
+           --  of subprograms in specs, where we generate an implied body.
+
+           and then Comes_From_Source (Import_Pragma (E))
+
+           --  Assume run-time knows what it is doing
+
+           and then not GNAT_Mode
+
+           --  Assume explicit Pure_Function means import is pure
+
+           and then not Has_Pragma_Pure_Function (E)
+
+           --  Don't need warning in relaxed semantics mode
+
+           and then not Relaxed_RM_Semantics
+
+           --  Assume convention Intrinsic is OK, since this is specialized.
+           --  This deals with the DEC unit current_exception.ads
+
+           and then Convention (E) /= Convention_Intrinsic
+
+            --  Assume that ASM interface knows what it is doing. This deals
+            --  with unsigned.ads in the AAMP back end.
+
+           and then Convention (E) /= Convention_Assembler
+         then
+            Error_Msg_N
+              ("pragma Import in Pure unit??", Import_Pragma (E));
+            Error_Msg_NE
+              ("\calls to & may be omitted (RM 10.2.1(18/3))??",
+               Import_Pragma (E), E);
+         end if;
+
          return True;
       end Freeze_Profile;
 
diff --git a/gcc/ada/sem_res.ads b/gcc/ada/sem_res.ads
index 42b8191..e94c36b 100644
--- a/gcc/ada/sem_res.ads
+++ b/gcc/ada/sem_res.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -45,7 +45,7 @@ package Sem_Res is
    --  Since in practice a lot of semantic analysis has to be postponed until
    --  types are known (e.g. static folding, setting of suppress flags), the
    --  Resolve routines also complete the semantic analysis, and call the
-   --  expander for possibly expansion of the completely type resolved node.
+   --  expander for possible expansion of the completely type resolved node.
 
    procedure Resolve (N : Node_Id; Typ : Entity_Id);
    procedure Resolve (N : Node_Id; Typ : Entity_Id; Suppress : Check_Id);
diff --git a/gcc/ada/sem_type.adb b/gcc/ada/sem_type.adb
index 9b9034a..a985008 100644
--- a/gcc/ada/sem_type.adb
+++ b/gcc/ada/sem_type.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -1539,6 +1539,8 @@ package body Sem_Type is
 
                if Nkind (Act1) in N_Op
                  and then Is_Overloaded (Act1)
+                 and then Nkind_In (Left_Opnd (Act1), N_Integer_Literal,
+                                                      N_Real_Literal)
                  and then Nkind_In (Right_Opnd (Act1), N_Integer_Literal,
                                                        N_Real_Literal)
                  and then Has_Compatible_Type (Act1, Standard_Boolean)