diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 31 | ||||
| -rw-r--r-- | gcc/ada/err_vars.ads | 2 | ||||
| -rw-r--r-- | gcc/ada/errout.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/errout.ads | 5 | ||||
| -rw-r--r-- | gcc/ada/gcc-interface/Make-lang.in | 12 | ||||
| -rw-r--r-- | gcc/ada/gcc-interface/Makefile.in | 76 | ||||
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 24 | ||||
| -rw-r--r-- | gcc/ada/gnat_rm.texi | 28 | ||||
| -rw-r--r-- | gcc/ada/opt.adb | 67 | ||||
| -rw-r--r-- | gcc/ada/opt.ads | 24 | ||||
| -rw-r--r-- | gcc/ada/par-prag.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/par.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_ch4.adb | 44 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 3 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 33 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 14 | ||||
| -rw-r--r-- | 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 <dewar@adacore.com> + + * 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 <miranda@adacore.com> * 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<g-enblsp-vms-ia64.adb \ - g-trasym.adb<g-trasym-vms-ia64.adb \ - s-asthan.adb<s-asthan-vms-ia64.adb \ - s-auxdec.adb<s-auxdec-vms-ia64.adb \ - s-osinte.adb<s-osinte-vms-ia64.adb \ - s-osinte.ads<s-osinte-vms-ia64.ads \ - s-vaflop.adb<s-vaflop-vms-ia64.adb \ - system.ads<system-vms-ia64.ads - - LIBGNAT_TARGET_PAIRS_AUX2 = \ - s-parame.ads<s-parame-vms-ia64.ads \ - $(ATOMICS_TARGET_PAIRS) - else - ifeq ($(strip $(filter-out alpha64 dec vms% openvms% alphavms%,$(targ))),) - LIBGNAT_TARGET_PAIRS_AUX1 = \ - g-enblsp.adb<g-enblsp-vms-alpha.adb \ - g-trasym.adb<g-trasym-vms-alpha.adb \ - s-asthan.adb<s-asthan-vms-alpha.adb \ - s-auxdec.adb<s-auxdec-vms-alpha.adb \ - s-osinte.adb<s-osinte-vms.adb \ - s-osinte.ads<s-osinte-vms.ads \ - s-traent.adb<s-traent-vms.adb \ - s-traent.ads<s-traent-vms.ads \ - s-vaflop.adb<s-vaflop-vms-alpha.adb \ - system.ads<system-vms_64.ads - - ifeq ($(strip $(filter-out express EXPRESS,$(THREAD_KIND))),) - LIBGNAT_TARGET_PAIRS_AUX2 = \ - s-parame.ads<s-parame-vms-restrict.ads - else - LIBGNAT_TARGET_PAIRS_AUX2 = \ - s-parame.ads<s-parame-vms-alpha.ads \ - $(ATOMICS_TARGET_PAIRS) - endif - endif - endif - LIBGNAT_TARGET_PAIRS = \ a-caldel.adb<a-caldel-vms.adb \ a-calend.adb<a-calend-vms.adb \ @@ -1543,11 +1504,6 @@ ifeq ($(strip $(filter-out alpha64 ia64 dec hp vms% openvms% alphavms%,$(targ))) g-socthi.ads<g-socthi-vms.ads \ g-socthi.adb<g-socthi-vms.adb \ g-stsifd.adb<g-stsifd-sockets.adb \ - i-c.ads<i-c-vms_64.ads \ - i-cstrin.ads<i-cstrin-vms_64.ads \ - i-cstrin.adb<i-cstrin-vms_64.adb \ - i-cpoint.ads<i-cpoint-vms_64.ads \ - i-cpoint.adb<i-cpoint-vms_64.adb \ i-cstrea.adb<i-cstrea-vms.adb \ memtrack.adb<memtrack-vms_64.adb \ s-auxdec.ads<s-auxdec-vms_64.ads \ @@ -1564,20 +1520,46 @@ ifeq ($(strip $(filter-out alpha64 ia64 dec hp vms% openvms% alphavms%,$(targ))) s-taspri.ads<s-taspri-vms.ads \ s-tpopsp.adb<s-tpopsp-posix-foreign.adb \ s-tpopde.adb<s-tpopde-vms.adb \ - s-tpopde.ads<s-tpopde-vms.ads \ - $(LIBGNAT_TARGET_PAIRS_AUX1) \ - $(LIBGNAT_TARGET_PAIRS_AUX2) + s-tpopde.ads<s-tpopde-vms.ads ifeq ($(strip $(filter-out ia64 hp vms% openvms%,$(targ))),) + LIBGNAT_TARGET_PAIRS += \ + g-enblsp.adb<g-enblsp-vms-ia64.adb \ + g-trasym.adb<g-trasym-vms-ia64.adb \ + s-asthan.adb<s-asthan-vms-ia64.adb \ + s-auxdec.adb<s-auxdec-vms-ia64.adb \ + s-osinte.adb<s-osinte-vms-ia64.adb \ + s-osinte.ads<s-osinte-vms-ia64.ads \ + s-vaflop.adb<s-vaflop-vms-ia64.adb \ + system.ads<system-vms-ia64.ads \ + s-parame.ads<s-parame-vms-ia64.ads \ + $(ATOMICS_TARGET_PAIRS) + TOOLS_TARGET_PAIRS= \ mlib-tgt-specific.adb<mlib-tgt-specific-vms-ia64.adb \ symbols.adb<symbols-vms.adb \ symbols-processing.adb<symbols-processing-vms-ia64.adb else + ifeq ($(strip $(filter-out alpha64 dec vms% openvms% alphavms%,$(targ))),) + LIBGNAT_TARGET_PAIRS += \ + g-enblsp.adb<g-enblsp-vms-alpha.adb \ + g-trasym.adb<g-trasym-vms-alpha.adb \ + s-asthan.adb<s-asthan-vms-alpha.adb \ + s-auxdec.adb<s-auxdec-vms-alpha.adb \ + s-osinte.adb<s-osinte-vms.adb \ + s-osinte.ads<s-osinte-vms.ads \ + s-traent.adb<s-traent-vms.adb \ + s-traent.ads<s-traent-vms.ads \ + s-vaflop.adb<s-vaflop-vms-alpha.adb \ + system.ads<system-vms_64.ads \ + s-parame.ads<s-parame-vms-alpha.ads \ + $(ATOMICS_TARGET_PAIRS) + TOOLS_TARGET_PAIRS= \ mlib-tgt-specific.adb<mlib-tgt-specific-vms-alpha.adb \ symbols.adb<symbols-vms.adb \ symbols-processing.adb<symbols-processing-vms-alpha.adb + endif endif adamsg.o: adamsg.msg diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 2bd24ad5431..06ab52cca99 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -389,6 +389,30 @@ procedure Gnat1drv is else Back_End_Handles_Limited_Types := False; end if; + + -- Set switches for formal verification modes + + if Debug_Flag_Dot_DD then + SPARK_Mode := True; + end if; + + if Debug_Flag_Dot_EE then + ALFA_Through_SPARK_Mode := True; + end if; + + if Debug_Flag_Dot_FF then + ALFA_Through_Why_Mode := True; + end if; + + ALFA_Mode := ALFA_Through_SPARK_Mode or ALFA_Through_Why_Mode; + + if ALFA_Mode then + Set_Error_Msg_Lang ("alfa"); + Formal_Verification_Mode := True; + elsif SPARK_Mode then + Set_Error_Msg_Lang ("spark"); + Formal_Verification_Mode := True; + end if; end Adjust_Global_Switches; -------------------- diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index acccd37665e..4849daab97c 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -192,6 +192,7 @@ Implementation Defined Pragmas * Pragma Source_File_Name:: * Pragma Source_File_Name_Project:: * Pragma Source_Reference:: +* Pragma SPARK_95:: * Pragma Static_Elaboration_Desired:: * Pragma Stream_Convert:: * Pragma Style_Checks:: @@ -818,6 +819,7 @@ consideration, the use of these pragmas should be minimized. * Pragma Source_File_Name:: * Pragma Source_File_Name_Project:: * Pragma Source_Reference:: +* Pragma SPARK_95:: * Pragma Static_Elaboration_Desired:: * Pragma Stream_Convert:: * Pragma Style_Checks:: @@ -4601,6 +4603,32 @@ The second argument must be a string literal, it cannot be a static string expression other than a string literal. This is because its value is needed for error messages issued by all phases of the compiler. +@node Pragma SPARK_95 +@unnumberedsec Pragma SPARK_95 +@findex SPARK_95 +@noindent +Syntax: +@smallexample @c ada +pragma SPARK_95; +@end smallexample + +@noindent +A configuration pragma that establishes SPARK 95 mode for the unit to which +it applies, regardless of the mode set by the command line switches. +In this mode, the compiler rejects constructs outside the SPARK 95 subset of +Ada, which provides a useful initial filter for those projects developed in +SPARK. Syntax and semantic error messages related to SPARK restrictions have +the form: + +@code{(spark) error message}. + +This is not a replacement for the semantic checks performed by the +SPARK Examiner tool, as the compiler only deals currently with code, +not at all with SPARK annotations, so it may well be the case that code which +passes the compiler in SPARK 95 mode is rejected by the SPARK Examiner, +e.g. due to the different visibility rules of the Examiner based on +@code{inherit} SPARK annotations. + @node Pragma Static_Elaboration_Desired @unnumberedsec Pragma Static_Elaboration_Desired @findex Static_Elaboration_Desired diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb index 1e7bf0f709e..0fea77d7447 100644 --- a/gcc/ada/opt.adb +++ b/gcc/ada/opt.adb @@ -29,7 +29,6 @@ -- -- ------------------------------------------------------------------------------ -with Debug; with Gnatvsn; use Gnatvsn; with System; use System; with Tree_IO; use Tree_IO; @@ -39,59 +38,6 @@ package body Opt is SU : constant := Storage_Unit; -- Shorthand for System.Storage_Unit - --------------- - -- ALFA_Mode -- - --------------- - - function ALFA_Mode return Boolean is - begin - return ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode; - end ALFA_Mode; - - ----------------------------- - -- ALFA_Through_SPARK_Mode -- - ----------------------------- - - function ALFA_Through_SPARK_Mode return Boolean is - begin - return Debug.Debug_Flag_Dot_EE; - end ALFA_Through_SPARK_Mode; - - --------------------------- - -- ALFA_Through_Why_Mode -- - --------------------------- - - function ALFA_Through_Why_Mode return Boolean is - begin - return Debug.Debug_Flag_Dot_FF; - end ALFA_Through_Why_Mode; - - --------------------- - -- Formal_Language -- - --------------------- - - function Formal_Language return String is - begin - pragma Assert (Formal_Verification_Mode); - if ALFA_Mode then - return "alfa"; - elsif SPARK_Mode then - return "spark"; - else - pragma Assert (False); - return ""; -- unreachable - end if; - end Formal_Language; - - ------------------------------ - -- Formal_Verification_Mode -- - ------------------------------ - - function Formal_Verification_Mode return Boolean is - begin - return ALFA_Mode or else SPARK_Mode; - end Formal_Verification_Mode; - ---------------------------------- -- Register_Opt_Config_Switches -- ---------------------------------- @@ -257,19 +203,6 @@ package body Opt is Short_Descriptors := Short_Descriptors_Config; end Set_Opt_Config_Switches; - ---------------- - -- SPARK_Mode -- - ---------------- - - function SPARK_Mode return Boolean is - begin - -- When dropping the debug flag in favor of a compiler option, - -- the option should implicitly set the SPARK_Version, so that this test - -- becomes simply SPARK_Version > 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; |