From 2933b16cf255cc606c6b29ee542d3eef6a063315 Mon Sep 17 00:00:00 2001 From: Robert Dewar Date: Mon, 1 Aug 2011 16:16:24 +0000 Subject: [PATCH] sem_util.ads, [...] (Last_Source_Statement): Replaces Last_Source_Node_In_Sequence. 2011-08-01 Robert Dewar * sem_util.ads, sem_util.adb, sem_ch6.adb (Last_Source_Statement): Replaces Last_Source_Node_In_Sequence. * err_vars.ads (Error_Msg_Lang): 16 is OK, don't need 4K * errout.adb (Set_Error_Msg_Lang): Takes arg with no parens, but stores parens and blank in string (this was inconsistently implemented). * errout.ads (Set_Error_Msg_Lang): Takes arg with no parens, but stores parens and blank in string (this was inconsistently implemented). * gnat1drv.adb (Set_Global_Switches): Set formal mode switches appropriately * opt.ads, opt.adb: Formal mode is now global switches, more consistent * par-prag.adb (Analyze_Pragma, case SPARK_95): Set opt switches appropriately and call Set_Error_Msg_Lang to set "spark" as language name. * par.adb: Remove unnecessary call to set formal language for errout * sem_prag.adb (P_Pragma, case SPARK_95): Set opt switches appropriately and call Set_Error_Msg_Lang to set "spark" as language name. * sem_ch4.adb (Analyze_Concatenation_Operand): remove procedure and calls to it, moved after resolution so that types are known * sem_res.adb (Resolve_Op_Concat): issue an error in formal mode if result of concatenation is not of type String (Resolve_Op_Concat_Arg): issue an error in formal mode if an operand of concatenation is not properly restricted * gnat_rm.texi: Add doc on pragma Spark_95. * gcc-interface/Makefile.in: Remove obsolete target pairs for Interfaces.C.* on VMS. Remove s-parame-vms-restrict.ads. * gcc-interface/Make-lang.in: Update dependencies. From-SVN: r177061 --- gcc/ada/ChangeLog | 31 ++++++++++++ gcc/ada/err_vars.ads | 2 +- gcc/ada/errout.adb | 7 ++- gcc/ada/errout.ads | 5 +- gcc/ada/gcc-interface/Make-lang.in | 12 ++--- gcc/ada/gcc-interface/Makefile.in | 76 ++++++++++++------------------ gcc/ada/gnat1drv.adb | 24 ++++++++++ gcc/ada/gnat_rm.texi | 28 +++++++++++ gcc/ada/opt.adb | 67 -------------------------- gcc/ada/opt.ads | 24 +++++----- gcc/ada/par-prag.adb | 8 ++-- gcc/ada/par.adb | 4 -- gcc/ada/sem_ch4.adb | 44 ----------------- gcc/ada/sem_ch6.adb | 3 +- gcc/ada/sem_prag.adb | 4 +- gcc/ada/sem_res.adb | 33 +++++++++++++ gcc/ada/sem_util.adb | 14 +++--- gcc/ada/sem_util.ads | 7 +-- 18 files changed, 191 insertions(+), 202 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b171ba0c213..9cfb1e2b753 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,34 @@ +2011-08-01 Robert Dewar + + * sem_util.ads, sem_util.adb, sem_ch6.adb (Last_Source_Statement): + Replaces Last_Source_Node_In_Sequence. + * err_vars.ads (Error_Msg_Lang): 16 is OK, don't need 4K + * errout.adb (Set_Error_Msg_Lang): Takes arg with no parens, but stores + parens and blank in string (this was inconsistently implemented). + * errout.ads + (Set_Error_Msg_Lang): Takes arg with no parens, but stores parens and + blank in string (this was inconsistently implemented). + * gnat1drv.adb + (Set_Global_Switches): Set formal mode switches appropriately + * opt.ads, opt.adb: Formal mode is now global switches, more consistent + * par-prag.adb + (Analyze_Pragma, case SPARK_95): Set opt switches appropriately and + call Set_Error_Msg_Lang to set "spark" as language name. + * par.adb: Remove unnecessary call to set formal language for errout + * sem_prag.adb (P_Pragma, case SPARK_95): Set opt switches + appropriately and call Set_Error_Msg_Lang to set "spark" as language + name. + * sem_ch4.adb (Analyze_Concatenation_Operand): remove procedure and + calls to it, moved after resolution so that types are known + * sem_res.adb (Resolve_Op_Concat): issue an error in formal mode if + result of concatenation is not of type String + (Resolve_Op_Concat_Arg): issue an error in formal mode if an operand of + concatenation is not properly restricted + * gnat_rm.texi: Add doc on pragma Spark_95. + * gcc-interface/Makefile.in: Remove obsolete target pairs for + Interfaces.C.* on VMS. Remove s-parame-vms-restrict.ads. + * gcc-interface/Make-lang.in: Update dependencies. + 2011-08-01 Javier Miranda * sem_disp.adb (Override_Dispatching_Operation): Enforce strictness of diff --git a/gcc/ada/err_vars.ads b/gcc/ada/err_vars.ads index 22f70f61251..2f1b048b398 100644 --- a/gcc/ada/err_vars.ads +++ b/gcc/ada/err_vars.ads @@ -150,7 +150,7 @@ package Err_Vars is -- Used if current message contains a ~ insertion character to indicate -- insertion of the string Error_Msg_String (1 .. Error_Msg_Strlen). - Error_Msg_Lang : String (1 .. 4096); + Error_Msg_Lang : String (1 .. 16); Error_Msg_Langlen : Natural; -- Used if current message contains a ~~ insertion character to indicate -- insertion of the string Error_Msg_Lang (1 .. Error_Msg_Langlen). diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index be963dbf952..59babb14581 100644 --- a/gcc/ada/errout.adb +++ b/gcc/ada/errout.adb @@ -2177,8 +2177,11 @@ package body Errout is procedure Set_Error_Msg_Lang (To : String) is begin - Error_Msg_Langlen := To'Length; - Error_Msg_Lang (1 .. Error_Msg_Langlen) := To; + Error_Msg_Lang (1) := '('; + Error_Msg_Lang (2 .. To'Length + 1) := To; + Error_Msg_Lang (To'Length + 2) := ')'; + Error_Msg_Lang (To'Length + 3) := ' '; + Error_Msg_Langlen := To'Length + 3; end Set_Error_Msg_Lang; ----------------------- diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads index 611ca02e0d0..57b8efe0abb 100644 --- a/gcc/ada/errout.ads +++ b/gcc/ada/errout.ads @@ -767,8 +767,9 @@ package Errout is -- on each element of the list, see above). procedure Set_Error_Msg_Lang (To : String); - -- Set Error_Msg_Lang and Error_Msg_Langlen used for insertion character ~~ - -- so that Error_Msg_Lang (1 .. Error_Msg_Langlen) = To. + -- Set Error_Msg_Lang/Error_Msg_Langlen used for insertion character ~~. + -- The argument is just the language name, e.g. "spark". The stored string + -- is of the form "(langname) ". procedure Set_Ignore_Errors (To : Boolean); -- Following a call to this procedure with To=True, all error calls are diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index 77d2b2eac97..c925db01cca 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -2817,12 +2817,12 @@ ada/nmake.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \ ada/urealp.ads ada/opt.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads ada/a-uncdea.ads \ - ada/gnatvsn.ads ada/hostparm.ads ada/opt.ads ada/opt.adb ada/system.ads \ - ada/s-exctab.ads ada/s-os_lib.ads ada/s-parame.ads ada/s-secsta.ads \ - ada/s-soflin.ads ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads \ - ada/s-stoele.adb ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads \ - ada/s-wchcon.ads ada/tree_io.ads ada/types.ads ada/unchconv.ads \ - ada/unchdeal.ads + ada/debug.ads ada/gnatvsn.ads ada/hostparm.ads ada/opt.ads ada/opt.adb \ + ada/system.ads ada/s-exctab.ads ada/s-os_lib.ads ada/s-parame.ads \ + ada/s-secsta.ads ada/s-soflin.ads ada/s-stache.ads ada/s-stalib.ads \ + ada/s-stoele.ads ada/s-stoele.adb ada/s-string.ads ada/s-traent.ads \ + ada/s-unstyp.ads ada/s-wchcon.ads ada/tree_io.ads ada/types.ads \ + ada/unchconv.ads ada/unchdeal.ads ada/osint-b.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \ ada/a-uncdea.ads ada/alloc.ads ada/debug.ads ada/hostparm.ads \ diff --git a/gcc/ada/gcc-interface/Makefile.in b/gcc/ada/gcc-interface/Makefile.in index 2616fea7b4d..580bbcdb460 100644 --- a/gcc/ada/gcc-interface/Makefile.in +++ b/gcc/ada/gcc-interface/Makefile.in @@ -1492,45 +1492,6 @@ LN_S = cp -p endif ifeq ($(strip $(filter-out alpha64 ia64 dec hp vms% openvms% alphavms%,$(targ))),) - ifeq ($(strip $(filter-out ia64 hp vms% openvms%,$(targ))),) - LIBGNAT_TARGET_PAIRS_AUX1 = \ - g-enblsp.adb SPARK_None. - - return Debug.Debug_Flag_Dot_DD or else SPARK_Version > SPARK_None; - end SPARK_Mode; - --------------- -- Tree_Read -- --------------- diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index ed6c53c43b4..32326ecd3c7 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1877,27 +1877,25 @@ package Opt is -- These modes are currently defined through debug flags - function Formal_Language return String; - -- Returns "alfa" in ALFA_Mode and "spark" in SPARK_Mode + Formal_Verification_Mode : Boolean := False; + -- Set True if ALFA_Mode or SPARK_Mode - function Formal_Verification_Mode return Boolean; - -- Shorthand for ALFA_Mode or else SPARK_Mode + ALFA_Mode : Boolean := False; + -- Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode - function ALFA_Mode return Boolean; - -- Shorthand for ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode - - function ALFA_Through_SPARK_Mode return Boolean; + ALFA_Through_SPARK_Mode : Boolean := False; -- Specific compiling mode targeting formal verification through -- the generation of SPARK code for those parts of the input code that - -- belong to the ALFA subset of Ada. It is set by the flag -gnatd.E. + -- belong to the ALFA subset of Ada. Set by debug flag -gnatd.E. - function ALFA_Through_Why_Mode return Boolean; + ALFA_Through_Why_Mode : Boolean := False; -- Specific compiling mode targeting formal verification through -- the generation of Why code for those parts of the input code that - -- belong to the ALFA subset of Ada. It is set by the flag -gnatd.F. + -- belong to the ALFA subset of Ada. Set by debuf flag -gnatd.F. - function SPARK_Mode return Boolean; - -- Accept the SPARK subset of Ada only. It is set by the flag -gnatd.D. + SPARK_Mode : Boolean := False; + -- Reject constructs not allowed by SPARK. Set by flag -gnatd.D or + -- by pragma SPARK_95. private diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 502cb70b253..93a5be90d83 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -893,13 +893,15 @@ begin -- SPARK_95 -- -------------- - -- This pragma must be processed at parse time, since we want to set - -- the SPARK version properly at parse time to recognize the appropriate + -- This pragma must be processed at parse time, since we want to set the + -- SPARK version properly at parse time to recognize the appropriate -- SPARK version syntax. when Pragma_SPARK_95 => SPARK_Version := SPARK_95; - Set_Error_Msg_Lang ("(" & Formal_Language & ") "); + SPARK_Mode := True; + Set_Error_Msg_Lang ("spark"); + Formal_Verification_Mode := True; ------------------------- -- Style_Checks (GNAT) -- diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb index b4c8d83e4dd..99f6806057d 100644 --- a/gcc/ada/par.adb +++ b/gcc/ada/par.adb @@ -1318,10 +1318,6 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is begin Compiler_State := Parsing; - if Formal_Verification_Mode then - Set_Error_Msg_Lang ("(" & Formal_Language & ") "); - end if; - -- Deal with configuration pragmas case first if Configuration_Pragmas then diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 23913612169..b5a8e18af01 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -67,11 +67,6 @@ 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. @@ -1357,7 +1352,6 @@ 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. @@ -1367,45 +1361,8 @@ 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 -- -------------------------------- @@ -1424,7 +1381,6 @@ 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 diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 84bb761e190..72a1529adb3 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1851,8 +1851,7 @@ package body Sem_Ch6 is if Formal_Verification_Mode then declare - Stat : constant Node_Id := - Last_Source_Node_In_Sequence (Statements (HSS)); + Stat : constant Node_Id := Last_Source_Statement (HSS); begin if Present (Stat) and then not Nkind_In (Stat, diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index f09f744ba8f..d2528acfc75 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -12334,7 +12334,9 @@ package body Sem_Prag is Check_Arg_Count (0); Check_Valid_Configuration_Pragma; SPARK_Version := SPARK_95; - Set_Error_Msg_Lang ("(" & Formal_Language & ") "); + SPARK_Mode := True; + Formal_Verification_Mode := True; + Set_Error_Msg_Lang ("spark"); -------------------------------- -- Static_Elaboration_Desired -- diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 2b44924825a..6cda48eb764 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7402,6 +7402,12 @@ package body Sem_Res is exit when NN = N; NN := Parent (NN); end loop; + + if Formal_Verification_Mode + and then Base_Type (Etype (N)) /= Standard_String + then + Error_Msg_F ("|~~result of concatenation should have type String", N); + end if; end Resolve_Op_Concat; --------------------------- @@ -7505,6 +7511,33 @@ package body Sem_Res is Resolve (Arg, Btyp); end if; + -- Concatenation is restricted in SPARK or ALFA: each operand must be + -- either a string literal, a static character expression, or another + -- concatenation. Arg cannot be a concatenation here as callers of + -- Resolve_Op_Concat_Arg call it separately on each final operand, past + -- concatenation operations. + + if Formal_Verification_Mode then + if Is_Character_Type (Etype (Arg)) then + if not Is_Static_Expression (Arg) then + Error_Msg_F ("|~~character operand for concatenation should be " + & "static", N); + end if; + + elsif Is_String_Type (Etype (Arg)) then + if Nkind (Arg) /= 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 Resolve_Op_Concat. + + else + null; + end if; + end if; + Check_Unset_Reference (Arg); end Resolve_Op_Concat_Arg; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 9a9b60e395a..f401f9441ae 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -7981,22 +7981,22 @@ package body Sem_Util is end case; end Known_To_Be_Assigned; - ---------------------------------- - -- Last_Source_Node_In_Sequence -- - ---------------------------------- + --------------------------- + -- Last_Source_Statement -- + --------------------------- - function Last_Source_Node_In_Sequence (List : List_Id) return Node_Id is + function Last_Source_Statement (HSS : Node_Id) return Node_Id is N : Node_Id; begin - N := Last (List); + N := Last (Statements (HSS)); while Present (N) loop exit when Comes_From_Source (N); - N := Prev (N); + Prev (N); end loop; return N; - end Last_Source_Node_In_Sequence; + end Last_Source_Statement; ------------------- -- May_Be_Lvalue -- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 29594393d2f..bb4e1c2bbbd 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -927,9 +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 Last_Source_Statement (HSS : Node_Id) return Node_Id; + -- HSS is a handled statement sequence. This function returns the last + -- statement in Statements (HSS) that has Comes_From_Source set. If no + -- such statement exists, Empty is returned. function Make_Simple_Return_Statement (Sloc : Source_Ptr; -- 2.30.2