Skip to content

R
riscv-gcc-1
Commit 2933b16c by Robert Dewar Committed by Arnaud Charlet
Options

sem_util.ads, [...] (Last_Source_Statement): Replaces Last_Source_Node_In_Sequence. 

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.

From-SVN: r177061
parent 05dbd302
Showing with 191 additions and 202 deletions
gcc/ada/ChangeLog
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
......
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).
......
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;
-----------------------
......
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
......
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 \
......
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
......
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;
--------------------
......
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
......
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 --
---------------
......
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
......
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) --
......
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
......
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
......
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,
......
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 --
......
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;
......
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 --
......
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;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment