+2011-08-02 Yannick Moy <moy@adacore.com>
+
+ * einfo.adb, einfo.ads (Body_Is_In_ALFA, Set_Body_Is_In_ALFA): get/set
+ for new flag denoting which subprogram bodies are in ALFA
+ * restrict.adb, sem_ch7.adb: Update comment
+ * sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb,
+ sem_ch9.adb, sem_res.adb: Add calls to
+ Current_Subprogram_Body_Is_Not_In_ALFA on unsupported constructs.
+ * sem_ch6.adb (Analyze_Function_Return): add calls to
+ Current_Subprogram_Body_Is_Not_In_ALFA on return statement in the
+ middle of the body, and extended return.
+ (Check_Missing_Return): add calls to Set_Body_Is_In_ALFA with argument
+ False when missing return.
+ (Analyze_Subprogram_Body_Helper): initialize the flag Body_Is_In_ALFA
+ to True for subprograms whose spec is in ALFA. Remove later on the flag
+ on the entity used for a subprogram body when there exists a separate
+ declaration.
+ * sem_util.adb, sem_util.ads (Current_Subprogram_Body_Is_Not_In_ALFA):
+ if Current_Subprogram is not Empty, set its flag Body_Is_In_ALFA to
+ False, otherwise do nothing.
+
2011-08-02 Robert Dewar <dewar@adacore.com>
* inline.adb, stand.ads, sem_ch6.adb, sem_ch8.adb: Minor reformatting.
-- Is_Safe_To_Reevaluate Flag249
-- Has_Predicates Flag250
- -- (unused) Flag251
+ -- Body_Is_In_ALFA Flag251
-- (unused) Flag252
-- (unused) Flag253
-- (unused) Flag254
return Node19 (Id);
end Body_Entity;
+ function Body_Is_In_ALFA (Id : E) return B is
+ begin
+ pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+ return Flag251 (Id);
+ end Body_Is_In_ALFA;
+
function Body_Needed_For_SAL (Id : E) return B is
begin
pragma Assert
Set_Node19 (Id, V);
end Set_Body_Entity;
+ procedure Set_Body_Is_In_ALFA (Id : E; V : B := True) is
+ begin
+ pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+ Set_Flag251 (Id, V);
+ end Set_Body_Is_In_ALFA;
+
procedure Set_Body_Needed_For_SAL (Id : E; V : B := True) is
begin
pragma Assert
end if;
W ("Address_Taken", Flag104 (Id));
+ W ("Body_Is_In_ALFA", Flag251 (Id));
W ("Body_Needed_For_SAL", Flag40 (Id));
W ("C_Pass_By_Copy", Flag125 (Id));
W ("Can_Never_Be_Null", Flag38 (Id));
-- S p e c --
-- --
-- Copyright (C) 1992-2011, 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- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- Present in package and generic package entities, points to the
-- corresponding package body entity if one is present.
+-- Body_Is_In_ALFA (Flag251)
+-- Present in subprogram entities. Set for subprograms whose body belongs
+-- to the ALFA subset, which are eligible for formal verification through
+-- SPARK or Why tool-sets.
+
-- Body_Needed_For_SAL (Flag40)
-- Present in package and subprogram entities that are compilation
-- units. Indicates that the source for the body must be included
-- Is_In_ALFA (Flag151)
-- Present in all entities. Set for entities that belong to the ALFA
-- subset, which are eligible for formal verification through SPARK or
--- Why tool-sets.
+-- Why tool-sets. For a subprogram, this only means that a call to the
+-- subprogram can be formally analyzed. Another flag, Body_Is_In_ALFA,
+-- defines which subprograms can be formally analyzed.
-- Is_Inlined (Flag11)
-- Present in all entities. Set for functions and procedures which are
-- E_Anonymous_Access_Protected_Subprogram_Type
E_Anonymous_Access_Type;
- subtype Access_Subprogram_Kind is Entity_Kind range
+ subtype Access_Subprogram_Kind is Entity_Kind range
E_Access_Subprogram_Type ..
-- E_Anonymous_Access_Subprogram_Type
-- E_Access_Protected_Subprogram_Type
-- E_Floating_Point_Type
E_Floating_Point_Subtype;
- subtype Object_Kind is Entity_Kind range
+ subtype Object_Kind is Entity_Kind range
E_Component ..
-- E_Constant
-- E_Discriminant
function Barrier_Function (Id : E) return N;
function Block_Node (Id : E) return N;
function Body_Entity (Id : E) return E;
+ function Body_Is_In_ALFA (Id : E) return B;
function Body_Needed_For_SAL (Id : E) return B;
function CR_Discriminant (Id : E) return E;
function C_Pass_By_Copy (Id : E) return B;
procedure Set_Barrier_Function (Id : E; V : N);
procedure Set_Block_Node (Id : E; V : N);
procedure Set_Body_Entity (Id : E; V : E);
+ procedure Set_Body_Is_In_ALFA (Id : E; V : B := True);
procedure Set_Body_Needed_For_SAL (Id : E; V : B := True);
procedure Set_CR_Discriminant (Id : E; V : E);
procedure Set_C_Pass_By_Copy (Id : E; V : B := True);
pragma Inline (Barrier_Function);
pragma Inline (Block_Node);
pragma Inline (Body_Entity);
+ pragma Inline (Body_Is_In_ALFA);
pragma Inline (Body_Needed_For_SAL);
pragma Inline (CR_Discriminant);
pragma Inline (C_Pass_By_Copy);
pragma Inline (Set_Barrier_Function);
pragma Inline (Set_Block_Node);
pragma Inline (Set_Body_Entity);
+ pragma Inline (Set_Body_Is_In_ALFA);
pragma Inline (Set_Body_Needed_For_SAL);
pragma Inline (Set_CR_Discriminant);
pragma Inline (Set_C_Pass_By_Copy);
return;
end if;
- -- In formal mode, issue an error for any use of class-wide, even if the
+ -- In SPARK mode, issue an error for any use of class-wide, even if the
-- No_Dispatch restriction is not set.
if R = No_Dispatch then
P : Node_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("raise statement is not allowed", N);
Check_Unreachable_Code (N);
-- Start of processing for Analyze_Raise_xxx_Error
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("raise statement is not allowed", N);
if No (Etype (N)) then
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2007, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
------------------------------------------------------------------------------
with Atree; use Atree;
+with Einfo; use Einfo;
with Errout; use Errout;
with Namet; use Namet;
with Opt; use Opt;
with Restrict; use Restrict;
with Rident; use Rident;
with Sem_Ch8; use Sem_Ch8;
+with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Stand; use Stand;
with Uintp; use Uintp;
return;
else
Find_Direct_Name (N);
+
+ if Present (Entity (N))
+ and then Is_Object (Entity (N))
+ and then not Is_In_ALFA (Entity (N))
+ then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+ end if;
end if;
end Analyze_Identifier;
Act_T := T;
- -- The object is in ALFA if-and-only-if its type is in ALFA
+ -- The object is in ALFA if-and-only-if its type is in ALFA and it is
+ -- not aliased.
- if Is_In_ALFA (T) then
+ if Is_In_ALFA (T) and then not Aliased_Present (N) then
Set_Is_In_ALFA (Id);
+ else
+ Current_Subprogram_Body_Is_Not_In_ALFA;
end if;
-- These checks should be performed before the initialization expression
procedure Analyze_Aggregate (N : Node_Id) is
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
if No (Etype (N)) then
Set_Etype (N, Any_Composite);
end if;
C : Node_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("allocator is not allowed", N);
-- Deal with allocator restrictions
return;
end if;
+ -- If this is an indirect call, or the subprogram called is not in
+ -- ALFA, then the call is not in ALFA.
+
+ if not Is_Subprogram (Nam_Ent)
+ or else not Is_In_ALFA (Nam_Ent)
+ then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+ end if;
+
Analyze_One_Call (N, Nam_Ent, True, Success);
-- If this is an indirect call, the return type of the access_to
L : Node_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
Candidate_Type := Empty;
-- The following code is equivalent to:
return;
end if;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("conditional expression is not allowed", N);
Else_Expr := Next (Then_Expr);
-- Start of processing for Analyze_Explicit_Dereference
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("explicit dereference is not allowed", N);
Analyze (P);
-- Start of processing for Analyze_Membership_Op
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
Analyze_Expression (L);
if No (R)
procedure Analyze_Null (N : Node_Id) is
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("null is not allowed", N);
Set_Etype (N, Any_Access);
T : Entity_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
Analyze_Expression (Expr);
Set_Etype (N, Any_Type);
Iterator : Node_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("quantified expression is not allowed", N);
Set_Etype (Ent, Standard_Void_Type);
Acc_Type : Entity_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
Analyze (P);
-- An interesting error check, if we take the 'Reference of an object
-- Start of processing for Analyze_Slice
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("slice is not allowed", N);
Analyze (P);
T : Entity_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
-- If Conversion_OK is set, then the Etype is already set, and the
-- only processing required is to analyze the expression. This is
-- used to construct certain "illegal" conversions which are not
procedure Analyze_Unchecked_Type_Conversion (N : Node_Id) is
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Find_Type (Subtype_Mark (N));
Analyze_Expression (Expression (N));
Set_Etype (N, Entity (Subtype_Mark (N)));
HSS : constant Node_Id := Handled_Statement_Sequence (N);
begin
- -- In formal mode, we reject block statements. Note that the case of
+ -- In SPARK mode, we reject block statements. Note that the case of
-- block statements generated by the expander is fine.
if Nkind (Original_Node (N)) = N_Block_Statement then
if Others_Present
and then List_Length (Alternatives (N)) = 1
then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("OTHERS as unique case alternative is not allowed", N);
end if;
else
if Has_Loop_In_Inner_Open_Scopes (U_Name) then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("exit label must name the closest enclosing loop", N);
end if;
Check_Unset_Reference (Cond);
end if;
- -- In formal mode, verify that the exit statement respects the SPARK
+ -- In SPARK mode, verify that the exit statement respects the SPARK
-- restrictions.
if Present (Cond) then
if Nkind (Parent (N)) /= N_Loop_Statement then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("exit with when clause must be directly in loop", N);
end if;
else
if Nkind (Parent (N)) /= N_If_Statement then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
if Nkind (Parent (N)) = N_Elsif_Part then
Check_SPARK_Restriction
("exit must be in IF without ELSIF", N);
end if;
elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("exit must be in IF directly in loop", N);
-- leads to an error mentioning the ELSE.
elsif Present (Else_Statements (Parent (N))) then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("exit must be in IF without ELSE", N);
-- An exit in an ELSIF does not reach here, as it would have been
-- detected in the case (Nkind (Parent (N)) /= N_If_Statement).
elsif Present (Elsif_Parts (Parent (N))) then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("exit must be in IF without ELSIF", N);
end if;
end if;
Label_Ent : Entity_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("goto statement is not allowed", N);
-- Actual semantic checks
(Nkind (Parent (Parent (N))) /= N_Subprogram_Body
or else Present (Next (N)))
then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("RETURN should be the last statement in function", N);
end if;
else
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("extended RETURN is not allowed", N);
-- Analyze parts specific to extended_return_statement:
and then not Nkind_In (Stat, N_Simple_Return_Statement,
N_Extended_Return_Statement)
then
+ Set_Body_Is_In_ALFA (Id, False);
Check_SPARK_Restriction
("last statement in function should be RETURN", Stat);
end if;
-- borrow the Check_Returns procedure here ???
if Return_Present (Id) then
+ Set_Body_Is_In_ALFA (Id, False);
Check_SPARK_Restriction
("procedure should not have RETURN", N);
end if;
end if;
end if;
+ -- By default, consider that the subprogram body is in ALFA if the spec
+ -- is in ALFA. This is reversed later if some expression or statement is
+ -- not in ALFA.
+
+ declare
+ Id : Entity_Id;
+ begin
+ if Present (Spec_Id) then
+ Id := Spec_Id;
+ else
+ Id := Body_Id;
+ end if;
+
+ if Is_In_ALFA (Id) then
+ Set_Body_Is_In_ALFA (Id);
+ end if;
+ end;
+
-- Do not inline any subprogram that contains nested subprograms, since
-- the backend inlining circuit seems to generate uninitialized
-- references in this case. We know this happens in the case of front
Set_Ekind (Body_Id, E_Subprogram_Body);
Set_Scope (Body_Id, Scope (Spec_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
+ Set_Is_In_ALFA (Body_Id, False);
-- Case of subprogram body with no previous spec
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
-- package.
procedure Check_One_Tagged_Type_Or_Extension_At_Most;
- -- Issue an error in formal mode if a package specification contains
- -- more than one tagged type or type extension. This is a restriction of
- -- SPARK.
+ -- Issue an error in SPARK mode if a package specification contains
+ -- more than one tagged type or type extension.
procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id);
-- Clears constant indications (Never_Set_In_Source, Constant_Value, and
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("abort statement is not allowed", N);
T_Name := First (Names (N));
procedure Analyze_Accept_Alternative (N : Node_Id) is
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Pragmas_Before (N)) then
Analyze_List (Pragmas_Before (N));
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("accept statement is not allowed", N);
-- Entry name is initialized to Any_Id. It should get reset to the
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("select statement is not allowed", N);
Check_Restriction (Max_Asynchronous_Select_Nesting, N);
Check_Restriction (No_Select_Statements, N);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("select statement is not allowed", N);
Check_Restriction (No_Select_Statements, N);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_Restriction (No_Delay, N);
if Present (Pragmas_Before (N)) then
E : constant Node_Id := Expression (N);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("delay statement is not allowed", N);
Check_Restriction (No_Relative_Delay, N);
Check_Restriction (No_Delay, N);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("delay statement is not allowed", N);
Check_Restriction (No_Delay, N);
Check_Potentially_Blocking_Operation (N);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
-- Entry_Name is initialized to Any_Id. It should get reset to the
-- matching entry entity. An error is signalled if it is not reset
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Index) then
Analyze (Index);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("entry call is not allowed", N);
if Present (Pragmas_Before (N)) then
begin
Generate_Definition (Def_Id);
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
-- Case of no discrete subtype definition
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Analyze (Def);
-- There is no elaboration of the entry index specification. Therefore,
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Set_Ekind (Body_Id, E_Protected_Body);
Spec_Id := Find_Concurrent_Spec (Body_Id);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("protected definition is not allowed", N);
Analyze_Declarations (Visible_Declarations (N));
end if;
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_Restriction (No_Protected_Types, N);
T := Find_Type_Name (N);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("requeue statement is not allowed", N);
Check_Restriction (No_Requeue_Statements, N);
Check_Unreachable_Code (N);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("select statement is not allowed", N);
Check_Restriction (No_Select_Statements, N);
begin
Generate_Definition (Id);
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
-- The node is rewritten as a protected type declaration, in exact
-- analogy with what is done with single tasks.
begin
Generate_Definition (Id);
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
-- The node is rewritten as a task type declaration, followed by an
-- object declaration of that anonymous task type.
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Set_Ekind (Body_Id, E_Task_Body);
Set_Scope (Body_Id, Current_Scope);
Spec_Id := Find_Concurrent_Spec (Body_Id);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("task definition is not allowed", N);
if Present (Visible_Declarations (N)) then
begin
Check_Restriction (No_Tasking, N);
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
T := Find_Type_Name (N);
Generate_Definition (T);
procedure Analyze_Terminate_Alternative (N : Node_Id) is
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Pragmas_Before (N)) then
Analyze_List (Pragmas_Before (N));
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("select statement is not allowed", N);
Check_Restriction (No_Select_Statements, N);
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Pragmas_Before (N)) then
Analyze_List (Pragmas_Before (N));
-- types or array types except String.
if Is_Boolean_Type (T) then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("comparison is not defined on Boolean type", N);
- elsif Is_Array_Type (T)
- and then Base_Type (T) /= Standard_String
- then
- Check_SPARK_Restriction
- ("comparison is not defined on array types other than String", N);
+
+ elsif Is_Array_Type (T) then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
+ if Base_Type (T) /= Standard_String then
+ Check_SPARK_Restriction
+ ("comparison is not defined on array types other than String",
+ N);
+ end if;
+
else
null;
end if;
-- String are only defined when, for each index position, the
-- operands have equal static bounds.
- if Is_Array_Type (T)
- and then Base_Type (T) /= Standard_String
- and then Base_Type (Etype (L)) = Base_Type (Etype (R))
- and then Etype (L) /= Any_Composite -- or else L in error
- and then Etype (R) /= Any_Composite -- or else R in error
- and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
- then
- Check_SPARK_Restriction
- ("array types should have matching static bounds", N);
+ if Is_Array_Type (T) then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
+ if Base_Type (T) /= Standard_String
+ and then Base_Type (Etype (L)) = Base_Type (Etype (R))
+ and then Etype (L) /= Any_Composite -- or else L in error
+ and then Etype (R) /= Any_Composite -- or else R in error
+ and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
+ then
+ Check_SPARK_Restriction
+ ("array types should have matching static bounds", N);
+ end if;
end if;
-- If the unique type is a class-wide type then it will be expanded
if Is_Array_Type (B_Typ)
and then Nkind (N) in N_Binary_Op
then
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
declare
Left_Typ : constant Node_Id := Etype (Left_Opnd (N));
Right_Typ : constant Node_Id := Etype (Right_Opnd (N));
end if;
end Current_Subprogram;
+ --------------------------------------------
+ -- Current_Subprogram_Body_Is_Not_In_ALFA --
+ --------------------------------------------
+
+ procedure Current_Subprogram_Body_Is_Not_In_ALFA is
+ Cur_Subp : constant Entity_Id := Current_Subprogram;
+ begin
+ if Present (Cur_Subp)
+ and then (Is_Subprogram (Cur_Subp)
+ or else Is_Generic_Subprogram (Cur_Subp))
+ then
+ Set_Body_Is_In_ALFA (Cur_Subp, False);
+ end if;
+ end Current_Subprogram_Body_Is_Not_In_ALFA;
+
---------------------
-- Defining_Entity --
---------------------
-- Current_Scope is returned. The returned value is Empty if this is called
-- from a library package which is not within any subprogram.
+ procedure Current_Subprogram_Body_Is_Not_In_ALFA;
+ -- If Current_Subprogram is not Empty, set its flag Body_Is_In_ALFA to
+ -- False, otherwise do nothing.
+
function Defining_Entity (N : Node_Id) return Entity_Id;
-- Given a declaration N, returns the associated defining entity. If the
-- declaration has a specification, the entity is obtained from the