From ad05f2e9b874e19cd3d66a3971c1c385959d466a Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 4 Aug 2011 12:03:49 +0200 Subject: [PATCH] [multiple changes] 2011-08-04 Yannick Moy * 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) 2011-08-04 Emmanuel Briot * prj-env.adb (Create_Config_Pragmas_File): fix handling of multi-unit source files with non-standard naming schemes, in imported projects From-SVN: r177353 --- gcc/ada/ChangeLog | 19 +++++++++ gcc/ada/alfa.adb | 91 +++++++++++--------------------------------- gcc/ada/alfa.ads | 5 +-- gcc/ada/cstand.adb | 5 --- gcc/ada/einfo.adb | 63 +----------------------------- gcc/ada/einfo.ads | 26 ------------- gcc/ada/prj-env.adb | 42 +++++++++++--------- gcc/ada/sem_ch11.adb | 1 - gcc/ada/sem_ch2.adb | 9 ----- gcc/ada/sem_ch3.adb | 78 ------------------------------------- gcc/ada/sem_ch4.adb | 52 ------------------------- gcc/ada/sem_ch5.adb | 41 +++----------------- gcc/ada/sem_ch6.adb | 52 ++----------------------- gcc/ada/sem_ch9.adb | 26 ------------- gcc/ada/sem_prag.adb | 57 +-------------------------- gcc/ada/sem_res.adb | 30 +++------------ gcc/ada/sem_util.adb | 62 ------------------------------ gcc/ada/sem_util.ads | 16 -------- gcc/ada/stand.ads | 29 -------------- 19 files changed, 83 insertions(+), 621 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 29f972a3f32..b9478251c54 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,22 @@ +2011-08-04 Yannick Moy + + * 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) + +2011-08-04 Emmanuel Briot + + * prj-env.adb (Create_Config_Pragmas_File): fix handling of multi-unit + source files with non-standard naming schemes, in imported projects + 2011-08-04 Emmanuel Briot * makeutl.adb (Complete_Mains): when a multi-unit source file is diff --git a/gcc/ada/alfa.adb b/gcc/ada/alfa.adb index 065b7d8c5bb..d61ad17c9b2 100644 --- a/gcc/ada/alfa.adb +++ b/gcc/ada/alfa.adb @@ -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 @@ package body ALFA is 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 @@ package body ALFA is 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; diff --git a/gcc/ada/alfa.ads b/gcc/ada/alfa.ads index 5ad7c61c1a6..3e630a0ad96 100644 --- a/gcc/ada/alfa.ads +++ b/gcc/ada/alfa.ads @@ -319,10 +319,7 @@ package ALFA is 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. diff --git a/gcc/ada/cstand.adb b/gcc/ada/cstand.adb index f025be93478..b3cc75f8e2c 100644 --- a/gcc/ada/cstand.adb +++ b/gcc/ada/cstand.adb @@ -570,10 +570,6 @@ 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)); @@ -1334,7 +1330,6 @@ package body CStand is 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); diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index f0f0904b5e7..1dc4658afd3 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -409,7 +409,7 @@ package body Einfo is -- 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 @@ package body Einfo is -- 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 @@ package body Einfo is 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 @@ 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); @@ -3126,12 +3115,6 @@ package body Einfo is 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 @@ 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); @@ -5899,41 +5877,6 @@ package body Einfo is 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 @@ package body Einfo is 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 @@ 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 23d3c3b42a8..c870728026a 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -486,11 +486,6 @@ package Einfo is -- 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 @@ package Einfo is -- 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 @@ 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. 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 @@ package Einfo is 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 @@ 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; @@ -6452,7 +6433,6 @@ package Einfo is 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 @@ package Einfo is 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 @@ 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); @@ -7286,7 +7264,6 @@ package Einfo is 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 @@ 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); @@ -7731,7 +7707,6 @@ package Einfo is 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 @@ 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/prj-env.adb b/gcc/ada/prj-env.adb index eb8593a9633..ff14df9dd7c 100644 --- a/gcc/ada/prj-env.adb +++ b/gcc/ada/prj-env.adb @@ -477,8 +477,6 @@ package body Prj.Env is File : File_Descriptor := Invalid_FD; Current_Naming : Naming_Id; - Iter : Source_Iterator; - Source : Source_Id; procedure Check (Project : Project_Id; @@ -509,11 +507,13 @@ package body Prj.Env is In_Tree : Project_Tree_Ref; State : in out Integer) is - pragma Unreferenced (State, In_Tree); + pragma Unreferenced (State); Lang : constant Language_Ptr := Get_Language_From_Name (Project, "ada"); Naming : Lang_Naming_Data; + Iter : Source_Iterator; + Source : Source_Id; begin if Current_Verbosity = High then @@ -528,6 +528,25 @@ package body Prj.Env is return; end if; + -- Visit all the files and process those that need an SFN pragma + + Iter := For_Each_Source (In_Tree, Project); + while Element (Iter) /= No_Source loop + Source := Element (Iter); + + Debug_Output ("MANU Source index=" & Source.Index'Img, + Name_Id (Source.File)); + + if Source.Index >= 1 + and then not Source.Locally_Removed + and then Source.Unit /= null + then + Put (Source); + end if; + + Next (Iter); + end loop; + Naming := Lang.Config.Naming_Data; -- Is the naming scheme of this project one that we know? @@ -684,6 +703,7 @@ package body Prj.Env is -- Start of processing for Create_Config_Pragmas_File begin + Debug_Output ("MANU Create_Config_Pragmas_File", For_Project.Name); if not For_Project.Config_Checked then Naming_Table.Init (Namings); @@ -692,22 +712,6 @@ package body Prj.Env is Check_Imported_Projects (For_Project, In_Tree, Dummy, Imported_First => False); - -- Visit all the files and process those that need an SFN pragma - - Iter := For_Each_Source (In_Tree, For_Project); - while Element (Iter) /= No_Source loop - Source := Element (Iter); - - if Source.Index >= 1 - and then not Source.Locally_Removed - and then Source.Unit /= null - then - Put (Source); - end if; - - Next (Iter); - end loop; - -- If there are no non standard naming scheme, issue the GNAT -- standard naming scheme. This will tell the compiler that -- a project file is used and will forbid any pragma SFN. diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index cf7f50e28a9..30b5585448d 100644 --- a/gcc/ada/sem_ch11.adb +++ b/gcc/ada/sem_ch11.adb @@ -434,7 +434,6 @@ package body Sem_Ch11 is 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); diff --git a/gcc/ada/sem_ch2.adb b/gcc/ada/sem_ch2.adb index d4393963a05..84cd62db2c6 100644 --- a/gcc/ada/sem_ch2.adb +++ b/gcc/ada/sem_ch2.adb @@ -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 @@ package body Sem_Ch2 is 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; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 0586b71c384..3f09dd63aae 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -3057,17 +3057,6 @@ package body Sem_Ch3 is 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 @@ package body Sem_Ch3 is 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 @@ package body Sem_Ch3 is 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 @@ package body Sem_Ch3 is 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 @@ package body Sem_Ch3 is (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 @@ package body Sem_Ch3 is 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 @@ 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 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 @@ 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 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 @@ 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 @@ -16550,19 +16494,6 @@ package body Sem_Ch3 is 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 @@ 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; -------------------------------------------------------- @@ -19718,7 +19641,6 @@ 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_ch4.adb b/gcc/ada/sem_ch4.adb index 2025224d3dd..5850c3c59e4 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -350,8 +350,6 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is -- 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 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is -- 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 @@ package body Sem_Ch4 is 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 @@ package body Sem_Ch4 is 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))); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index afd338df094..2716d5817cb 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -1113,8 +1113,6 @@ package body Sem_Ch5 is 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 @@ package body Sem_Ch5 is -- 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 @@ package body Sem_Ch5 is 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 @@ package body Sem_Ch5 is 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 @@ package body Sem_Ch5 is 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 @@ package body Sem_Ch5 is 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 @@ package body Sem_Ch5 is 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. diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 1566890c3de..b3df5cf0f3d 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -664,21 +664,18 @@ package body Sem_Ch6 is 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 @@ 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 if Is_Array_Type (Typ) @@ -1932,11 +1922,11 @@ package body Sem_Ch6 is 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 @@ package body Sem_Ch6 is 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 @@ package body Sem_Ch6 is -- 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 @@ package body Sem_Ch6 is 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 @@ package body Sem_Ch6 is 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 @@ 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, except as a renaming if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol @@ -8905,14 +8869,6 @@ package body Sem_Ch6 is 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 diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 9ded3d25d93..399d36e8771 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -101,7 +101,6 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram ("entry is not in ALFA", N); if Present (Index) then Analyze (Index); @@ -861,7 +851,6 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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 @@ package body Sem_Ch9 is 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)); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 249e4bfba37..081c46a2312 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -6090,18 +6090,6 @@ package body Sem_Prag is -- 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 @@ package body Sem_Prag is 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 diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 753b10241e3..f91eea49fb9 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -5817,23 +5817,14 @@ package body Sem_Res is -- 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 @@ package body Sem_Res is 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 @@ package body Sem_Res is -- 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 @@ package body Sem_Res is 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)); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index d5b26405c7d..6616ab8488d 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -141,14 +141,6 @@ package body Sem_Util is -- 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 @@ package body Sem_Util is 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 -- --------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 62b75670654..a282bf6cdad 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -277,22 +277,6 @@ package Sem_Util is -- 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 diff --git a/gcc/ada/stand.ads b/gcc/ada/stand.ads index 07c86b65ecf..d369b40ac73 100644 --- a/gcc/ada/stand.ads +++ b/gcc/ada/stand.ads @@ -313,35 +313,6 @@ 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 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 -- ------------------------------------- -- 2.30.2