Follow-up of changes to define which entities are in the ALFA subset for formal
verification. Here, we define a flag Body_Is_In_ALFA that applies to entities
for subprograms, which is set to True when the subprogram body can be analyzed
formally. This is the initial definition, to be refined.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-02 Yannick Moy <m...@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.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 177175)
+++ sem_ch3.adb (working copy)
@@ -3030,10 +3030,13 @@
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
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb (revision 177175)
+++ sem_ch5.adb (working copy)
@@ -815,7 +815,7 @@
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
@@ -1113,6 +1113,7 @@
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;
@@ -1194,6 +1195,7 @@
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;
@@ -1235,17 +1237,19 @@
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);
@@ -1254,6 +1258,7 @@
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);
@@ -1261,12 +1266,14 @@
-- 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;
@@ -1295,6 +1302,7 @@
Label_Ent : Entity_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("goto statement is not allowed", N);
-- Actual semantic checks
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 177156)
+++ sem_ch7.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- 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- --
@@ -875,9 +875,8 @@
-- 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
Index: sem_ch9.adb
===================================================================
--- sem_ch9.adb (revision 177175)
+++ sem_ch9.adb (working copy)
@@ -101,6 +101,7 @@
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));
@@ -139,6 +140,7 @@
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));
@@ -172,6 +174,7 @@
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
@@ -403,6 +406,7 @@
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);
@@ -449,6 +453,7 @@
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);
@@ -495,6 +500,7 @@
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_Restriction (No_Delay, N);
if Present (Pragmas_Before (N)) then
@@ -546,6 +552,7 @@
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);
@@ -564,6 +571,7 @@
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);
@@ -592,6 +600,7 @@
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
@@ -824,6 +833,7 @@
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Index) then
Analyze (Index);
@@ -851,6 +861,7 @@
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
@@ -886,6 +897,7 @@
begin
Generate_Definition (Def_Id);
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
-- Case of no discrete subtype definition
@@ -955,6 +967,7 @@
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Analyze (Def);
-- There is no elaboration of the entry index specification. Therefore,
@@ -996,6 +1009,7 @@
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);
@@ -1114,6 +1128,7 @@
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));
@@ -1167,6 +1182,7 @@
end if;
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_Restriction (No_Protected_Types, N);
T := Find_Type_Name (N);
@@ -1308,6 +1324,7 @@
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);
@@ -1582,6 +1599,7 @@
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);
@@ -1702,6 +1720,7 @@
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.
@@ -1763,6 +1782,7 @@
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.
@@ -1840,6 +1860,7 @@
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);
@@ -1960,6 +1981,7 @@
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
@@ -1994,6 +2016,7 @@
begin
Check_Restriction (No_Tasking, N);
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
T := Find_Type_Name (N);
Generate_Definition (T);
@@ -2099,6 +2122,7 @@
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));
@@ -2120,6 +2144,7 @@
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);
@@ -2156,6 +2181,7 @@
begin
Tasking_Used := True;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Pragmas_Before (N)) then
Analyze_List (Pragmas_Before (N));
Index: einfo.adb
===================================================================
--- einfo.adb (revision 177174)
+++ einfo.adb (working copy)
@@ -518,7 +518,7 @@
-- Is_Safe_To_Reevaluate Flag249
-- Has_Predicates Flag250
- -- (unused) Flag251
+ -- Body_Is_In_ALFA Flag251
-- (unused) Flag252
-- (unused) Flag253
-- (unused) Flag254
@@ -651,6 +651,12 @@
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
@@ -3098,6 +3104,12 @@
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
@@ -7349,6 +7361,7 @@
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));
Index: einfo.ads
===================================================================
--- einfo.ads (revision 177174)
+++ einfo.ads (working copy)
@@ -7,7 +7,7 @@
-- 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- --
@@ -486,6 +486,11 @@
-- 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
@@ -2273,7 +2278,9 @@
-- 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
@@ -4336,7 +4343,7 @@
-- 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
@@ -4536,7 +4543,7 @@
-- 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
@@ -5933,6 +5940,7 @@
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;
@@ -6519,6 +6527,7 @@
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);
@@ -7212,6 +7221,7 @@
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);
@@ -7653,6 +7663,7 @@
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);
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 177175)
+++ sem_util.adb (working copy)
@@ -2311,6 +2311,21 @@
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 --
---------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 177173)
+++ sem_util.ads (working copy)
@@ -277,6 +277,10 @@
-- 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
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 177175)
+++ sem_res.adb (working copy)
@@ -5964,13 +5964,19 @@
-- 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;
@@ -6821,15 +6827,18 @@
-- 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
@@ -7365,6 +7374,8 @@
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));
Index: sem_ch2.adb
===================================================================
--- sem_ch2.adb (revision 176998)
+++ sem_ch2.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- 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- --
@@ -24,12 +24,14 @@
------------------------------------------------------------------------------
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;
@@ -74,6 +76,13 @@
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;
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb (revision 177175)
+++ sem_ch4.adb (working copy)
@@ -350,6 +350,8 @@
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;
@@ -369,6 +371,7 @@
C : Node_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("allocator is not allowed", N);
-- Deal with allocator restrictions
@@ -982,6 +985,15 @@
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
@@ -1358,6 +1370,8 @@
L : Node_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
Candidate_Type := Empty;
-- The following code is equivalent to:
@@ -1506,6 +1520,7 @@
return;
end if;
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("conditional expression is not allowed", N);
Else_Expr := Next (Then_Expr);
@@ -1706,6 +1721,7 @@
-- 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);
@@ -2467,6 +2483,8 @@
-- Start of processing for Analyze_Membership_Op
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
Analyze_Expression (L);
if No (R)
@@ -2588,6 +2606,7 @@
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);
@@ -3216,6 +3235,8 @@
T : Entity_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
+
Analyze_Expression (Expr);
Set_Etype (N, Any_Type);
@@ -3274,6 +3295,7 @@
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);
@@ -3439,6 +3461,8 @@
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
@@ -4302,6 +4326,7 @@
-- Start of processing for Analyze_Slice
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("slice is not allowed", N);
Analyze (P);
@@ -4346,6 +4371,8 @@
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
@@ -4476,6 +4503,7 @@
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)));
Index: restrict.adb
===================================================================
--- restrict.adb (revision 177175)
+++ restrict.adb (working copy)
@@ -371,7 +371,7 @@
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
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 177176)
+++ sem_ch6.adb (working copy)
@@ -638,11 +638,13 @@
(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:
@@ -1909,6 +1911,7 @@
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;
@@ -1927,6 +1930,7 @@
-- 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;
@@ -2236,6 +2240,24 @@
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
@@ -2467,6 +2489,7 @@
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
Index: sem_ch11.adb
===================================================================
--- sem_ch11.adb (revision 177175)
+++ sem_ch11.adb (working copy)
@@ -443,6 +443,7 @@
P : Node_Id;
begin
+ Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("raise statement is not allowed", N);
Check_Unreachable_Code (N);
@@ -610,6 +611,7 @@
-- 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
