Patchwork [Ada] Add flag Body_Is_In_ALFA on subprogram entities

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 2, 2011, 3:15 p.m.
Message ID <20110802151518.GA10206@adacore.com>
Download mbox | patch
Permalink /patch/107944/
State New
Headers show

Comments

Arnaud Charlet - Aug. 2, 2011, 3:15 p.m.
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  <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.

Patch

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