SPARK LRM was modified to allow the names of constants to occur as operands
of concatenation. The SPARK restriction has been updated to reflect this change.
The following now compiles quietly:
pragma Restrictions (SPARK);
procedure Concat is
subtype Small_Range is Positive range 1 .. 1;
subtype Small_String is String (Small_Range);
C : constant Character := 'c';
X : constant Small_String := Small_String'(others => C);
procedure Something (Arg : String) is
begin
null;
end Something;
begin
Something ("with" & X);
end Concat;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-03 Yannick Moy <m...@adacore.com>
* sem_res.adb
(Resolve_Op_Concat_Arg): do not issue a SPARK violation when argument of
concatenation is the name of a constant
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 177254)
+++ sem_res.adb (working copy)
@@ -7774,10 +7774,10 @@
end if;
-- Concatenation is restricted in SPARK: 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.
+ -- string literal, the name of a string constant, a static character or
+ -- string 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 Is_Character_Type (Etype (Arg)) then
if not Is_Static_Expression (Arg) then
@@ -7786,7 +7786,10 @@
end if;
elsif Is_String_Type (Etype (Arg)) then
- if not Is_Static_Expression (Arg) then
+ if not (Nkind_In (Arg, N_Identifier, N_Expanded_Name)
+ and then Is_Constant_Object (Entity (Arg)))
+ and then not Is_Static_Expression (Arg)
+ then
Check_SPARK_Restriction
("string operand for concatenation should be static", N);
end if;
