+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
-- --
-- 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- --
-- --
------------------------------------------------------------------------------
-package body Ada.Assertions is
+package body Ada.Assertions with
+ SPARK_Mode
+is
------------
-- Assert --
-- --
-- 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.
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;
-- 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;
-- 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
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;
-- --
-- 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- --
-- 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);
-- --
-- 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- --
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)
projects / gcc.git / commitdiff