From: Yannick Moy Date: Thu, 4 Aug 2011 13:35:20 +0000 (+0000) Subject: gnat_rm.texi: Document new pragma and aspect. X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dac3bede918b07ddb13d2efae1fbda9f4d81468f;p=gcc.git gnat_rm.texi: Document new pragma and aspect. 2011-08-04 Yannick Moy * gnat_rm.texi: Document new pragma and aspect. * aspects.adb, aspects.ads (Aspect_Id): new value Aspect_Test_Case (No_Duplicates_Allowed): new constant array defining whether duplicates aspects of each kind can appear on the same declaration. * einfo.adb, einfo.ads (Spec_PPC_List): replace field with Contract field, which points to a node holding the previous Spec_PPC_List. * exp_ch9.adb, sem_ch6.adb, sem_prag.adb: Reach to Spec_PPC_List through the indirection with Contract. * exp_util.adb (Insert_Actions): raise Program_Error on N_Contract node * par-prag.adb (Prag): do nothing on Test_Case pragma * sem.adb (Analyze): abort on N_Contract, on which Analyze should not be called directly. * sem_attr.adb (Analyze_Attribute): allow attribute 'Result in component Ensures of Test_Case. * sem_ch12.adb, sem_ch6.adb, sem_ch9.adb (Analyze_Generic_Subprogram_Declaration, Analyze_Subprogram_Instantiation, Analyze_Abstract_Subprogram_Declaration, Analyze_Subprogram_Body_Helper, Analyze_Subprogram_Specification, Analyze_Entry_Declaration): insert contract in subprogram node at point of definition * sem_ch13.adb (Aspect_Loop): do not raise error on duplicate Test_Case aspect (Analyze_Aspect_Specifications): analyze Test_Case aspect and create corresponding pragma (Check_Aspect_At_Freeze_Point): raise Program_Error on Test_Case aspect * sem_ch3.adb (Analyze_Declarations): insert analysis of test-cases, similar to the analysis of pre/post (Derive_Subprogram): insert contract in subprogram node at point of derivation. * sem_prag.adb, sem_prag.ads (Check_Arg_Is_String_Literal, Check_Identifier): new checking procedures to be called in treatment of pragmas (Check_Test_Case): new procedure to check that a Test_Case aspect or pragma is well-formed. This does not check currently that 'Result is used only in the Ensures component of a Test_Case. (Analyze_Pragma): add case for Test_Case (Analyze_TC_In_Decl_Part): pre-analyze the Requires and Ensures components of a Test_Case. (Preanalyze_TC_Args): new procedure to preanalyze the boolean expressions in the 3rd (and 4th if present) arguments of a Test_Case pragma, treated as spec expressions. (Sig_Flags): add value -1 for Test_Case. * sem_util.adb, sem_util.ads (Get_Ensures_From_Test_Case_Pragma, Get_Requires_From_Test_Case_Pragma): getters for both expression components of a Test_Case. * sinfo.adb, sinfo.ads (N_Contract): new kind of node used as indirection between an entry or [generic] subprogram entity and its pre/post + test-cases. (Spec_PPC_List, Spec_TC_List, Set_Spec_PPC_List, Set_Spec_TC_List): get/set for fields of an N_Contract node. * snames.ads-tmpl (Name_Test_Case, Name_Ensures, Name_Mode, Name_Normal, Name_Requires, Name_Robustness, Pragma_Test_Case): new names and pragma for Test_Case. * sprint.adb (Sprint_Node): raise Program_Error on N_Contract node From-SVN: r177384 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 2db1c79bf23..8484bcfac18 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,61 @@ +2011-08-04 Yannick Moy + + * gnat_rm.texi: Document new pragma and aspect. + * aspects.adb, aspects.ads (Aspect_Id): new value Aspect_Test_Case + (No_Duplicates_Allowed): new constant array defining whether duplicates + aspects of each kind can appear on the same declaration. + * einfo.adb, einfo.ads (Spec_PPC_List): replace field with Contract + field, which points to a node holding the previous Spec_PPC_List. + * exp_ch9.adb, sem_ch6.adb, sem_prag.adb: Reach to Spec_PPC_List + through the indirection with Contract. + * exp_util.adb (Insert_Actions): raise Program_Error on N_Contract node + * par-prag.adb (Prag): do nothing on Test_Case pragma + * sem.adb (Analyze): abort on N_Contract, on which Analyze should not + be called directly. + * sem_attr.adb (Analyze_Attribute): allow attribute 'Result in + component Ensures of Test_Case. + * sem_ch12.adb, sem_ch6.adb, sem_ch9.adb + (Analyze_Generic_Subprogram_Declaration, + Analyze_Subprogram_Instantiation, + Analyze_Abstract_Subprogram_Declaration, + Analyze_Subprogram_Body_Helper, + Analyze_Subprogram_Specification, Analyze_Entry_Declaration): + insert contract in subprogram node at point of definition + * sem_ch13.adb + (Aspect_Loop): do not raise error on duplicate Test_Case aspect + (Analyze_Aspect_Specifications): analyze Test_Case aspect and create + corresponding pragma + (Check_Aspect_At_Freeze_Point): raise Program_Error on Test_Case aspect + * sem_ch3.adb (Analyze_Declarations): insert analysis of test-cases, + similar to the analysis of pre/post + (Derive_Subprogram): insert contract in subprogram node at point of + derivation. + * sem_prag.adb, sem_prag.ads + (Check_Arg_Is_String_Literal, Check_Identifier): + new checking procedures to be called in treatment of pragmas + (Check_Test_Case): new procedure to check that a Test_Case aspect or + pragma is well-formed. This does not check currently that 'Result is + used only in the Ensures component of a Test_Case. + (Analyze_Pragma): add case for Test_Case + (Analyze_TC_In_Decl_Part): pre-analyze the Requires and Ensures + components of a Test_Case. + (Preanalyze_TC_Args): new procedure to preanalyze the boolean + expressions in the 3rd (and 4th if present) arguments of a Test_Case + pragma, treated as spec expressions. + (Sig_Flags): add value -1 for Test_Case. + * sem_util.adb, sem_util.ads (Get_Ensures_From_Test_Case_Pragma, + Get_Requires_From_Test_Case_Pragma): getters for both expression + components of a Test_Case. + * sinfo.adb, sinfo.ads (N_Contract): new kind of node used as + indirection between an entry or [generic] subprogram entity and its + pre/post + test-cases. + (Spec_PPC_List, Spec_TC_List, Set_Spec_PPC_List, Set_Spec_TC_List): + get/set for fields of an N_Contract node. + * snames.ads-tmpl (Name_Test_Case, Name_Ensures, Name_Mode, + Name_Normal, Name_Requires, Name_Robustness, Pragma_Test_Case): new + names and pragma for Test_Case. + * sprint.adb (Sprint_Node): raise Program_Error on N_Contract node + 2011-08-04 Vincent Celier * gnat_ugn.texi: Improve documentation of gnatmake switch diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index aafe74b1725..7495a2d5aa7 100755 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2010, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-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- -- @@ -222,6 +222,7 @@ package body Aspects is Aspect_Stream_Size => Aspect_Stream_Size, Aspect_Suppress => Aspect_Suppress, Aspect_Suppress_Debug_Info => Aspect_Suppress_Debug_Info, + Aspect_Test_Case => Aspect_Test_Case, Aspect_Type_Invariant => Aspect_Invariant, Aspect_Unchecked_Union => Aspect_Unchecked_Union, Aspect_Universal_Aliasing => Aspect_Universal_Aliasing, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 64fb038a5ee..4b2d814bdca 100755 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2010, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-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- -- @@ -69,6 +69,7 @@ package Aspects is Aspect_Storage_Size, Aspect_Stream_Size, Aspect_Suppress, + Aspect_Test_Case, -- GNAT Aspect_Type_Invariant, Aspect_Unsuppress, Aspect_Value_Size, -- GNAT @@ -128,6 +129,13 @@ package Aspects is Aspect_Post => True, others => False); + -- The following array indicates aspects for which multiple occurrences of + -- the same aspect attached to the same declaration are allowed. + + No_Duplicates_Allowed : constant array (Aspect_Id) of Boolean := + (Aspect_Test_Case => False, + others => True); + -- The following subtype defines aspects corresponding to library unit -- pragmas, these can only validly appear as aspects for library units, -- and result in a corresponding pragma being inserted immediately after @@ -185,6 +193,7 @@ package Aspects is Aspect_Storage_Size => Expression, Aspect_Stream_Size => Expression, Aspect_Suppress => Name, + Aspect_Test_Case => Expression, Aspect_Type_Invariant => Expression, Aspect_Unsuppress => Name, Aspect_Value_Size => Expression, @@ -252,6 +261,7 @@ package Aspects is Aspect_Stream_Size => Name_Stream_Size, Aspect_Suppress => Name_Suppress, Aspect_Suppress_Debug_Info => Name_Suppress_Debug_Info, + Aspect_Test_Case => Name_Test_Case, Aspect_Type_Invariant => Name_Type_Invariant, Aspect_Unchecked_Union => Name_Unchecked_Union, Aspect_Universal_Aliasing => Name_Universal_Aliasing, diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 383ec9cdd13..a53d07ff299 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -209,7 +209,7 @@ package body Einfo is -- Finalizer Node24 -- Related_Expression Node24 - -- Spec_PPC_List Node24 + -- Contract Node24 -- Interface_Alias Node25 -- Interfaces Elist25 @@ -982,6 +982,15 @@ package body Einfo is return Node18 (Id); end Entry_Index_Constant; + function Contract (Id : E) return N is + begin + pragma Assert + (Ekind_In (Id, E_Entry, E_Entry_Family) + or else Is_Subprogram (Id) + or else Is_Generic_Subprogram (Id)); + return Node24 (Id); + end Contract; + function Entry_Parameters_Type (Id : E) return E is begin return Node15 (Id); @@ -2650,15 +2659,6 @@ package body Einfo is return Node19 (Id); end Spec_Entity; - function Spec_PPC_List (Id : E) return N is - begin - pragma Assert - (Ekind_In (Id, E_Entry, E_Entry_Family) - or else Is_Subprogram (Id) - or else Is_Generic_Subprogram (Id)); - return Node24 (Id); - end Spec_PPC_List; - function Static_Predicate (Id : E) return S is begin pragma Assert (Is_Discrete_Type (Id)); @@ -3451,6 +3451,15 @@ package body Einfo is Set_Node18 (Id, V); end Set_Entry_Index_Constant; + procedure Set_Contract (Id : E; V : N) is + begin + pragma Assert + (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void) + or else Is_Subprogram (Id) + or else Is_Generic_Subprogram (Id)); + Set_Node24 (Id, V); + end Set_Contract; + procedure Set_Entry_Parameters_Type (Id : E; V : E) is begin Set_Node15 (Id, V); @@ -5189,15 +5198,6 @@ package body Einfo is Set_Node19 (Id, V); end Set_Spec_Entity; - procedure Set_Spec_PPC_List (Id : E; V : N) is - begin - pragma Assert - (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void) - or else Is_Subprogram (Id) - or else Is_Generic_Subprogram (Id)); - Set_Node24 (Id, V); - end Set_Spec_PPC_List; - procedure Set_Static_Predicate (Id : E; V : S) is begin pragma Assert @@ -8534,8 +8534,11 @@ package body Einfo is Type_Kind => Write_Str ("Related_Expression"); - when Subprogram_Kind => - Write_Str ("Spec_PPC_List"); + when E_Entry | + E_Entry_Family | + Subprogram_Kind | + Generic_Subprogram_Kind => + Write_Str ("Contract"); when others => Write_Str ("Field24???"); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 3fb2e41b93b..29baab0b43e 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -1009,6 +1009,11 @@ package Einfo is -- accept statement for a member of the family, and in the prefix of -- 'COUNT when it applies to a family member. +-- Contract (Node24) +-- Present in entries, and in subprogram and generic subprogram entities. +-- Points to the contract of the entity, holding both pre- and +-- postconditions as well as test-cases. + -- Entry_Parameters_Type (Node15) -- Present in entries. Points to the access-to-record type that is -- constructed by the expander to hold a reference to the parameter @@ -3641,14 +3646,6 @@ package Einfo is -- case where there is a separate spec, where this field references -- the corresponding parameter entities in the spec. --- Spec_PPC_List (Node24) --- Present in entries, and in subprogram and generic subprogram entities. --- Points to a list of Precondition and Postcondition pragma nodes for --- preconditions and postconditions declared in the spec. The last pragma --- encountered is at the head of this list, so it is in reverse order of --- textual appearance. Note that this includes precondition/postcondition --- pragmas generated to correspond to Pre/Post aspects. - -- Static_Predicate (List25) -- Present in discrete types/subtypes with predicates (Has_Predicates -- set True). Points to a list of expression and N_Range nodes that @@ -5126,7 +5123,7 @@ package Einfo is -- Accept_Address (Elist21) -- Scope_Depth_Value (Uint22) -- Protection_Object (Node23) (protected kind) - -- Spec_PPC_List (Node24) (for entry only) + -- Contract (Node24) (for entry only) -- PPC_Wrapper (Node25) -- Default_Expressions_Processed (Flag108) -- Entry_Accepted (Flag152) @@ -5226,7 +5223,7 @@ package Einfo is -- Generic_Renamings (Elist23) (for an instance) -- Inner_Instances (Elist23) (generic case only) -- Protection_Object (Node23) (for concurrent kind) - -- Spec_PPC_List (Node24) + -- Contract (Node24) -- Interface_Alias (Node25) -- Overridden_Operation (Node26) -- Wrapped_Entity (Node27) (non-generic case only) @@ -5490,7 +5487,7 @@ package Einfo is -- Generic_Renamings (Elist23) (for an instance) -- Inner_Instances (Elist23) (generic case only) -- Protection_Object (Node23) (for concurrent kind) - -- Spec_PPC_List (Node24) + -- Contract (Node24) -- Interface_Alias (Node25) -- Static_Initialization (Node26) (init_proc only) -- Overridden_Operation (Node26) (never for init proc) @@ -6039,6 +6036,7 @@ package Einfo is function Entry_Formal (Id : E) return E; function Entry_Index_Constant (Id : E) return E; function Entry_Index_Type (Id : E) return E; + function Contract (Id : E) return N; function Entry_Parameters_Type (Id : E) return E; function Enum_Pos_To_Rep (Id : E) return E; function Enumeration_Pos (Id : E) return U; @@ -6333,7 +6331,6 @@ package Einfo is function Size_Depends_On_Discriminant (Id : E) return B; function Small_Value (Id : E) return R; function Spec_Entity (Id : E) return E; - function Spec_PPC_List (Id : E) return N; function Static_Predicate (Id : E) return S; function Storage_Size_Variable (Id : E) return E; function Static_Elaboration_Desired (Id : E) return B; @@ -6626,6 +6623,7 @@ package Einfo is procedure Set_Entry_Component (Id : E; V : E); procedure Set_Entry_Formal (Id : E; V : E); procedure Set_Entry_Index_Constant (Id : E; V : E); + procedure Set_Contract (Id : E; V : N); procedure Set_Entry_Parameters_Type (Id : E; V : E); procedure Set_Enum_Pos_To_Rep (Id : E; V : E); procedure Set_Enumeration_Pos (Id : E; V : U); @@ -6926,7 +6924,6 @@ package Einfo is procedure Set_Size_Known_At_Compile_Time (Id : E; V : B := True); procedure Set_Small_Value (Id : E; V : R); procedure Set_Spec_Entity (Id : E; V : E); - procedure Set_Spec_PPC_List (Id : E; V : N); procedure Set_Static_Predicate (Id : E; V : S); procedure Set_Storage_Size_Variable (Id : E; V : E); procedure Set_Static_Elaboration_Desired (Id : E; V : B); @@ -7280,6 +7277,7 @@ package Einfo is pragma Inline (Component_Clause); pragma Inline (Component_Size); pragma Inline (Component_Type); + pragma Inline (Contract); pragma Inline (Corresponding_Concurrent_Type); pragma Inline (Corresponding_Discriminant); pragma Inline (Corresponding_Equality); @@ -7664,7 +7662,6 @@ package Einfo is pragma Inline (Size_Known_At_Compile_Time); pragma Inline (Small_Value); pragma Inline (Spec_Entity); - pragma Inline (Spec_PPC_List); pragma Inline (Static_Predicate); pragma Inline (Storage_Size_Variable); pragma Inline (Static_Elaboration_Desired); @@ -7724,6 +7721,7 @@ package Einfo is pragma Inline (Set_Component_Clause); pragma Inline (Set_Component_Size); pragma Inline (Set_Component_Type); + pragma Inline (Set_Contract); pragma Inline (Set_Corresponding_Concurrent_Type); pragma Inline (Set_Corresponding_Discriminant); pragma Inline (Set_Corresponding_Equality); @@ -8063,7 +8061,6 @@ package Einfo is pragma Inline (Set_Size_Known_At_Compile_Time); pragma Inline (Set_Small_Value); pragma Inline (Set_Spec_Entity); - pragma Inline (Set_Spec_PPC_List); pragma Inline (Set_Static_Predicate); pragma Inline (Set_Storage_Size_Variable); pragma Inline (Set_Static_Elaboration_Desired); diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index 43ec7aff0b7..eba59842af1 100644 --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada/exp_ch9.adb @@ -1660,7 +1660,7 @@ package body Exp_Ch9 is P : Node_Id; begin - P := Spec_PPC_List (E); + P := Spec_PPC_List (Contract (E)); if No (P) then return; end if; @@ -10871,7 +10871,7 @@ package body Exp_Ch9 is Ent := First_Entity (Tasktyp); while Present (Ent) loop if Ekind_In (Ent, E_Entry, E_Entry_Family) - and then Present (Spec_PPC_List (Ent)) + and then Present (Spec_PPC_List (Contract (Ent))) then Build_PPC_Wrapper (Ent, N); end if; diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 83fed95a675..b993785f29d 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -3186,6 +3186,11 @@ package body Exp_Util is null; end if; + -- A contract node should not belong to the tree + + when N_Contract => + raise Program_Error; + -- For all other node types, keep climbing tree when diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index d1f2b8c6acc..70a678a00c4 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -203,6 +203,7 @@ Implementation Defined Pragmas * Pragma Task_Info:: * Pragma Task_Name:: * Pragma Task_Storage:: +* Pragma Test_Case:: * Pragma Thread_Local_Storage:: * Pragma Time_Slice:: * Pragma Title:: @@ -835,6 +836,7 @@ consideration, the use of these pragmas should be minimized. * Pragma Task_Info:: * Pragma Task_Name:: * Pragma Task_Storage:: +* Pragma Test_Case:: * Pragma Thread_Local_Storage:: * Pragma Time_Slice:: * Pragma Title:: @@ -3967,7 +3969,7 @@ In addition, the boolean expression which is the condition which must be true may contain references to function'Result in the case of a function to refer to the returned value. -@code{Postcondition} pragmas may appear either immediate following the +@code{Postcondition} pragmas may appear either immediately following the (separate) declaration of a subprogram, or at the start of the declarations of a subprogram body. Only other pragmas may intervene (that is appear between the subprogram declaration and its @@ -4133,7 +4135,7 @@ end Math_Functions; @end smallexample @noindent -@code{Precondition} pragmas may appear either immediate following the +@code{Precondition} pragmas may appear either immediately following the (separate) declaration of a subprogram, or at the start of the declarations of a subprogram body. Only other pragmas may intervene (that is appear between the subprogram declaration and its @@ -5007,6 +5009,58 @@ created, depending on the target. This pragma can appear anywhere a @code{Storage_Size} attribute definition clause is allowed for a task type. +@node Pragma Test_Case +@unnumberedsec Pragma Test_Case +@cindex Test cases +@findex Test_Case +@noindent +Syntax: + +@smallexample @c ada +pragma Test_Case ( + [Name =>] String_Expression + ,[Mode =>] (Normal | Robustness) + [, Requires => Boolean_Expression] + [, Ensures => Boolean_Expression]); +@end smallexample + +@noindent +The @code{Test_Case} pragma applies to the same entities as pragmas +@code{Precondition} and @code{Postcondition}. In particular, the +placement and visibility rules are identical to those described for pre- +and postconditions. But the presence of pragma @code{Test_Case} does not +lead to any modification of the code generated by the compiler. Rather, +its purpose is to document finer-grain specifications for use by testing +and verification tools. + +The compiler checks that boolean expression given in @code{Requires} and +@code{Ensures} are valid, where the rules for @code{Requires} are the +same as the rule for an expression in @code{Precondition} and the rules +for @code{Ensures} are the same as the rule for an expression in +@code{Postcondition}. In particular, attributes @code{'Old} and +@code{'Result} can only be used within the @code{Ensures} +expression. The following is an example of use within a package spec: + +@smallexample @c ada +package Math_Functions is + ... + function Sqrt (Arg : Float) return Float; + pragma Test_Case (Name => ``Test_1``, + Mode => Normal, + Requires => Arg < 100, + Ensures => Sqrt'Result < 10); + ... +end Math_Functions; +@end smallexample + +@noindent +@code{Test_Case} pragmas may appear either immediately following the +(separate) declaration of a subprogram, or at the start of the +declarations of a subprogram body. Only other pragmas may intervene +(that is appear between the subprogram declaration and its test cases, +or appear before the test case in the declaration sequence in a +subprogram body). + @node Pragma Thread_Local_Storage @unnumberedsec Pragma Thread_Local_Storage @findex Thread_Local_Storage @@ -16589,6 +16643,7 @@ A complete description of the AIs may be found in @item @code{Stream_Size} @tab @item @code{Suppress} @tab @item @code{Suppress_Debug_Info} @tab -- GNAT +@item @code{Test_Case} @tab -- GNAT @item @code{Unchecked_Union} @tab @item @code{Universal_Aliasing} @tab -- GNAT @item @code{Unmodified} @tab -- GNAT diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index e34d99f8439..111dee19b7b 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1239,6 +1239,7 @@ begin Pragma_Task_Info | Pragma_Task_Name | Pragma_Task_Storage | + Pragma_Test_Case | Pragma_Thread_Local_Storage | Pragma_Time_Slice | Pragma_Title | diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index 5b434993803..59626e86aa1 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.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- -- @@ -650,6 +650,7 @@ package body Sem is N_Component_Definition | N_Component_List | N_Constrained_Array_Definition | + N_Contract | N_Decimal_Fixed_Point_Definition | N_Defining_Character_Literal | N_Defining_Identifier | diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index e7dd01ad088..7a03ad1bc9b 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -4046,9 +4046,29 @@ package body Sem_Attr is Prag := Parent (Prag); end loop; - if Nkind (Prag) /= N_Pragma - or else Get_Pragma_Id (Prag) /= Pragma_Postcondition - then + if Nkind (Prag) /= N_Pragma then + Error_Attr + ("% attribute can only appear in postcondition of function", + P); + + elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then + declare + Arg_Ens : constant Node_Id := + Get_Ensures_From_Test_Case_Pragma (Prag); + Arg : Node_Id; + + begin + Arg := N; + while Arg /= Prag and Arg /= Arg_Ens loop + Arg := Parent (Arg); + end loop; + + if Arg /= Arg_Ens then + Error_Attr ("% attribute misplaced inside Test_Case", P); + end if; + end; + + elsif Get_Pragma_Id (Prag) /= Pragma_Postcondition then Error_Attr ("% attribute can only appear in postcondition of function", P); diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index f2d8a35ea46..7dc34d83a18 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -2839,6 +2839,7 @@ package body Sem_Ch12 is Spec := Specification (N); Id := Defining_Entity (Spec); Generate_Definition (Id); + Set_Contract (Id, Make_Contract (Sloc (Id))); if Nkind (Id) = N_Defining_Operator_Symbol then Error_Msg_N @@ -4367,6 +4368,8 @@ package body Sem_Ch12 is end if; Generate_Definition (Act_Decl_Id); + Set_Contract (Anon_Id, Make_Contract (Sloc (Anon_Id))); -- ??? needed? + Set_Contract (Act_Decl_Id, Make_Contract (Sloc (Act_Decl_Id))); Set_Is_Inlined (Act_Decl_Id, Is_Inlined (Gen_Unit)); Set_Is_Inlined (Anon_Id, Is_Inlined (Gen_Unit)); diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 5a28908763a..50d295486de 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -812,53 +812,56 @@ package body Sem_Ch13 is -- test allows duplicate Pre/Post's that we generate internally -- to escape being flagged here. - Anod := First (L); - while Anod /= Aspect loop - if Same_Aspect (A_Id, Get_Aspect_Id (Chars (Identifier (Anod)))) - and then Comes_From_Source (Aspect) - then - Error_Msg_Name_1 := Nam; - Error_Msg_Sloc := Sloc (Anod); + if No_Duplicates_Allowed (A_Id) then + Anod := First (L); + while Anod /= Aspect loop + if Same_Aspect + (A_Id, Get_Aspect_Id (Chars (Identifier (Anod)))) + and then Comes_From_Source (Aspect) + then + Error_Msg_Name_1 := Nam; + Error_Msg_Sloc := Sloc (Anod); - -- Case of same aspect specified twice + -- Case of same aspect specified twice - if Class_Present (Anod) = Class_Present (Aspect) then - if not Class_Present (Anod) then - Error_Msg_NE - ("aspect% for & previously given#", - Id, E); - else - Error_Msg_NE - ("aspect `%''Class` for & previously given#", - Id, E); - end if; + if Class_Present (Anod) = Class_Present (Aspect) then + if not Class_Present (Anod) then + Error_Msg_NE + ("aspect% for & previously given#", + Id, E); + else + Error_Msg_NE + ("aspect `%''Class` for & previously given#", + Id, E); + end if; - -- Case of Pre and Pre'Class both specified + -- Case of Pre and Pre'Class both specified - elsif Nam = Name_Pre then - if Class_Present (Aspect) then - Error_Msg_NE - ("aspect `Pre''Class` for & is not allowed here", - Id, E); - Error_Msg_NE - ("\since aspect `Pre` previously given#", - Id, E); + elsif Nam = Name_Pre then + if Class_Present (Aspect) then + Error_Msg_NE + ("aspect `Pre''Class` for & is not allowed here", + Id, E); + Error_Msg_NE + ("\since aspect `Pre` previously given#", + Id, E); - else - Error_Msg_NE - ("aspect `Pre` for & is not allowed here", - Id, E); - Error_Msg_NE - ("\since aspect `Pre''Class` previously given#", - Id, E); + else + Error_Msg_NE + ("aspect `Pre` for & is not allowed here", + Id, E); + Error_Msg_NE + ("\since aspect `Pre''Class` previously given#", + Id, E); + end if; end if; - end if; - -- Allowed case of X and X'Class both specified - end if; + -- Allowed case of X and X'Class both specified + end if; - Next (Anod); - end loop; + Next (Anod); + end loop; + end if; -- Copy expression for later processing by the procedures -- Check_Aspect_At_[Freeze_Point | End_Of_Declarations] @@ -1219,7 +1222,7 @@ package body Sem_Ch13 is Aspect_Static_Predicate => -- Construct the pragma (always a pragma Predicate, with - -- flags recording whether + -- flags recording whether it is static/dynamic). Aitem := Make_Pragma (Loc, @@ -1255,6 +1258,64 @@ package body Sem_Ch13 is Ensure_Freeze_Node (E); Set_Is_Delayed_Aspect (Aspect); Delay_Required := True; + + when Aspect_Test_Case => declare + Args : List_Id; + Comp_Expr : Node_Id; + Comp_Assn : Node_Id; + + begin + Args := New_List; + + if Nkind (Expr) /= N_Aggregate then + Error_Msg_NE + ("wrong syntax for aspect `Test_Case` for &", Id, E); + goto Continue; + end if; + + Comp_Expr := First (Expressions (Expr)); + while Present (Comp_Expr) loop + Append (Relocate_Node (Comp_Expr), Args); + Next (Comp_Expr); + end loop; + + Comp_Assn := First (Component_Associations (Expr)); + while Present (Comp_Assn) loop + if List_Length (Choices (Comp_Assn)) /= 1 + or else + Nkind (First (Choices (Comp_Assn))) /= N_Identifier + then + Error_Msg_NE + ("wrong syntax for aspect `Test_Case` for &", Id, E); + goto Continue; + end if; + + Append (Make_Pragma_Argument_Association ( + Sloc => Sloc (Comp_Assn), + Chars => Chars (First (Choices (Comp_Assn))), + Expression => Relocate_Node (Expression (Comp_Assn))), + Args); + Next (Comp_Assn); + end loop; + + -- Build the test-case pragma + + Aitem := + Make_Pragma (Loc, + Pragma_Identifier => + Make_Identifier (Sloc (Id), Name_Test_Case), + Pragma_Argument_Associations => + Args); + + Set_From_Aspect_Specification (Aitem, True); + Set_Is_Delayed_Aspect (Aspect); + + -- Insert immediately after the entity declaration + + Insert_After (N, Aitem); + + goto Continue; + end; end case; -- If a delay is required, we delay the freeze (not much point in @@ -5330,6 +5391,12 @@ package body Sem_Ch13 is when Boolean_Aspects => raise Program_Error; + -- Test_Case aspect applies to entries and subprograms, hence should + -- never be delayed. + + when Aspect_Test_Case => + raise Program_Error; + -- Default_Value is resolved with the type entity in question when Aspect_Default_Value => @@ -5354,8 +5421,7 @@ package body Sem_Ch13 is when Aspect_Storage_Pool => T := Class_Wide_Type (RTE (RE_Root_Storage_Pool)); - when - Aspect_Alignment | + when Aspect_Alignment | Aspect_Component_Size | Aspect_Machine_Radix | Aspect_Object_Size | @@ -5375,7 +5441,7 @@ package body Sem_Ch13 is Analyze (Expression (ASN)); return; - -- Suppress/Unsupress/Warnings should never be delayed + -- Suppress/Unsuppress/Warnings should never be delayed when Aspect_Suppress | Aspect_Unsuppress | diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 721ded18548..53ba892bd8e 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2180,11 +2180,18 @@ package body Sem_Ch3 is if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then Spec := Specification (Original_Node (Decl)); Sent := Defining_Unit_Name (Spec); - Prag := Spec_PPC_List (Sent); + + Prag := Spec_PPC_List (Contract (Sent)); while Present (Prag) loop Analyze_PPC_In_Decl_Part (Prag, Sent); Prag := Next_Pragma (Prag); end loop; + + Prag := Spec_TC_List (Contract (Sent)); + while Present (Prag) loop + Analyze_TC_In_Decl_Part (Prag, Sent); + Prag := Next_Pragma (Prag); + end loop; end if; Next (Decl); @@ -13001,6 +13008,7 @@ package body Sem_Ch3 is New_Subp := New_Entity (Nkind (Parent_Subp), Sloc (Derived_Type)); Set_Ekind (New_Subp, Ekind (Parent_Subp)); + Set_Contract (New_Subp, Make_Contract (Sloc (New_Subp))); -- Check whether the inherited subprogram is a private operation that -- should be inherited but not yet made visible. Such subprograms can diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index d0e51e51870..98b6d91c4ff 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -230,6 +230,7 @@ package body Sem_Ch6 is Check_SPARK_Restriction ("abstract subprogram is not allowed", N); Generate_Definition (Designator); + Set_Contract (Designator, Make_Contract (Sloc (Designator))); Set_Is_Abstract_Subprogram (Designator); New_Overloaded_Entity (Designator); Check_Delayed_Subprogram (Designator); @@ -2539,6 +2540,7 @@ package body Sem_Ch6 is if Nkind (N) /= N_Subprogram_Body_Stub then Set_Acts_As_Spec (N); Generate_Definition (Body_Id); + Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id))); Generate_Reference (Body_Id, Body_Id, 'b', Set_Ref => False, Force => True); Generate_Reference_To_Formals (Body_Id); @@ -2981,6 +2983,7 @@ package body Sem_Ch6 is Designator := Analyze_Subprogram_Specification (Specification (N)); Generate_Definition (Designator); + -- ??? why this call, already in Analyze_Subprogram_Specification if Debug_Flag_C then Write_Str ("==> subprogram spec "); @@ -3170,6 +3173,7 @@ package body Sem_Ch6 is -- Proceed with analysis Generate_Definition (Designator); + Set_Contract (Designator, Make_Contract (Sloc (Designator))); if Nkind (N) = N_Function_Specification then Set_Ekind (Designator, E_Function); @@ -7300,7 +7304,8 @@ package body Sem_Ch6 is begin for J in Inherited'Range loop - P := Spec_PPC_List (Inherited (J)); + P := Spec_PPC_List (Contract (Inherited (J))); + while Present (P) loop Error_Msg_Sloc := Sloc (P); @@ -9193,7 +9198,7 @@ package body Sem_Ch6 is -- the body will be analyzed and converted when we scan the body -- declarations below. - Prag := Spec_PPC_List (Spec_Id); + Prag := Spec_PPC_List (Contract (Spec_Id)); while Present (Prag) loop if Pragma_Name (Prag) = Name_Precondition then @@ -9222,7 +9227,7 @@ package body Sem_Ch6 is -- Now deal with inherited preconditions for J in Inherited'Range loop - Prag := Spec_PPC_List (Inherited (J)); + Prag := Spec_PPC_List (Contract (Inherited (J))); while Present (Prag) loop if Pragma_Name (Prag) = Name_Precondition @@ -9402,7 +9407,7 @@ package body Sem_Ch6 is -- Loop through PPC pragmas from spec - Prag := Spec_PPC_List (Spec); + Prag := Spec_PPC_List (Contract (Spec)); loop if Pragma_Name (Prag) = Name_Postcondition and then (not Class or else Class_Present (Prag)) @@ -9427,14 +9432,14 @@ package body Sem_Ch6 is -- Start of processing for Spec_Postconditions begin - if Present (Spec_PPC_List (Spec_Id)) then + if Present (Spec_PPC_List (Contract (Spec_Id))) then Process_Post_Conditions (Spec_Id, Class => False); end if; -- Process inherited postconditions for J in Inherited'Range loop - if Present (Spec_PPC_List (Inherited (J))) then + if Present (Spec_PPC_List (Contract (Inherited (J)))) then Process_Post_Conditions (Inherited (J), Class => True); end if; end loop; diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 399d36e8771..410c02661b7 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -885,6 +885,7 @@ package body Sem_Ch9 is begin Generate_Definition (Def_Id); + Set_Contract (Def_Id, Make_Contract (Sloc (Def_Id))); Tasking_Used := True; -- Case of no discrete subtype definition diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 081c46a2312..2a218612a26 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -179,6 +179,11 @@ package body Sem_Prag is -- original one, following the renaming chain) is returned. Otherwise the -- entity is returned unchanged. Should be in Einfo??? + procedure Preanalyze_TC_Args (Arg_Req, Arg_Ens : Node_Id); + -- Preanalyze the boolean expressions in the Requires and Ensures arguments + -- of a Test_Case pragma if present (possibly Empty). We treat these as + -- spec expressions (i.e. similar to a default expression). + procedure rv; -- This is a dummy function called by the processing for pragma Reviewable. -- It is there for assisting front end debugging. By placing a Reviewable @@ -333,6 +338,10 @@ package body Sem_Prag is -- Check the specified argument Arg to make sure that it is an integer -- literal. If not give error and raise Pragma_Exit. + procedure Check_Arg_Is_String_Literal (Arg : Node_Id); + -- Check the specified argument Arg to make sure that it is a string + -- literal. If not give error and raise Pragma_Exit. + procedure Check_Arg_Is_Library_Level_Local_Name (Arg : Node_Id); -- Check the specified argument Arg to make sure that it has the proper -- syntactic form for a local name and meets the semantic requirements @@ -410,6 +419,12 @@ package body Sem_Prag is -- Checks that Arg, whose expression is an entity name, references a -- first subtype. + procedure Check_Identifier (Arg : Node_Id; Id : Name_Id); + -- Checks that the given argument has an identifier, and if so, requires + -- it to match the given identifier name. If there is no identifier, or + -- a non-matching identifier, then an error message is given and + -- Error_Pragmas raised. + procedure Check_In_Main_Program; -- Common checks for pragmas that appear within a main program -- (Priority, Main_Storage, Time_Slice, Relative_Deadline, CPU). @@ -478,6 +493,27 @@ package body Sem_Prag is -- that the constraint is static as required by the restrictions for -- Unchecked_Union. + procedure Check_Test_Case; + -- Called to process a test-case pragma. The treatment is similar to the + -- one for pre- and postcondition in Check_Precondition_Postcondition. + -- There are three cases: + -- + -- The pragma appears after a subprogram spec + -- + -- The first step is to analyze the pragma, but this is skipped if + -- the subprogram spec appears within a package specification + -- (because this is the case where we delay analysis till the end of + -- the spec). Then (whether or not it was analyzed), the pragma is + -- chained to the subprogram in question (using Spec_TC_List and + -- Next_Pragma). + -- + -- The pragma appears at the start of subprogram body declarations + -- + -- In this case an immediate return to the caller is made, and the + -- pragma is NOT analyzed. + -- + -- In all other cases, an error message for bad placement is given + procedure Check_Valid_Configuration_Pragma; -- Legality checks for placement of a configuration pragma @@ -860,6 +896,19 @@ package body Sem_Prag is end if; end Check_Arg_Is_Integer_Literal; + --------------------------------- + -- Check_Arg_Is_String_Literal -- + --------------------------------- + + procedure Check_Arg_Is_String_Literal (Arg : Node_Id) is + Argx : constant Node_Id := Get_Pragma_Arg (Arg); + begin + if Nkind (Argx) /= N_String_Literal then + Error_Pragma_Arg + ("argument for pragma% must be string literal", Argx); + end if; + end Check_Arg_Is_String_Literal; + ------------------------------------------- -- Check_Arg_Is_Library_Level_Local_Name -- ------------------------------------------- @@ -1036,6 +1085,7 @@ package body Sem_Prag is Error_Pragma_Arg ("invalid argument for pragma%", Argx); end if; end Check_Arg_Is_One_Of; + --------------------------------- -- Check_Arg_Is_Queuing_Policy -- --------------------------------- @@ -1364,6 +1414,24 @@ package body Sem_Prag is end if; end Check_First_Subtype; + ---------------------- + -- Check_Identifier -- + ---------------------- + + procedure Check_Identifier (Arg : Node_Id; Id : Name_Id) is + begin + if Present (Arg) + and then Nkind (Arg) = N_Pragma_Argument_Association + then + if Chars (Arg) = No_Name or else Chars (Arg) /= Id then + Error_Msg_Name_1 := Pname; + Error_Msg_Name_2 := Id; + Error_Msg_N ("pragma% argument expects identifier%", Arg); + raise Pragma_Exit; + end if; + end if; + end Check_Identifier; + --------------------------- -- Check_In_Main_Program -- --------------------------- @@ -1571,10 +1639,10 @@ package body Sem_Prag is PO : Node_Id; procedure Chain_PPC (PO : Node_Id); - -- If PO is a subprogram declaration node (or a generic subprogram - -- declaration node), then the precondition/postcondition applies - -- to this subprogram and the processing for the pragma is completed. - -- Otherwise the pragma is misplaced. + -- If PO is an entry or a [generic] subprogram declaration node, then + -- the precondition/postcondition applies to this subprogram and the + -- processing for the pragma is completed. Otherwise the pragma is + -- misplaced. --------------- -- Chain_PPC -- @@ -1637,7 +1705,7 @@ package body Sem_Prag is if Pragma_Name (N) = Name_Precondition then if not From_Aspect_Specification (N) then - P := Spec_PPC_List (S); + P := Spec_PPC_List (Contract (S)); while Present (P) loop if Pragma_Name (P) = Name_Precondition and then From_Aspect_Specification (P) @@ -1666,7 +1734,7 @@ package body Sem_Prag is begin for J in Inherited'Range loop - P := Spec_PPC_List (Inherited (J)); + P := Spec_PPC_List (Contract (Inherited (J))); while Present (P) loop if Pragma_Name (P) = Name_Precondition and then Class_Present (P) @@ -1691,8 +1759,8 @@ package body Sem_Prag is -- Chain spec PPC pragma to list for subprogram - Set_Next_Pragma (N, Spec_PPC_List (S)); - Set_Spec_PPC_List (S, N); + Set_Next_Pragma (N, Spec_PPC_List (Contract (S))); + Set_Spec_PPC_List (Contract (S), N); -- Return indicating spec case @@ -1870,6 +1938,135 @@ package body Sem_Prag is end case; end Check_Static_Constraint; + --------------------- + -- Check_Test_Case -- + --------------------- + + procedure Check_Test_Case is + P : Node_Id; + PO : Node_Id; + + procedure Chain_TC (PO : Node_Id); + -- If PO is an entry or a [generic] subprogram declaration node, then + -- the test-case applies to this subprogram and the processing for + -- the pragma is completed. Otherwise the pragma is misplaced. + + -------------- + -- Chain_TC -- + -------------- + + procedure Chain_TC (PO : Node_Id) is + S : Entity_Id; + + begin + if Nkind (PO) = N_Abstract_Subprogram_Declaration then + if From_Aspect_Specification (N) then + Error_Pragma + ("aspect% cannot be applied to abstract subprogram"); + else + Error_Pragma + ("pragma% cannot be applied to abstract subprogram"); + end if; + + elsif not Nkind_In (PO, N_Subprogram_Declaration, + N_Generic_Subprogram_Declaration, + N_Entry_Declaration) + then + Pragma_Misplaced; + end if; + + -- Here if we have [generic] subprogram or entry declaration + + if Nkind (PO) = N_Entry_Declaration then + S := Defining_Entity (PO); + else + S := Defining_Unit_Name (Specification (PO)); + end if; + + -- Note: we do not analyze the pragma at this point. Instead we + -- delay this analysis until the end of the declarative part in + -- which the pragma appears. This implements the required delay + -- in this analysis, allowing forward references. The analysis + -- happens at the end of Analyze_Declarations. + + -- Chain spec TC pragma to list for subprogram + + Set_Next_Pragma (N, Spec_TC_List (Contract (S))); + Set_Spec_TC_List (Contract (S), N); + end Chain_TC; + + -- Start of processing for Check_Test_Case + + begin + if not Is_List_Member (N) then + Pragma_Misplaced; + end if; + + -- Search prior declarations + + P := N; + while Present (Prev (P)) loop + P := Prev (P); + + -- If the previous node is a generic subprogram, do not go to to + -- the original node, which is the unanalyzed tree: we need to + -- attach the test-case to the analyzed version at this point. + -- They get propagated to the original tree when analyzing the + -- corresponding body. + + if Nkind (P) not in N_Generic_Declaration then + PO := Original_Node (P); + else + PO := P; + end if; + + -- Skip past prior pragma + + if Nkind (PO) = N_Pragma then + null; + + -- Skip stuff not coming from source + + elsif not Comes_From_Source (PO) then + null; + + -- Only remaining possibility is subprogram declaration + + else + Chain_TC (PO); + return; + end if; + end loop; + + -- If we fall through loop, pragma is at start of list, so see if it + -- is at the start of declarations of a subprogram body. + + if Nkind (Parent (N)) = N_Subprogram_Body + and then List_Containing (N) = Declarations (Parent (N)) + then + if Operating_Mode /= Generate_Code + or else Inside_A_Generic + then + -- Analyze pragma expressions for correctness and for ASIS use + + Preanalyze_TC_Args (Get_Requires_From_Test_Case_Pragma (N), + Get_Ensures_From_Test_Case_Pragma (N)); + end if; + + return; + + -- See if it is in the pragmas after a library level subprogram + + elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then + Chain_TC (Unit (Parent (Parent (N)))); + return; + end if; + + -- If we fall through, pragma was misplaced + + Pragma_Misplaced; + end Check_Test_Case; + -------------------------------------- -- Check_Valid_Configuration_Pragma -- -------------------------------------- @@ -12904,9 +13101,9 @@ package body Sem_Prag is end if; end; - -------------- + --------------- -- Task_Info -- - -------------- + --------------- -- pragma Task_Info (EXPRESSION); @@ -13023,6 +13220,38 @@ package body Sem_Prag is end if; end Task_Storage; + --------------- + -- Test_Case -- + --------------- + + -- pragma Test_Case ([Name =>] String_Expression + -- ,[Mode =>] (Normal | Robustness) + -- [, Requires => Boolean_Expression] + -- [, Ensures => Boolean_Expression]); + + when Pragma_Test_Case => Test_Case : declare + + begin + GNAT_Pragma; + Check_At_Least_N_Arguments (3); + Check_At_Most_N_Arguments (4); + Check_Arg_Order + ((Name_Name, Name_Mode, Name_Requires, Name_Ensures)); + + Check_Optional_Identifier (Arg1, Name_Name); + Check_Arg_Is_String_Literal (Arg1); + Check_Optional_Identifier (Arg2, Name_Mode); + Check_Arg_Is_One_Of (Arg2, Name_Normal, Name_Robustness); + if Arg_Count = 4 then + Check_Identifier (Arg3, Name_Requires); + Check_Identifier (Arg4, Name_Ensures); + else + Check_Arg_Is_One_Of (Arg3, Name_Requires, Name_Ensures); + end if; + + Check_Test_Case; + end Test_Case; + -------------------------- -- Thread_Local_Storage -- -------------------------- @@ -13887,6 +14116,30 @@ package body Sem_Prag is when Pragma_Exit => null; end Analyze_Pragma; + ----------------------------- + -- Analyze_TC_In_Decl_Part -- + ----------------------------- + + procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id) is + begin + -- Install formals and push subprogram spec onto scope stack so that we + -- can see the formals from the pragma. + + Install_Formals (S); + Push_Scope (S); + + -- Preanalyze the boolean expressions, we treat these as spec + -- expressions (i.e. similar to a default expression). + + Preanalyze_TC_Args (Get_Requires_From_Test_Case_Pragma (N), + Get_Ensures_From_Test_Case_Pragma (N)); + + -- Remove the subprogram from the scope stack now that the pre-analysis + -- of the expressions in the test-case is done. + + End_Scope; + end Analyze_TC_In_Decl_Part; + ------------------- -- Check_Enabled -- ------------------- @@ -14214,6 +14467,7 @@ package body Sem_Prag is Pragma_Task_Info => -1, Pragma_Task_Name => -1, Pragma_Task_Storage => 0, + Pragma_Test_Case => -1, Pragma_Thread_Local_Storage => 0, Pragma_Time_Slice => -1, Pragma_Title => -1, @@ -14355,6 +14609,26 @@ package body Sem_Prag is end if; end Is_Pragma_String_Literal; + ------------------------ + -- Preanalyze_TC_Args -- + ------------------------ + + procedure Preanalyze_TC_Args (Arg_Req, Arg_Ens : Node_Id) is + begin + -- Preanalyze the boolean expressions, we treat these as spec + -- expressions (i.e. similar to a default expression). + + if Present (Arg_Req) then + Preanalyze_Spec_Expression + (Get_Pragma_Arg (Arg_Req), Standard_Boolean); + end if; + + if Present (Arg_Ens) then + Preanalyze_Spec_Expression + (Get_Pragma_Arg (Arg_Ens), Standard_Boolean); + end if; + end Preanalyze_TC_Args; + -------------------------------------- -- Process_Compilation_Unit_Pragmas -- -------------------------------------- diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 4106120b094..5d9c741b09d 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.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- -- @@ -46,6 +46,14 @@ package Sem_Prag is procedure Analyze_Pragma (N : Node_Id); -- Analyze procedure for pragma reference node N + procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id); + -- Special analyze routine for test-case pragma that appears within a + -- declarative part where the pragma is associated with a subprogram + -- specification. N is the pragma node, and S is the entity for the related + -- subprogram. This procedure does a preanalysis of the expressions in the + -- pragma as "spec expressions" (see section in Sem "Handling of Default + -- and Per-Object Expressions..."). + function Check_Enabled (Nam : Name_Id) return Boolean; -- This function is used in connection with pragmas Assertion, Check, -- Precondition, and Postcondition to determine if Check pragmas (or diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 8db690506ae..5974f9cd57d 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -4223,6 +4223,28 @@ package body Sem_Util is end if; end Get_Enum_Lit_From_Pos; + --------------------------------------- + -- Get_Ensures_From_Test_Case_Pragma -- + --------------------------------------- + + function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id is + Args : constant List_Id := Pragma_Argument_Associations (N); + Res : Node_Id; + + begin + if List_Length (Args) = 4 then + Res := Pick (Args, 4); + + else + Res := Pick (Args, 3); + if Chars (Res) /= Name_Ensures then + Res := Empty; + end if; + end if; + + return Res; + end Get_Ensures_From_Test_Case_Pragma; + ------------------------ -- Get_Generic_Entity -- ------------------------ @@ -4352,6 +4374,23 @@ package body Sem_Util is return R; end Get_Renamed_Entity; + ---------------------------------------- + -- Get_Requires_From_Test_Case_Pragma -- + ---------------------------------------- + + function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id is + Args : constant List_Id := Pragma_Argument_Associations (N); + Res : Node_Id; + + begin + Res := Pick (Args, 3); + if Chars (Res) /= Name_Requires then + Res := Empty; + end if; + + return Res; + end Get_Requires_From_Test_Case_Pragma; + ------------------------- -- Get_Subprogram_Body -- ------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 7c7ddd65227..e880601bdf8 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -484,6 +484,9 @@ package Sem_Util is -- If expression N references a part of an object, return this object. -- Otherwise return Empty. Expression N should have been resolved already. + function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id; + -- Return the Ensures components of Test_Case pragma N, or Empty otherwise + function Get_Generic_Entity (N : Node_Id) return Entity_Id; -- Returns the true generic entity in an instantiation. If the name in the -- instantiation is a renaming, the function returns the renamed generic. @@ -530,6 +533,9 @@ package Sem_Util is -- not a renamed entity, returns its argument. It is an error to call this -- with any other kind of entity. + function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id; + -- Return the Requires components of Test_Case pragma N, or Empty otherwise + function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id; -- Nod is either a procedure call statement, or a function call, or an -- accept statement node. This procedure finds the Entity_Id of the related diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index f2a11ba8923..5ff5c474c6e 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -2766,6 +2766,22 @@ package body Sinfo is return Node1 (N); end Source_Type; + function Spec_PPC_List + (N : Node_Id) return Node_Id is + begin + pragma Assert (False + or else NT (N).Nkind = N_Contract); + return Node1 (N); + end Spec_PPC_List; + + function Spec_TC_List + (N : Node_Id) return Node_Id is + begin + pragma Assert (False + or else NT (N).Nkind = N_Contract); + return Node2 (N); + end Spec_TC_List; + function Specification (N : Node_Id) return Node_Id is begin @@ -5792,6 +5808,22 @@ package body Sinfo is Set_Node1 (N, Val); -- semantic field, no parent set end Set_Source_Type; + procedure Set_Spec_PPC_List + (N : Node_Id; Val : Node_Id) is + begin + pragma Assert (False + or else NT (N).Nkind = N_Contract); + Set_Node1 (N, Val); -- semantic field, no parent set + end Set_Spec_PPC_List; + + procedure Set_Spec_TC_List + (N : Node_Id; Val : Node_Id) is + begin + pragma Assert (False + or else NT (N).Nkind = N_Contract); + Set_Node2 (N, Val); -- semantic field, no parent set + end Set_Spec_TC_List; + procedure Set_Specification (N : Node_Id; Val : Node_Id) is begin diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index a7134754a6e..13ee674e1ce 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1694,12 +1694,12 @@ package Sinfo is -- which gigi must do size validation for. -- Split_PPC (Flag17) - -- When a Pre or Postaspect specification is processed, it is broken - -- into AND THEN sections. The left most section has Split_PPC set to - -- False, indicating that it is the original specification (e.g. for - -- posting errors). For other sections, Split_PPC is set to True. - -- This flag is set in both the N_Aspect_Specification node itself, - -- and in the pragma which is generated from this node. + -- When a Pre or Post aspect specification is processed, it is broken + -- into AND THEN sections. The left most section has Split_PPC set to + -- False, indicating that it is the original specification (e.g. for + -- posting errors). For other sections, Split_PPC is set to True. + -- This flag is set in both the N_Aspect_Specification node itself, + -- and in the pragma which is generated from this node. -- Static_Processing_OK (Flag4-Sem) -- Present in N_Aggregate nodes. When the Compile_Time_Known_Aggregate @@ -6894,6 +6894,39 @@ package Sinfo is -- Is_Elsif (Flag13) (set if comes from ELSIF) -- plus fields for expression + -------------- + -- Contract -- + -------------- + + -- This node is used to hold the various parts of an entry or subprogram + -- contract, consisting in pre- and postconditions on the one hand, and + -- test-cases on the other hand. + + -- It is referenced from an entry, a subprogram or a generic subprogram + -- entity. + + -- Sprint syntax: as the node should not appear in the tree, but + -- only attached to an entry or [generic] subprogram + -- entity. + + -- N_Contract + -- Sloc points to the subprogram's name + -- Spec_PPC_List (Node1) (set to Empty if none) + -- Spec_TC_List (Node2) (set to Empty if none) + + -- Spec_PPC_List points to a list of Precondition and Postcondition + -- pragma nodes for preconditions and postconditions declared in the + -- spec of the entry/subprogram. The last pragma encountered is at the + -- head of this list, so it is in reverse order of textual appearance. + -- Note that this includes precondition/postcondition pragmas generated + -- to correspond to Pre/Post aspects. + + -- Spec_TC_List points to a list of Test_Case pragma nodes for + -- test-cases declared in the spec of the entry/subprogram. The last + -- pragma encountered is at the head of this list, so it is in reverse + -- order of textual appearance. Note that this includes test-case + -- pragmas generated to correspond to Test_Case aspects. + ------------------- -- Expanded_Name -- ------------------- @@ -7746,6 +7779,7 @@ package Sinfo is N_Component_Association, N_Component_Definition, N_Component_List, + N_Contract, N_Derived_Type_Definition, N_Decimal_Fixed_Point_Definition, N_Defining_Program_Unit_Name, @@ -8850,6 +8884,12 @@ package Sinfo is function Source_Type (N : Node_Id) return Entity_Id; -- Node1 + function Spec_PPC_List + (N : Node_Id) return Node_Id; -- Node1 + + function Spec_TC_List + (N : Node_Id) return Node_Id; -- Node2 + function Specification (N : Node_Id) return Node_Id; -- Node1 @@ -9813,6 +9853,12 @@ package Sinfo is procedure Set_Source_Type (N : Node_Id; Val : Entity_Id); -- Node1 + procedure Set_Spec_PPC_List + (N : Node_Id; Val : Node_Id); -- Node1 + + procedure Set_Spec_TC_List + (N : Node_Id; Val : Node_Id); -- Node2 + procedure Set_Specification (N : Node_Id; Val : Node_Id); -- Node1 @@ -11447,6 +11493,13 @@ package Sinfo is 4 => False, -- unused 5 => False), -- Etype (Node5-Sem) + N_Contract => + (1 => False, -- Spec_PPC_List (Node1) + 2 => False, -- Spec_TC_List (Node2) + 3 => False, -- unused + 4 => False, -- unused + 5 => False), -- unused + N_Expanded_Name => (1 => True, -- Chars (Name1) 2 => True, -- Selector_Name (Node2) @@ -11931,6 +11984,8 @@ package Sinfo is pragma Inline (Selector_Names); pragma Inline (Shift_Count_OK); pragma Inline (Source_Type); + pragma Inline (Spec_PPC_List); + pragma Inline (Spec_TC_List); pragma Inline (Specification); pragma Inline (Split_PPC); pragma Inline (Statements); @@ -12248,6 +12303,8 @@ package Sinfo is pragma Inline (Set_Selector_Names); pragma Inline (Set_Shift_Count_OK); pragma Inline (Set_Source_Type); + pragma Inline (Set_Spec_PPC_List); + pragma Inline (Set_Spec_TC_List); pragma Inline (Set_Specification); pragma Inline (Set_Split_PPC); pragma Inline (Set_Statements); diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index c3c7bead3b6..ba35d51d119 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -544,6 +544,7 @@ package Snames is Name_Suppress_Debug_Info : constant Name_Id := N + $; -- GNAT Name_Suppress_Initialization : constant Name_Id := N + $; -- GNAT Name_System_Name : constant Name_Id := N + $; -- Ada 83 + Name_Test_Case : constant Name_Id := N + $; -- GNAT Name_Task_Info : constant Name_Id := N + $; -- GNAT Name_Task_Name : constant Name_Id := N + $; -- GNAT Name_Task_Storage : constant Name_Id := N + $; -- VMS @@ -624,6 +625,7 @@ package Snames is Name_Descriptor : constant Name_Id := N + $; Name_Dot_Replacement : constant Name_Id := N + $; Name_Dynamic : constant Name_Id := N + $; + Name_Ensures : constant Name_Id := N + $; Name_Entity : constant Name_Id := N + $; Name_Entry_Count : constant Name_Id := N + $; Name_External_Name : constant Name_Id := N + $; @@ -646,6 +648,7 @@ package Snames is Name_Mechanism : constant Name_Id := N + $; Name_Message : constant Name_Id := N + $; Name_Mixedcase : constant Name_Id := N + $; + Name_Mode : constant Name_Id := N + $; Name_Modified_GPL : constant Name_Id := N + $; Name_Name : constant Name_Id := N + $; Name_NCA : constant Name_Id := N + $; @@ -657,13 +660,16 @@ package Snames is Name_No_Requeue_Statements : constant Name_Id := N + $; Name_No_Task_Attributes : constant Name_Id := N + $; Name_No_Task_Attributes_Package : constant Name_Id := N + $; + Name_Normal : constant Name_Id := N + $; Name_On : constant Name_Id := N + $; Name_Policy : constant Name_Id := N + $; Name_Parameter_Types : constant Name_Id := N + $; Name_Reference : constant Name_Id := N + $; + Name_Requires : constant Name_Id := N + $; Name_Restricted : constant Name_Id := N + $; Name_Result_Mechanism : constant Name_Id := N + $; Name_Result_Type : constant Name_Id := N + $; + Name_Robustness : constant Name_Id := N + $; Name_Runtime : constant Name_Id := N + $; Name_SB : constant Name_Id := N + $; Name_Secondary_Stack_Size : constant Name_Id := N + $; @@ -1634,6 +1640,7 @@ package Snames is Pragma_Suppress_Debug_Info, Pragma_Suppress_Initialization, Pragma_System_Name, + Pragma_Test_Case, Pragma_Task_Info, Pragma_Task_Name, Pragma_Task_Storage, diff --git a/gcc/ada/sprint.adb b/gcc/ada/sprint.adb index 503c6f4366e..5c6f3297a88 100644 --- a/gcc/ada/sprint.adb +++ b/gcc/ada/sprint.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- -- @@ -1348,6 +1348,12 @@ package body Sprint is Sprint_Node (Component_Definition (Node)); + -- A contract node should not appear in the tree. It is a semantic + -- node attached to entry and [generic] subprogram entities. + + when N_Contract => + raise Program_Error; + when N_Decimal_Fixed_Point_Definition => Write_Str_With_Col_Check_Sloc (" delta "); Sprint_Node (Delta_Expression (Node));