OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes]

Browse Source 
2017-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb Flag301 is now known as Ignore_SPARK_Mode_Pragmas.
	(Ignore_SPARK_Mode_Pragmas): New routine.
	(Set_Ignore_SPARK_Mode_Pragmas): New routine.
	(Write_Entity_Flags): Add an entry for Ignore_SPARK_Mode_Pragmas.
	* einfo.ads Add new attribute Ignore_SPARK_Mode_Pragmas and update
	related entities.
	(Ignore_SPARK_Mode_Pragmas): New routine
	along with pragma Inline.
	(Set_Ignore_SPARK_Mode_Pragmas): New routine along with pragma Inline.
	* opt.ads Rename flag Ignore_Pragma_SPARK_Mode to
	Ignore_SPARK_Mode_Pragmas_In_Instance.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper):
	Save and restore the value of global flag
	Ignore_SPARK_Mode_Pragmas_In_Instance. Set or reinstate the value
	of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when either
	the corresponding spec or the body must ignore all SPARK_Mode
	pragmas found within.
	(Analyze_Subprogram_Declaration): Mark
	the spec when it needs to ignore all SPARK_Mode pragmas found
	within to allow the body to infer this property in case it is
	instantiated or inlined later.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Save and restore the
	value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
	the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
	when the corresponding spec also ignored all SPARK_Mode pragmas
	found within.
	(Analyze_Package_Declaration): Mark the spec when
	it needs to ignore all SPARK_Mode pragmas found within to allow
	the body to infer this property in case it is instantiated or
	inlined later.
	* sem_ch12.adb (Analyze_Formal_Package_Declaration):
	Save and restore the value of flag
	Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
	formal spec when it needs to ignore all SPARK_Mode
	pragmas found within to allow the body to infer this
	property in case it is instantiated or inlined later.
	(Analyze_Package_Instantiation): Save and restore the value
	of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark
	the instance spec when it needs to ignore all SPARK_Mode
	pragmas found within to allow the body to infer this
	property in case it is instantiated or inlined later.
	(Analyze_Subprogram_Instantiation): Save and restore the value
	of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
	instance spec and anonymous package when they need to ignore
	all SPARK_Mode pragmas found within to allow the body to infer
	this property in case it is instantiated or inlined later.
	(Instantiate_Package_Body): Save and restore the value of global
	flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of
	global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the
	corresponding instance spec also ignored all SPARK_Mode pragmas
	found within.
	(Instantiate_Subprogram_Body): Save and restore the
	value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
	the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
	when the corresponding instance spec also ignored all SPARK_Mode
	pragmas found within.
	* sem_prag.adb (Analyze_Pragma): Update the reference to
	Ignore_Pragma_SPARK_Mode.
	* sem_util.adb (SPARK_Mode_Is_Off): A construct which ignored
	all SPARK_Mode pragmas defined within yields mode "off".

2017-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* bindgen.adb, exp_dbug.adb, errout.adb, fname.adb: Minor reformatting.

2017-04-25  Bob Duff  <duff@adacore.com>

	* exp_atag.adb (Build_CW_Membership): Add "Suppress =>
	All_Checks" to avoid generating unnecessary checks.
	* exp_ch4.adb (Expand_N_In, Make_Tag_Check): Add "Suppress =>
	All_Checks".
	* sem.ads: Fix comment.
	* expander.ads: Fix comment.
	* exp_atag.ads: Fix comment: "Index = 0" should be
	"Index >= 0".

2017-04-25  Gary Dismukes  <dismukes@adacore.com>

	* s-taprop-linux.adb: Minor editorial fixes.

From-SVN: r247182
This commit is contained in:
Arnaud Charlet 2017-04-25 12:49:34 +02:00
parent 1f0bcd44fe
commit cf9a473e64
19 changed files with 377 additions and 122 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

82
gcc/ada/ChangeLog
View File

@ -1,3 +1,85 @@
2017-04-25 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb Flag301 is now known as Ignore_SPARK_Mode_Pragmas.
(Ignore_SPARK_Mode_Pragmas): New routine.
(Set_Ignore_SPARK_Mode_Pragmas): New routine.
(Write_Entity_Flags): Add an entry for Ignore_SPARK_Mode_Pragmas.
* einfo.ads Add new attribute Ignore_SPARK_Mode_Pragmas and update
related entities.
(Ignore_SPARK_Mode_Pragmas): New routine
along with pragma Inline.
(Set_Ignore_SPARK_Mode_Pragmas): New routine along with pragma Inline.
* opt.ads Rename flag Ignore_Pragma_SPARK_Mode to
Ignore_SPARK_Mode_Pragmas_In_Instance.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper):
Save and restore the value of global flag
Ignore_SPARK_Mode_Pragmas_In_Instance. Set or reinstate the value
of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when either
the corresponding spec or the body must ignore all SPARK_Mode
pragmas found within.
(Analyze_Subprogram_Declaration): Mark
the spec when it needs to ignore all SPARK_Mode pragmas found
within to allow the body to infer this property in case it is
instantiated or inlined later.
* sem_ch7.adb (Analyze_Package_Body_Helper): Save and restore the
value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
when the corresponding spec also ignored all SPARK_Mode pragmas
found within.
(Analyze_Package_Declaration): Mark the spec when
it needs to ignore all SPARK_Mode pragmas found within to allow
the body to infer this property in case it is instantiated or
inlined later.
* sem_ch12.adb (Analyze_Formal_Package_Declaration):
Save and restore the value of flag
Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
formal spec when it needs to ignore all SPARK_Mode
pragmas found within to allow the body to infer this
property in case it is instantiated or inlined later.
(Analyze_Package_Instantiation): Save and restore the value
of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark
the instance spec when it needs to ignore all SPARK_Mode
pragmas found within to allow the body to infer this
property in case it is instantiated or inlined later.
(Analyze_Subprogram_Instantiation): Save and restore the value
of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
instance spec and anonymous package when they need to ignore
all SPARK_Mode pragmas found within to allow the body to infer
this property in case it is instantiated or inlined later.
(Instantiate_Package_Body): Save and restore the value of global
flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of
global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the
corresponding instance spec also ignored all SPARK_Mode pragmas
found within.
(Instantiate_Subprogram_Body): Save and restore the
value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
when the corresponding instance spec also ignored all SPARK_Mode
pragmas found within.
* sem_prag.adb (Analyze_Pragma): Update the reference to
Ignore_Pragma_SPARK_Mode.
* sem_util.adb (SPARK_Mode_Is_Off): A construct which ignored
all SPARK_Mode pragmas defined within yields mode "off".
2017-04-25 Hristian Kirtchev <kirtchev@adacore.com>
* bindgen.adb, exp_dbug.adb, errout.adb, fname.adb: Minor reformatting.
2017-04-25 Bob Duff <duff@adacore.com>
* exp_atag.adb (Build_CW_Membership): Add "Suppress =>
All_Checks" to avoid generating unnecessary checks.
* exp_ch4.adb (Expand_N_In, Make_Tag_Check): Add "Suppress =>
All_Checks".
* sem.ads: Fix comment.
* expander.ads: Fix comment.
* exp_atag.ads: Fix comment: "Index = 0" should be
"Index >= 0".
2017-04-25 Gary Dismukes <dismukes@adacore.com>
* s-taprop-linux.adb: Minor editorial fixes.
2017-04-25 Eric Botcazou <ebotcazou@adacore.com>
* sem_util.adb (New_Copy_Tree): Put back the declarations of the

4
gcc/ada/bindgen.adb
View File

@ -1120,8 +1120,8 @@ package body Bindgen is
-- where we increment the elaboration entity if one exists.
-- Likewise for lone specs with an elaboration entity defined
-- despite No_Elaboration_Code, e.g. when requested to
-- preserve control flow.
-- despite No_Elaboration_Code, e.g. when requested to preserve
-- control flow.
if (U.Utype = Is_Body or else U.Utype = Is_Spec_Only)
and then Units.Table (Unum_Spec).Set_Elab_Entity

49
gcc/ada/einfo.adb
View File

@ -620,7 +620,7 @@ package body Einfo is
-- Body_Needed_For_Inlining Flag299
-- Has_Private_Extension Flag300
-- (unused) Flag301
-- Ignore_SPARK_Mode_Pragmas Flag301
-- (unused) Flag302
-- (unused) Flag303
-- (unused) Flag304
@ -1981,6 +1981,29 @@ package body Einfo is
return Node4 (Id);
end Homonym;
function Ignore_SPARK_Mode_Pragmas (Id : E) return B is
begin
pragma Assert
(Ekind_In (Id, E_Protected_Body, -- concurrent variants
E_Protected_Type,
E_Task_Body,
E_Task_Type)
or else
Ekind_In (Id, E_Entry, -- overloadable variants
E_Entry_Family,
E_Function,
E_Generic_Function,
E_Generic_Procedure,
E_Operator,
E_Procedure,
E_Subprogram_Body)
or else
Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
E_Package_Body));
return Flag301 (Id);
end Ignore_SPARK_Mode_Pragmas;
function Import_Pragma (Id : E) return E is
begin
pragma Assert (Is_Subprogram (Id));
@ -5073,6 +5096,29 @@ package body Einfo is
Set_Elist24 (Id, V);
end Set_Incomplete_Actuals;
procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True) is
begin
pragma Assert
(Ekind_In (Id, E_Protected_Body, -- concurrent variants
E_Protected_Type,
E_Task_Body,
E_Task_Type)
or else
Ekind_In (Id, E_Entry, -- overloadable variants
E_Entry_Family,
E_Function,
E_Generic_Function,
E_Generic_Procedure,
E_Operator,
E_Procedure,
E_Subprogram_Body)
or else
Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
E_Package_Body));
Set_Flag301 (Id, V);
end Set_Ignore_SPARK_Mode_Pragmas;
procedure Set_Import_Pragma (Id : E; V : E) is
begin
pragma Assert (Is_Subprogram (Id));
@ -9402,6 +9448,7 @@ package body Einfo is
W ("Has_Visible_Refinement", Flag263 (Id));
W ("Has_Volatile_Components", Flag87 (Id));
W ("Has_Xref_Entry", Flag182 (Id));
W ("Ignore_SPARK_Mode_Pragmas", Flag301 (Id));
W ("In_Package_Body", Flag48 (Id));
W ("In_Private_Part", Flag45 (Id));
W ("In_Use", Flag8 (Id));

29
gcc/ada/einfo.ads
View File

@ -2164,6 +2164,13 @@ package Einfo is
-- scopes. Homonyms in the same scope are overloaded. Used for name
-- resolution and for the generation of debugging information.
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Present in concurrent type, entry, operator, [generic] package,
-- package body, [generic] subprogram, and subprogram body entities.
-- Set when the entity appears in an instance subject to SPARK_Mode
-- "off" and indicates that all SPARK_Mode pragmas found within must
-- be ignored.
-- Implementation_Base_Type (synthesized)
-- Applies to all entities. For types, similar to Base_Type, but never
-- returns a private type when applied to a non-private type. Instead in
@ -5922,14 +5929,15 @@ package Einfo is
-- Extra_Formals (Node28)
-- Contract (Node34)
-- SPARK_Pragma (Node40) (protected kind)
-- Needs_No_Actuals (Flag22)
-- Uses_Sec_Stack (Flag95)
-- Default_Expressions_Processed (Flag108)
-- Entry_Accepted (Flag152)
-- Sec_Stack_Needed_For_Return (Flag167)
-- Has_Expanded_Contract (Flag240)
-- SPARK_Pragma_Inherited (Flag265) (protected kind)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Entry_Wrapper (Flag297)
-- Needs_No_Actuals (Flag22)
-- Sec_Stack_Needed_For_Return (Flag167)
-- SPARK_Pragma_Inherited (Flag265) (protected kind)
-- Uses_Sec_Stack (Flag95)
-- Address_Clause (synth)
-- Entry_Index_Type (synth)
-- First_Formal (synth)
@ -6056,6 +6064,7 @@ package Einfo is
-- Has_Nested_Subprogram (Flag282)
-- Has_Out_Or_In_Out_Parameter (Flag110)
-- Has_Recursive_Call (Flag143)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Abstract_Subprogram (Flag19) (non-generic case only)
-- Is_Called (Flag102) (non-generic case only)
-- Is_Constructor (Flag76)
@ -6209,6 +6218,7 @@ package Einfo is
-- SPARK_Pragma (Node40)
-- Default_Expressions_Processed (Flag108)
-- Has_Nested_Subprogram (Flag282)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Intrinsic_Subprogram (Flag64)
-- Is_Machine_Code_Subprogram (Flag137)
-- Is_Primitive (Flag218)
@ -6272,6 +6282,7 @@ package Einfo is
-- Has_Forward_Instantiation (Flag175)
-- Has_Master_Entity (Flag21)
-- Has_RACW (Flag214) (non-generic case only)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- In_Package_Body (Flag48)
-- In_Use (Flag8)
-- Is_Instantiated (Flag126)
@ -6299,6 +6310,7 @@ package Einfo is
-- SPARK_Aux_Pragma (Node41)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Subprogram_Descriptors (Flag50)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
-- Scope_Depth (synth)
@ -6367,6 +6379,7 @@ package Einfo is
-- Has_Master_Entity (Flag21)
-- Has_Nested_Block_With_Handler (Flag101)
-- Has_Nested_Subprogram (Flag282)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Abstract_Subprogram (Flag19) (non-generic case only)
-- Is_Asynchronous (Flag81)
-- Is_Called (Flag102) (non-generic case only)
@ -6406,6 +6419,7 @@ package Einfo is
-- E_Protected_Body
-- SPARK_Pragma (Node40)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- SPARK_Pragma_Inherited (Flag265)
-- (any others??? First/Last Entity, Scope_Depth???)
@ -6427,6 +6441,7 @@ package Einfo is
-- Entry_Max_Queue_Lengths_Array (Node35)
-- SPARK_Pragma (Node40)
-- SPARK_Aux_Pragma (Node41)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Sec_Stack_Needed_For_Return (Flag167) ???
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
@ -6557,6 +6572,7 @@ package Einfo is
-- E_Task_Body
-- Contract (Node34)
-- SPARK_Pragma (Node40)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- SPARK_Pragma_Inherited (Flag265)
-- (any others??? First/Last Entity, Scope_Depth???)
@ -6580,6 +6596,7 @@ package Einfo is
-- Delay_Cleanups (Flag114)
-- Has_Master_Entity (Flag21)
-- Has_Storage_Size_Clause (Flag23) (base type only)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Sec_Stack_Needed_For_Return (Flag167) ???
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
@ -7103,6 +7120,7 @@ package Einfo is
function Has_Xref_Entry (Id : E) return B;
function Hiding_Loop_Variable (Id : E) return E;
function Homonym (Id : E) return E;
function Ignore_SPARK_Mode_Pragmas (Id : E) return B;
function Import_Pragma (Id : E) return E;
function Incomplete_Actuals (Id : E) return L;
function In_Package_Body (Id : E) return B;
@ -7788,6 +7806,7 @@ package Einfo is
procedure Set_Has_Xref_Entry (Id : E; V : B := True);
procedure Set_Hiding_Loop_Variable (Id : E; V : E);
procedure Set_Homonym (Id : E; V : E);
procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True);
procedure Set_Import_Pragma (Id : E; V : E);
procedure Set_Incomplete_Actuals (Id : E; V : L);
procedure Set_In_Package_Body (Id : E; V : B := True);
@ -8587,6 +8606,7 @@ package Einfo is
pragma Inline (Has_Xref_Entry);
pragma Inline (Hiding_Loop_Variable);
pragma Inline (Homonym);
pragma Inline (Ignore_SPARK_Mode_Pragmas);
pragma Inline (Import_Pragma);
pragma Inline (Incomplete_Actuals);
pragma Inline (In_Package_Body);
@ -9109,6 +9129,7 @@ package Einfo is
pragma Inline (Set_Has_Xref_Entry);
pragma Inline (Set_Hiding_Loop_Variable);
pragma Inline (Set_Homonym);
pragma Inline (Set_Ignore_SPARK_Mode_Pragmas);
pragma Inline (Set_Import_Pragma);
pragma Inline (Set_Incomplete_Actuals);
pragma Inline (Set_In_Package_Body);

4
gcc/ada/errout.adb
View File

@ -508,10 +508,12 @@ package body Errout is
Error_Msg_Internal
("info: in inlined body #",
Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
elsif Is_Warning_Msg or Is_Style_Msg then
Error_Msg_Internal
(Warn_Insertion & "in inlined body #",
Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
else
Error_Msg_Internal
("error in inlined body #",
@ -525,10 +527,12 @@ package body Errout is
Error_Msg_Internal
("info: in instantiation #",
Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
elsif Is_Warning_Msg or else Is_Style_Msg then
Error_Msg_Internal
(Warn_Insertion & "in instantiation #",
Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
else
Error_Msg_Internal
("instantiation error #",

13
gcc/ada/exp_atag.adb
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2006-2014, Free Software Foundation, Inc. --
-- Copyright (C) 2006-2016, 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- --
@ -178,7 +178,7 @@ package body Exp_Atag is
-- Typ_TSD : constant Type_Specific_Data_Ptr
-- := Build_TSD (Address!(Typ_Tag));
-- Index : constant Integer := Obj_TSD.Idepth - Typ_TSD.Idepth
-- Index > 0 and then Obj_TSD.Tags_Table (Index) = Typ'Tag
-- Index >= 0 and then Obj_TSD.Tags_Table (Index) = Typ'Tag
Insert_Action (Related_Nod,
Make_Object_Declaration (Loc,
@ -199,7 +199,8 @@ package body Exp_Atag is
Constant_Present => True,
Object_Definition => New_Occurrence_Of
(RTE (RE_Type_Specific_Data_Ptr), Loc),
Expression => Build_TSD (Loc, New_Occurrence_Of (Tag_Addr, Loc))));
Expression => Build_TSD (Loc, New_Occurrence_Of (Tag_Addr, Loc))),
Suppress => All_Checks);
Insert_Action (Related_Nod,
Make_Object_Declaration (Loc,
@ -209,7 +210,8 @@ package body Exp_Atag is
(RTE (RE_Type_Specific_Data_Ptr), Loc),
Expression => Build_TSD (Loc,
Unchecked_Convert_To (RTE (RE_Address),
Typ_Tag_Node))));
Typ_Tag_Node))),
Suppress => All_Checks);
Insert_Action (Related_Nod,
Make_Object_Declaration (Loc,
@ -230,7 +232,8 @@ package body Exp_Atag is
Prefix => New_Occurrence_Of (Typ_TSD, Loc),
Selector_Name =>
New_Occurrence_Of
(RTE_Record_Component (RE_Idepth), Loc)))));
(RTE_Record_Component (RE_Idepth), Loc)))),
Suppress => All_Checks);
New_Node :=
Make_And_Then (Loc,

4
gcc/ada/exp_atag.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2006-2011, Free Software Foundation, Inc. --
-- Copyright (C) 2006-2016, 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- --
@ -54,7 +54,7 @@ package Exp_Atag is
-- computed in constant time by the formula:
--
-- Index := TSD (Obj'Tag).Idepth - TSD (Typ'Tag).Idepth;
-- Index > 0 and then TSD (Obj'Tag).Tags_Table (Index) = Typ'Tag
-- Index >= 0 and then TSD (Obj'Tag).Tags_Table (Index) = Typ'Tag
--
-- Related_Nod is the node where the implicit declaration of variable Index
-- is inserted. Obj_Tag_Node is relocated.

6
gcc/ada/exp_ch4.adb
View File

@ -5859,7 +5859,8 @@ package body Exp_Ch4 is
if Tagged_Type_Expansion then
Tagged_Membership (N, SCIL_Node, New_N);
Rewrite (N, New_N);
Analyze_And_Resolve (N, Restyp);
Analyze_And_Resolve
(N, Restyp, Suppress => All_Checks);
-- Update decoration of relocated node referenced by the
-- SCIL node.
@ -10908,7 +10909,8 @@ package body Exp_Ch4 is
Insert_Action (N,
Make_Raise_Constraint_Error (Loc,
Condition => Cond,
Reason => CE_Tag_Check_Failed));
Reason => CE_Tag_Check_Failed),
Suppress => All_Checks);
end Make_Tag_Check;
-- Start of processing for Tagged_Conversion

18
gcc/ada/exp_dbug.adb
View File

@ -343,8 +343,10 @@ package body Exp_Dbug is
begin
Enable :=
Enable or else (Ekind (T) in Array_Kind
and then Present (Packed_Array_Impl_Type (T)));
Enable
or else
(Ekind (T) in Array_Kind
and then Present (Packed_Array_Impl_Type (T)));
end Enable_If_Packed_Array;
----------------------
@ -359,7 +361,7 @@ package body Exp_Dbug is
elsif Nkind (N) = N_Identifier
and then Scope_Contains (Scope (Entity (N)), Ent)
and then (Ekind (Entity (N)) = E_Constant
or else Ekind (Entity (N)) = E_In_Parameter)
or else Ekind (Entity (N)) = E_In_Parameter)
then
Prepend_String_To_Buffer (Get_Name_String (Chars (Entity (N))));
@ -375,25 +377,25 @@ package body Exp_Dbug is
-- Scope_Contains --
--------------------
function Scope_Contains (Sc : Node_Id; Ent : Entity_Id) return Boolean
is
function Scope_Contains (Sc : Node_Id; Ent : Entity_Id) return Boolean is
Cur : Node_Id := Scope (Ent);
begin
while Present (Cur) loop
if Cur = Sc then
return True;
end if;
Cur := Scope (Cur);
end loop;
return False;
end Scope_Contains;
-- Start of processing for Debug_Renaming_Declaration
begin
if not Comes_From_Source (N)
and then not Needs_Debug_Info (Ent)
then
if not Comes_From_Source (N) and then not Needs_Debug_Info (Ent) then
return Empty;
end if;

8
gcc/ada/expander.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2016, 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- --
@ -66,9 +66,9 @@
-- always the case).
-- In both these cases, Replace or Rewrite must be used to achieve the
-- of the node, since the Expander routine is only passed the Node_Id
-- of the node to be expanded, and the resulting expanded Node_Id must
-- be the same (the parameter to Expand is mode in, not mode in-out).
-- expansion of the node, since the Expander routine is only passed the
-- Node_Id of the node to be expanded, and the resulting expanded Node_Id
-- must be the same (the parameter to Expand is mode in, not mode in-out).
-- For nodes other than subexpressions, it is not necessary to preserve the
-- original tree in the Expand routines, unlike the case for modifications

23
gcc/ada/fname.adb
View File

@ -59,14 +59,13 @@ package body Fname is
function Has_Internal_Extension (Fname : String) return Boolean;
pragma Inline (Has_Internal_Extension);
-- True if the extension is appropriate for an internal/predefined
-- unit. That means ".ads" or ".adb" for source files, and ".ali" for
-- ALI files.
-- True if the extension is appropriate for an internal/predefined unit.
-- That means ".ads" or ".adb" for source files, and ".ali" for ALI files.
function Has_Prefix (X, Prefix : String) return Boolean;
pragma Inline (Has_Prefix);
-- True if Prefix is at the beginning of X. For example,
-- Has_Prefix("a-filename.ads", Prefix => "a-") is True.
-- Has_Prefix ("a-filename.ads", Prefix => "a-") is True.
----------------------------
-- Has_Internal_Extension --
@ -145,14 +144,14 @@ package body Fname is
subtype Str8 is String (1 .. 8);
Renaming_Names : constant array (1 .. 8) of Str8 :=
("calendar", -- Calendar
"machcode", -- Machine_Code
"unchconv", -- Unchecked_Conversion
"unchdeal", -- Unchecked_Deallocation
"directio", -- Direct_IO
"ioexcept", -- IO_Exceptions
"sequenio", -- Sequential_IO
"text_io."); -- Text_IO
("calendar", -- Calendar
"machcode", -- Machine_Code
"unchconv", -- Unchecked_Conversion
"unchdeal", -- Unchecked_Deallocation
"directio", -- Direct_IO
"ioexcept", -- IO_Exceptions
"sequenio", -- Sequential_IO
"text_io."); -- Text_IO
-- Note: the implementation is optimized to perform uniform comparisons
-- on string slices whose length is known at compile time and at most 8

12
gcc/ada/opt.ads
View File

@ -814,18 +814,18 @@ package Opt is
-- default value appropriate to the system (in Osint.Initialize), and then
-- reset if a command line switch is used to change the setting.
Ignore_Pragma_SPARK_Mode : Boolean := False;
-- GNAT
-- Set True to ignore the semantics and effects of pragma SPARK_Mode when
-- the pragma appears inside an instance whose enclosing context is subject
-- to SPARK_Mode "off".
Ignore_Rep_Clauses : Boolean := False;
-- GNAT
-- Set True to ignore all representation clauses. Useful when compiling
-- code from foreign compilers for checking or ASIS purposes. Can be
-- set True by use of -gnatI.
Ignore_SPARK_Mode_Pragmas_In_Instance : Boolean := False;
-- GNAT
-- Set True to ignore the semantics and effects of pragma SPARK_Mode when
-- the pragma appears inside an instance whose enclosing context is subject
-- to SPARK_Mode "off". This property applies to nested instances.
Ignore_Style_Checks_Pragmas : Boolean := False;
-- GNAT
-- Set True to ignore all Style_Checks pragmas. Can be set True by use

4
gcc/ada/s-taprop-linux.adb
View File

@ -849,8 +849,8 @@ package body System.Task_Primitives.Operations is
end if;
end loop;
-- Cover the odd situtation if someone decides to change
-- Parameters.Max_Task_Image_Length to less than 16 characters
-- Cover the odd situation where someone decides to change
-- Parameters.Max_Task_Image_Length to less than 16 characters.
if Len > Parameters.Max_Task_Image_Length then
Len := Parameters.Max_Task_Image_Length;

20
gcc/ada/sem.ads
View File

@ -165,7 +165,7 @@
------------------
-- For certain kind of expressions, such as aggregates, we need to defer
-- expansion of the aggregate and its inner expressions after the whole
-- expansion of the aggregate and its inner expressions until after the whole
-- set of expressions appearing inside the aggregate have been analyzed.
-- Consider, for instance the following example:
--
@ -177,17 +177,17 @@
-- repeatedly (for instance in the above aggregate "new Thing (Function_Call)"
-- needs to be called 100 times.)
-- The reason why this mechanism does not work is that the expanded code for
-- the children is typically inserted above the parent and thus when the
-- father gets expanded no re-evaluation takes place. For instance in the case
-- of aggregates if "new Thing (Function_Call)" is expanded before of the
-- aggregate the expanded code will be placed outside of the aggregate and
-- when expanding the aggregate the loop from 1 to 100 will not surround the
-- The reason this mechanism does not work is that the expanded code for the
-- children is typically inserted above the parent and thus when the father
-- gets expanded no re-evaluation takes place. For instance in the case of
-- aggregates if "new Thing (Function_Call)" is expanded before the aggregate
-- the expanded code will be placed outside of the aggregate and when
-- expanding the aggregate the loop from 1 to 100 will not surround the
-- expanded code for "new Thing (Function_Call)".
-- To remedy this situation we introduce a new flag which signals whether we
-- want a full analysis (i.e. expansion is enabled) or a pre-analysis which
-- performs Analysis and Resolution but no expansion.
-- To remedy this situation we introduce a flag that signals whether we want a
-- full analysis (i.e. expansion is enabled) or a pre-analysis which performs
-- Analysis and Resolution but no expansion.
-- After the complete pre-analysis of an expression has been carried out we
-- can transform the expression and then carry out the full three stage

140
gcc/ada/sem_ch12.adb
View File

@ -2605,8 +2605,8 @@ package body Sem_Ch12 is
-- Local variables
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
-- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Associations : Boolean := True;
New_N : Node_Id;
@ -2782,7 +2782,12 @@ package body Sem_Ch12 is
-- all SPARK_Mode pragmas within the generic_package_name.
if SPARK_Mode /= On then
Ignore_Pragma_SPARK_Mode := True;
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
-- Mark the formal spec in case the body is instantiated at a later
-- pass. This preserves the original context in effect for the body.
Set_Ignore_SPARK_Mode_Pragmas (Formal);
end if;
Analyze (Specification (N));
@ -2843,7 +2848,7 @@ package body Sem_Ch12 is
Analyze_Aspect_Specifications (N, Pack_Id);
end if;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
end Analyze_Formal_Package_Declaration;
---------------------------------
@ -3622,8 +3627,8 @@ package body Sem_Ch12 is
Inline_Now : Boolean := False;
Has_Inline_Always : Boolean := False;
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
-- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
@ -3865,7 +3870,13 @@ package body Sem_Ch12 is
-- the instance.
if SPARK_Mode /= On then
Ignore_Pragma_SPARK_Mode := True;
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
-- Mark the instance spec in case the body is instantiated at a
-- later pass. This preserves the original context in effect for
-- the body.
Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
end if;
Gen_Decl := Unit_Declaration_Node (Gen_Unit);
@ -4433,11 +4444,6 @@ package body Sem_Ch12 is
Set_Defining_Identifier (N, Act_Decl_Id);
end if;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
Style_Check := Save_Style_Check;
-- Check that if N is an instantiation of System.Dim_Float_IO or
-- System.Dim_Integer_IO, the formal type has a dimension system.
@ -4460,6 +4466,11 @@ package body Sem_Ch12 is
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
Style_Check := Save_Style_Check;
if Mode_Set then
Restore_Ghost_Mode (Mode);
end if;
@ -4474,10 +4485,10 @@ package body Sem_Ch12 is
Restore_Env;
end if;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
Style_Check := Save_Style_Check;
Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
Style_Check := Save_Style_Check;
if Mode_Set then
Restore_Ghost_Mode (Mode);
@ -5119,8 +5130,8 @@ package body Sem_Ch12 is
-- Local variables
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
-- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
@ -5201,15 +5212,6 @@ package body Sem_Ch12 is
Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
else
-- If the context of the instance is subject to SPARK_Mode "off" or
-- the annotation is altogether missing, set the global flag which
-- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
-- the instance.
if SPARK_Mode /= On then
Ignore_Pragma_SPARK_Mode := True;
end if;
Set_Entity (Gen_Id, Gen_Unit);
Set_Is_Instantiated (Gen_Unit);
@ -5348,6 +5350,22 @@ package body Sem_Ch12 is
Set_Has_Pragma_Inline_Always
(Anon_Id, Has_Pragma_Inline_Always (Gen_Unit));
-- If the context of the instance is subject to SPARK_Mode "off" or
-- the annotation is altogether missing, set the global flag which
-- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
-- the instance.
if SPARK_Mode /= On then
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
-- Mark both the instance spec and the anonymous package in case
-- the body is instantiated at a later pass. This preserves the
-- original context in effect for the body.
Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
Set_Ignore_SPARK_Mode_Pragmas (Anon_Id);
end if;
if not Is_Intrinsic_Subprogram (Gen_Unit) then
Check_Elab_Instantiation (N);
end if;
@ -5421,10 +5439,6 @@ package body Sem_Ch12 is
Env_Installed := False;
Generic_Renamings.Set_Last (0);
Generic_Renamings_HTable.Reset;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
end if;
<<Leave>>
@ -5432,6 +5446,10 @@ package body Sem_Ch12 is
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
if Mode_Set then
Restore_Ghost_Mode (Mode);
end if;
@ -5446,9 +5464,9 @@ package body Sem_Ch12 is
Restore_Env;
end if;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
if Mode_Set then
Restore_Ghost_Mode (Mode);
@ -10847,7 +10865,8 @@ package body Sem_Ch12 is
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
Loc : constant Source_Ptr := Sloc (Inst_Node);
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
Save_ISMP : constant Boolean :=
Ignore_SPARK_Mode_Pragmas_In_Instance;
Save_Style_Check : constant Boolean := Style_Check;
procedure Check_Initialized_Types;
@ -11009,13 +11028,16 @@ package body Sem_Ch12 is
Save_Env (Gen_Unit, Act_Decl_Id);
Style_Check := False;
-- If the context of the instance is subject to SPARK_Mode "off" or
-- the annotation is altogether missing, set the global flag which
-- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
-- the instance.
-- If the context of the instance is subject to SPARK_Mode "off", the
-- annotation is missing, or the body is instantiated at a later pass
-- and its spec ignored SPARK_Mode pragma, set the global flag which
-- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the
-- instance.
if SPARK_Mode /= On then
Ignore_Pragma_SPARK_Mode := True;
if SPARK_Mode /= On
or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
then
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
@ -11186,8 +11208,6 @@ package body Sem_Ch12 is
end if;
Restore_Env;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
Style_Check := Save_Style_Check;
-- If we have no body, and the unit requires a body, then complain. This
-- complaint is suppressed if we have detected other errors (since a
@ -11209,7 +11229,7 @@ package body Sem_Ch12 is
-- was already detected, since this can cause blowups.
else
return;
goto Leave;
end if;
-- Case of package that does not need a body
@ -11244,6 +11264,9 @@ package body Sem_Ch12 is
Expander_Mode_Restore;
<<Leave>>
Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
Style_Check := Save_Style_Check;
Restore_Ghost_Mode (Mode);
end Instantiate_Package_Body;
@ -11269,8 +11292,9 @@ package body Sem_Ch12 is
Pack_Id : constant Entity_Id :=
Defining_Unit_Name (Parent (Act_Decl));
Saved_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
Saved_Style_Check : constant Boolean := Style_Check;
Saved_ISMP : constant Boolean :=
Ignore_SPARK_Mode_Pragmas_In_Instance;
Saved_Style_Check : constant Boolean := Style_Check;
Saved_Warnings : constant Warning_Record := Save_Warnings;
Act_Body : Node_Id;
@ -11363,13 +11387,16 @@ package body Sem_Ch12 is
Save_Env (Gen_Unit, Act_Decl_Id);
Style_Check := False;
-- If the context of the instance is subject to SPARK_Mode "off" or
-- the annotation is altogether missing, set the global flag which
-- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
-- the instance.
-- If the context of the instance is subject to SPARK_Mode "off", the
-- annotation is missing, or the body is instantiated at a later pass
-- and its spec ignored SPARK_Mode pragma, set the global flag which
-- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the
-- instance.
if SPARK_Mode /= On then
Ignore_Pragma_SPARK_Mode := True;
if SPARK_Mode /= On
or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
then
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
@ -11473,8 +11500,6 @@ package body Sem_Ch12 is
end if;
Restore_Env;
Ignore_Pragma_SPARK_Mode := Saved_IPSM;
Style_Check := Saved_Style_Check;
Restore_Warnings (Saved_Warnings);
-- Body not found. Error was emitted already. If there were no previous
@ -11549,6 +11574,9 @@ package body Sem_Ch12 is
Expander_Mode_Restore;
<<Leave>>
Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
Style_Check := Saved_Style_Check;
Restore_Ghost_Mode (Mode);
end Instantiate_Subprogram_Body;
@ -11562,12 +11590,12 @@ package body Sem_Ch12 is
Analyzed_Formal : Node_Id;
Actual_Decls : List_Id) return List_Id
is
Gen_T : constant Entity_Id := Defining_Identifier (Formal);
A_Gen_T : constant Entity_Id :=
Defining_Identifier (Analyzed_Formal);
Ancestor : Entity_Id := Empty;
Def : constant Node_Id := Formal_Type_Definition (Formal);
Gen_T : constant Entity_Id := Defining_Identifier (Formal);
Act_T : Entity_Id;
Ancestor : Entity_Id := Empty;
Decl_Node : Node_Id;
Decl_Nodes : List_Id;
Loc : Source_Ptr;

44
gcc/ada/sem_ch6.adb
View File

@ -3298,8 +3298,9 @@ package body Sem_Ch6 is
-- Local variables
Mode : Ghost_Mode_Type;
Mode_Set : Boolean := False;
Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
Mode : Ghost_Mode_Type;
Mode_Set : Boolean := False;
-- Start of processing for Analyze_Subprogram_Body_Helper
@ -3371,7 +3372,7 @@ package body Sem_Ch6 is
else
Enter_Name (Body_Id);
return;
goto Leave;
end if;
-- Non-generic case, find the subprogram declaration, if one was seen,
@ -3381,7 +3382,7 @@ package body Sem_Ch6 is
-- analysis.
elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
return;
goto Leave;
else
Body_Id := Analyze_Subprogram_Specification (Body_Spec);
@ -3868,6 +3869,29 @@ package body Sem_Ch6 is
Set_SPARK_Pragma_Inherited (Body_Id);
end if;
-- A subprogram body may be instantiated or inlined at a later pass.
-- Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when it
-- applied to the initial declaration of the body.
if Present (Spec_Id) then
if Ignore_SPARK_Mode_Pragmas (Spec_Id) then
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
else
-- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
-- case the body is instantiated or inlined later and out of context.
-- The body uses this attribute to restore the value of the global
-- flag.
if Ignore_SPARK_Mode_Pragmas_In_Instance then
Set_Ignore_SPARK_Mode_Pragmas (Body_Id);
elsif Ignore_SPARK_Mode_Pragmas (Body_Id) then
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
end if;
-- If this is the proper body of a stub, we must verify that the stub
-- conforms to the body, and to the previous spec if one was present.
-- We know already that the body conforms to that spec. This test is
@ -4056,6 +4080,7 @@ package body Sem_Ch6 is
Protected_Body_Subprogram (Spec_Id);
Prot_Ext_Formal : Entity_Id := Extra_Formals (Spec_Id);
Impl_Ext_Formal : Entity_Id := Extra_Formals (Impl_Subp);
begin
while Present (Prot_Ext_Formal) loop
pragma Assert (Present (Impl_Ext_Formal));
@ -4406,6 +4431,8 @@ package body Sem_Ch6 is
end if;
<<Leave>>
Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
if Mode_Set then
Restore_Ghost_Mode (Mode);
end if;
@ -4470,6 +4497,15 @@ package body Sem_Ch6 is
Set_SPARK_Pragma_Inherited (Designator);
end if;
-- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case
-- the body of this subprogram is instantiated or inlined later and out
-- of context. The body uses this attribute to restore the value of the
-- global flag.
if Ignore_SPARK_Mode_Pragmas_In_Instance then
Set_Ignore_SPARK_Mode_Pragmas (Designator);
end if;
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
Write_Name (Chars (Designator));

21
gcc/ada/sem_ch7.adb
View File

@ -539,6 +539,8 @@ package body Sem_Ch7 is
-- Local variables
Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
@ -738,6 +740,14 @@ package body Sem_Ch7 is
Set_SPARK_Aux_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id);
Set_SPARK_Aux_Pragma_Inherited (Body_Id);
-- A package body may be instantiated or inlined at a later pass.
-- Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when
-- it applied to the package spec.
if Ignore_SPARK_Mode_Pragmas (Spec_Id) then
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
end if;
Set_Categorization_From_Pragmas (N);
@ -931,6 +941,8 @@ package body Sem_Ch7 is
end if;
end if;
Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
Restore_Ghost_Mode (Mode);
end Analyze_Package_Body_Helper;
@ -969,6 +981,15 @@ package body Sem_Ch7 is
Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Id);
Set_SPARK_Aux_Pragma_Inherited (Id);
-- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
-- case the body of this package is instantiated or inlined later and
-- out of context. The body uses this attribute to restore the value
-- of the global flag.
if Ignore_SPARK_Mode_Pragmas_In_Instance then
Set_Ignore_SPARK_Mode_Pragmas (Id);
end if;
end if;
-- Analyze aspect specifications immediately, since we need to recognize

2
gcc/ada/sem_prag.adb
View File

@ -21689,7 +21689,7 @@ package body Sem_Prag is
-- enclosing context has SPARK_Mode set to "off", the pragma has
-- no semantic effect.
if Ignore_Pragma_SPARK_Mode then
if Ignore_SPARK_Mode_Pragmas_In_Instance then
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
return;

16
gcc/ada/sem_util.adb
View File

@ -3622,11 +3622,21 @@ package body Sem_Util is
-----------------------
function SPARK_Mode_Is_Off (N : Node_Id) return Boolean is
Prag : constant Node_Id := SPARK_Pragma (Defining_Entity (N));
Id : constant Entity_Id := Defining_Entity (N);
Prag : constant Node_Id := SPARK_Pragma (Id);
begin
return
Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
-- Default the mode to "off" when the context is an instance and all
-- SPARK_Mode pragmas found within are to be ignored.
if Ignore_SPARK_Mode_Pragmas (Id) then
return True;
else
return
Present (Prag)
and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
end if;
end SPARK_Mode_Is_Off;
-- Start of processing for Check_State_Refinements