From 1d801f212f02cc2f62cfae39ce23589f645828df Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 1 Aug 2011 18:05:30 +0200 Subject: [PATCH] [multiple changes] 2011-08-01 Yannick Moy * par-ch4.adb (P_Name): issue a syntax error in SPARK mode on character literal or operator symbol which is prefixed * sem_attr.adb (Analyze_Access_Attribute): issue an error in formal mode on access attributes. * sem_ch4.adb (Analyze_Concatenation_Operand): new procedure to check that concatenation operands are properly restricted in formal mode (Analyze_Concatenation, Analyze_Concatenation_Rest): call new procedure Analyze_Concatenation_Operand. Issue an error in formal mode if the result of the concatenation has a type different from String. (Analyze_Conditional_Expression, Analyze_Explicit_Dereference, Analyze_Quantified_Expression, Analyze_Slice, Analyze_Null): issue an error in formal mode on unsupported constructs * sem_ch5.adb (Analyze_Block_Statement): only issue error on source block statement * sem_util.ads, sem_util.adb (Last_Source_Node_In_Sequence): new function which returns the last node in a list of nodes for which Comes_From_Source returns True, if any * sem_ch6.adb (Check_Missing_Return): minor refactoring to use Last_Source_Node_In_Sequence * sem_ch8.adb (Analyze_Exception_Renaming, Analyze_Generic_Renaming, Analyze_Object_Renaming, Analyze_Use_Package): issue an error in formal mode on unsupported constructs * sem_ch9.adb Do not return after issuing error in formal mode, as the rest of the actions may be needed later on since the error is marked as not serious. * sinfo.ads: Typos in comments. 2011-08-01 Pascal Obry * projects.texi: Minor editing. From-SVN: r177057 --- gcc/ada/ChangeLog | 33 ++++++++++++++++ gcc/ada/par-ch4.adb | 13 ++++++ gcc/ada/projects.texi | 26 ++++++++---- gcc/ada/sem_attr.adb | 8 ++++ gcc/ada/sem_ch4.adb | 92 +++++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_ch5.adb | 4 +- gcc/ada/sem_ch6.adb | 28 +++++-------- gcc/ada/sem_ch8.adb | 47 +++++++++++++++++++++- gcc/ada/sem_ch9.adb | 10 ----- gcc/ada/sem_util.adb | 18 +++++++++ gcc/ada/sem_util.ads | 4 ++ gcc/ada/sinfo.ads | 6 +-- 12 files changed, 249 insertions(+), 40 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d79f7c7c793..f044856f4e3 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,36 @@ +2011-08-01 Yannick Moy + + * par-ch4.adb (P_Name): issue a syntax error in SPARK mode on character + literal or operator symbol which is prefixed + * sem_attr.adb (Analyze_Access_Attribute): issue an error in formal + mode on access attributes. + * sem_ch4.adb (Analyze_Concatenation_Operand): new procedure to check + that concatenation operands are properly restricted in formal mode + (Analyze_Concatenation, Analyze_Concatenation_Rest): call new procedure + Analyze_Concatenation_Operand. Issue an error in formal mode if the + result of the concatenation has a type different from String. + (Analyze_Conditional_Expression, Analyze_Explicit_Dereference, + Analyze_Quantified_Expression, Analyze_Slice, + Analyze_Null): issue an error in formal mode on unsupported constructs + * sem_ch5.adb + (Analyze_Block_Statement): only issue error on source block statement + * sem_util.ads, sem_util.adb (Last_Source_Node_In_Sequence): new + function which returns the last node in a list of nodes for which + Comes_From_Source returns True, if any + * sem_ch6.adb (Check_Missing_Return): minor refactoring to use + Last_Source_Node_In_Sequence + * sem_ch8.adb (Analyze_Exception_Renaming, Analyze_Generic_Renaming, + Analyze_Object_Renaming, Analyze_Use_Package): issue an error in formal + mode on unsupported constructs + * sem_ch9.adb Do not return after issuing error in formal mode, as the + rest of the actions may be needed later on since the error is marked as + not serious. + * sinfo.ads: Typos in comments. + +2011-08-01 Pascal Obry + + * projects.texi: Minor editing. + 2011-08-01 Yannick Moy * err_vars.ads (Error_Msg_Lang, Error_Msg_Langlen): new variables for diff --git a/gcc/ada/par-ch4.adb b/gcc/ada/par-ch4.adb index 74ab7604a8a..338ee641593 100644 --- a/gcc/ada/par-ch4.adb +++ b/gcc/ada/par-ch4.adb @@ -209,8 +209,21 @@ package body Ch4 is -- designator. if Token not in Token_Class_Desig then + + -- Selector name cannot be a character literal in SPARK + + if SPARK_Mode and then Token = Tok_Char_Literal then + Error_Msg_SC ("|~~character literal cannot be prefixed"); + end if; + goto Scan_Name_Extension_Dot; else + -- Selector name cannot be an operator symbol in SPARK + + if SPARK_Mode and then Token = Tok_Operator_Symbol then + Error_Msg_SC ("|~~operator symbol cannot be prefixed"); + end if; + Prefix_Node := Name_Node; Name_Node := New_Node (N_Selected_Component, Prev_Token_Ptr); Set_Prefix (Name_Node, Prefix_Node); diff --git a/gcc/ada/projects.texi b/gcc/ada/projects.texi index 3b05c44d5b3..788445914fa 100644 --- a/gcc/ada/projects.texi +++ b/gcc/ada/projects.texi @@ -736,9 +736,10 @@ Notice the three steps described earlier: The default output of GPRbuild's execution is kept reasonably simple and easy to understand. In particular, some of the less frequently used commands are not shown, and some parameters are abbreviated. So it is not possible to rerun the -effect of the gprbuild command by cut-and-pasting its output. GPRbuild's option -@code{-v} provides a much more verbose output which includes, among other -information, more complete compilation, post-compilation and link commands. +effect of the @command{gprbuild} command by cut-and-pasting its output. +GPRbuild's option @code{-v} provides a much more verbose output which includes, +among other information, more complete compilation, post-compilation and link +commands. @c --------------------------------------------- @node Executable File Names @@ -1112,6 +1113,7 @@ the search stops: @itemize @bullet @item First, the file is searched relative to the directory that contains the current project file. + @item @cindex @code{ADA_PROJECT_PATH} @cindex @code{GPR_PROJECT_PATH} @@ -1119,12 +1121,22 @@ the search stops: ^environment variables^logical names^ @b{GPR_PROJECT_PATH} and @b{ADA_PROJECT_PATH} (in that order) if they exist. The former is recommended, the latter is kept for backward compatibility. + @item Finally, it is searched relative to the default project directories. - Such directories depends on the tool used. For @command{gnatmake}, there is - one default project directory: @file{/lib/gnat/}. In our example, - @file{gtkada.gpr} is found in the predefined directory if it was installed at - the same root as GNAT. + Such directories depends on the tool used. The different locations searched + in the specified order are: + + @itemize @bullet + @item @file{//lib/gnat} + (for @command{gprbuild} only and if option @option{--target} is specified) + @item @file{/share/gpr/} + (for @command{gnatmake} and @command{gprbuild}) + @item @file{/lib/gnat/} + (for @command{gnatmake} and @command{gprbuild}) + @end itemize + In our example, @file{gtkada.gpr} is found in the predefined directory if + it was installed at the same root as GNAT. @end itemize @noindent diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 1b6d3ef30b6..f2556a7f2a4 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -565,6 +565,14 @@ package body Sem_Attr is -- Start of processing for Analyze_Access_Attribute begin + -- Access attribute is not allowed in SPARK or ALFA + + if Formal_Verification_Mode and then Comes_From_Source (N) then + Error_Attr_P ("|~~% attribute is not allowed"); + end if; + + -- Proceed with analysis + Check_E0; if Nkind (P) = N_Character_Literal then diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index cd247cb8180..23913612169 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -67,6 +67,11 @@ package body Sem_Ch4 is -- Local Subprograms -- ----------------------- + procedure Analyze_Concatenation_Operand (N : Node_Id); + -- Checks that concatenation operands are properly restricted in SPARK or + -- ALFA: each operand must be either a string literal, a static character + -- expression, or another concatenation. + procedure Analyze_Concatenation_Rest (N : Node_Id); -- Does the "rest" of the work of Analyze_Concatenation, after the left -- operand has been analyzed. See Analyze_Concatenation for details. @@ -369,6 +374,14 @@ package body Sem_Ch4 is C : Node_Id; begin + -- Allocator is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~allocator is not allowed", N); + end if; + + -- Proceed with analysis + -- Deal with allocator restrictions -- In accordance with H.4(7), the No_Allocators restriction only applies @@ -1344,6 +1357,7 @@ package body Sem_Ch4 is -- First analyze L ... Analyze_Expression (L); + Analyze_Concatenation_Operand (L); -- ... then walk NN back up until we reach N (where we started), calling -- Analyze_Concatenation_Rest along the way. @@ -1353,8 +1367,45 @@ package body Sem_Ch4 is exit when NN = N; NN := Parent (NN); end loop; + + if Formal_Verification_Mode + and then Etype (N) /= Standard_String + then + Error_Msg_F ("|~~result of concatenation should have type String", N); + end if; end Analyze_Concatenation; + ----------------------------------- + -- Analyze_Concatenation_Operand -- + ----------------------------------- + + -- Concatenation is restricted in SPARK or ALFA: each operand must be + -- either a string literal, a static character expression, or another + -- concatenation. N cannot be a concatenation here as Analyze_Concatenation + -- and Analyze_Concatenation_Rest call Analyze_Concatenation_Operand + -- separately on each final operand, past concatenation operations. + + procedure Analyze_Concatenation_Operand (N : Node_Id) is + begin + if Formal_Verification_Mode then + if Is_Character_Type (Etype (N)) then + if not Is_Static_Expression (N) then + Error_Msg_F ("|~~character operand for concatenation should be " + & "static", N); + end if; + elsif Is_String_Type (Etype (N)) then + if Nkind (N) /= N_String_Literal then + Error_Msg_F ("|~~string operand for concatenation should be " + & "a literal", N); + end if; + + -- Do not issue error on an operand that is neither a character nor + -- a string, as the error is issued in Analyze_Concatenation_Rest. + + end if; + end if; + end Analyze_Concatenation_Operand; + -------------------------------- -- Analyze_Concatenation_Rest -- -------------------------------- @@ -1373,6 +1424,7 @@ package body Sem_Ch4 is begin Analyze_Expression (R); + Analyze_Concatenation_Operand (R); -- If the entity is present, the node appears in an instance, and -- denotes a predefined concatenation operation. The resulting type is @@ -1467,6 +1519,14 @@ package body Sem_Ch4 is return; end if; + -- Conditional expression is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~conditional expression is not allowed", N); + end if; + + -- Proceed with analysis + Else_Expr := Next (Then_Expr); if Comes_From_Source (N) then @@ -1665,6 +1725,14 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Explicit_Dereference begin + -- Explicit dereference is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~explicit dereference is not allowed", N); + end if; + + -- Proceed with analysis + Analyze (P); Set_Etype (N, Any_Type); @@ -2542,6 +2610,14 @@ package body Sem_Ch4 is procedure Analyze_Null (N : Node_Id) is begin + -- Null is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~null is not allowed", N); + end if; + + -- Proceed with analysis + Set_Etype (N, Any_Access); end Analyze_Null; @@ -3226,6 +3302,14 @@ package body Sem_Ch4 is Iterator : Node_Id; begin + -- Quantified expression is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~quantified expression is not allowed", N); + end if; + + -- Proceed with analysis + Set_Etype (Ent, Standard_Void_Type); Set_Parent (Ent, N); @@ -4252,6 +4336,14 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Slice begin + -- Slice is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~slice is not allowed", N); + end if; + + -- Proceed with analysis + Analyze (P); Analyze (D); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index e572aa20791..1673e5365ca 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -808,7 +808,9 @@ package body Sem_Ch5 is begin -- Block statement is not allowed in SPARK or ALFA - if Formal_Verification_Mode then + if Formal_Verification_Mode + and then Comes_From_Source (N) + then Error_Msg_F ("|~~block statement is not allowed", N); end if; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 213f55addb9..992222198d7 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1851,25 +1851,17 @@ package body Sem_Ch6 is if Formal_Verification_Mode then declare - Stat : Node_Id := Last (Statements (HSS)); + Stat : constant Node_Id := + Last_Source_Node_In_Sequence (Statements (HSS)); begin - while Present (Stat) loop - if Comes_From_Source (Stat) then - if not Nkind_In (Nkind (Stat), - N_Simple_Return_Statement, - N_Extended_Return_Statement) - then - Error_Msg_F ("|~~last statement in function " - & "should be RETURN", N); - end if; - exit; - end if; - - -- Reach before the generated statements at the end of - -- the function. - - Stat := Prev (Stat); - end loop; + if Present (Stat) + and then not Nkind_In (Nkind (Stat), + N_Simple_Return_Statement, + N_Extended_Return_Statement) + then + Error_Msg_F ("|~~last statement in function should " + & "be RETURN", Stat); + end if; end; elsif Return_Present (Id) then diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 59e96109388..11a31481aa2 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -455,7 +455,7 @@ package body Sem_Ch8 is -- private with on E. procedure Find_Expanded_Name (N : Node_Id); - -- The input is a selected component is known to be expanded name. Verify + -- The input is a selected component known to be an expanded name. Verify -- legality of selector given the scope denoted by prefix, and change node -- N into a expanded name with a properly set Entity field. @@ -526,6 +526,14 @@ package body Sem_Ch8 is Nam : constant Node_Id := Name (N); begin + -- Exception renaming is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~exception renaming is not allowed", N); + end if; + + -- Proceed with analysis + Enter_Name (Id); Analyze (Nam); @@ -617,6 +625,14 @@ package body Sem_Ch8 is Inst : Boolean := False; -- prevent junk warning begin + -- Generic renaming is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~generic renaming is not allowed", N); + end if; + + -- Proceed with analysis + if Name (N) = Error then return; end if; @@ -707,6 +723,14 @@ package body Sem_Ch8 is -- Start of processing for Analyze_Object_Renaming begin + -- Object renaming is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~object renaming is not allowed", N); + end if; + + -- Proceed with analysis + if Nam = Error then return; end if; @@ -2540,6 +2564,15 @@ package body Sem_Ch8 is -- Start of processing for Analyze_Use_Package begin + -- Use package is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Error_Msg_F ("|~~use clause is not allowed", N); + return; + end if; + + -- Proceed with analysis + Set_Hidden_By_Use_Clause (N, No_Elist); -- Use clause is not allowed in a spec of a predefined package @@ -5468,6 +5501,18 @@ package body Sem_Ch8 is elsif Is_Entity_Name (P) then P_Name := Entity (P); + -- Selector name is restricted in SPARK + + if SPARK_Mode then + if Is_Subprogram (P_Name) then + Error_Msg_F + ("|~~prefix of expanded name cannot be a subprogram", P); + elsif Ekind (P_Name) = E_Loop then + Error_Msg_F + ("|~~prefix of expanded name cannot be a loop statement", P); + end if; + end if; + -- The prefix may denote an enclosing type which is the completion -- of an incomplete type declaration. diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 523f62167a6..0fb1ae6f342 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -104,7 +104,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~abort statement is not allowed", N); - return; end if; -- Proceed with analysis @@ -182,7 +181,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~accept statement is not allowed", N); - return; end if; -- Proceed with analysis @@ -421,7 +419,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~select statement is not allowed", N); - return; end if; -- Proceed with analysis @@ -475,7 +472,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~select statement is not allowed", N); - return; end if; -- Proceed with analysis @@ -580,7 +576,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~delay statement is not allowed", N); - return; end if; -- Proceed with analysis @@ -606,7 +601,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~delay statement is not allowed", N); - return; end if; -- Proceed with analysis @@ -901,7 +895,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~entry call is not allowed", N); - return; end if; -- Proceed with analysis @@ -1360,7 +1353,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~requeue statement is not allowed", N); - return; end if; -- Proceed with analysis @@ -1642,7 +1634,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~select statement is not allowed", N); - return; end if; -- Proceed with analysis @@ -2179,7 +2170,6 @@ package body Sem_Ch9 is if Formal_Verification_Mode then Error_Msg_F ("|~~select statement is not allowed", N); - return; end if; -- Proceed with analysis diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 45e4a4f202c..e93a2997091 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -7981,6 +7981,24 @@ package body Sem_Util is end case; end Known_To_Be_Assigned; + ---------------------------------- + -- Last_Source_Node_In_Sequence -- + ---------------------------------- + + function Last_Source_Node_In_Sequence (List : List_Id) return Node_Id is + N : Node_Id := Last (List); + begin + while Present (N) loop + exit when Comes_From_Source (N); + + -- Reach before the generated statements at the end of the function + + N := Prev (N); + end loop; + + return N; + end Last_Source_Node_In_Sequence; + ------------------- -- May_Be_Lvalue -- ------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index df74a1f5689..29594393d2f 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -927,6 +927,10 @@ package Sem_Util is -- direction. Cases which may possibly be assignments but are not known to -- be may return True from May_Be_Lvalue, but False from this function. + function Last_Source_Node_In_Sequence (List : List_Id) return Node_Id; + -- Returns the last node in List for which Comes_From_Source returns True, + -- if any, or Empty otherwise. + function Make_Simple_Return_Statement (Sloc : Source_Ptr; Expression : Node_Id := Empty) return Node_Id diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 57129f99b6e..fb8f203f7ec 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -6939,7 +6939,7 @@ package Sinfo is -- This node is created by the analyzer/expander to handle some -- expansion cases, notably short circuit forms where there are - -- actions associated with the right hand operand. + -- actions associated with the right-hand side operand. -- The N_Expression_With_Actions node represents an expression with -- an associated set of actions (which are executable statements and @@ -6953,8 +6953,8 @@ package Sinfo is -- executing all the actions. -- Note: if the actions contain declarations, then these declarations - -- maybe referenced with in the expression. It is thus appropriate for - -- the back end to create a scope that encompasses the construct (any + -- may be referenced within the expression. It is thus appropriate for + -- the back-end to create a scope that encompasses the construct (any -- declarations within the actions will definitely not be referenced -- once elaboration of the construct is completed). -- 2.30.2