[multiple changes]
2015-10-26 Ed Schonberg <schonberg@adacore.com> * exp_ch4.adb (Expand_N_Case_Expression): In the scope of a predicate function, delay the expansion of the expression only if the target type has a specified Static_ Predicate aspect, because the expression is processed later. A dynamic predicate must be expanded in standard fashion. 2015-10-26 Claire Dross <dross@adacore.com> * a-nudira.ads: Remove SPARK_Mode as it currently causes an error. 2015-10-26 Arnaud Charlet <charlet@adacore.com> * sem_aggr.adb, sem_type.adb, sem_ch12.adb, sem_res.adb, sem_ch4.adb, sem_ch8.adb, exp_aggr.adb, sem_eval.adb, s-fatgen.adb, a-tienio.adb: Fix typos. 2015-10-26 Hristian Kirtchev <kirtchev@adacore.com> * sem_ch13.adb (Analyze_Aspect_Specifications): The processing for aspects Abstract_State, Ghost, Initial_Condition, Initializes and Refined_State no longer have to take SPARK_Mode into account. (Insert_After_SPARK_Mode): Removed. (Insert_Pragma): Update profile and comment on usage. The routine can now insert a pragma after the "header" of an instance. * sem_prag.adb (Analyze_If_Available): New routine. (Analyze_Pragma): Do not reset the Analyzed flag of various SPARK pragmas as they use the Is_Analyzed_Pragma attribute to avoid reanalysis. Various pragmas now trigger the analysis of related pragmas that depend on or are dependent on the current pragma. Remove the declaration order checks related to pragmas Abstract_State, Initial_Condition and Initializes. (Analyze_Pre_Post_Condition): Analyze pragmas SPARK_Mode and Volatile_Function prior to analyzing the pre/postcondition. (Check_Declaration_Order): Removed. (Check_Distinct_Name): Ensure that a potentially duplicated pragma Test_Case is not the pragma being analyzed. (Is_Followed_By_Pragma): Removed. From-SVN: r229331
This commit is contained in:
parent
2ba4f1fb6e
commit
21d7ef70aa
|
@ -1,3 +1,43 @@
|
|||
2015-10-26 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* exp_ch4.adb (Expand_N_Case_Expression): In the scope of a
|
||||
predicate function, delay the expansion of the expression only
|
||||
if the target type has a specified Static_ Predicate aspect,
|
||||
because the expression is processed later. A dynamic predicate
|
||||
must be expanded in standard fashion.
|
||||
|
||||
2015-10-26 Claire Dross <dross@adacore.com>
|
||||
|
||||
* a-nudira.ads: Remove SPARK_Mode as it currently causes an error.
|
||||
|
||||
2015-10-26 Arnaud Charlet <charlet@adacore.com>
|
||||
|
||||
* sem_aggr.adb, sem_type.adb, sem_ch12.adb, sem_res.adb, sem_ch4.adb,
|
||||
sem_ch8.adb, exp_aggr.adb, sem_eval.adb, s-fatgen.adb, a-tienio.adb:
|
||||
Fix typos.
|
||||
|
||||
2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* sem_ch13.adb (Analyze_Aspect_Specifications): The processing
|
||||
for aspects Abstract_State, Ghost, Initial_Condition, Initializes
|
||||
and Refined_State no longer have to take SPARK_Mode into account.
|
||||
(Insert_After_SPARK_Mode): Removed.
|
||||
(Insert_Pragma): Update profile and comment on usage. The routine can
|
||||
now insert a pragma after the "header" of an instance.
|
||||
* sem_prag.adb (Analyze_If_Available): New routine.
|
||||
(Analyze_Pragma): Do not reset the Analyzed flag of various
|
||||
SPARK pragmas as they use the Is_Analyzed_Pragma attribute to
|
||||
avoid reanalysis. Various pragmas now trigger the analysis
|
||||
of related pragmas that depend on or are dependent on the
|
||||
current pragma. Remove the declaration order checks related
|
||||
to pragmas Abstract_State, Initial_Condition and Initializes.
|
||||
(Analyze_Pre_Post_Condition): Analyze pragmas SPARK_Mode and
|
||||
Volatile_Function prior to analyzing the pre/postcondition.
|
||||
(Check_Declaration_Order): Removed.
|
||||
(Check_Distinct_Name): Ensure that a potentially duplicated pragma
|
||||
Test_Case is not the pragma being analyzed.
|
||||
(Is_Followed_By_Pragma): Removed.
|
||||
|
||||
2015-10-26 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_ch6.adb: Handle subprogram bodies without previous specs.
|
||||
|
|
|
@ -29,7 +29,7 @@
|
|||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
package body Ada.Numerics.Discrete_Random with SPARK_Mode => Off is
|
||||
package body Ada.Numerics.Discrete_Random is
|
||||
|
||||
package SRN renames System.Random_Numbers;
|
||||
use SRN;
|
||||
|
|
|
@ -41,7 +41,7 @@ with System.Random_Numbers;
|
|||
generic
|
||||
type Result_Subtype is (<>);
|
||||
|
||||
package Ada.Numerics.Discrete_Random with SPARK_Mode is
|
||||
package Ada.Numerics.Discrete_Random is
|
||||
|
||||
-- Basic facilities
|
||||
|
||||
|
@ -65,7 +65,6 @@ package Ada.Numerics.Discrete_Random with SPARK_Mode is
|
|||
function Value (Coded_State : String) return State;
|
||||
|
||||
private
|
||||
pragma SPARK_Mode (Off);
|
||||
|
||||
type Generator is new System.Random_Numbers.Generator;
|
||||
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2012, 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- --
|
||||
|
@ -97,7 +97,7 @@ package body Ada.Text_IO.Enumeration_IO is
|
|||
begin
|
||||
-- Ensure that Item is valid before attempting to retrieve the Image, to
|
||||
-- prevent the possibility of out-of-bounds addressing of index or image
|
||||
-- tables. Units in the run-time library are normally compiled with
|
||||
-- tables. Units in the run-time library are normally compiled with
|
||||
-- checks suppressed, which includes instantiated generics.
|
||||
|
||||
if not Item'Valid then
|
||||
|
|
|
@ -2477,7 +2477,7 @@ package body Exp_Aggr is
|
|||
then
|
||||
Ancestor_Is_Expression := True;
|
||||
|
||||
-- Set up finalization data for enclosing record, because
|
||||
-- Set up finalization data for enclosing record, because
|
||||
-- controlled subcomponents of the ancestor part will be
|
||||
-- attached to it.
|
||||
|
||||
|
@ -3559,7 +3559,7 @@ package body Exp_Aggr is
|
|||
end if;
|
||||
|
||||
if Nkind (N) = N_Aggregate
|
||||
and then Present (Component_Associations (N))
|
||||
and then Present (Component_Associations (N))
|
||||
then
|
||||
Expr := First (Component_Associations (N));
|
||||
while Present (Expr) loop
|
||||
|
@ -3936,7 +3936,7 @@ package body Exp_Aggr is
|
|||
-- If the size is known, or all the components are static, try to
|
||||
-- build a fully positional aggregate.
|
||||
|
||||
-- The size of the type may not be known for an aggregate with
|
||||
-- The size of the type may not be known for an aggregate with
|
||||
-- discriminated array components, but if the components are static
|
||||
-- it is still possible to verify statically that the length is
|
||||
-- compatible with the upper bound of the type, and therefore it is
|
||||
|
@ -3980,7 +3980,7 @@ package body Exp_Aggr is
|
|||
|
||||
else
|
||||
Error_Msg_N
|
||||
("non-static object requires elaboration code??", N);
|
||||
("non-static object requires elaboration code??", N);
|
||||
exit;
|
||||
end if;
|
||||
|
||||
|
|
|
@ -4864,12 +4864,14 @@ package body Exp_Ch4 is
|
|||
return;
|
||||
end if;
|
||||
|
||||
-- If the case expression is a predicate specification, do not
|
||||
-- expand, because it will be converted to the proper predicate
|
||||
-- form when building the predicate function.
|
||||
-- If the case expression is a predicate specification, and the type
|
||||
-- to which it applies has a static predicate aspect, do not expand,
|
||||
-- because it will be converted to the proper predicate form later.
|
||||
|
||||
if Ekind_In (Current_Scope, E_Function, E_Procedure)
|
||||
and then Is_Predicate_Function (Current_Scope)
|
||||
and then
|
||||
Has_Static_Predicate_Aspect (Etype (First_Entity (Current_Scope)))
|
||||
then
|
||||
return;
|
||||
end if;
|
||||
|
|
|
@ -744,7 +744,7 @@ package body System.Fat_Gen is
|
|||
else
|
||||
Result := Machine (Radix_To_M_Minus_1 + Result) - Radix_To_M_Minus_1;
|
||||
|
||||
if Result > abs X then
|
||||
if Result > abs X then
|
||||
Result := Result - 1.0;
|
||||
end if;
|
||||
|
||||
|
|
|
@ -401,7 +401,7 @@ package body Sem_Aggr is
|
|||
-- is set in Resolve_Array_Aggregate but the aggregate is not
|
||||
-- immediately replaced with a raise CE. In fact, Array_Aggr_Subtype must
|
||||
-- first construct the proper itype for the aggregate (Gigi needs
|
||||
-- this). After constructing the proper itype we will eventually replace
|
||||
-- this). After constructing the proper itype we will eventually replace
|
||||
-- the top-level aggregate with a raise CE (done in Resolve_Aggregate).
|
||||
-- Of course in cases such as:
|
||||
--
|
||||
|
@ -412,7 +412,7 @@ package body Sem_Aggr is
|
|||
-- (in this particular case the bounds will be 1 .. 2).
|
||||
|
||||
procedure Make_String_Into_Aggregate (N : Node_Id);
|
||||
-- A string literal can appear in a context in which a one dimensional
|
||||
-- A string literal can appear in a context in which a one dimensional
|
||||
-- array of characters is expected. This procedure simply rewrites the
|
||||
-- string as an aggregate, prior to resolution.
|
||||
|
||||
|
@ -2718,7 +2718,7 @@ package body Sem_Aggr is
|
|||
if Etype (Imm_Type) = Base_Type (A_Type) then
|
||||
return True;
|
||||
|
||||
-- The base type of the parent type may appear as a private
|
||||
-- The base type of the parent type may appear as a private
|
||||
-- extension if it is declared as such in a parent unit of the
|
||||
-- current one. For consistency of the subsequent analysis use
|
||||
-- the partial view for the ancestor part.
|
||||
|
|
|
@ -149,7 +149,7 @@ package body Sem_Ch12 is
|
|||
-- However, for private types, this by itself does not insure that the
|
||||
-- proper VIEW of the entity is used (the full type may be visible at the
|
||||
-- point of generic definition, but not at instantiation, or vice-versa).
|
||||
-- In order to reference the proper view, we special-case any reference
|
||||
-- In order to reference the proper view, we special-case any reference
|
||||
-- to private types in the generic object, by saving both views, one in
|
||||
-- the generic and one in the semantic copy. At time of instantiation, we
|
||||
-- check whether the two views are consistent, and exchange declarations if
|
||||
|
@ -708,7 +708,7 @@ package body Sem_Ch12 is
|
|||
-- If the instantiation happens textually before the body of the generic,
|
||||
-- the instantiation of the body must be analyzed after the generic body,
|
||||
-- and not at the point of instantiation. Such early instantiations can
|
||||
-- happen if the generic and the instance appear in a package declaration
|
||||
-- happen if the generic and the instance appear in a package declaration
|
||||
-- because the generic body can only appear in the corresponding package
|
||||
-- body. Early instantiations can also appear if generic, instance and
|
||||
-- body are all in the declarative part of a subprogram or entry. Entities
|
||||
|
@ -807,7 +807,7 @@ package body Sem_Ch12 is
|
|||
-- Within the generic part, entities in the formal package are
|
||||
-- visible. To validate subsequent type declarations, indicate
|
||||
-- the correspondence between the entities in the analyzed formal,
|
||||
-- and the entities in the actual package. There are three packages
|
||||
-- and the entities in the actual package. There are three packages
|
||||
-- involved in the instantiation of a formal package: the parent
|
||||
-- generic P1 which appears in the generic declaration, the fake
|
||||
-- instantiation P2 which appears in the analyzed generic, and whose
|
||||
|
@ -1101,8 +1101,8 @@ package body Sem_Ch12 is
|
|||
-- include an Others clause.
|
||||
|
||||
procedure Process_Default (F : Entity_Id);
|
||||
-- Add a copy of the declaration of generic formal F to the list of
|
||||
-- associations, and add an explicit box association for F if there
|
||||
-- Add a copy of the declaration of generic formal F to the list of
|
||||
-- associations, and add an explicit box association for F if there
|
||||
-- is none yet, and the default comes from an Others_Choice.
|
||||
|
||||
function Renames_Standard_Subprogram (Subp : Entity_Id) return Boolean;
|
||||
|
@ -1268,7 +1268,7 @@ package body Sem_Ch12 is
|
|||
-- insert actuals for those defaults, and cannot rely on their
|
||||
-- names to disambiguate them.
|
||||
|
||||
if Actual = First_Named then
|
||||
if Actual = First_Named then
|
||||
Next (First_Named);
|
||||
|
||||
elsif Present (Actual) then
|
||||
|
@ -2883,7 +2883,7 @@ package body Sem_Ch12 is
|
|||
end if;
|
||||
|
||||
-- Default name may be overloaded, in which case the interpretation
|
||||
-- with the correct profile must be selected, as for a renaming.
|
||||
-- with the correct profile must be selected, as for a renaming.
|
||||
-- If the definition is an indexed component, it must denote a
|
||||
-- member of an entry family. If it is a selected component, it
|
||||
-- can be a protected operation.
|
||||
|
@ -4600,14 +4600,14 @@ package body Sem_Ch12 is
|
|||
Scope_Stack.Table (Scope_Stack.Last - J + 1).First_Use_Clause :=
|
||||
Use_Clauses (J);
|
||||
Install_Use_Clauses (Use_Clauses (J));
|
||||
end loop;
|
||||
end loop;
|
||||
|
||||
else
|
||||
for J in reverse 1 .. Num_Scopes loop
|
||||
Scope_Stack.Table (Scope_Stack.Last - J + 1).First_Use_Clause :=
|
||||
Use_Clauses (J);
|
||||
Install_Use_Clauses (Use_Clauses (J));
|
||||
end loop;
|
||||
end loop;
|
||||
end if;
|
||||
|
||||
-- Restore status of instances. If one of them is a body, make its
|
||||
|
@ -5897,7 +5897,7 @@ package body Sem_Ch12 is
|
|||
and then not Comes_From_Source (E1)
|
||||
and then Chars (E1) /= Chars (E2)
|
||||
then
|
||||
while Present (E1) and then Chars (E1) /= Chars (E2) loop
|
||||
while Present (E1) and then Chars (E1) /= Chars (E2) loop
|
||||
Next_Entity (E1);
|
||||
end loop;
|
||||
end if;
|
||||
|
@ -7695,14 +7695,14 @@ package body Sem_Ch12 is
|
|||
|
||||
begin
|
||||
E1 := First_Entity (P);
|
||||
while Present (E1) and then E1 /= Instance loop
|
||||
while Present (E1) and then E1 /= Instance loop
|
||||
if Ekind (E1) = E_Package
|
||||
and then Nkind (Parent (E1)) = N_Package_Renaming_Declaration
|
||||
then
|
||||
if Renamed_Object (E1) = Pack then
|
||||
return True;
|
||||
|
||||
elsif E1 = P or else Renamed_Object (E1) = P then
|
||||
elsif E1 = P or else Renamed_Object (E1) = P then
|
||||
return False;
|
||||
|
||||
elsif Is_Actual_Of_Previous_Formal (E1) then
|
||||
|
@ -8724,7 +8724,7 @@ package body Sem_Ch12 is
|
|||
if Scop = Par_I then
|
||||
null;
|
||||
|
||||
-- If the next node is a source body we must freeze in
|
||||
-- If the next node is a source body we must freeze in
|
||||
-- the current scope as well.
|
||||
|
||||
elsif Present (Next (N))
|
||||
|
@ -9472,7 +9472,7 @@ package body Sem_Ch12 is
|
|||
-- same order.
|
||||
|
||||
function Get_Formal_Entity (N : Node_Id) return Entity_Id;
|
||||
-- Retrieve entity of defining entity of generic formal parameter.
|
||||
-- Retrieve entity of defining entity of generic formal parameter.
|
||||
-- Only the declarations of formals need to be considered when
|
||||
-- linking them to actuals, but the declarative list may include
|
||||
-- internal entities generated during analysis, and those are ignored.
|
||||
|
@ -9571,7 +9571,7 @@ package body Sem_Ch12 is
|
|||
|
||||
Actual := Entity (Name (Original_Node (Formal_Node)));
|
||||
|
||||
-- The actual in the formal package declaration may be a
|
||||
-- The actual in the formal package declaration may be a
|
||||
-- renamed generic package, in which case we want to retrieve
|
||||
-- the original generic in order to traverse its formal part.
|
||||
|
||||
|
@ -9710,7 +9710,7 @@ package body Sem_Ch12 is
|
|||
Analyze (Actual);
|
||||
|
||||
if not Is_Entity_Name (Actual)
|
||||
or else Ekind (Entity (Actual)) /= E_Package
|
||||
or else Ekind (Entity (Actual)) /= E_Package
|
||||
then
|
||||
Error_Msg_N
|
||||
("expect package instance to instantiate formal", Actual);
|
||||
|
@ -12259,7 +12259,7 @@ package body Sem_Ch12 is
|
|||
end if;
|
||||
|
||||
-- Verify that limitedness matches. If parent is a limited
|
||||
-- interface then the generic formal is not unless declared
|
||||
-- interface then the generic formal is not unless declared
|
||||
-- explicitly so. If not declared limited, the actual cannot be
|
||||
-- limited (see AI05-0087).
|
||||
|
||||
|
|
|
@ -1208,39 +1208,28 @@ package body Sem_Ch13 is
|
|||
procedure Decorate (Asp : Node_Id; Prag : Node_Id);
|
||||
-- Establish linkages between an aspect and its corresponding pragma
|
||||
|
||||
procedure Insert_After_SPARK_Mode
|
||||
(Prag : Node_Id;
|
||||
Ins_Nod : Node_Id;
|
||||
Decls : List_Id);
|
||||
procedure Insert_Pragma
|
||||
(Prag : Node_Id;
|
||||
Is_Instance : Boolean := False);
|
||||
-- Subsidiary to the analysis of aspects
|
||||
-- Abstract_State
|
||||
-- Ghost
|
||||
-- Initializes
|
||||
-- Initial_Condition
|
||||
-- Refined_State
|
||||
-- Insert node Prag before node Ins_Nod. If Ins_Nod is for pragma
|
||||
-- SPARK_Mode, then skip SPARK_Mode. Decls is the associated declarative
|
||||
-- list where Prag is to reside.
|
||||
|
||||
procedure Insert_Pragma (Prag : Node_Id);
|
||||
-- Subsidiary to the analysis of aspects
|
||||
-- Attach_Handler
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Ghost
|
||||
-- Global
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
-- Post
|
||||
-- Pre
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_State
|
||||
-- SPARK_Mode
|
||||
-- Warnings
|
||||
-- Insert pragma Prag such that it mimics the placement of a source
|
||||
-- pragma of the same kind.
|
||||
--
|
||||
-- procedure Proc (Formal : ...) with Global => ...;
|
||||
--
|
||||
-- procedure Proc (Formal : ...);
|
||||
-- pragma Global (...);
|
||||
-- pragma of the same kind. Flag Is_Generic should be set when the
|
||||
-- context denotes a generic instance.
|
||||
|
||||
--------------
|
||||
-- Decorate --
|
||||
|
@ -1254,42 +1243,14 @@ package body Sem_Ch13 is
|
|||
Set_Parent (Prag, Asp);
|
||||
end Decorate;
|
||||
|
||||
-----------------------------
|
||||
-- Insert_After_SPARK_Mode --
|
||||
-----------------------------
|
||||
|
||||
procedure Insert_After_SPARK_Mode
|
||||
(Prag : Node_Id;
|
||||
Ins_Nod : Node_Id;
|
||||
Decls : List_Id)
|
||||
is
|
||||
Decl : Node_Id := Ins_Nod;
|
||||
|
||||
begin
|
||||
-- Skip SPARK_Mode
|
||||
|
||||
if Present (Decl)
|
||||
and then Nkind (Decl) = N_Pragma
|
||||
and then Pragma_Name (Decl) = Name_SPARK_Mode
|
||||
then
|
||||
Decl := Next (Decl);
|
||||
end if;
|
||||
|
||||
if Present (Decl) then
|
||||
Insert_Before (Decl, Prag);
|
||||
|
||||
-- Aitem acts as the last declaration
|
||||
|
||||
else
|
||||
Append_To (Decls, Prag);
|
||||
end if;
|
||||
end Insert_After_SPARK_Mode;
|
||||
|
||||
-------------------
|
||||
-- Insert_Pragma --
|
||||
-------------------
|
||||
|
||||
procedure Insert_Pragma (Prag : Node_Id) is
|
||||
procedure Insert_Pragma
|
||||
(Prag : Node_Id;
|
||||
Is_Instance : Boolean := False)
|
||||
is
|
||||
Aux : Node_Id;
|
||||
Decl : Node_Id;
|
||||
Decls : List_Id;
|
||||
|
@ -1365,7 +1326,39 @@ package body Sem_Ch13 is
|
|||
Set_Visible_Declarations (Specification (N), Decls);
|
||||
end if;
|
||||
|
||||
Prepend_To (Decls, Prag);
|
||||
-- The visible declarations of a generic instance have the
|
||||
-- following structure:
|
||||
|
||||
-- <renamings of generic formals>
|
||||
-- <renamings of internally-generated spec and body>
|
||||
-- <first source declaration>
|
||||
|
||||
-- Insert the pragma before the first source declaration by
|
||||
-- skipping the instance "header".
|
||||
|
||||
if Is_Instance then
|
||||
Decl := First (Decls);
|
||||
while Present (Decl) and then not Comes_From_Source (Decl) loop
|
||||
Decl := Next (Decl);
|
||||
end loop;
|
||||
|
||||
-- The instance "header" is followed by at least one source
|
||||
-- declaration.
|
||||
|
||||
if Present (Decl) then
|
||||
Insert_Before (Decl, Prag);
|
||||
|
||||
-- Otherwise the pragma is placed after the instance "header"
|
||||
|
||||
else
|
||||
Append_To (Decls, Prag);
|
||||
end if;
|
||||
|
||||
-- Otherwise this is not a generic instance
|
||||
|
||||
else
|
||||
Prepend_To (Decls, Prag);
|
||||
end if;
|
||||
|
||||
-- When the aspect is associated with a protected unit declaration,
|
||||
-- insert the generated pragma at the top of the visible declarations
|
||||
|
@ -2298,8 +2291,6 @@ package body Sem_Ch13 is
|
|||
|
||||
when Aspect_Abstract_State => Abstract_State : declare
|
||||
Context : Node_Id := N;
|
||||
Decl : Node_Id;
|
||||
Decls : List_Id;
|
||||
|
||||
begin
|
||||
-- When aspect Abstract_State appears on a generic package,
|
||||
|
@ -2318,54 +2309,12 @@ package body Sem_Ch13 is
|
|||
Make_Pragma_Argument_Association (Loc,
|
||||
Expression => Relocate_Node (Expr))),
|
||||
Pragma_Name => Name_Abstract_State);
|
||||
|
||||
Decorate (Aspect, Aitem);
|
||||
|
||||
Decls := Visible_Declarations (Specification (Context));
|
||||
|
||||
-- In general pragma Abstract_State must be at the top
|
||||
-- of the existing visible declarations to emulate its
|
||||
-- source counterpart. The only exception to this is a
|
||||
-- generic instance in which case the pragma must be
|
||||
-- inserted after the association renamings.
|
||||
|
||||
if Present (Decls) then
|
||||
Decl := First (Decls);
|
||||
|
||||
-- The visible declarations of a generic instance have
|
||||
-- the following structure:
|
||||
|
||||
-- <renamings of generic formals>
|
||||
-- <renamings of internally-generated spec and body>
|
||||
-- <first source declaration>
|
||||
|
||||
-- The pragma must be inserted before the first source
|
||||
-- declaration, skip the instance "header".
|
||||
|
||||
if Is_Generic_Instance (Defining_Entity (Context)) then
|
||||
while Present (Decl)
|
||||
and then not Comes_From_Source (Decl)
|
||||
loop
|
||||
Decl := Next (Decl);
|
||||
end loop;
|
||||
end if;
|
||||
|
||||
-- When aspects Abstract_State, Ghost,
|
||||
-- Initial_Condition and Initializes are out of order,
|
||||
-- ensure that pragma SPARK_Mode is always at the top
|
||||
-- of the declarations to properly enabled/suppress
|
||||
-- errors.
|
||||
|
||||
Insert_After_SPARK_Mode
|
||||
(Prag => Aitem,
|
||||
Ins_Nod => Decl,
|
||||
Decls => Decls);
|
||||
|
||||
-- Otherwise the pragma forms a new declarative list
|
||||
|
||||
else
|
||||
Set_Visible_Declarations
|
||||
(Specification (Context), New_List (Aitem));
|
||||
end if;
|
||||
Insert_Pragma
|
||||
(Prag => Aitem,
|
||||
Is_Instance =>
|
||||
Is_Generic_Instance (Defining_Entity (Context)));
|
||||
|
||||
else
|
||||
Error_Msg_NE
|
||||
|
@ -2526,10 +2475,7 @@ package body Sem_Ch13 is
|
|||
-- declarations or after an object, a [generic] subprogram, or
|
||||
-- a type declaration.
|
||||
|
||||
when Aspect_Ghost => Ghost : declare
|
||||
Decls : List_Id;
|
||||
|
||||
begin
|
||||
when Aspect_Ghost =>
|
||||
Make_Aitem_Pragma
|
||||
(Pragma_Argument_Associations => New_List (
|
||||
Make_Pragma_Argument_Association (Loc,
|
||||
|
@ -2537,40 +2483,8 @@ package body Sem_Ch13 is
|
|||
Pragma_Name => Name_Ghost);
|
||||
|
||||
Decorate (Aspect, Aitem);
|
||||
|
||||
-- When the aspect applies to a [generic] package, insert
|
||||
-- the pragma at the top of the visible declarations. This
|
||||
-- emulates the placement of a source pragma.
|
||||
|
||||
if Nkind_In (N, N_Generic_Package_Declaration,
|
||||
N_Package_Declaration)
|
||||
then
|
||||
Decls := Visible_Declarations (Specification (N));
|
||||
|
||||
if No (Decls) then
|
||||
Decls := New_List;
|
||||
Set_Visible_Declarations (N, Decls);
|
||||
end if;
|
||||
|
||||
-- When aspects Abstract_State, Ghost, Initial_Condition
|
||||
-- and Initializes are out of order, ensure that pragma
|
||||
-- SPARK_Mode is always at the top of the declarations to
|
||||
-- properly enabled/suppress errors.
|
||||
|
||||
Insert_After_SPARK_Mode
|
||||
(Prag => Aitem,
|
||||
Ins_Nod => First (Decls),
|
||||
Decls => Decls);
|
||||
|
||||
-- Otherwise the context is an object, [generic] subprogram
|
||||
-- or type declaration.
|
||||
|
||||
else
|
||||
Insert_Pragma (Aitem);
|
||||
end if;
|
||||
|
||||
Insert_Pragma (Aitem);
|
||||
goto Continue;
|
||||
end Ghost;
|
||||
|
||||
-- Global
|
||||
|
||||
|
@ -2604,7 +2518,6 @@ package body Sem_Ch13 is
|
|||
|
||||
when Aspect_Initial_Condition => Initial_Condition : declare
|
||||
Context : Node_Id := N;
|
||||
Decls : List_Id;
|
||||
|
||||
begin
|
||||
-- When aspect Initial_Condition appears on a generic
|
||||
|
@ -2618,30 +2531,20 @@ package body Sem_Ch13 is
|
|||
if Nkind_In (Context, N_Generic_Package_Declaration,
|
||||
N_Package_Declaration)
|
||||
then
|
||||
Decls := Visible_Declarations (Specification (Context));
|
||||
|
||||
Make_Aitem_Pragma
|
||||
(Pragma_Argument_Associations => New_List (
|
||||
Make_Pragma_Argument_Association (Loc,
|
||||
Expression => Relocate_Node (Expr))),
|
||||
Pragma_Name =>
|
||||
Name_Initial_Condition);
|
||||
|
||||
Decorate (Aspect, Aitem);
|
||||
Insert_Pragma
|
||||
(Prag => Aitem,
|
||||
Is_Instance =>
|
||||
Is_Generic_Instance (Defining_Entity (Context)));
|
||||
|
||||
if No (Decls) then
|
||||
Decls := New_List;
|
||||
Set_Visible_Declarations (Context, Decls);
|
||||
end if;
|
||||
|
||||
-- When aspects Abstract_State, Ghost, Initial_Condition
|
||||
-- and Initializes are out of order, ensure that pragma
|
||||
-- SPARK_Mode is always at the top of the declarations to
|
||||
-- properly enabled/suppress errors.
|
||||
|
||||
Insert_After_SPARK_Mode
|
||||
(Prag => Aitem,
|
||||
Ins_Nod => First (Decls),
|
||||
Decls => Decls);
|
||||
-- Otherwise the context is illegal
|
||||
|
||||
else
|
||||
Error_Msg_NE
|
||||
|
@ -2663,7 +2566,6 @@ package body Sem_Ch13 is
|
|||
|
||||
when Aspect_Initializes => Initializes : declare
|
||||
Context : Node_Id := N;
|
||||
Decls : List_Id;
|
||||
|
||||
begin
|
||||
-- When aspect Initializes appears on a generic package,
|
||||
|
@ -2677,29 +2579,19 @@ package body Sem_Ch13 is
|
|||
if Nkind_In (Context, N_Generic_Package_Declaration,
|
||||
N_Package_Declaration)
|
||||
then
|
||||
Decls := Visible_Declarations (Specification (Context));
|
||||
|
||||
Make_Aitem_Pragma
|
||||
(Pragma_Argument_Associations => New_List (
|
||||
Make_Pragma_Argument_Association (Loc,
|
||||
Expression => Relocate_Node (Expr))),
|
||||
Pragma_Name => Name_Initializes);
|
||||
|
||||
Decorate (Aspect, Aitem);
|
||||
Insert_Pragma
|
||||
(Prag => Aitem,
|
||||
Is_Instance =>
|
||||
Is_Generic_Instance (Defining_Entity (Context)));
|
||||
|
||||
if No (Decls) then
|
||||
Decls := New_List;
|
||||
Set_Visible_Declarations (Context, Decls);
|
||||
end if;
|
||||
|
||||
-- When aspects Abstract_State, Ghost, Initial_Condition
|
||||
-- and Initializes are out of order, ensure that pragma
|
||||
-- SPARK_Mode is always at the top of the declarations to
|
||||
-- properly enabled/suppress errors.
|
||||
|
||||
Insert_After_SPARK_Mode
|
||||
(Prag => Aitem,
|
||||
Ins_Nod => First (Decls),
|
||||
Decls => Decls);
|
||||
-- Otherwise the context is illegal
|
||||
|
||||
else
|
||||
Error_Msg_NE
|
||||
|
@ -2813,39 +2705,24 @@ package body Sem_Ch13 is
|
|||
|
||||
-- Refined_State
|
||||
|
||||
when Aspect_Refined_State => Refined_State : declare
|
||||
Decls : List_Id;
|
||||
when Aspect_Refined_State =>
|
||||
|
||||
begin
|
||||
-- The corresponding pragma for Refined_State is inserted in
|
||||
-- the declarations of the related package body. This action
|
||||
-- synchronizes both the source and from-aspect versions of
|
||||
-- the pragma.
|
||||
|
||||
if Nkind (N) = N_Package_Body then
|
||||
Decls := Declarations (N);
|
||||
|
||||
Make_Aitem_Pragma
|
||||
(Pragma_Argument_Associations => New_List (
|
||||
Make_Pragma_Argument_Association (Loc,
|
||||
Expression => Relocate_Node (Expr))),
|
||||
Pragma_Name => Name_Refined_State);
|
||||
|
||||
Decorate (Aspect, Aitem);
|
||||
Insert_Pragma (Aitem);
|
||||
|
||||
if No (Decls) then
|
||||
Decls := New_List;
|
||||
Set_Declarations (N, Decls);
|
||||
end if;
|
||||
|
||||
-- Pragma Refined_State must be inserted after pragma
|
||||
-- SPARK_Mode in the tree. This ensures that any error
|
||||
-- messages dependent on SPARK_Mode will be properly
|
||||
-- enabled/suppressed.
|
||||
|
||||
Insert_After_SPARK_Mode
|
||||
(Prag => Aitem,
|
||||
Ins_Nod => First (Decls),
|
||||
Decls => Decls);
|
||||
-- Otherwise the context is illegal
|
||||
|
||||
else
|
||||
Error_Msg_NE
|
||||
|
@ -2853,7 +2730,6 @@ package body Sem_Ch13 is
|
|||
end if;
|
||||
|
||||
goto Continue;
|
||||
end Refined_State;
|
||||
|
||||
-- Relative_Deadline
|
||||
|
||||
|
|
|
@ -1802,7 +1802,7 @@ package body Sem_Ch4 is
|
|||
-- call to a user-defined equality operator.
|
||||
|
||||
-- For the predefined case, the result is Boolean, regardless of the
|
||||
-- type of the operands. The operands may even be limited, if they are
|
||||
-- type of the operands. The operands may even be limited, if they are
|
||||
-- generic actuals. If they are overloaded, label the left argument with
|
||||
-- the common type that must be present, or with the type of the formal
|
||||
-- of the user-defined function.
|
||||
|
@ -3196,7 +3196,7 @@ package body Sem_Ch4 is
|
|||
-- Try_Indexed_Call and there is nothing else to do.
|
||||
|
||||
if Is_Indexed
|
||||
and then Nkind (N) = N_Slice
|
||||
and then Nkind (N) = N_Slice
|
||||
then
|
||||
return;
|
||||
end if;
|
||||
|
@ -5422,7 +5422,7 @@ package body Sem_Ch4 is
|
|||
-- and no further processing is required (this is the case of an
|
||||
-- operator constructed by Exp_Fixd for a fixed point operation)
|
||||
-- Otherwise add one interpretation with universal fixed result
|
||||
-- If the operator is given in functional notation, it comes
|
||||
-- If the operator is given in functional notation, it comes
|
||||
-- from source and Fixed_As_Integer cannot apply.
|
||||
|
||||
if (Nkind (N) not in N_Op
|
||||
|
|
|
@ -107,7 +107,7 @@ package body Sem_Ch8 is
|
|||
-- Open scopes, that is to say scopes currently being compiled, have their
|
||||
-- corresponding rows of entities in order, innermost scope first.
|
||||
|
||||
-- The scopes of packages that are mentioned in context clauses appear in
|
||||
-- The scopes of packages that are mentioned in context clauses appear in
|
||||
-- no particular order, interspersed among open scopes. This is because
|
||||
-- in the course of analyzing the context of a compilation, a package
|
||||
-- declaration is first an open scope, and subsequently an element of the
|
||||
|
@ -191,7 +191,7 @@ package body Sem_Ch8 is
|
|||
-- removed from visibility chains on exit from the corresponding scope.
|
||||
-- From the outside, these entities are always accessed by selected
|
||||
-- notation, and the entity chain for the record type, protected type,
|
||||
-- etc. is traversed sequentially in order to find the designated entity.
|
||||
-- etc. is traversed sequentially in order to find the designated entity.
|
||||
|
||||
-- The discriminants of a type and the operations of a protected type or
|
||||
-- task are unchained on exit from the first view of the type, (such as
|
||||
|
@ -224,7 +224,7 @@ package body Sem_Ch8 is
|
|||
|
||||
-- The Rtsfind mechanism can force a call to Semantics while another
|
||||
-- compilation is in progress. The unit retrieved by Rtsfind must be
|
||||
-- compiled in its own context, and has no access to the visibility of
|
||||
-- compiled in its own context, and has no access to the visibility of
|
||||
-- the unit currently being compiled. The procedures Save_Scope_Stack and
|
||||
-- Restore_Scope_Stack make entities in current open scopes invisible
|
||||
-- before compiling the retrieved unit, and restore the compilation
|
||||
|
|
|
@ -814,7 +814,7 @@ package body Sem_Eval is
|
|||
V := UI_Negate (Intval (Right_Opnd (N)));
|
||||
return;
|
||||
|
||||
elsif Nkind (N) = N_Attribute_Reference then
|
||||
elsif Nkind (N) = N_Attribute_Reference then
|
||||
if Attribute_Name (N) = Name_Succ then
|
||||
R := First (Expressions (N));
|
||||
V := Uint_1;
|
||||
|
@ -2909,7 +2909,7 @@ package body Sem_Eval is
|
|||
-- Eval_Op_Not --
|
||||
-----------------
|
||||
|
||||
-- The not operation is a static functions, so the result is potentially
|
||||
-- The not operation is a static functions, so the result is potentially
|
||||
-- static if the operand is potentially static (RM 4.9(7), 4.9(20)).
|
||||
|
||||
procedure Eval_Op_Not (N : Node_Id) is
|
||||
|
|
File diff suppressed because it is too large
Load Diff
|
@ -251,7 +251,7 @@ package body Sem_Res is
|
|||
(N : Node_Id;
|
||||
Op : Entity_Id;
|
||||
Typ : Entity_Id);
|
||||
-- An operator can rename another, e.g. in an instantiation. In that
|
||||
-- An operator can rename another, e.g. in an instantiation. In that
|
||||
-- case, the proper operator node must be constructed and resolved.
|
||||
|
||||
procedure Set_String_Literal_Subtype (N : Node_Id; Typ : Entity_Id);
|
||||
|
@ -2285,7 +2285,7 @@ package body Sem_Res is
|
|||
then
|
||||
exit Interp_Loop;
|
||||
|
||||
elsif Nkind (N) in N_Unary_Op
|
||||
elsif Nkind (N) in N_Unary_Op
|
||||
and then Etype (Right_Opnd (N)) = Any_Type
|
||||
then
|
||||
exit Interp_Loop;
|
||||
|
@ -11234,7 +11234,7 @@ package body Sem_Res is
|
|||
New_N : Node_Id;
|
||||
|
||||
begin
|
||||
if Nkind (N) in N_Binary_Op then
|
||||
if Nkind (N) in N_Binary_Op then
|
||||
Append (Left_Opnd (N), Actuals);
|
||||
end if;
|
||||
|
||||
|
|
|
@ -1977,7 +1977,7 @@ package body Sem_Type is
|
|||
return It2;
|
||||
end if;
|
||||
|
||||
elsif Nkind (N) in N_Unary_Op then
|
||||
elsif Nkind (N) in N_Unary_Op then
|
||||
if Etype (Right_Opnd (N)) = Etype (First_Formal (Nam1)) then
|
||||
return It1;
|
||||
else
|
||||
|
|
Loading…
Reference in New Issue