diff options
Diffstat (limited to 'gcc/ada/restrict.ads')
| -rw-r--r-- | gcc/ada/restrict.ads | 53 |
1 files changed, 16 insertions, 37 deletions
diff --git a/gcc/ada/restrict.ads b/gcc/ada/restrict.ads index f54fb4b811a..19439731a37 100644 --- a/gcc/ada/restrict.ads +++ b/gcc/ada/restrict.ads @@ -101,9 +101,9 @@ package Restrict is (No_Unchecked_Deallocation, "a-uncdea"), (No_Unchecked_Deallocation, "unchdeal")); - -- The following map has True for all GNAT pragmas. It is used to - -- implement pragma Restrictions (No_Implementation_Restrictions) - -- (which is why this restriction itself is excluded from the list). + -- The following map has True for all GNAT-defined Restrictions. It is used + -- to implement pragma Restrictions (No_Implementation_Restrictions) (which + -- is why this restriction itself is excluded from the list). Implementation_Restriction : array (All_Restrictions) of Boolean := (Simple_Barriers => True, @@ -142,7 +142,7 @@ package Restrict is No_Wide_Characters => True, Static_Priorities => True, Static_Storage_Size => True, - SPARK => True, + SPARK_05 => True, others => False); -- The following table records entries made by Restrictions pragmas @@ -176,34 +176,6 @@ package Restrict is Table_Increment => 200, Table_Name => "Name_No_Dependences"); - ------------------------------- - -- SPARK Restriction Control -- - ------------------------------- - - -- SPARK HIDE directives allow the effect of the SPARK restriction to be - -- turned off for a specified region of code, and the following tables are - -- the data structures used to keep track of these regions. - - -- The table contains pairs of source locations, the first being the start - -- location for hidden region, and the second being the end location. - - -- Note that the start location is included in the hidden region, while - -- the end location is excluded from it. (It typically corresponds to the - -- next token during scanning.) - - type SPARK_Hide_Entry is record - Start : Source_Ptr; - Stop : Source_Ptr; - end record; - - package SPARK_Hides is new Table.Table ( - Table_Component_Type => SPARK_Hide_Entry, - Table_Index_Type => Natural, - Table_Low_Bound => 1, - Table_Initial => 100, - Table_Increment => 200, - Table_Name => "SPARK Hides"); - ----------------- -- Subprograms -- ----------------- @@ -282,10 +254,10 @@ package Restrict is (Msg : String; N : Node_Id; Force : Boolean := False); - -- Node N represents a construct not allowed in formal mode. If this is a - -- source node, or if the restriction is forced (Force = True), and the - -- SPARK restriction is set, then an error is issued on N. Msg is appended - -- to the restriction failure message. + -- Node N represents a construct not allowed in formal mode. If this is + -- a source node, or if the restriction is forced (Force = True), and + -- the SPARK_05 restriction is set, then an error is issued on N. Msg + -- is appended to the restriction failure message. procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id); -- Same as Check_SPARK_Restriction except there is a continuation message @@ -330,6 +302,11 @@ package Restrict is -- identifier, and if so returns the corresponding Restriction_Id value, -- otherwise returns Not_A_Restriction_Id. + function OK_No_Dependence_Unit_Name (N : Node_Id) return Boolean; + -- Used in checking No_Dependence argument of pragma Restrictions or + -- pragma Restrictions_Warning, or attribute Restriction_Set. Returns + -- True if N has the proper form for a unit name, False otherwise. + function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean; -- Determine if given location is covered by a hidden region range in the -- SPARK hides table. @@ -380,7 +357,9 @@ package Restrict is -- restrictions are set. procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr); - -- Insert a new hidden region range in the SPARK hides table + -- Insert a new hidden region range in the SPARK hides table. The effect + -- is to hide any SPARK violation messages which are in the range Loc1 to + -- Loc2-1 (i.e. Loc2 is the first location for reenabling checks). procedure Set_Profile_Restrictions (P : Profile_Name; |