[Ada] Detect illegal use of unconstrained string type in SPARK mode

[Arnaud Charlet <charlet at adacore dot com>]

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  <sango@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.

Attachment: difs
Description: Text document