From 643d4979f0d04d35acbea16b5c9f704616b204dc Mon Sep 17 00:00:00 2001 From: charlet Date: Fri, 30 Jan 2015 15:25:38 +0000 Subject: [PATCH] 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. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@220288 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/ChangeLog | 21 ++++++++++++ gcc/ada/a-assert.adb | 6 ++-- gcc/ada/{a-assert.adb => a-assert.ads} | 60 +++++++++++++++++++++------------- 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, 107 insertions(+), 30 deletions(-) copy gcc/ada/{a-assert.adb => a-assert.ads} (58%) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f9cbac4c1c1..f748f63273b 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,26 @@ 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 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 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.adb b/gcc/ada/a-assert.ads similarity index 58% copy from gcc/ada/a-assert.adb copy to gcc/ada/a-assert.ads index 9a03c815b0f..d0ce6f08316 100644 --- a/gcc/ada/a-assert.adb +++ b/gcc/ada/a-assert.ads @@ -2,11 +2,15 @@ -- -- -- GNAT RUN-TIME COMPONENTS -- -- -- --- A D A . A S S E R T -- +-- A D A . A S S E R T I O N S -- -- -- --- B o d y -- +-- Copyright (C) 2015, Free Software Foundation, Inc. -- -- -- --- Copyright (C) 2007-2012 Free Software Foundation, Inc. -- +-- S p e c -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- 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- -- @@ -25,28 +29,38 @@ -- . -- -- -- -- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- -- -- ------------------------------------------------------------------------------ -package body Ada.Assertions is - - ------------ - -- Assert -- - ------------ - - procedure Assert (Check : Boolean) is - begin - if Check = False then - raise Ada.Assertions.Assertion_Error; - end if; - end Assert; - - procedure Assert (Check : Boolean; Message : String) is - begin - if Check = False then - raise Ada.Assertions.Assertion_Error with Message; - end if; - end Assert; +-- 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. + +pragma Warnings (Off); +with System.Assertions; +pragma Warnings (On); + +package Ada.Assertions with + SPARK_Mode +is + pragma Pure (Assertions); + + Assertion_Error : exception renames System.Assertions.Assert_Failure; + -- This is the renaming that is allowed by 11.4.2(24). Note that the + -- Exception_Name will refer to the one in System.Assertions (see + -- AARM-11.4.1(12.b)). + + procedure Assert (Check : Boolean) with + Pre => Check; + + 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.11.4.GIT