cstand.adb (Create_Standard): sets Is_In_ALFA component of standard types.

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

	* cstand.adb (Create_Standard): sets Is_In_ALFA component of standard
	types.
	* einfo.adb, einfo.ads (Is_In_ALFA): add flag for all entities
	(Is_In_ALFA, Set_Is_In_ALFA): new subprograms to access flag Is_In_ALFA
	* sem_ch3.adb
	(Analyze_Object_Declaration): set Is_In_ALFA flag for objects
	(Constrain_Enumeration): set Is_In_ALFA flag for enumeration subtypes
	(Constrain_Integer): set Is_In_ALFA flag for integer subtypes
	(Enumeration_Type_Declaration): set Is_In_ALFA flag for enumeration
	types.
	(Set_Scalar_Range_For_Subtype): unset Is_In_ALFA flag for subtypes with
	non-static range.
	* sem_ch6.adb (Analyze_Return_Type): unset Is_In_ALFA flag for
	functions whose return type is not in ALFA.
	(Analyze_Subprogram_Specification): set Is_In_ALFA flag for subprogram
	specifications.
	(Process_Formals): unset Is_In_ALFA flag for subprograms if a
	parameter's type is not in ALFA.
	* stand.ads (Standard_Type_Is_In_ALFA): array defines which standard
	types are in ALFA.

From-SVN: r177174

gcc/ada/ChangeLog

+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* cstand.adb (Create_Standard): sets Is_In_ALFA component of standard
+	types.
+	* einfo.adb, einfo.ads (Is_In_ALFA): add flag for all entities
+	(Is_In_ALFA, Set_Is_In_ALFA): new subprograms to access flag Is_In_ALFA
+	* sem_ch3.adb
+	(Analyze_Object_Declaration): set Is_In_ALFA flag for objects
+	(Constrain_Enumeration): set Is_In_ALFA flag for enumeration subtypes
+	(Constrain_Integer): set Is_In_ALFA flag for integer subtypes
+	(Enumeration_Type_Declaration): set Is_In_ALFA flag for enumeration
+	types.
+	(Set_Scalar_Range_For_Subtype): unset Is_In_ALFA flag for subtypes with
+	non-static range.
+	* sem_ch6.adb (Analyze_Return_Type): unset Is_In_ALFA flag for
+	functions whose return type is not in ALFA.
+	(Analyze_Subprogram_Specification): set Is_In_ALFA flag for subprogram
+	specifications.
+	(Process_Formals): unset Is_In_ALFA flag for subprograms if a
+	parameter's type is not in ALFA.
+	* stand.ads (Standard_Type_Is_In_ALFA): array defines which standard
+	types are in ALFA.
+
 2011-08-02  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch6 (Analyze_Expression_Function): treat the function as

gcc/ada/cstand.adb

@@ -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- --
@@ -570,6 +570,10 @@ package body CStand is
             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));

gcc/ada/einfo.adb

@@ -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- --
@@ -408,6 +408,7 @@ package body Einfo is
    --    Is_Compilation_Unit             Flag149
    --    Has_Pragma_Elaborate_Body       Flag150
 
+   --    Is_In_ALFA                      Flag151
    --    Entry_Accepted                  Flag152
    --    Is_Obsolescent                  Flag153
    --    Has_Per_Object_Constraint       Flag154
@@ -517,7 +518,6 @@ package body Einfo is
    --    Is_Safe_To_Reevaluate           Flag249
    --    Has_Predicates                  Flag250
 
-   --    (unused)                        Flag151
    --    (unused)                        Flag251
    --    (unused)                        Flag252
    --    (unused)                        Flag253
@@ -1844,6 +1844,11 @@ package body Einfo is
       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);
@@ -4332,6 +4337,11 @@ package body Einfo is
       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);
@@ -7476,6 +7486,7 @@ package body Einfo is
       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));

gcc/ada/einfo.ads

@@ -2270,6 +2270,11 @@ package Einfo is
 --    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.
+
 --    Is_Inlined (Flag11)
 --       Present in all entities. Set for functions and procedures which are
 --       to be inlined. For subprograms created during expansion, this flag
@@ -6135,6 +6140,7 @@ package Einfo is
    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;
@@ -6723,6 +6729,7 @@ package Einfo is
    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);
@@ -7440,6 +7447,7 @@ package Einfo is
    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);
@@ -7854,6 +7862,7 @@ package Einfo is
    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);

gcc/ada/sem_ch3.adb

@@ -3030,6 +3030,12 @@ package body Sem_Ch3 is
 
       Act_T := T;
 
+      --  The object is in ALFA if-and-only-if its type is in ALFA
+
+      if Is_In_ALFA (T) then
+         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.
@@ -3987,9 +3993,9 @@ package body Sem_Ch3 is
 
       if Skip
         or else (Present (Etype (Id))
-                   and then (Is_Private_Type (Etype (Id))
-                               or else Is_Task_Type (Etype (Id))
-                               or else Is_Rewrite_Substitution (N)))
+                  and then (Is_Private_Type (Etype (Id))
+                             or else Is_Task_Type (Etype (Id))
+                             or else Is_Rewrite_Substitution (N)))
       then
          null;
 
@@ -4017,7 +4023,7 @@ package body Sem_Ch3 is
 
       if Has_Predicates (T)
         or else (Present (Ancestor_Subtype (T))
-                   and then Has_Predicates (Ancestor_Subtype (T)))
+                  and then Has_Predicates (Ancestor_Subtype (T)))
       then
          Set_Has_Predicates (Id);
          Set_Has_Delayed_Freeze (Id);
@@ -7914,11 +7920,11 @@ package body Sem_Ch3 is
    begin
       --  Set common attributes
 
-      Set_Scope         (Derived_Type, Current_Scope);
+      Set_Scope          (Derived_Type, Current_Scope);
 
-      Set_Ekind         (Derived_Type, Ekind    (Parent_Base));
-      Set_Etype         (Derived_Type,           Parent_Base);
-      Set_Has_Task      (Derived_Type, Has_Task (Parent_Base));
+      Set_Ekind          (Derived_Type, Ekind    (Parent_Base));
+      Set_Etype          (Derived_Type,           Parent_Base);
+      Set_Has_Task       (Derived_Type, Has_Task (Parent_Base));
 
       Set_Size_Info      (Derived_Type,                 Parent_Type);
       Set_RM_Size        (Derived_Type, RM_Size        (Parent_Type));
@@ -11496,6 +11502,16 @@ package body Sem_Ch3 is
       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 Nkind (Original_Node (Parent (Def_Id))) = N_Subtype_Declaration
+        and then 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)));
@@ -11718,6 +11734,16 @@ package body Sem_Ch3 is
       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 Nkind (Original_Node (Parent (Def_Id))) = N_Subtype_Declaration
+        and then 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
@@ -14469,6 +14495,12 @@ package body Sem_Ch3 is
       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
 
@@ -17929,8 +17961,8 @@ package body Sem_Ch3 is
 
       if Nkind (R) = N_Range then
 
-         --  In SPARK/ALFA, all ranges should be static, with the exception of
-         --  the discrete type definition of a loop parameter specification.
+         --  In SPARK, all ranges should be static, with the exception of the
+         --  discrete type definition of a loop parameter specification.
 
          if not In_Iter_Schm
            and then not Is_Static_Range (R)
@@ -19387,6 +19419,14 @@ package body Sem_Ch3 is
       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;
 
    --------------------------------------------------------
@@ -19558,6 +19598,7 @@ package body Sem_Ch3 is
       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;

gcc/ada/sem_ch6.adb

@@ -1456,6 +1456,13 @@ package body Sem_Ch6 is
             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 or ALFA
 
             if Is_Array_Type (Typ)
@@ -3106,6 +3113,11 @@ package body Sem_Ch6 is
    --  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 or ALFA, except as
       --  a renaming.
 
@@ -8652,8 +8664,8 @@ package body Sem_Ch6 is
       begin
          return Is_Class_Wide_Type (Designated_Type (Etype (D)))
            or else (Nkind (D) =  N_Attribute_Reference
-                      and then Attribute_Name (D) = Name_Access
-                      and then Is_Class_Wide_Type (Etype (Prefix (D))));
+                     and then Attribute_Name (D) = Name_Access
+                     and then Is_Class_Wide_Type (Etype (Prefix (D))));
       end Is_Class_Wide_Default;
 
    --  Start of processing for Process_Formals
@@ -8828,6 +8840,16 @@ package body Sem_Ch6 is
          end if;
 
          Set_Etype (Formal, Formal_Type);
+
+         --  If the type of a subprogram's formal parameter is not in ALFA,
+         --  then the subprogram is not in ALFA.
+
+         if Nkind (Parent (First (T))) in N_Subprogram_Specification
+           and then not Is_In_ALFA (Formal_Type)
+         then
+            Set_Is_In_ALFA (Defining_Entity (Parent (First (T))), False);
+         end if;
+
          Default := Expression (Param_Spec);
 
          if Present (Default) then

gcc/ada/stand.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          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- --
@@ -313,6 +313,34 @@ package Stand is
    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 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 --
    -------------------------------------