From 20a65dcba9a95dd40a8794324e833d5ff9f07544 Mon Sep 17 00:00:00 2001 From: Robert Dewar Date: Tue, 23 Apr 2013 09:56:06 +0000 Subject: [PATCH] exp_prag.adb (Expand_Pragma_Check): Check for Assert rather than Assertion. 2013-04-23 Robert Dewar * exp_prag.adb (Expand_Pragma_Check): Check for Assert rather than Assertion. * sem_prag.adb (Is_Valid_Assertion_Kind): Moved to spec (Effective_Name): New function (Analyze_Pragma, case Check): Disallow [Statement_]Assertions (Check_Kind): Implement Statement_Assertions (Check_Applicable_Policy): Use Effective_Name (Is_Valid_Assertion_Kind): Allow Statement_Assertions. * sem_prag.ads (Is_Valid_Assertion_Kind): Moved here from body (Effective_Name): New function. * sem_res.adb: Minor reformatting. * snames.ads-tmpl (Name_Statement_Assertions): New entry. * gnat_rm.texi: Add documentation of new assertion kind Statement_Assertions. From-SVN: r198187 --- gcc/ada/ChangeLog | 16 ++++ gcc/ada/exp_prag.adb | 4 +- gcc/ada/gnat_rm.texi | 31 ++++++- gcc/ada/sem_prag.adb | 197 ++++++++++++++++++++++++---------------- gcc/ada/sem_prag.ads | 35 +++++-- gcc/ada/sem_res.adb | 19 ++-- gcc/ada/snames.ads-tmpl | 1 + 7 files changed, 204 insertions(+), 99 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 216d437cde3..4bdf9e6d747 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,19 @@ +2013-04-23 Robert Dewar + + * exp_prag.adb (Expand_Pragma_Check): Check for Assert rather + than Assertion. + * sem_prag.adb (Is_Valid_Assertion_Kind): Moved to spec + (Effective_Name): New function (Analyze_Pragma, case Check): + Disallow [Statement_]Assertions (Check_Kind): Implement + Statement_Assertions (Check_Applicable_Policy): Use Effective_Name + (Is_Valid_Assertion_Kind): Allow Statement_Assertions. + * sem_prag.ads (Is_Valid_Assertion_Kind): Moved here from body + (Effective_Name): New function. + * sem_res.adb: Minor reformatting. + * snames.ads-tmpl (Name_Statement_Assertions): New entry. + * gnat_rm.texi: Add documentation of new assertion kind + Statement_Assertions. + 2013-04-23 Robert Dewar * sinfo.ads, einfo.adb, sem_res.adb, exp_ch6.adb, aspects.adb: Minor diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index 38efb8616ff..36191fb656e 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -377,7 +377,7 @@ package body Exp_Prag is -- For Assert, we just use the location - if Nam = Name_Assertion then + if Nam = Name_Assert then null; -- For predicate, we generate the string "predicate failed @@ -446,7 +446,7 @@ package body Exp_Prag is then return; - elsif Nam = Name_Assertion then + elsif Nam = Name_Assert then Error_Msg_N ("?A?assertion will fail at run time", N); else diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index a70a78dec6c..a7c1514eaff 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -1251,7 +1251,8 @@ RM_ASSERTION_KIND ::= Assert | Type_Invariant | Type_Invariant'Class -ID_ASSERTION_KIND ::= Assert_And_Cut | +ID_ASSERTION_KIND ::= Assertions | + Assert_And_Cut | Assume | Contract_Cases | Debug | @@ -1262,6 +1263,7 @@ ID_ASSERTION_KIND ::= Assert_And_Cut | Postcondition | Precondition | Predicate + Statement_Assertions POLICY_IDENTIFIER ::= Check | Disable | Ignore @end smallexample @@ -1292,6 +1294,15 @@ useful when the pragma or aspect argument references subprograms in a with'ed package which is replaced by a dummy package for the final build. +The implementation defined policy @code{Assertions} applies to all +assertion kinds. The form with no assertion kind given implies this +choice, so it applies to all assertion kinds (RM defined, and +implementation defined). + +The implementation defined policy @code{Statement_Assertions} +applies to @code{Assert}, @code{Assert_And_Cut}, +@code{Assume}, and @code{Loop_Invariant}. + @node Pragma Assume_No_Invalid_Values @unnumberedsec Pragma Assume_No_Invalid_Values @findex Assume_No_Invalid_Values @@ -1460,6 +1471,11 @@ Checks introduced by this pragma are normally deactivated by default. They can be activated either by the command line option @option{-gnata}, which turns on all checks, or individually controlled using pragma @code{Check_Policy}. +The identifiers @code{Assertions} and @code{Statement_Assertions} are not +permitted as check kinds, since this would cause confusion with the use +of these identifiers in @code{Assertion_Policy} and @code{Check_Policy} +pragmas, where they are used to refer to sets of assertions. + @node Pragma Check_Float_Overflow @unnumberedsec Pragma Check_Float_Overflow @cindex Floating-point overflow @@ -2860,7 +2876,18 @@ the standard runtime libraries be recompiled. The two argument form specifies the representation to be used for the specified floating-point type. On all systems other than OpenVMS, the argument must -be @code{IEEE_Float} and the pragma has no effect. On OpenVMS, the +be @code{IEEE_Float} to specify the use of IEEE format, as follows: + +@itemize @bullet +@item +For a digits value of 6, 32-bit IEEE short format will be used. +@item +For a digits value of 15, 64-bit IEEE long format will be used. +@item +No other value of digits is permitted. +@end itemize + +On OpenVMS, the argument may be @code{VAX_Float} to specify the use of the VAX float format, as follows: diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index bacb3406615..f0045a37c17 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -181,13 +181,6 @@ package body Sem_Prag is -- original one, following the renaming chain) is returned. Otherwise the -- entity is returned unchanged. Should be in Einfo??? - function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean; - -- Returns True if Nam is one of the names recognized as a valid assertion - -- kind by the Assertion_Policy pragma. Note that the 'Class cases are - -- represented by the corresponding special names Name_uPre, Name_uPost, - -- Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant, - -- and _Type_Invariant). - procedure Preanalyze_CTC_Args (N, 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 @@ -352,9 +345,7 @@ package body Sem_Prag is -- In ASIS mode, for a pragma generated from a source aspect, also -- analyze the original aspect expression. - if ASIS_Mode - and then Present (Corresponding_Aspect (N)) - then + if ASIS_Mode and then Present (Corresponding_Aspect (N)) then Preanalyze_Assert_Expression (Expression (Corresponding_Aspect (N)), Standard_Boolean); end if; @@ -2222,9 +2213,7 @@ package body Sem_Prag is -- In ASIS mode, for a pragma generated from a source aspect, -- also analyze the original aspect expression. - if ASIS_Mode - and then Present (Corresponding_Aspect (N)) - then + if ASIS_Mode and then Present (Corresponding_Aspect (N)) then Preanalyze_Assert_Expression (Expression (Corresponding_Aspect (N)), Standard_Boolean); end if; @@ -2411,9 +2400,7 @@ package body Sem_Prag is -- In ASIS mode, for a pragma generated from a source aspect, also -- analyze the original aspect expression. - if ASIS_Mode - and then Present (Corresponding_Aspect (N)) - then + if ASIS_Mode and then Present (Corresponding_Aspect (N)) then Check_Expr_Is_Static_Expression (Original_Node (Get_Pragma_Arg (Arg1)), Standard_String); end if; @@ -2882,10 +2869,7 @@ package body Sem_Prag is -- Get name from corresponding aspect - if Present (Corresponding_Aspect (N)) then - Error_Msg_Name_1 := - Chars (Identifier (Corresponding_Aspect (N))); - end if; + Error_Msg_Name_1 := Effective_Name (N); end if; end Fix_Error; @@ -6765,10 +6749,7 @@ package body Sem_Prag is -- Here to start processing for recognized pragma Prag_Id := Get_Pragma_Id (Pname); - - if Present (Corresponding_Aspect (N)) then - Pname := Chars (Identifier (Corresponding_Aspect (N))); - end if; + Pname := Effective_Name (N); -- Check applicable policy. We skip this for a pragma that came from -- an aspect, since we already dealt with the Disable case, and we set @@ -7426,9 +7407,9 @@ package body Sem_Prag is Check_Arg_Order ((Name_Check, Name_Message)); Check_Optional_Identifier (Arg1, Name_Check); - -- We treat pragma Assert as equivalent to: + -- We treat pragma Assert[_And_Cut] as equivalent to: - -- pragma Check (Assertion, condition [, msg]); + -- pragma Check (Assert[_And_Cut], condition [, msg]); -- So rewrite pragma in this manner, transfer the message -- argument if present, and analyze the result @@ -7443,8 +7424,7 @@ package body Sem_Prag is Expr := Get_Pragma_Arg (Arg1); Newa := New_List ( Make_Pragma_Argument_Association (Loc, - Expression => Make_Identifier (Loc, Name_Assertion)), - + Expression => Make_Identifier (Loc, Pname)), Make_Pragma_Argument_Association (Sloc (Expr), Expression => Expr)); @@ -8083,6 +8063,9 @@ package body Sem_Prag is -- Invariant'Class | -- Type_Invariant'Class + -- The identifiers Assertions and Statement_Assertions are not + -- allowed, since they have special meaning for Check_Policy. + when Pragma_Check => Check : declare Expr : Node_Id; Eloc : Source_Ptr; @@ -8108,6 +8091,23 @@ package body Sem_Prag is Check_Arg_Is_Identifier (Arg1); Cname := Chars (Get_Pragma_Arg (Arg1)); + -- Check forbidden name Assertions or Statement_Assertions + + case Cname is + when Name_Assertions => + Error_Pragma_Arg + ("""Assertions"" is not allowed as a check kind " + & "for pragma%", Arg1); + + when Name_Statement_Assertions => + Error_Pragma_Arg + ("""Statement_Assertions"" is not allowed as a check kind " + & "for pragma%", Arg1); + + when others => + null; + end case; + -- Set Check_On to indicate check status -- If this comes from an aspect, we have already taken care of @@ -17945,8 +17945,13 @@ package body Sem_Prag is begin if Nam = Pnm - or else (Is_Valid_Assertion_Kind (Nam) - and then Pnm = Name_Assertion) + or else (Pnm = Name_Assertion + and then Is_Valid_Assertion_Kind (Nam)) + or else (Pnm = Name_Statement_Assertions + and then Nam_In (Nam, Name_Assert, + Name_Assert_And_Cut, + Name_Assume, + Name_Loop_Invariant)) then case (Chars (Get_Pragma_Arg (Last (PPA)))) is when Name_On | Name_Check => @@ -17985,36 +17990,9 @@ package body Sem_Prag is PP : Node_Id; Policy : Name_Id; - Ename : Name_Id; - -- Effective name of aspect or pragma, this is simply the name of - -- the aspect or pragma, except in the case of a pragma derived from - -- an aspect, in which case it is the name of the aspect (which may be - -- different, e.g. Pre aspect generating Precondition pragma). It also - -- deals with the 'Class cases for an aspect. + Ename : constant Name_Id := Effective_Name (N); begin - if Nkind (N) = N_Pragma then - if Present (Corresponding_Aspect (N)) then - Ename := Chars (Identifier (Corresponding_Aspect (N))); - else - Ename := Chars (Pragma_Identifier (N)); - end if; - - else - pragma Assert (Nkind (N) = N_Aspect_Specification); - Ename := Chars (Identifier (N)); - - if Class_Present (N) then - case Ename is - when Name_Invariant => Ename := Name_uInvariant; - when Name_Pre => Ename := Name_uPre; - when Name_Post => Ename := Name_uPost; - when Name_Type_Invariant => Ename := Name_uType_Invariant; - when others => raise Program_Error; - end case; - end if; - end if; - -- No effect if not valid assertion kind name if not Is_Valid_Assertion_Kind (Ename) then @@ -18072,6 +18050,66 @@ package body Sem_Prag is Name_Priority_Specific_Dispatching); end Delay_Config_Pragma_Analyze; + -------------------- + -- Effective_Name -- + -------------------- + + function Effective_Name (N : Node_Id) return Name_Id is + Pras : Node_Id; + Name : Name_Id; + + begin + pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma)); + Pras := N; + + if Is_Rewrite_Substitution (Pras) + and then Nkind (Original_Node (Pras)) = N_Pragma + then + Pras := Original_Node (Pras); + end if; + + -- Case where we came from aspect specication + + if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then + Pras := Corresponding_Aspect (Pras); + end if; + + -- Get name from aspect or pragma + + if Nkind (Pras) = N_Pragma then + Name := Pragma_Name (Pras); + else + Name := Chars (Identifier (Pras)); + end if; + + -- Deal with 'Class + + if Class_Present (Pras) then + case Name is + + -- Names that need converting to special _xxx form + + when Name_Pre => Name := Name_uPre; + when Name_Post => Name := Name_uPost; + when Name_Invariant => Name := Name_uInvariant; + when Name_Type_Invariant => Name := Name_uType_Invariant; + + -- Names already in special _xxx form (leave them alone) + + when Name_uPre => null; + when Name_uPost => null; + when Name_uInvariant => null; + when Name_uType_Invariant => null; + + -- Anything else is impossible with Class_Present set True + + when others => raise Program_Error; + end case; + end if; + + return Name; + end Effective_Name; + ------------------------- -- Get_Base_Subprogram -- ------------------------- @@ -18521,31 +18559,32 @@ package body Sem_Prag is when -- RM defined - Name_Assert | - Name_Static_Predicate | - Name_Dynamic_Predicate | - Name_Pre | - Name_uPre | - Name_Post | - Name_uPost | - Name_Type_Invariant | - Name_uType_Invariant | + Name_Assert | + Name_Static_Predicate | + Name_Dynamic_Predicate | + Name_Pre | + Name_uPre | + Name_Post | + Name_uPost | + Name_Type_Invariant | + Name_uType_Invariant | -- Impl defined - Name_Assert_And_Cut | - Name_Assume | - Name_Contract_Cases | - Name_Debug | - Name_Invariant | - Name_uInvariant | - Name_Loop_Invariant | - Name_Loop_Variant | - Name_Postcondition | - Name_Precondition | - Name_Predicate => return True; + Name_Assert_And_Cut | + Name_Assume | + Name_Contract_Cases | + Name_Debug | + Name_Invariant | + Name_uInvariant | + Name_Loop_Invariant | + Name_Loop_Variant | + Name_Postcondition | + Name_Precondition | + Name_Predicate | + Name_Statement_Assertions => return True; - when others => return False; + when others => return False; end case; end Is_Valid_Assertion_Kind; diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 860005ec5ae..54ddc43f827 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -104,10 +104,30 @@ package Sem_Prag is -- True have their analysis delayed until after the main program is parsed -- and analyzed. + function Effective_Name (N : Node_Id) return Name_Id; + -- N is a pragma node or aspect specification node. This function returns + -- the name of the pragma or aspect, taking into account possible rewrites, + -- and also cases where a pragma comes from an attribute (in such cases, + -- the name can be different from the pragma name, e.g. Pre generates + -- a Precondition pragma. This also deals with the presence of 'Class + -- which results in one of the special names Name_uPre, Name_uPost, + -- Name_uInvariant, or Name_uType_Invariant being returned to represent + -- the corresponding aspects with x'Class names. + procedure Initialize; -- Initializes data structures used for pragma processing. Must be called -- before analyzing each new main source program. + function Is_Config_Static_String (Arg : Node_Id) return Boolean; + -- This is called for a configuration pragma that requires either string + -- literal or a concatenation of string literals. We cannot use normal + -- static string processing because it is too early in the case of the + -- pragma appearing in a configuration pragmas file. If Arg is of an + -- appropriate form, then this call obtains the string (doing any necessary + -- concatenations) and places it in Name_Buffer, setting Name_Len to its + -- length, and then returns True. If it is not of the correct form, then an + -- appropriate error message is posted, and False is returned. + function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean; -- The node N is a node for an entity and the issue is whether the -- occurrence is a reference for the purposes of giving warnings about @@ -124,15 +144,12 @@ package Sem_Prag is -- False is returned, then the argument is treated as an entity reference -- to the operator. - function Is_Config_Static_String (Arg : Node_Id) return Boolean; - -- This is called for a configuration pragma that requires either string - -- literal or a concatenation of string literals. We cannot use normal - -- static string processing because it is too early in the case of the - -- pragma appearing in a configuration pragmas file. If Arg is of an - -- appropriate form, then this call obtains the string (doing any necessary - -- concatenations) and places it in Name_Buffer, setting Name_Len to its - -- length, and then returns True. If it is not of the correct form, then an - -- appropriate error message is posted, and False is returned. + function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean; + -- Returns True if Nam is one of the names recognized as a valid assertion + -- kind by the Assertion_Policy pragma. Note that the 'Class cases are + -- represented by the corresponding special names Name_uPre, Name_uPost, + -- Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant, + -- and _Type_Invariant). procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id); -- This routine makes aspects from precondition or postcondition pragmas diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 1cb465a89bc..6a0f666e280 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -8908,27 +8908,32 @@ package body Sem_Res is Orig : constant Node_Id := Original_Node (Parent (N)); begin + -- Special handling of Asssert pragma + if Nkind (Orig) = N_Pragma and then Pragma_Name (Orig) = Name_Assert then - -- Don't want to warn if original condition is explicit False - declare Expr : constant Node_Id := Original_Node (Expression (First (Pragma_Argument_Associations (Orig)))); + begin + -- Don't warn if original condition is explicit False, + -- since obviously the failure is expected in this case. + if Is_Entity_Name (Expr) and then Entity (Expr) = Standard_False then null; - else - -- Issue warning. We do not want the deletion of the - -- IF/AND-THEN to take this message with it. We achieve - -- this by making sure that the expanded code points to - -- the Sloc of the expression, not the original pragma. + -- Issue warning. We do not want the deletion of the + -- IF/AND-THEN to take this message with it. We achieve this + -- by making sure that the expanded code points to the Sloc + -- of the expression, not the original pragma. + + else -- Note: Use Error_Msg_F here rather than Error_Msg_N. -- The source location of the expression is not usually -- the best choice here. For example, it gets located on diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index d1854b2705c..ad98f556482 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -761,6 +761,7 @@ package Snames is Name_Simple_Barriers : constant Name_Id := N + $; Name_Spec_File_Name : constant Name_Id := N + $; Name_State : constant Name_Id := N + $; + Name_Statement_Assertions : constant Name_Id := N + $; Name_Static : constant Name_Id := N + $; Name_Stack_Size : constant Name_Id := N + $; Name_Strict : constant Name_Id := N + $;