diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 23 | ||||
| -rw-r--r-- | gcc/ada/cstand.adb | 6 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 15 | ||||
| -rw-r--r-- | gcc/ada/einfo.ads | 9 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 61 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 26 | ||||
| -rw-r--r-- | gcc/ada/stand.ads | 30 |
7 files changed, 154 insertions, 16 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index e8407ba..d9c354f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,26 @@ +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 diff --git a/gcc/ada/cstand.adb b/gcc/ada/cstand.adb index 26d5017..64ec043 100644 --- a/gcc/ada/cstand.adb +++ b/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)); diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 6e1f089..062e1fd4 100644 --- a/gcc/ada/einfo.adb +++ b/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)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index ae89212..aa5b0e2 100644 --- a/gcc/ada/einfo.ads +++ b/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); diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index d99abef..afa0f85 100644 --- a/gcc/ada/sem_ch3.adb +++ b/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; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 1ca71fc..170533d 100644 --- a/gcc/ada/sem_ch6.adb +++ b/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 diff --git a/gcc/ada/stand.ads b/gcc/ada/stand.ads index dd5e9a7..40c51d0 100644 --- a/gcc/ada/stand.ads +++ b/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 -- ------------------------------------- |