When the SPARK restriction mode was set, check that a declaration of
unconstrained type is allowed only for constants of type string.
compiling above string_type.ad(s|b) with SPARK mode
gcc -c -gnat05 -gnatec=../spark.adc string_type.adb
the following output must yield:
string_type.adb:1:19: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:1:19: use clause is not allowed
string_type.adb:9:07: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:9:07: declaration of object of unconstrained type not allowed
string_type.adb:9:12: unconstrained subtype not allowed (need initialization)
string_type.adb:9:12: provide initial value or explicit array bounds
string_type.adb:10:07: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:10:07: declaration of object of unconstrained type not allowed
string_type.adb:10:22: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:10:22: attribute "Image" is not allowed
string_type.adb:10:22: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:10:22: initialization expression is not appropriate
string_type.adb:11:07: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:11:07: declaration of object of unconstrained type not allowed
string_type.adb:12:07: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:12:07: declaration of object of unconstrained type not allowed
string_type.adb:16:31: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:16:31: initialization expression is not appropriate
string_type.adb:17:07: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:17:07: declaration of object of unconstrained type not allowed
string_type.adb:17:22: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:17:22: attribute "Image" is not allowed
string_type.adb:17:22: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:17:22: initialization expression is not appropriate
string_type.adb:18:19: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:18:19: subtype mark required
string_type.adb:18:27: violation of restriction "SPARK" at ../spark.adc:1
string_type.adb:18:27: subtype mark required
string_type.ads:4:27: violation of restriction "SPARK" at ../spark.adc:1
string_type.ads:4:27: subtype mark required
package String_Type is
subtype Line_Index is Integer range 1 .. 100;
subtype Line1 is String(Line_Index);
subtype Line2 is String(Positive range 2 .. 100);
procedure String_Eq (My_Line : out String;
My_Line1 : out Line1;
My_Line2 : out Line2;
X : Integer);
end String_Type;
with Ada.Text_IO; use Ada.Text_IO;
package body String_Type is
--# main_program;
procedure String_Eq (My_Line : out String;
My_Line1 : out Line1;
My_Line2 : out Line2;
X : Integer )
is
S1 : String;
S2 : String := Integer'Image (X);
S3 : String := "abc";
S4 : String := "abc" & "def";
S5 : constant String := "abc";
S6 : constant String := "abc" & "def";
S7 : constant String := S5 & S6;
S8 : constant String := Get_Line;
S9 : String := Integer'Image (X);
Next_Line : String (1 .. 100);
Next_Line1 : Line1;
Next_Line2 : Line2;
begin
null;
end String_Eq;
end String_Type;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-09-05 Marc Sango <sa...@adacore.com>
* sem_ch3.adb (Analyze_Object_Declaration): Remove
the wrong test and add the correct test to detect the violation
of illegal use of unconstrained string type in SPARK mode.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 178537)
+++ sem_ch3.adb (working copy)
@@ -3267,6 +3267,16 @@
if Is_Indefinite_Subtype (T) then
+ -- In SPARK, a declaration of unconstrained type is allowed
+ -- only for constants of type string.
+
+ if Is_String_Type (T)
+ and then not Constant_Present (Original_Node (N)) then
+ Check_SPARK_Restriction
+ ("declaration of object of unconstrained type not allowed",
+ N);
+ end if;
+
-- Nothing to do in deferred constant case
if Constant_Present (N) and then No (E) then
@@ -3313,21 +3323,10 @@
-- Case of initialization present
else
- -- Check restrictions in Ada 83 and SPARK modes
+ -- Check restrictions in Ada 83
if not Constant_Present (N) then
- -- In SPARK, a declaration of unconstrained type is allowed
- -- only for constants of type string.
-
- -- Isn't following check the wrong way round???
-
- if Nkind (E) = N_String_Literal then
- Check_SPARK_Restriction
- ("declaration of object of unconstrained type not allowed",
- E);
- end if;
-
-- Unconstrained variables not allowed in Ada 83 mode
if Ada_Version = Ada_83
