Patchwork [Ada] Remove detection of entities in the ALFA subset for formal verification

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 4, 2011, 10:04 a.m.
Message ID <20110804100419.GA22003@adacore.com>
Download mbox | patch
Permalink /patch/108401/
State New
Headers show

Comments

Arnaud Charlet - Aug. 4, 2011, 10:04 a.m.
The detection of entities in ALFA is best left in a back-end of the compiler,
so all the machinery for flagging entities as in ALFA, and the body of
subprograms as in ALFA, have been removed.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-08-04  Yannick Moy  <moy@adacore.com>

	* alfa.adb, alfa.ads (Get_Entity_For_Decl): remove function, partial
	duplicate of Defining_Entity
	(Get_Unique_Entity_For_Decl): rename function into
	Unique_Defining_Entity
	* einfo.adb, einfo.ads (Is_In_ALFA, Body_Is_In_ALFA): remove flags
	(Formal_Proof_On): remove synthesized flag
	* cstand.adb, sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb,
	sem_ch5.adb, sem_ch6.adb, sem_ch9.adb, sem_res.adb, sem_util.adb,
	sem_util.ads, stand.ads: Remove treatment associated to entities in ALFA
	* sem_prag.adb (Analyze_Pragma): remove special treatment for pragma
	Annotate (Formal_Proof)

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 177340)
+++ sem_ch3.adb	(working copy)
@@ -3057,17 +3057,6 @@ 
 
       Act_T := T;
 
-      --  The object is in ALFA if-and-only-if its type is in ALFA and it is
-      --  not aliased.
-
-      if not Is_In_ALFA (T) then
-         Mark_Non_ALFA_Subprogram ("object type is not in ALFA", N);
-      elsif Aliased_Present (N) then
-         Mark_Non_ALFA_Subprogram ("ALIASED is not in ALFA", N);
-      else
-         Set_Is_In_ALFA (Id);
-      end if;
-
       --  These checks should be performed before the initialization expression
       --  is considered, so that the Object_Definition node is still the same
       --  as in source code.
@@ -4661,7 +4650,6 @@ 
       Nb_Index      : Nat;
       P             : constant Node_Id := Parent (Def);
       Priv          : Entity_Id;
-      T_In_ALFA     : Boolean := True;
 
    begin
       if Nkind (Def) = N_Constrained_Array_Definition then
@@ -4742,12 +4730,6 @@ 
 
          Make_Index (Index, P, Related_Id, Nb_Index);
 
-         if Present (Etype (Index))
-           and then not Is_In_ALFA (Etype (Index))
-         then
-            T_In_ALFA := False;
-         end if;
-
          --  Check error of subtype with predicate for index type
 
          Bad_Predicated_Subtype_Use
@@ -4769,18 +4751,10 @@ 
             Check_SPARK_Restriction ("subtype mark required", Component_Typ);
          end if;
 
-         if Present (Element_Type)
-           and then not Is_In_ALFA (Element_Type)
-         then
-            T_In_ALFA := False;
-         end if;
-
       --  Ada 2005 (AI-230): Access Definition case
 
       else pragma Assert (Present (Access_Definition (Component_Def)));
 
-         T_In_ALFA := False;
-
          --  Indicate that the anonymous access type is created by the
          --  array type declaration.
 
@@ -4857,12 +4831,6 @@ 
                                (Implicit_Base, Finalize_Storage_Only
                                                         (Element_Type));
 
-         --  Final check for static bounds on array
-
-         if not Has_Static_Array_Bounds (T) then
-            T_In_ALFA := False;
-         end if;
-
       --  Unconstrained array case
 
       else
@@ -4887,8 +4855,6 @@ 
 
       Set_Component_Type (Base_Type (T), Element_Type);
       Set_Packed_Array_Type (T, Empty);
-      Set_Is_In_ALFA (T, T_In_ALFA);
-      Set_Is_In_ALFA (Base_Type (T), T_In_ALFA);
 
       if Aliased_Present (Component_Definition (Def)) then
          Check_SPARK_Restriction
@@ -11599,14 +11565,6 @@ 
       C : constant Node_Id   := Constraint (S);
 
    begin
-      --  By default, consider that the enumeration subtype is in ALFA if the
-      --  entity of its subtype mark is in ALFA. This is reversed later if the
-      --  range of the subtype is not static.
-
-      if Is_In_ALFA (T) then
-         Set_Is_In_ALFA (Def_Id);
-      end if;
-
       Set_Ekind (Def_Id, E_Enumeration_Subtype);
 
       Set_First_Literal     (Def_Id, First_Literal (Base_Type (T)));
@@ -11829,14 +11787,6 @@ 
       C : constant Node_Id   := Constraint (S);
 
    begin
-      --  By default, consider that the integer subtype is in ALFA if the
-      --  entity of its subtype mark is in ALFA. This is reversed later if the
-      --  range of the subtype is not static.
-
-      if Is_In_ALFA (T) then
-         Set_Is_In_ALFA (Def_Id);
-      end if;
-
       Set_Scalar_Range_For_Subtype (Def_Id, Range_Expression (C), T);
 
       if Is_Modular_Integer_Type (T) then
@@ -14586,12 +14536,6 @@ 
       Set_Enum_Esize      (T);
       Set_Enum_Pos_To_Rep (T, Empty);
 
-      --  Enumeration type is in ALFA only if it is not a character type
-
-      if not Is_Character_Type (T) then
-         Set_Is_In_ALFA (T);
-      end if;
-
       --  Set Discard_Names if configuration pragma set, or if there is
       --  a parameterless pragma in the current declarative region
 
@@ -16550,19 +16494,6 @@ 
          then
             Set_Is_Non_Static_Subtype (Def_Id);
          end if;
-
-         --  By default, consider that the subtype is in ALFA if its base type
-         --  is in ALFA.
-
-         Set_Is_In_ALFA (Def_Id, Is_In_ALFA (Base_Type (Def_Id)));
-
-         --  In ALFA, all subtypes should have a static range
-
-         if Nkind (R) = N_Range
-           and then not Is_Static_Range (R)
-         then
-            Set_Is_In_ALFA (Def_Id, False);
-         end if;
       end if;
 
       --  Final step is to label the index with this constructed type
@@ -19539,14 +19470,6 @@ 
       Set_Ekind (Def_Id, E_Void);
       Process_Range_Expr_In_Decl (R, Subt);
       Set_Ekind (Def_Id, Kind);
-
-      --  In ALFA, all subtypes should have a static range
-
-      if Nkind (R) = N_Range
-        and then not Is_Static_Range (R)
-      then
-         Set_Is_In_ALFA (Def_Id, False);
-      end if;
    end Set_Scalar_Range_For_Subtype;
 
    --------------------------------------------------------
@@ -19718,7 +19641,6 @@ 
       Set_Scalar_Range   (T, Def);
       Set_RM_Size        (T, UI_From_Int (Minimum_Size (T)));
       Set_Is_Constrained (T);
-      Set_Is_In_ALFA     (T);
    end Signed_Integer_Type_Declaration;
 
 end Sem_Ch3;
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb	(revision 177335)
+++ sem_ch5.adb	(working copy)
@@ -1113,8 +1113,6 @@ 
       if Others_Present
         and then List_Length (Alternatives (N)) = 1
       then
-         Mark_Non_ALFA_Subprogram
-           ("OTHERS as unique case alternative is not in ALFA", N);
          Check_SPARK_Restriction
            ("OTHERS as unique case alternative is not allowed", N);
       end if;
@@ -1164,7 +1162,7 @@ 
    --  loop. Otherwise there must be an innermost open loop on the stack, to
    --  which the statement implicitly refers.
 
-   --  Additionally, in formal mode:
+   --  Additionally, in SPARK mode:
 
    --    The exit can only name the closest enclosing loop;
 
@@ -1196,9 +1194,6 @@ 
 
          else
             if Has_Loop_In_Inner_Open_Scopes (U_Name) then
-               Mark_Non_ALFA_Subprogram
-                 ("exit label must name the closest enclosing loop"
-                   & " in ALFA", N);
                Check_SPARK_Restriction
                  ("exit label must name the closest enclosing loop", N);
             end if;
@@ -1245,9 +1240,6 @@ 
 
       if Present (Cond) then
          if Nkind (Parent (N)) /= N_Loop_Statement then
-            Mark_Non_ALFA_Subprogram
-              ("exit with when clause must be directly in loop"
-                & " in ALFA", N);
             Check_SPARK_Restriction
               ("exit with when clause must be directly in loop", N);
          end if;
@@ -1255,36 +1247,26 @@ 
       else
          if Nkind (Parent (N)) /= N_If_Statement then
             if Nkind (Parent (N)) = N_Elsif_Part then
-               Mark_Non_ALFA_Subprogram
-                 ("exit must be in IF without ELSIF in ALFA", N);
                Check_SPARK_Restriction
                  ("exit must be in IF without ELSIF", N);
             else
-               Mark_Non_ALFA_Subprogram
-                 ("exit must be directly in IF in ALFA", N);
                Check_SPARK_Restriction ("exit must be directly in IF", N);
             end if;
 
          elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
-            Mark_Non_ALFA_Subprogram
-              ("exit must be in IF directly in loop in ALFA", N);
             Check_SPARK_Restriction
               ("exit must be in IF directly in loop", N);
 
-            --  First test the presence of ELSE, so that an exit in an ELSE
-            --  leads to an error mentioning the ELSE.
+         --  First test the presence of ELSE, so that an exit in an ELSE leads
+         --  to an error mentioning the ELSE.
 
          elsif Present (Else_Statements (Parent (N))) then
-            Mark_Non_ALFA_Subprogram
-              ("exit must be in IF without ELSE in ALFA", N);
             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).
+         --  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
-            Mark_Non_ALFA_Subprogram
-              ("exit must be in IF without ELSIF in ALFA", N);
             Check_SPARK_Restriction ("exit must be in IF without ELSIF", N);
          end if;
       end if;
@@ -1313,7 +1295,6 @@ 
       Label_Ent   : Entity_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram ("goto statement is not in ALFA", N);
       Check_SPARK_Restriction ("goto statement is not allowed", N);
 
       --  Actual semantic checks
@@ -2093,18 +2074,6 @@ 
                   Set_Etype (Id, Etype (DS));
                end if;
 
-               --  The entity for iterating over a loop is always in ALFA if
-               --  its type is in ALFA, and it is not an iteration over
-               --  elements of a container using the OF syntax.
-
-               if Is_In_ALFA (Etype (Id))
-                 and then
-                   (No (Iterator_Specification (N))
-                     or else not Of_Present (Iterator_Specification (N)))
-               then
-                  Set_Is_In_ALFA (Id);
-               end if;
-
                --  Treat a range as an implicit reference to the type, to
                --  inhibit spurious warnings.
 
Index: sem_ch9.adb
===================================================================
--- sem_ch9.adb	(revision 177335)
+++ sem_ch9.adb	(working copy)
@@ -101,7 +101,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("abort statement is not in ALFA", N);
       Check_SPARK_Restriction ("abort statement is not allowed", N);
 
       T_Name := First (Names (N));
@@ -140,7 +139,6 @@ 
    procedure Analyze_Accept_Alternative (N : Node_Id) is
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("accept is not in ALFA", N);
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
@@ -174,7 +172,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("accept statement is not in ALFA", N);
       Check_SPARK_Restriction ("accept statement is not allowed", N);
 
       --  Entry name is initialized to Any_Id. It should get reset to the
@@ -406,7 +403,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("select statement is not in ALFA", N);
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (Max_Asynchronous_Select_Nesting, N);
       Check_Restriction (No_Select_Statements, N);
@@ -453,7 +449,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("select statement is not in ALFA", N);
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -500,7 +495,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("delay is not in ALFA", N);
       Check_Restriction (No_Delay, N);
 
       if Present (Pragmas_Before (N)) then
@@ -552,7 +546,6 @@ 
       E : constant Node_Id := Expression (N);
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("delay statement is not in ALFA", N);
       Check_SPARK_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Relative_Delay, N);
       Check_Restriction (No_Delay, N);
@@ -571,7 +564,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("delay statement is not in ALFA", N);
       Check_SPARK_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Delay, N);
       Check_Potentially_Blocking_Operation (N);
@@ -600,7 +592,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("entry is not in ALFA", N);
 
       --  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
@@ -833,7 +824,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("entry is not in ALFA", N);
 
       if Present (Index) then
          Analyze (Index);
@@ -861,7 +851,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("entry call is not in ALFA", N);
       Check_SPARK_Restriction ("entry call is not allowed", N);
 
       if Present (Pragmas_Before (N)) then
@@ -897,7 +886,6 @@ 
    begin
       Generate_Definition (Def_Id);
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("entry is not in ALFA", N);
 
       --  Case of no discrete subtype definition
 
@@ -967,7 +955,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("entry is not in ALFA", N);
       Analyze (Def);
 
       --  There is no elaboration of the entry index specification. Therefore,
@@ -1009,7 +996,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("protected body is not in ALFA", N);
       Set_Ekind (Body_Id, E_Protected_Body);
       Spec_Id := Find_Concurrent_Spec (Body_Id);
 
@@ -1128,7 +1114,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("protected definition is not in ALFA", N);
       Check_SPARK_Restriction ("protected definition is not allowed", N);
       Analyze_Declarations (Visible_Declarations (N));
 
@@ -1182,7 +1167,6 @@ 
       end if;
 
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("protected type is not in ALFA", N);
       Check_Restriction (No_Protected_Types, N);
 
       T := Find_Type_Name (N);
@@ -1324,7 +1308,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("requeue statement is not in ALFA", N);
       Check_SPARK_Restriction ("requeue statement is not allowed", N);
       Check_Restriction (No_Requeue_Statements, N);
       Check_Unreachable_Code (N);
@@ -1599,7 +1582,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("select statement is not in ALFA", N);
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -1720,7 +1702,6 @@ 
    begin
       Generate_Definition (Id);
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("protected object is not in ALFA", N);
 
       --  The node is rewritten as a protected type declaration, in exact
       --  analogy with what is done with single tasks.
@@ -1782,7 +1763,6 @@ 
    begin
       Generate_Definition (Id);
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("task is not in ALFA", N);
 
       --  The node is rewritten as a task type declaration, followed by an
       --  object declaration of that anonymous task type.
@@ -1860,7 +1840,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("task body is not in ALFA", N);
       Set_Ekind (Body_Id, E_Task_Body);
       Set_Scope (Body_Id, Current_Scope);
       Spec_Id := Find_Concurrent_Spec (Body_Id);
@@ -1981,7 +1960,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("task definition is not in ALFA", N);
       Check_SPARK_Restriction ("task definition is not allowed", N);
 
       if Present (Visible_Declarations (N)) then
@@ -2016,7 +1994,6 @@ 
    begin
       Check_Restriction (No_Tasking, N);
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("task type is not in ALFA", N);
       T := Find_Type_Name (N);
       Generate_Definition (T);
 
@@ -2122,7 +2099,6 @@ 
    procedure Analyze_Terminate_Alternative (N : Node_Id) is
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("terminate is not in ALFA", N);
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
@@ -2144,7 +2120,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("select statement is not in ALFA", N);
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -2181,7 +2156,6 @@ 
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram ("triggering statement is not in ALFA", N);
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 177349)
+++ einfo.adb	(working copy)
@@ -409,7 +409,7 @@ 
    --    Is_Compilation_Unit             Flag149
    --    Has_Pragma_Elaborate_Body       Flag150
 
-   --    Is_In_ALFA                      Flag151
+   --    (unused)                        Flag151
    --    Entry_Accepted                  Flag152
    --    Is_Obsolescent                  Flag153
    --    Has_Per_Object_Constraint       Flag154
@@ -519,7 +519,7 @@ 
    --    Is_Safe_To_Reevaluate           Flag249
    --    Has_Predicates                  Flag250
 
-   --    Body_Is_In_ALFA                 Flag251
+   --    (unused)                        Flag251
    --    Is_Processed_Transient          Flag252
    --    Is_Postcondition_Proc           Flag253
    --    (unused)                        Flag254
@@ -652,12 +652,6 @@ 
       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
@@ -1854,11 +1848,6 @@ 
       return Flag24 (Id);
    end Is_Imported;
 
-   function Is_In_ALFA (Id : E) return B is
-   begin
-      return Flag151 (Id);
-   end Is_In_ALFA;
-
    function Is_Inlined (Id : E) return B is
    begin
       return Flag11 (Id);
@@ -3126,12 +3115,6 @@ 
       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
@@ -4374,11 +4357,6 @@ 
       Set_Flag24 (Id, V);
    end Set_Is_Imported;
 
-   procedure Set_Is_In_ALFA (Id : E; V : B := True) is
-   begin
-      Set_Flag151 (Id, V);
-   end Set_Is_In_ALFA;
-
    procedure Set_Is_Inlined (Id : E; V : B := True) is
    begin
       Set_Flag11 (Id, V);
@@ -5899,41 +5877,6 @@ 
       end if;
    end First_Formal_With_Extras;
 
-   ---------------------
-   -- Formal_Proof_On --
-   ---------------------
-
-   function Formal_Proof_On (Id : E) return B is
-      N    : Node_Id;
-      Arg1 : Node_Id;
-      Arg2 : Node_Id;
-
-   begin
-      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
-
-      N := First_Rep_Item (Id);
-      while Present (N) loop
-         if Nkind (N) = N_Pragma
-           and then Get_Pragma_Id (Pragma_Name (N)) = Pragma_Annotate
-           and then Present (Pragma_Argument_Associations (N))
-           and then List_Length (Pragma_Argument_Associations (N)) = 2
-         then
-            Arg1 := First (Pragma_Argument_Associations (N));
-            Arg2 := Next (Arg1);
-
-            if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof
-              and then Chars (Get_Pragma_Arg (Arg2)) = Name_On
-            then
-               return True;
-            end if;
-         end if;
-
-         Next_Rep_Item (N);
-      end loop;
-
-      return False;
-   end Formal_Proof_On;
-
    -------------------------------------
    -- Get_Attribute_Definition_Clause --
    -------------------------------------
@@ -7449,7 +7392,6 @@ 
       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));
@@ -7587,7 +7529,6 @@ 
       W ("Is_Hidden_Open_Scope",            Flag171 (Id));
       W ("Is_Immediately_Visible",          Flag7   (Id));
       W ("Is_Imported",                     Flag24  (Id));
-      W ("Is_In_ALFA",                      Flag151 (Id));
       W ("Is_Inlined",                      Flag11  (Id));
       W ("Is_Instantiated",                 Flag126 (Id));
       W ("Is_Interface",                    Flag186 (Id));
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 177349)
+++ einfo.ads	(working copy)
@@ -486,11 +486,6 @@ 
 --       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
@@ -1272,11 +1267,6 @@ 
 --       Float_Rep_Kind. Together with the Digits_Value uniquely defines
 --       the floating-point representation to be used.
 
---    Formal_Proof_On (synthesized)
---       Applies to subprogram and generic subprogram entities. Returns True if
---       the Rep_Item chain for the subprogram has a pragma Annotate which
---       forces formal proof on the subprogram's body.
-
 --    Freeze_Node (Node7)
 --       Present in all entities. If there is an associated freeze node for
 --       the entity, this field references this freeze node. If no freeze
@@ -2279,13 +2269,6 @@ 
 --    Is_Incomplete_Type (synthesized)
 --       Applies to all entities, true for incomplete types and subtypes
 
---    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. 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
 --       to be inlined. For subprograms created during expansion, this flag
@@ -5997,7 +5980,6 @@ 
    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;
@@ -6205,7 +6187,6 @@ 
    function Is_Hidden_Open_Scope                (Id : E) return B;
    function Is_Immediately_Visible              (Id : E) return B;
    function Is_Imported                         (Id : E) return B;
-   function Is_In_ALFA                          (Id : E) return B;
    function Is_Inlined                          (Id : E) return B;
    function Is_Interface                        (Id : E) return B;
    function Is_Instantiated                     (Id : E) return B;
@@ -6452,7 +6433,6 @@ 
    function First_Component_Or_Discriminant     (Id : E) return E;
    function First_Formal                        (Id : E) return E;
    function First_Formal_With_Extras            (Id : E) return E;
-   function Formal_Proof_On                     (Id : E) return B;
    function Has_Attach_Handler                  (Id : E) return B;
    function Has_Entries                         (Id : E) return B;
    function Has_Foreign_Convention              (Id : E) return B;
@@ -6589,7 +6569,6 @@ 
    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);
@@ -6800,7 +6779,6 @@ 
    procedure Set_Is_Hidden_Open_Scope            (Id : E; V : B := True);
    procedure Set_Is_Immediately_Visible          (Id : E; V : B := True);
    procedure Set_Is_Imported                     (Id : E; V : B := True);
-   procedure Set_Is_In_ALFA                      (Id : E; V : B := True);
    procedure Set_Is_Inlined                      (Id : E; V : B := True);
    procedure Set_Is_Interface                    (Id : E; V : B := True);
    procedure Set_Is_Instantiated                 (Id : E; V : B := True);
@@ -7286,7 +7264,6 @@ 
    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);
@@ -7522,7 +7499,6 @@ 
    pragma Inline (Is_Imported);
    pragma Inline (Is_Incomplete_Or_Private_Type);
    pragma Inline (Is_Incomplete_Type);
-   pragma Inline (Is_In_ALFA);
    pragma Inline (Is_Inlined);
    pragma Inline (Is_Interface);
    pragma Inline (Is_Instantiated);
@@ -7731,7 +7707,6 @@ 
    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);
@@ -7941,7 +7916,6 @@ 
    pragma Inline (Set_Is_Hidden_Open_Scope);
    pragma Inline (Set_Is_Immediately_Visible);
    pragma Inline (Set_Is_Imported);
-   pragma Inline (Set_Is_In_ALFA);
    pragma Inline (Set_Is_Inlined);
    pragma Inline (Set_Is_Interface);
    pragma Inline (Set_Is_Instantiated);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 177351)
+++ sem_prag.adb	(working copy)
@@ -6090,18 +6090,6 @@ 
          --  external tool and a tool-specific function. These arguments are
          --  not analyzed.
 
-         --  The following is a special form used in conjunction with the
-         --  ALFA subset of Ada:
-
-         --    pragma Annotate (Formal_Proof, MODE);
-         --    MODE ::= On | Off
-
-         --    This pragma either forces (mode On) or disables (mode Off)
-         --    formal verification of the subprogram in which it is added. When
-         --    formal verification is forced, all violations of the the ALFA
-         --    subset of Ada present in the subprogram are reported as errors
-         --    to the user.
-
          when Pragma_Annotate => Annotate : declare
             Arg : Node_Id;
             Exp : Node_Id;
@@ -6113,52 +6101,9 @@ 
             Check_No_Identifiers;
             Store_Note (N);
 
-            --  Special processing for Formal_Proof case
-
-            if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then
-               if No (Arg2) then
-                  Error_Pragma_Arg
-                    ("missing second argument for pragma%", Arg1);
-               end if;
-
-               Check_Arg_Count (2);
-               Check_Arg_Is_One_Of (Arg2, Name_On, Name_Off);
-
-               declare
-                  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
-                     --  Notify user if some ALFA violation occurred before
-                     --  this point in Cur_Subp. These violations are not
-                     --  precisly located, but this is better than ignoring
-                     --  these violations.
-
-                     if Chars (Get_Pragma_Arg (Arg2)) = Name_On
-                       and then (not Is_In_ALFA (Cur_Subp)
-                                  or else not Body_Is_In_ALFA (Cur_Subp))
-                     then
-                        Error_Pragma
-                          ("pragma% is placed after violation"
-                           & " of ALFA");
-                     end if;
-
-                     --  We treat this as a Rep_Item to record it on the rep
-                     --  item chain for easy location later on.
-
-                     Record_Rep_Item (Cur_Subp, N);
-
-                  else
-                     Error_Pragma ("wrong placement for pragma%");
-                  end if;
-               end;
-
             --  Second parameter is optional, it is never analyzed
 
-            elsif No (Arg2) then
+            if No (Arg2) then
                null;
 
             --  Here if we have a second parameter
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 177351)
+++ sem_util.adb	(working copy)
@@ -141,14 +141,6 @@ 
    --  T is a derived tagged type. Check whether the type extension is null.
    --  If the parent type is fully initialized, T can be treated as such.
 
-   procedure Mark_Non_ALFA_Subprogram_Unconditional
-     (Msg : String;
-      N   : Node_Id);
-   --  Perform the action for Mark_Non_ALFA_Subprogram_Body, which allows the
-   --  latter to be small and inlined. If the subprogram being marked as not in
-   --  ALFA is annotated with Formal_Proof being On, then an error is issued
-   --  with message Msg on node N.
-
    ------------------------------
    --  Abstract_Interface_List --
    ------------------------------
@@ -2323,60 +2315,6 @@ 
       end if;
    end Current_Subprogram;
 
-   ------------------------------
-   -- Mark_Non_ALFA_Subprogram --
-   ------------------------------
-
-   procedure Mark_Non_ALFA_Subprogram (Msg : String; N : Node_Id) is
-   begin
-      --  Isolate marking of the current subprogram body so that the body of
-      --  Mark_Non_ALFA_Subprogram is small and inlined.
-
-      if ALFA_Mode then
-         Mark_Non_ALFA_Subprogram_Unconditional (Msg, N);
-      end if;
-   end Mark_Non_ALFA_Subprogram;
-
-   --------------------------------------------
-   -- Mark_Non_ALFA_Subprogram_Unconditional --
-   --------------------------------------------
-
-   procedure Mark_Non_ALFA_Subprogram_Unconditional
-     (Msg : String;
-      N   : Node_Id)
-   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
-         --  If the subprogram has been annotated with Formal_Proof being On,
-         --  then an error must be issued to notify the user that this
-         --  subprogram unexpectedly falls outside the ALFA subset.
-
-         if Formal_Proof_On (Cur_Subp) then
-            Error_Msg_F (Msg, N);
-         end if;
-
-         --  If the non-ALFA construct is in a precondition or postcondition,
-         --  then mark the subprogram as not in ALFA, because neither the
-         --  subprogram nor its callers can be proved formally.
-
-         --  If the non-ALFA construct is in a regular piece of code inside the
-         --  body of the subprogram, then mark the subprogram body as not in
-         --  ALFA, because the subprogram cannot be proved formally, but its
-         --  callers could.
-
-         if In_Pre_Post_Expression then
-            Set_Is_In_ALFA (Cur_Subp, False);
-         else
-            Set_Body_Is_In_ALFA (Cur_Subp, False);
-         end if;
-      end if;
-   end Mark_Non_ALFA_Subprogram_Unconditional;
-
    ---------------------
    -- Defining_Entity --
    ---------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 177334)
+++ sem_util.ads	(working copy)
@@ -277,22 +277,6 @@ 
    --  Current_Scope is returned. The returned value is Empty if this is called
    --  from a library package which is not within any subprogram.
 
-   procedure Mark_Non_ALFA_Subprogram (Msg : String; N : Node_Id);
-   --  If Current_Subprogram is not Empty, mark either its specification or its
-   --  body as not being in ALFA.
-
-   --  This procedure may be called during the analysis of a precondition or
-   --  postcondition, as indicated by the flag In_Pre_Post_Expression, or
-   --  during the analysis of a subprogram's body. In the first case, the
-   --  specification of Current_Subprogram must be marked as not being in ALFA,
-   --  as the contract is considered to be part of the specification, so that
-   --  calls to this subprogram are not in ALFA. In the second case, mark the
-   --  body as not being in ALFA, which does not prevent the subprogram's
-   --  specification, and calls to the subprogram, from being in ALFA.
-
-   --  If the subprogram being marked as not in ALFA is annotated with
-   --  Formal_Proof On, then an error is issued with message Msg on node N.
-
    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 177350)
+++ sem_res.adb	(working copy)
@@ -5817,23 +5817,14 @@ 
       --  types or array types except String.
 
       if Is_Boolean_Type (T) then
-         Mark_Non_ALFA_Subprogram
-           ("ordering operator on boolean type is not in ALFA", N);
          Check_SPARK_Restriction
            ("comparison is not defined on Boolean type", N);
 
-      elsif Is_Array_Type (T) then
-         Mark_Non_ALFA_Subprogram
-           ("ordering operator on array type is not in ALFA", N);
-
-         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;
+      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);
       end if;
 
       --  Check comparison on unordered enumeration
@@ -5883,11 +5874,6 @@ 
          Append_To (Expressions (N), Error);
       end if;
 
-      if Root_Type (Typ) /= Standard_Boolean then
-         Mark_Non_ALFA_Subprogram
-           ("non-boolean conditional expression is not in ALFA", N);
-      end if;
-
       Set_Etype (N, Typ);
       Eval_Conditional_Expression (N);
    end Resolve_Conditional_Expression;
@@ -6688,9 +6674,6 @@ 
          --  operands have equal static bounds.
 
          if Is_Array_Type (T) then
-            Mark_Non_ALFA_Subprogram
-              ("equality operator on array is not in ALFA", N);
-
             --  Protect call to Matching_Static_Array_Bounds to avoid costly
             --  operation if not needed.
 
@@ -7262,9 +7245,6 @@ 
       if Is_Array_Type (B_Typ)
         and then Nkind (N) in N_Binary_Op
       then
-         Mark_Non_ALFA_Subprogram
-           ("binary operator on array is not in ALFA", N);
-
          declare
             Left_Typ  : constant Node_Id := Etype (Left_Opnd (N));
             Right_Typ : constant Node_Id := Etype (Right_Opnd (N));
Index: alfa.adb
===================================================================
--- alfa.adb	(revision 177318)
+++ alfa.adb	(working copy)
@@ -26,6 +26,7 @@ 
 with Atree;    use Atree;
 with Output;   use Output;
 with Put_ALFA;
+with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
 
 package body ALFA is
@@ -144,74 +145,6 @@ 
       end loop;
    end dalfa;
 
-   -------------------------
-   -- Get_Entity_For_Decl --
-   -------------------------
-
-   function Get_Entity_For_Decl (N : Node_Id) return Entity_Id is
-      E : Entity_Id := Empty;
-
-   begin
-      case Nkind (N) is
-         when N_Subprogram_Declaration |
-              N_Subprogram_Body        |
-              N_Package_Declaration    =>
-            E := Defining_Unit_Name (Specification (N));
-
-         when N_Package_Body =>
-            E := Defining_Unit_Name (N);
-
-         when N_Object_Declaration =>
-            E := Defining_Identifier (N);
-
-         when others =>
-            null;
-      end case;
-
-      if Nkind (E) = N_Defining_Program_Unit_Name then
-         E := Defining_Identifier (E);
-      end if;
-
-      return E;
-   end Get_Entity_For_Decl;
-
-   --------------------------------
-   -- Get_Unique_Entity_For_Decl --
-   --------------------------------
-
-   function Get_Unique_Entity_For_Decl (N : Node_Id) return Entity_Id is
-      E : Entity_Id := Empty;
-
-   begin
-      case Nkind (N) is
-         when N_Subprogram_Declaration |
-              N_Package_Declaration    =>
-            E := Defining_Unit_Name (Specification (N));
-
-         when N_Package_Body =>
-            E := Corresponding_Spec (N);
-
-         when N_Subprogram_Body =>
-            if Acts_As_Spec (N) then
-               E := Defining_Unit_Name (Specification (N));
-            else
-               E := Corresponding_Spec (N);
-            end if;
-
-         when N_Object_Declaration =>
-            E := Defining_Identifier (N);
-
-         when others =>
-            null;
-      end case;
-
-      if Nkind (E) = N_Defining_Program_Unit_Name then
-         E := Defining_Identifier (E);
-      end if;
-
-      return E;
-   end Get_Unique_Entity_For_Decl;
-
    ----------------
    -- Initialize --
    ----------------
@@ -270,4 +203,26 @@ 
       Debug_Put_ALFA;
    end palfa;
 
+   ----------------------------
+   -- Unique_Defining_Entity --
+   ----------------------------
+
+   function Unique_Defining_Entity (N : Node_Id) return Entity_Id is
+   begin
+      case Nkind (N) is
+         when N_Package_Body =>
+            return Corresponding_Spec (N);
+
+         when N_Subprogram_Body =>
+            if Acts_As_Spec (N) then
+               return Defining_Entity (N);
+            else
+               return Corresponding_Spec (N);
+            end if;
+
+         when others =>
+            return Defining_Entity (N);
+      end case;
+   end Unique_Defining_Entity;
+
 end ALFA;
Index: alfa.ads
===================================================================
--- alfa.ads	(revision 177318)
+++ alfa.ads	(working copy)
@@ -319,10 +319,7 @@ 
    procedure Initialize_ALFA_Tables;
    --  Reset tables for a new compilation
 
-   function Get_Entity_For_Decl (N : Node_Id) return Entity_Id;
-   --  Return the entity for declaration N
-
-   function Get_Unique_Entity_For_Decl (N : Node_Id) return Entity_Id;
+   function Unique_Defining_Entity (N : Node_Id) return Entity_Id;
    --  Return the entity which represents declaration N, so that matching
    --  declaration and body have the same entity.
 
Index: sem_ch2.adb
===================================================================
--- sem_ch2.adb	(revision 177335)
+++ sem_ch2.adb	(working copy)
@@ -24,14 +24,12 @@ 
 ------------------------------------------------------------------------------
 
 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;
@@ -76,13 +74,6 @@ 
          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
-            Mark_Non_ALFA_Subprogram ("object is not in ALFA", N);
-         end if;
       end if;
    end Analyze_Identifier;
 
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 177350)
+++ sem_ch4.adb	(working copy)
@@ -350,8 +350,6 @@ 
 
    procedure Analyze_Aggregate (N : Node_Id) is
    begin
-      Mark_Non_ALFA_Subprogram ("aggregate is not in ALFA", N);
-
       if No (Etype (N)) then
          Set_Etype (N, Any_Composite);
       end if;
@@ -371,7 +369,6 @@ 
       C        : Node_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram ("allocator is not in ALFA", N);
       Check_SPARK_Restriction ("allocator is not allowed", N);
 
       --  Deal with allocator restrictions
@@ -978,15 +975,6 @@ 
             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) then
-            Mark_Non_ALFA_Subprogram ("indirect call is not in ALFA", N);
-         elsif not Is_In_ALFA (Nam_Ent) then
-            Mark_Non_ALFA_Subprogram ("call to subprogram not in ALFA", N);
-         end if;
-
          Analyze_One_Call (N, Nam_Ent, True, Success);
 
          --  If this is an indirect call, the return type of the access_to
@@ -1363,8 +1351,6 @@ 
       L  : Node_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram ("concatenation is not in ALFA", N);
-
       Candidate_Type := Empty;
 
       --  The following code is equivalent to:
@@ -1517,26 +1503,6 @@ 
 
       Else_Expr := Next (Then_Expr);
 
-      --  In ALFA, boolean conditional expressions are allowed:
-      --    * if they have no ELSE part, in which case the expression is
-      --      equivalent to
-
-      --        NOT Condition OR ELSE Then_Expr
-
-      --    * in pre- and postconditions, where the Condition cannot have side-
-      --      effects (in ALFA) and thus the expression is equivalent to
-
-      --        (Condition AND THEN Then_Expr)
-      --          and (NOT Condition AND THEN Then_Expr)
-
-      --  Non-boolean conditional expressions are marked as not in ALFA during
-      --  resolution.
-
-      if Present (Else_Expr) and then not In_Pre_Post_Expression then
-         Mark_Non_ALFA_Subprogram
-           ("this form of conditional expression is not in ALFA", N);
-      end if;
-
       if Comes_From_Source (N) then
          Check_Compiler_Unit (N);
       end if;
@@ -1733,7 +1699,6 @@ 
    --  Start of processing for Analyze_Explicit_Dereference
 
    begin
-      Mark_Non_ALFA_Subprogram ("explicit dereference is not in ALFA", N);
       Check_SPARK_Restriction ("explicit dereference is not allowed", N);
 
       Analyze (P);
@@ -2616,7 +2581,6 @@ 
 
    procedure Analyze_Null (N : Node_Id) is
    begin
-      Mark_Non_ALFA_Subprogram ("null is not in ALFA", N);
       Check_SPARK_Restriction ("null is not allowed", N);
 
       Set_Etype (N, Any_Access);
@@ -3248,8 +3212,6 @@ 
       T    : Entity_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram ("qualified expression is not in ALFA", N);
-
       Analyze_Expression (Expr);
 
       Set_Etype (N, Any_Type);
@@ -3308,7 +3270,6 @@ 
       Iterator : Node_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram ("quantified expression is not in ALFA", N);
       Check_SPARK_Restriction ("quantified expression is not allowed", N);
 
       Set_Etype  (Ent,  Standard_Void_Type);
@@ -3474,8 +3435,6 @@ 
       Acc_Type : Entity_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram ("reference is not in ALFA", N);
-
       Analyze (P);
 
       --  An interesting error check, if we take the 'Reference of an object
@@ -4340,7 +4299,6 @@ 
    --  Start of processing for Analyze_Slice
 
    begin
-      Mark_Non_ALFA_Subprogram ("slice is not in ALFA", N);
       Check_SPARK_Restriction ("slice is not allowed", N);
 
       Analyze (P);
@@ -4406,14 +4364,6 @@ 
       Analyze_Expression (Expr);
       Validate_Remote_Type_Type_Conversion (N);
 
-      --  Type conversion between scalar types are allowed in ALFA. All other
-      --  type conversions are not allowed.
-
-      if not (Is_Scalar_Type (Etype (Expr)) and then Is_Scalar_Type (T)) then
-         Mark_Non_ALFA_Subprogram
-           ("only type conversion between scalar types is in ALFA", N);
-      end if;
-
       --  Only remaining step is validity checks on the argument. These
       --  are skipped if the conversion does not come from the source.
 
@@ -4523,8 +4473,6 @@ 
 
    procedure Analyze_Unchecked_Type_Conversion (N : Node_Id) is
    begin
-      Mark_Non_ALFA_Subprogram
-        ("unchecked type conversion is not in ALFA", N);
       Find_Type (Subtype_Mark (N));
       Analyze_Expression (Expression (N));
       Set_Etype (N, Entity (Subtype_Mark (N)));
Index: cstand.adb
===================================================================
--- cstand.adb	(revision 177274)
+++ cstand.adb	(working copy)
@@ -570,10 +570,6 @@ 
             Decl := New_Node (N_Full_Type_Declaration, Stloc);
          end if;
 
-         if Standard_Type_Is_In_ALFA (S) then
-            Set_Is_In_ALFA (Standard_Entity (S));
-         end if;
-
          Set_Is_Frozen (Standard_Entity (S));
          Set_Is_Public (Standard_Entity (S));
          Set_Defining_Identifier (Decl, Standard_Entity (S));
@@ -1334,7 +1330,6 @@ 
       Set_Scope (Universal_Integer, Standard_Standard);
       Build_Signed_Integer_Type
         (Universal_Integer, Standard_Long_Long_Integer_Size);
-      Set_Is_In_ALFA (Universal_Integer);
 
       Universal_Real := New_Standard_Entity;
       Decl := New_Node (N_Full_Type_Declaration, Stloc);
Index: stand.ads
===================================================================
--- stand.ads	(revision 177274)
+++ stand.ads	(working copy)
@@ -313,35 +313,6 @@ 
    Boolean_Literals : array (Boolean) of Entity_Id;
    --  Entities for the two boolean literals, used by the expander
 
-   --  Standard types which are in ALFA are associated set to True
-
-   Standard_Type_Is_In_ALFA : array (S_Types) of Boolean :=
-     (S_Boolean             => True,
-
-      S_Short_Short_Integer => True,
-      S_Short_Integer       => True,
-      S_Integer             => True,
-      S_Long_Integer        => True,
-      S_Long_Long_Integer   => True,
-
-      S_Natural             => True,
-      S_Positive            => True,
-
-      S_Short_Float         => False,
-      S_Float               => False,
-      S_Long_Float          => False,
-      S_Long_Long_Float     => False,
-
-      S_Character           => False,
-      S_Wide_Character      => False,
-      S_Wide_Wide_Character => False,
-
-      S_String              => False,
-      S_Wide_String         => False,
-      S_Wide_Wide_String    => False,
-
-      S_Duration            => False);
-
    -------------------------------------
    -- Semantic Phase Special Entities --
    -------------------------------------
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 177352)
+++ sem_ch6.adb	(working copy)
@@ -664,21 +664,18 @@ 
             Check_Limited_Return (Expr);
          end if;
 
-         --  RETURN only allowed in SPARK is as the last statement function
+         --  RETURN only allowed in SPARK as the last statement in function
 
          if Nkind (Parent (N)) /= N_Handled_Sequence_Of_Statements
            and then
              (Nkind (Parent (Parent (N))) /= N_Subprogram_Body
                or else Present (Next (N)))
          then
-            Mark_Non_ALFA_Subprogram
-              ("RETURN should be the last statement in ALFA", N);
             Check_SPARK_Restriction
               ("RETURN should be the last statement in function", N);
          end if;
 
       else
-         Mark_Non_ALFA_Subprogram ("extended RETURN is not in ALFA", N);
          Check_SPARK_Restriction ("extended RETURN is not allowed", N);
 
          --  Analyze parts specific to extended_return_statement:
@@ -1491,13 +1488,6 @@ 
             Typ := Entity (Result_Definition (N));
             Set_Etype (Designator, Typ);
 
-            --  If the result type of a subprogram is not in ALFA, then the
-            --  subprogram is not in ALFA.
-
-            if not Is_In_ALFA (Typ) then
-               Set_Is_In_ALFA (Designator, False);
-            end if;
-
             --  Unconstrained array as result is not allowed in SPARK
 
             if Is_Array_Type (Typ)
@@ -1932,11 +1922,11 @@ 
             Check_Returns (HSS, 'P', Missing_Ret, Spec_Id);
          end if;
 
-         --  Special checks in formal mode
+         --  Special checks in SPARK mode
 
          if Nkind (Body_Spec) = N_Function_Specification then
 
-            --  In formal mode, last statement of a function should be a return
+            --  In SPARK mode, last statement of a function should be a return
 
             declare
                Stat : constant Node_Id := Last_Source_Statement (HSS);
@@ -1945,13 +1935,12 @@ 
                  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;
             end;
 
-         --  In formal mode, verify that a procedure has no return
+         --  In SPARK mode, verify that a procedure has no return
 
          elsif Nkind (Body_Spec) = N_Procedure_Specification then
             if Present (Spec_Id) then
@@ -1964,7 +1953,6 @@ 
             --  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;
@@ -2282,24 +2270,6 @@ 
          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
@@ -2531,7 +2501,6 @@ 
          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
 
@@ -3177,11 +3146,6 @@ 
    --  Start of processing for Analyze_Subprogram_Specification
 
    begin
-      --  By default, consider that the subprogram spec is in ALFA. This is
-      --  reversed later if some parameter or result is not in ALFA.
-
-      Set_Is_In_ALFA (Designator);
-
       --  User-defined operator is not allowed in SPARK, except as a renaming
 
       if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
@@ -8905,14 +8869,6 @@ 
 
          Set_Etype (Formal, Formal_Type);
 
-         --  The parameter is in ALFA if-and-only-if its type is in ALFA
-
-         if Is_In_ALFA (Formal_Type) then
-            Set_Is_In_ALFA (Formal);
-         else
-            Mark_Non_ALFA_Subprogram ("formal is not in ALFA", Formal);
-         end if;
-
          Default := Expression (Param_Spec);
 
          if Present (Default) then
Index: sem_ch11.adb
===================================================================
--- sem_ch11.adb	(revision 177335)
+++ sem_ch11.adb	(working copy)
@@ -434,7 +434,6 @@ 
       P              : Node_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram ("raise statement is not in ALFA", N);
       Check_SPARK_Restriction ("raise statement is not allowed", N);
       Check_Unreachable_Code (N);