===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -56,11 +56,28 @@
-- Error_Recovery : Cannot raise Error_Resync
function P_Handled_Sequence_Of_Statements return Node_Id is
- Handled_Stmt_Seq_Node : Node_Id;
+ Handled_Stmt_Seq_Node : Node_Id;
+ Seq_Is_Hidden_In_SPARK : Boolean;
+ Hidden_Region_Start : Source_Ptr;
begin
Handled_Stmt_Seq_Node :=
New_Node (N_Handled_Sequence_Of_Statements, Token_Ptr);
+
+ -- In SPARK, a HIDE directive can be placed at the beginning of a
+ -- package initialization, thus hiding the sequence of statements (and
+ -- possible exception handlers) from SPARK tool-set. No violation of the
+ -- SPARK restriction should be issued on nodes in a hidden part, which
+ -- is obtained by marking such hidden parts.
+
+ if Token = Tok_SPARK_Hide then
+ Seq_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Seq_Is_Hidden_In_SPARK := False;
+ end if;
+
Set_Statements
(Handled_Stmt_Seq_Node, P_Sequence_Of_Statements (SS_Extm_Sreq));
@@ -70,6 +87,10 @@
(Handled_Stmt_Seq_Node, Parse_Exception_Handlers);
end if;
+ if Seq_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
+
return Handled_Stmt_Seq_Node;
end P_Handled_Sequence_Of_Statements;
@@ -229,10 +250,26 @@
-- Error recovery: cannot raise Error_Resync
function Parse_Exception_Handlers return List_Id is
- Handler : Node_Id;
- Handlers_List : List_Id;
+ Handler : Node_Id;
+ Handlers_List : List_Id;
+ Handler_Is_Hidden_In_SPARK : Boolean;
+ Hidden_Region_Start : Source_Ptr;
begin
+ -- In SPARK, a HIDE directive can be placed at the beginning of a
+ -- sequence of exception handlers for a subprogram implementation, thus
+ -- hiding the exception handlers from SPARK tool-set. No violation of
+ -- the SPARK restriction should be issued on nodes in a hidden part,
+ -- which is obtained by marking such hidden parts.
+
+ if Token = Tok_SPARK_Hide then
+ Handler_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Handler_Is_Hidden_In_SPARK := False;
+ end if;
+
Handlers_List := New_List;
P_Pragmas_Opt (Handlers_List);
@@ -253,6 +290,10 @@
end loop;
end if;
+ if Handler_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
+
return Handlers_List;
end Parse_Exception_Handlers;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -184,7 +184,7 @@
Tok_Separate | Tok_EOF | Tok_Semicolon | Tok_Arrow |
Tok_Vertical_Bar | Tok_Dot_Dot | Tok_Project | Tok_Extends |
Tok_External | Tok_External_As_List | Tok_Comment |
- Tok_End_Of_Line | Tok_Special | No_Token =>
+ Tok_End_Of_Line | Tok_Special | Tok_SPARK_Hide | No_Token =>
System.CRC32.Update
(System.CRC32.CRC32 (Checksum),
@@ -249,7 +249,7 @@
Tok_Separate | Tok_EOF | Tok_Semicolon | Tok_Arrow |
Tok_Vertical_Bar | Tok_Dot_Dot | Tok_Project | Tok_Extends |
Tok_External | Tok_External_As_List | Tok_Comment |
- Tok_End_Of_Line | Tok_Special | No_Token =>
+ Tok_End_Of_Line | Tok_Special | Tok_SPARK_Hide | No_Token =>
System.CRC32.Update
(System.CRC32.CRC32 (Checksum),
@@ -1761,6 +1761,42 @@
Token := Tok_Comment;
return;
end if;
+
+ if Source (Start_Of_Comment) = '#' then
+ declare
+ Scan_SPARK_Ptr : Source_Ptr;
+
+ begin
+ Scan_SPARK_Ptr := Start_Of_Comment + 1;
+
+ -- Scan out blanks
+
+ while Source (Scan_SPARK_Ptr) = ' '
+ or else Source (Scan_SPARK_Ptr) = HT
+ loop
+ Scan_SPARK_Ptr := Scan_SPARK_Ptr + 1;
+ end loop;
+
+ -- Recognize HIDE directive. SPARK input cannot be
+ -- encoded as wide characters, so only deal with
+ -- lower/upper case.
+
+ if (Source (Scan_SPARK_Ptr) = 'h'
+ or else Source (Scan_SPARK_Ptr) = 'H')
+ and then (Source (Scan_SPARK_Ptr + 1) = 'i'
+ or else Source (Scan_SPARK_Ptr + 1) = 'I')
+ and then (Source (Scan_SPARK_Ptr + 2) = 'd'
+ or else Source (Scan_SPARK_Ptr + 2) = 'D')
+ and then (Source (Scan_SPARK_Ptr + 3) = 'e'
+ or else Source (Scan_SPARK_Ptr + 3) = 'E')
+ and then (Source (Scan_SPARK_Ptr + 4) = ' '
+ or else Source (Scan_SPARK_Ptr + 4) = HT)
+ then
+ Token := Tok_SPARK_Hide;
+ return;
+ end if;
+ end;
+ end if;
end if;
end Minus_Case;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -213,6 +213,9 @@
-- characters '#', '$', '?', '@', '`', '\', '^', '~', or '_'. The
-- character value itself is stored in Scans.Special_Character.
+ Tok_SPARK_Hide,
+ -- HIDE directive in SPARK
+
No_Token);
-- No_Token is used for initializing Token values to indicate that
-- no value has been set yet.
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -628,6 +628,9 @@
else
Scan_Body_Or_Expression_Function : declare
+ Body_Is_Hidden_In_SPARK : Boolean;
+ Hidden_Region_Start : Source_Ptr;
+
function Likely_Expression_Function return Boolean;
-- Returns True if we have a probable case of an expression
-- function omitting the parentheses, if so, returns True
@@ -770,7 +773,26 @@
Body_Node :=
New_Node (N_Subprogram_Body, Sloc (Specification_Node));
Set_Specification (Body_Node, Specification_Node);
+
+ -- In SPARK, a HIDE directive can be placed at the beginning
+ -- of a subprogram implementation, thus hiding the
+ -- subprogram body from SPARK tool-set. No violation of the
+ -- SPARK restriction should be issued on nodes in a hidden
+ -- part, which is obtained by marking such hidden parts.
+
+ if Token = Tok_SPARK_Hide then
+ Body_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Body_Is_Hidden_In_SPARK := False;
+ end if;
+
Parse_Decls_Begin_End (Body_Node);
+
+ if Body_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
end if;
return Body_Node;
===================================================================
@@ -119,6 +119,12 @@
begin
if Force or else Comes_From_Source (N) then
+ if Restriction_Check_Required (SPARK)
+ and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
+ then
+ return;
+ end if;
+
-- Since the call to Restriction_Msg from Check_Restriction may set
-- Error_Msg_Sloc to the location of the pragma restriction, save and
-- restore the previous value of the global variable around the call.
@@ -141,6 +147,12 @@
if Comes_From_Source (N) then
+ if Restriction_Check_Required (SPARK)
+ and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
+ then
+ return;
+ end if;
+
-- Since the call to Restriction_Msg from Check_Restriction may set
-- Error_Msg_Sloc to the location of the pragma restriction, save and
-- restore the previous value of the global variable around the call.
@@ -548,6 +560,25 @@
return Not_A_Restriction_Id;
end Get_Restriction_Id;
+ --------------------------------
+ -- Is_In_Hidden_Part_In_SPARK --
+ --------------------------------
+
+ function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean is
+ begin
+ -- Loop through table of hidden ranges
+
+ for J in SPARK_Hides.First .. SPARK_Hides.Last loop
+ if SPARK_Hides.Table (J).Start <= Loc
+ and then Loc <= SPARK_Hides.Table (J).Stop
+ then
+ return True;
+ end if;
+ end loop;
+
+ return False;
+ end Is_In_Hidden_Part_In_SPARK;
+
-------------------------------
-- No_Exception_Handlers_Set --
-------------------------------
@@ -841,6 +872,17 @@
end Same_Unit;
------------------------------
+ -- Set_Hidden_Part_In_SPARK --
+ ------------------------------
+
+ procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr) is
+ begin
+ SPARK_Hides.Increment_Last;
+ SPARK_Hides.Table (SPARK_Hides.Last).Start := Loc1;
+ SPARK_Hides.Table (SPARK_Hides.Last).Stop := Loc2;
+ end Set_Hidden_Part_In_SPARK;
+
+ ------------------------------
-- Set_Profile_Restrictions --
------------------------------
===================================================================
@@ -174,6 +174,30 @@
Table_Increment => 200,
Table_Name => "Name_No_Dependence");
+ -------------------------------
+ -- SPARK Restriction Control --
+ -------------------------------
+
+ -- SPARK HIDE directives allow turning off SPARK restriction 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.
+
+ 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 --
-----------------
@@ -289,6 +313,10 @@
-- identifier, and if so returns the corresponding Restriction_Id
-- value, otherwise returns Not_A_Restriction_Id.
+ 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.
+
function No_Exception_Handlers_Set return Boolean;
-- Test to see if current restrictions settings specify that no exception
-- handlers are present. This function is called by Gigi when it needs to
@@ -334,6 +362,9 @@
-- of individual Restrictions pragmas). Returns True only if all the
-- required restrictions are set.
+ procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr);
+ -- Insert a new hidden region range in the SPARK hides table
+
procedure Set_Profile_Restrictions
(P : Profile_Name;
N : Node_Id;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -110,6 +110,10 @@
-- Dummy node to attach aspect specifications to until we properly
-- figure out where they eventually belong.
+ Body_Is_Hidden_In_SPARK : Boolean;
+ Private_Part_Is_Hidden_In_SPARK : Boolean;
+ Hidden_Region_Start : Source_Ptr;
+
begin
Push_Scope_Stack;
Scope.Table (Scope.Last).Etyp := E_Name;
@@ -153,7 +157,26 @@
else
Package_Node := New_Node (N_Package_Body, Package_Sloc);
Set_Defining_Unit_Name (Package_Node, Name_Node);
+
+ -- In SPARK, a HIDE directive can be placed at the beginning of a
+ -- package implementation, thus hiding the package body from SPARK
+ -- tool-set. No violation of the SPARK restriction should be
+ -- issued on nodes in a hidden part, which is obtained by marking
+ -- such hidden parts.
+
+ if Token = Tok_SPARK_Hide then
+ Body_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Body_Is_Hidden_In_SPARK := False;
+ end if;
+
Parse_Decls_Begin_End (Package_Node);
+
+ if Body_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
end if;
-- Cases other than Package_Body
@@ -249,9 +272,28 @@
end if;
Scan; -- past PRIVATE
+
+ if Token = Tok_SPARK_Hide then
+ Private_Part_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Private_Part_Is_Hidden_In_SPARK := False;
+ end if;
+
Set_Private_Declarations
(Specification_Node, P_Basic_Declarative_Items);
+ -- In SPARK, a HIDE directive can be placed at the beginning
+ -- of a private part, thus hiding all declarations in the
+ -- private part from SPARK tool-set. No violation of the
+ -- SPARK restriction should be issued on nodes in a hidden
+ -- part, which is obtained by marking such hidden parts.
+
+ if Private_Part_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
+
-- Deal gracefully with multiple PRIVATE parts
while Token = Tok_Private loop