This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
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
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |