From e5cabfacf0240d107d986831cd13a63777c34a12 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 30 Jan 2015 16:25:38 +0100 Subject: [PATCH] [multiple changes] 2015-01-30 Robert Dewar * 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 * 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 * a-assert.ads, a-assert.adb: Mark package spec in SPARK. Set assertion policy for Pre to Ignore. (Assert): Add precondition. From-SVN: r220288 --- gcc/ada/ChangeLog | 21 +++++++++++++++++++++ gcc/ada/a-assert.adb | 6 ++++-- gcc/ada/a-assert.ads | 42 ++++++++++++++++++++++++++++++++++++------ gcc/ada/einfo.ads | 4 ++-- gcc/ada/freeze.adb | 38 ++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_res.ads | 4 ++-- gcc/ada/sem_type.adb | 4 +++- 7 files changed, 106 insertions(+), 13 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f9cbac4c1c1..f748f63273b 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,24 @@ +2015-01-30 Robert Dewar + + * 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 + + * 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 + + * 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 * sem_prag.adb (Process_Import_Or_Interface): Warn if used in diff --git a/gcc/ada/a-assert.adb b/gcc/ada/a-assert.adb index 9a03c815b0f..54b84b4e750 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 232201b157d..d0ce6f08316 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 -- +-- . -- +-- -- +-- 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 0c9fb61c917..ae714da56d3 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 3c88297aae9..2864fb1e6b9 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 42b819186dc..e94c36bbb1f 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 9b9034a74b0..a985008f51b 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) -- 2.30.2