mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-03-22 07:00:29 +08:00
Code Issues Packages Projects Releases Wiki Activity

[multiple changes]

Browse Source 
2015-03-13  Claire Dross  <dross@adacore.com>

	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline
	subprograms with unconstrained record parameters containing
	Itype declarations.
	* sinfo.ads Document GNATprove assumption that type should match
	in the AST.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract):
	Do not check for Refined_Depends and Refined_Globals contracts
	as they are optional.

2015-03-13  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch12.adb (Instantiate_Type): For a floating-point type,
	capture dimension info if any, because the generated subtype
	declaration does not come from source and will not process dimensions.
	* sem_dim,adb (Analyze_Dimension_Extension_Or_Record_Aggregate):
	Do not analyze expressions with an initialization procedure
	because aggregates will have been checked at the point of record
	declaration.

2015-03-13  Robert Dewar  <dewar@adacore.com>

	* aspects.ads, aspects.adb: Add entries for aspect Unimplemented.
	* einfo.ads, einfo.adb (Is_Unimplemented): New flag.
	* sem_ch13.adb: Add dummy entry for aspect Unimplemented.
	* snames.ads-tmpl: Add entry for Name_Unimplemented.

From-SVN: r221420
This commit is contained in:
Arnaud Charlet 2015-03-13 14:28:15 +01:00
parent 9fc0f6728d
commit d3ef4bd61f
12 changed files with 176 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
gcc/ada/ChangeLog
View File

@ -1,3 +1,31 @@
2015-03-13 Claire Dross <dross@adacore.com>
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline
subprograms with unconstrained record parameters containing
Itype declarations.
* sinfo.ads Document GNATprove assumption that type should match
in the AST.
* sem_ch6.adb (Analyze_Subprogram_Body_Contract):
Do not check for Refined_Depends and Refined_Globals contracts
as they are optional.
2015-03-13 Ed Schonberg <schonberg@adacore.com>
* sem_ch12.adb (Instantiate_Type): For a floating-point type,
capture dimension info if any, because the generated subtype
declaration does not come from source and will not process dimensions.
* sem_dim,adb (Analyze_Dimension_Extension_Or_Record_Aggregate):
Do not analyze expressions with an initialization procedure
because aggregates will have been checked at the point of record
declaration.
2015-03-13 Robert Dewar <dewar@adacore.com>
* aspects.ads, aspects.adb: Add entries for aspect Unimplemented.
* einfo.ads, einfo.adb (Is_Unimplemented): New flag.
* sem_ch13.adb: Add dummy entry for aspect Unimplemented.
* snames.ads-tmpl: Add entry for Name_Unimplemented.
2015-03-13 Gary Dismukes <dismukes@adacore.com>
* style.adb (Missing_Overriding): Apply the

3
gcc/ada/aspects.adb
View File

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2010-2014, Free Software Foundation, Inc. --
-- Copyright (C) 2010-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- --
@ -595,6 +595,7 @@ package body Aspects is
Aspect_Thread_Local_Storage => Aspect_Thread_Local_Storage,
Aspect_Type_Invariant => Aspect_Invariant,
Aspect_Unchecked_Union => Aspect_Unchecked_Union,
Aspect_Unimplemented => Aspect_Unimplemented,
Aspect_Universal_Aliasing => Aspect_Universal_Aliasing,
Aspect_Universal_Data => Aspect_Universal_Data,
Aspect_Unmodified => Aspect_Unmodified,

6
gcc/ada/aspects.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2010-2014, Free Software Foundation, Inc. --
-- Copyright (C) 2010-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- --
@ -140,6 +140,7 @@ package Aspects is
Aspect_Synchronization,
Aspect_Test_Case, -- GNAT
Aspect_Type_Invariant,
Aspect_Unimplemented, -- GNAT
Aspect_Unsuppress,
Aspect_Value_Size, -- GNAT
Aspect_Variable_Indexing,
@ -369,6 +370,7 @@ package Aspects is
Aspect_Synchronization => Name,
Aspect_Test_Case => Expression,
Aspect_Type_Invariant => Expression,
Aspect_Unimplemented => Optional_Expression,
Aspect_Unsuppress => Name,
Aspect_Value_Size => Expression,
Aspect_Variable_Indexing => Name,
@ -490,6 +492,7 @@ package Aspects is
Aspect_Test_Case => Name_Test_Case,
Aspect_Type_Invariant => Name_Type_Invariant,
Aspect_Unchecked_Union => Name_Unchecked_Union,
Aspect_Unimplemented => Name_Unimplemented,
Aspect_Universal_Aliasing => Name_Universal_Aliasing,
Aspect_Universal_Data => Name_Universal_Data,
Aspect_Unmodified => Name_Unmodified,
@ -717,6 +720,7 @@ package Aspects is
Aspect_SPARK_Mode => Never_Delay,
Aspect_Synchronization => Never_Delay,
Aspect_Test_Case => Never_Delay,
Aspect_Unimplemented => Never_Delay,
Aspect_Warnings => Never_Delay,
Aspect_Alignment => Rep_Aspect,

13
gcc/ada/einfo.adb
View File

@ -584,8 +584,8 @@ package body Einfo is
-- Is_Static_Type Flag281
-- Has_Nested_Subprogram Flag282
-- Uplevel_Reference_Noted Flag283
-- Is_Unimplemented Flag284
-- (unused) Flag284
-- (unused) Flag285
-- (unused) Flag286
-- (unused) Flag287
@ -2456,6 +2456,11 @@ package body Einfo is
return Flag246 (Id);
end Is_Underlying_Record_View;
function Is_Unimplemented (Id : E) return B is
begin
return Flag284 (Id);
end Is_Unimplemented;
function Is_Unsigned_Type (Id : E) return B is
begin
pragma Assert (Is_Type (Id));
@ -5398,6 +5403,11 @@ package body Einfo is
Set_Flag246 (Id, V);
end Set_Is_Underlying_Record_View;
procedure Set_Is_Unimplemented (Id : E; V : B := True) is
begin
Set_Flag284 (Id, V);
end Set_Is_Unimplemented;
procedure Set_Is_Unsigned_Type (Id : E; V : B := True) is
begin
pragma Assert (Is_Discrete_Or_Fixed_Point_Type (Id));
@ -8767,6 +8777,7 @@ package body Einfo is
W ("Is_True_Constant", Flag163 (Id));
W ("Is_Unchecked_Union", Flag117 (Id));
W ("Is_Underlying_Record_View", Flag246 (Id));
W ("Is_Unimplemented", Flag284 (Id));
W ("Is_Unsigned_Type", Flag144 (Id));
W ("Is_Valued_Procedure", Flag127 (Id));
W ("Is_Visible_Formal", Flag206 (Id));

16
gcc/ada/einfo.ads
View File

@ -2745,8 +2745,8 @@ package Einfo is
-- including generic formal parameters.
-- Is_Obsolescent (Flag153)
-- Defined in all entities. Set for any entity for which a valid pragma
-- Obsolescent applies.
-- Defined in all entities. Set for any entity to which a valid pragma
-- or aspect Obsolescent applies.
-- Is_Only_Out_Parameter (Flag226)
-- Defined in formal parameter entities. Set if this parameter is the
@ -3090,6 +3090,10 @@ package Einfo is
-- as its corresponding record type, but whose parent is the full view
-- of the parent in the original type extension.
-- Is_Unimplemented (Flag284)
-- Defined in all entities. Set for any entity to which a valid pragma
-- or aspect Unimplemented applies.
-- Is_Unsigned_Type (Flag144)
-- Defined in all types, but can be set only for discrete and fixed-point
-- type and subtype entities. This flag is only valid if the entity is
@ -5299,6 +5303,7 @@ package Einfo is
-- Is_Thunk (Flag225)
-- Is_Trivial_Subprogram (Flag235)
-- Is_Unchecked_Union (Flag117)
-- Is_Unimplemented (Flag284)
-- Is_Visible_Formal (Flag206)
-- Kill_Elaboration_Checks (Flag32)
-- Kill_Range_Checks (Flag33)
@ -5784,6 +5789,7 @@ package Einfo is
-- SPARK_Pragma (Node32)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Import_Pragma (Node35) (non-generic case only)
-- Body_Needed_For_SAL (Flag40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Default_Expressions_Processed (Flag108)
@ -5951,6 +5957,7 @@ package Einfo is
-- Subprograms_For_Type (Node29)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Import_Pragma (Node35)
-- Has_Invariants (Flag232)
-- Is_Machine_Code_Subprogram (Flag137)
-- Is_Pure (Flag44)
@ -6089,6 +6096,7 @@ package Einfo is
-- SPARK_Pragma (Node32)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Import_Pragma (Node35) (non-generic case only)
-- Body_Needed_For_SAL (Flag40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Cleanups (Flag114)
@ -6894,6 +6902,7 @@ package Einfo is
function Is_True_Constant (Id : E) return B;
function Is_Unchecked_Union (Id : E) return B;
function Is_Underlying_Record_View (Id : E) return B;
function Is_Unimplemented (Id : E) return B;
function Is_Unsigned_Type (Id : E) return B;
function Is_Valued_Procedure (Id : E) return B;
function Is_Visible_Formal (Id : E) return B;
@ -7548,6 +7557,7 @@ package Einfo is
procedure Set_Is_True_Constant (Id : E; V : B := True);
procedure Set_Is_Unchecked_Union (Id : E; V : B := True);
procedure Set_Is_Underlying_Record_View (Id : E; V : B := True);
procedure Set_Is_Unimplemented (Id : E; V : B := True);
procedure Set_Is_Unsigned_Type (Id : E; V : B := True);
procedure Set_Is_Valued_Procedure (Id : E; V : B := True);
procedure Set_Is_Visible_Formal (Id : E; V : B := True);
@ -8352,6 +8362,7 @@ package Einfo is
pragma Inline (Is_Type);
pragma Inline (Is_Unchecked_Union);
pragma Inline (Is_Underlying_Record_View);
pragma Inline (Is_Unimplemented);
pragma Inline (Is_Unsigned_Type);
pragma Inline (Is_Valued_Procedure);
pragma Inline (Is_Visible_Formal);
@ -8807,6 +8818,7 @@ package Einfo is
pragma Inline (Set_Is_True_Constant);
pragma Inline (Set_Is_Unchecked_Union);
pragma Inline (Set_Is_Underlying_Record_View);
pragma Inline (Set_Is_Unimplemented);
pragma Inline (Set_Is_Unsigned_Type);
pragma Inline (Set_Is_Valued_Procedure);
pragma Inline (Set_Is_Visible_Formal);

83
gcc/ada/inline.adb
View File

@ -1335,6 +1335,11 @@ package body Inline is
(Spec_Id : Entity_Id;
Body_Id : Entity_Id) return Boolean
is
function Has_Parameter_With_Discriminant_Dependent_Fields
(Id : Entity_Id) return Boolean;
-- Returns true if the subprogram as parameters of an unconstrained
-- record types with fields whose types depend on a discriminant.
function Has_Some_Contract (Id : Entity_Id) return Boolean;
-- Returns True if subprogram Id has any contract (Pre, Post, Global,
-- Depends, etc.)
@ -1351,6 +1356,73 @@ package body Inline is
-- Returns True if subprogram Id was defined originally as an expression
-- function.
------------------------------------------------------
-- Has_Parameter_With_Discriminant_Dependent_Fields --
------------------------------------------------------
function Has_Parameter_With_Discriminant_Dependent_Fields
(Id : Entity_Id) return Boolean
is
E : Entity_Id := Id;
Spec : Node_Id := Parent (E);
begin
-- Get the specification of the subprogram. Go through alias if
-- needed.
if Nkind (Spec) = N_Defining_Program_Unit_Name then
Spec := Parent (Spec);
end if;
while Nkind (Spec) not in N_Subprogram_Specification loop
pragma Assert (Present (Alias (E)));
E := Alias (E);
Spec := Parent (E);
if Nkind (Spec) = N_Defining_Program_Unit_Name then
Spec := Parent (Spec);
end if;
end loop;
declare
Params : constant List_Id := Parameter_Specifications (Spec);
Param : Node_Id;
Param_Ty : Entity_Id;
begin
if Is_Non_Empty_List (Params) then
Param := First (Params);
while Present (Param) loop
Param_Ty := Etype (Defining_Identifier (Param));
-- If the parameter is an unconstrained record, check if
-- it has components whose types depend on a discriminant.
if Is_Record_Type (Param_Ty)
and then not Is_Constrained (Param_Ty)
then
declare
Comp : Node_Id := First_Component (Param_Ty);
begin
while Present (Comp) loop
if Has_Discriminant_Dependent_Constraint (Comp) then
return True;
end if;
Comp := Next_Component (Comp);
end loop;
end;
end if;
Param := Next (Param);
end loop;
end if;
end;
return False;
end Has_Parameter_With_Discriminant_Dependent_Fields;
-----------------------
-- Has_Some_Contract --
-----------------------
@ -1497,11 +1569,20 @@ package body Inline is
elsif Instantiation_Location (Sloc (Id)) /= No_Location then
return False;
-- Don't inline predicate functions (treated specially by GNATprove)
-- Do not inline predicate functions (treated specially by GNATprove)
elsif Is_Predicate_Function (Id) then
return False;
-- Do not inline subprograms with a parameter of an unconstrained
-- record type if it has discrimiant dependent fields. Indeed, with
-- such parameters, the frontend cannot always ensure type compliance
-- in record component accesses (in particular with records containing
-- packed arrays).
elsif Has_Parameter_With_Discriminant_Dependent_Fields (Id) then
return False;
-- Otherwise, this is a subprogram declared inside the private part of a
-- package, or inside a package body, or locally in a subprogram, and it
-- does not have any contract. Inline it.

8
gcc/ada/sem_ch12.adb
View File

@ -12456,6 +12456,14 @@ package body Sem_Ch12 is
end;
end if;
-- For a floating-point type, capture dimension info if any, because
-- the generated subtype declaration does not come from source and
-- will not process dimensions.
if Is_Floating_Point_Type (Act_T) then
Copy_Dimensions (Act_T, Subt);
end if;
return Decl_Nodes;
end Instantiate_Type;

5
gcc/ada/sem_ch13.adb
View File

@ -1642,6 +1642,8 @@ package body Sem_Ch13 is
-- Processing based on specific aspect
case A_Id is
when Aspect_Unimplemented =>
null; -- ??? temp for now
-- No_Aspect should be impossible
@ -9024,7 +9026,8 @@ package body Sem_Ch13 is
Aspect_Refined_Post |
Aspect_Refined_State |
Aspect_SPARK_Mode |
Aspect_Test_Case =>
Aspect_Test_Case |
Aspect_Unimplemented =>
raise Program_Error;
end case;

32
gcc/ada/sem_ch6.adb
View File

@ -2203,22 +2203,6 @@ package body Sem_Ch6 is
if Present (Ref_Global) then
Analyze_Refined_Global_In_Decl_Part (Ref_Global);
-- When the corresponding Global pragma references a state with
-- visible refinement, the body requires Refined_Global. Such a
-- refinement is not required when SPARK checks are suppressed.
else
Prag := Get_Pragma (Spec_Id, Pragma_Global);
if SPARK_Mode /= Off
and then Present (Prag)
and then Contains_Refined_State (Prag)
then
Error_Msg_NE
("body of subprogram& requires global refinement",
Body_Decl, Spec_Id);
end if;
end if;
-- Refined_Depends must be analyzed after Refined_Global in order to
@ -2226,22 +2210,6 @@ package body Sem_Ch6 is
if Present (Ref_Depends) then
Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
-- When the corresponding Depends pragma references a state with
-- visible refinement, the body requires Refined_Depends. Such a
-- refinement is not required when SPARK checks are suppressed.
else
Prag := Get_Pragma (Spec_Id, Pragma_Depends);
if SPARK_Mode /= Off
and then Present (Prag)
and then Contains_Refined_State (Prag)
then
Error_Msg_NE
("body of subprogram& requires dependance refinement",
Body_Decl, Spec_Id);
end if;
end if;
end Analyze_Completion_Contract;

12
gcc/ada/sem_dim.adb
View File

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2011-2014, Free Software Foundation, Inc. --
-- Copyright (C) 2011-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- --
@ -27,6 +27,7 @@ with Aspects; use Aspects;
with Atree; use Atree;
with Einfo; use Einfo;
with Errout; use Errout;
with Exp_Util; use Exp_Util;
with Lib; use Lib;
with Namet; use Namet;
with Nlists; use Nlists;
@ -1792,9 +1793,14 @@ package body Sem_Dim is
begin
-- Aspect is an Ada 2012 feature. Note that there is no need to check
-- dimensions for aggregates that don't come from source.
-- dimensions for aggregates that don't come from source, or if we are
-- within an initialization procedure, whose expressions have been
-- checked at the point of record declaration.
if Ada_Version < Ada_2012 or else not Comes_From_Source (N) then
if Ada_Version < Ada_2012
or else not Comes_From_Source (N)
or else Inside_Init_Proc
then
return;
end if;

11
gcc/ada/sinfo.ads
View File

@ -617,6 +617,17 @@ package Sinfo is
-- checks on empty ranges, which typically appear in deactivated
-- code in a particular configuration).
-- 6. Subtypes should match in the AST, even after a generic is
-- instantiated. In particular, GNATprove relies on the fact that,
-- on a selected component, the type of the selected component is
-- the type of the corresponding component in the prefix of the
-- selected component.
--
-- Note that, in some cases, we know that this rule is broken by the
-- frontend. In particular, if the selected component is a packed
-- array depending on a discriminant of a unconstrained formal object
-- parameter of a generic.
-----------------------
-- Check Flag Fields --
-----------------------

1
gcc/ada/snames.ads-tmpl
View File

@ -144,6 +144,7 @@ package Snames is
Name_Dynamic_Predicate : constant Name_Id := N + $;
Name_Static_Predicate : constant Name_Id := N + $;
Name_Synchronization : constant Name_Id := N + $;
Name_Unimplemented : constant Name_Id := N + $;
-- Some special names used by the expander. Note that the lower case u's
-- at the start of these names get translated to extra underscores. These