[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
This commit is contained in:
parent
b7db11490f
commit
e5cabfacf0
|
@ -1,3 +1,24 @@
|
|||
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
|
||||
|
|
|
@ -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 --
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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;
|
||||
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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)
|
||||
|
|
Loading…
Reference in New Issue