From patchwork Tue Aug 2 15:07:21 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 107943 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) by ozlabs.org (Postfix) with SMTP id 7CF04B6F8D for ; Wed, 3 Aug 2011 01:07:43 +1000 (EST) Received: (qmail 29345 invoked by alias); 2 Aug 2011 15:07:42 -0000 Received: (qmail 29335 invoked by uid 22791); 2 Aug 2011 15:07:39 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL,BAYES_00 X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Tue, 02 Aug 2011 15:07:22 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 3806F2BAD59; Tue, 2 Aug 2011 11:07:21 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id ui2fpgn6-5AR; Tue, 2 Aug 2011 11:07:21 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 224EE2BAD58; Tue, 2 Aug 2011 11:07:21 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 10C443FEE8; Tue, 2 Aug 2011 11:07:21 -0400 (EDT) Date: Tue, 2 Aug 2011 11:07:21 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] New entity flag defines which entities are in ALFA subset Message-ID: <20110802150720.GA8297@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org The ALFA subset corresponds to those entities which can be formally analyzed through the SPARK or Why tool-sets. This is the initial work to identify these entities, for integer/enumeration types and subtypes, objects of such types and subprogram specifications. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-02 Yannick Moy * 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. Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 177169) +++ sem_ch3.adb (working copy) @@ -3030,6 +3030,12 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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: einfo.adb =================================================================== --- einfo.adb (revision 177161) +++ einfo.adb (working copy) @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2011, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -408,6 +408,7 @@ -- 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 @@ -- Is_Safe_To_Reevaluate Flag249 -- Has_Predicates Flag250 - -- (unused) Flag151 -- (unused) Flag251 -- (unused) Flag252 -- (unused) Flag253 @@ -1844,6 +1844,11 @@ 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 @@ 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 @@ 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 177162) +++ einfo.ads (working copy) @@ -2270,6 +2270,11 @@ -- 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 @@ 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 @@ 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 @@ 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 @@ 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: cstand.adb =================================================================== --- cstand.adb (revision 177146) +++ cstand.adb (working copy) @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2011, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -570,6 +570,10 @@ 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)); Index: stand.ads =================================================================== --- stand.ads (revision 177145) +++ stand.ads (working copy) @@ -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 @@ 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 -- ------------------------------------- Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 177173) +++ sem_ch6.adb (working copy) @@ -1456,6 +1456,13 @@ 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 @@ -- 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 @@ 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 @@ 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