-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- 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- --
-- --
------------------------------------------------------------------------------
+with Aspects; use Aspects;
with Atree; use Atree;
with Casing; use Casing;
with Einfo; use Einfo;
package body Restrict is
Restricted_Profile_Result : Boolean := False;
- -- This switch memoizes the result of Restricted_Profile function
- -- calls for improved efficiency. Its setting is valid only if
- -- Restricted_Profile_Cached is True. Note that if this switch
- -- is ever set True, it need never be turned off again.
+ -- This switch memoizes the result of Restricted_Profile function calls for
+ -- improved efficiency. Valid only if Restricted_Profile_Cached is True.
+ -- Note: if this switch is ever set True, it is never turned off again.
Restricted_Profile_Cached : Boolean := False;
- -- This flag is set to True if the Restricted_Profile_Result
- -- contains the correct cached result of Restricted_Profile calls.
+ -- This flag is set to True if the Restricted_Profile_Result contains the
+ -- correct cached result of Restricted_Profile calls.
+
+ No_Specification_Of_Aspects : array (Aspect_Id) of Source_Ptr :=
+ (others => No_Location);
+ -- Entries in this array are set to point to a previously occuring pragma
+ -- that activates a No_Specification_Of_Aspect check.
+
+ No_Specification_Of_Aspect_Warning : array (Aspect_Id) of Boolean :=
+ (others => True);
+ -- An entry in this array is set False in reponse to a previous call to
+ -- Set_No_Speficiation_Of_Aspect for pragmas in the main unit that
+ -- specify Warning as False. Once set False, an entry is never reset.
+
+ No_Specification_Of_Aspect_Set : Boolean := False;
+ -- Set True if any entry of No_Specifcation_Of_Aspects has been set True.
+ -- Once set True, this is never turned off again.
-----------------------
-- Local Subprograms --
Check_Restriction (No_Elaboration_Code, N);
end Check_Elaboration_Code_Allowed;
- ------------------------------
- -- Check_Formal_Restriction --
- ------------------------------
+ -----------------------------
+ -- Check_SPARK_Restriction --
+ -----------------------------
- procedure Check_Formal_Restriction
+ procedure Check_SPARK_Restriction
(Msg : String;
N : Node_Id;
Force : Boolean := False)
Msg_Issued : Boolean;
Save_Error_Msg_Sloc : Source_Ptr;
begin
- if Force or else Comes_From_Source (N) then
+ if Force or else Comes_From_Source (Original_Node (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
if Msg_Issued then
Error_Msg_F ("\\| " & Msg, N);
- elsif SPARK_Mode then
- Error_Msg_F ("|~~" & Msg, N);
end if;
end if;
- end Check_Formal_Restriction;
+ end Check_SPARK_Restriction;
- procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id) is
+ procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id) is
Msg_Issued : Boolean;
Save_Error_Msg_Sloc : Source_Ptr;
begin
pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
- if Comes_From_Source (N) then
+ if Comes_From_Source (Original_Node (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
if Msg_Issued then
Error_Msg_F ("\\| " & Msg1, N);
Error_Msg_F (Msg2, N);
- elsif SPARK_Mode then
- Error_Msg_F ("|~~" & Msg1, N);
- Error_Msg_F (Msg2, N);
end if;
end if;
- end Check_Formal_Restriction;
+ end Check_SPARK_Restriction;
-----------------------------------------
-- Check_Implicit_Dynamic_Code_Allowed --
begin
Msg_Issued := False;
- -- In CodePeer mode, we do not want to check for any restriction, or set
- -- additional restrictions other than those already set in gnat1drv.adb
- -- so that we have consistency between each compilation.
+ -- In CodePeer and Alfa mode, we do not want to check for any
+ -- restriction, or set additional restrictions other than those already
+ -- set in gnat1drv.adb so that we have consistency between each
+ -- compilation.
- if CodePeer_Mode then
+ if CodePeer_Mode or Alfa_Mode then
return;
end if;
- -- In formal mode, issue an error for any use of class-wide, even if the
+ -- In SPARK mode, issue an error for any use of class-wide, even if the
-- No_Dispatch restriction is not set.
if R = No_Dispatch then
- Check_Formal_Restriction ("class-wide is not allowed", N);
+ Check_SPARK_Restriction ("class-wide is not allowed", N);
end if;
if UI_Is_In_Int_Range (V) then
-- Loop through entries in No_Dependence table to check each one in turn
- for J in No_Dependence.First .. No_Dependence.Last loop
- DU := No_Dependence.Table (J).Unit;
+ for J in No_Dependences.First .. No_Dependences.Last loop
+ DU := No_Dependences.Table (J).Unit;
if Same_Unit (U, DU) then
Error_Msg_Sloc := Sloc (DU);
Error_Msg_Node_1 := DU;
- if No_Dependence.Table (J).Warn then
+ if No_Dependences.Table (J).Warn then
Error_Msg
("?violation of restriction `No_Dependence '='> &`#",
Sloc (Err));
end loop;
end Check_Restriction_No_Dependence;
+ --------------------------------------------------
+ -- Check_Restriction_No_Specification_Of_Aspect --
+ --------------------------------------------------
+
+ procedure Check_Restriction_No_Specification_Of_Aspect (N : Node_Id) is
+ A_Id : Aspect_Id;
+ Id : Node_Id;
+
+ begin
+ -- Ignore call if no instances of this restriction set
+
+ if not No_Specification_Of_Aspect_Set then
+ return;
+ end if;
+
+ -- Ignore call if node N is not in the main source unit, since we only
+ -- give messages for . This avoids giving messages for aspects that are
+ -- specified in withed units.
+
+ if not In_Extended_Main_Source_Unit (N) then
+ return;
+ end if;
+
+ Id := Identifier (N);
+ A_Id := Get_Aspect_Id (Chars (Id));
+ pragma Assert (A_Id /= No_Aspect);
+
+ Error_Msg_Sloc := No_Specification_Of_Aspects (A_Id);
+
+ if Error_Msg_Sloc /= No_Location then
+ Error_Msg_Node_1 := Id;
+ Error_Msg_Warn := No_Specification_Of_Aspect_Warning (A_Id);
+ Error_Msg_N
+ ("<violation of restriction `No_Specification_Of_Aspect '='> &`#",
+ Id);
+ end if;
+ end Check_Restriction_No_Specification_Of_Aspect;
+
--------------------------------------
-- Check_Wide_Character_Restriction --
--------------------------------------
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 --
-------------------------------
procedure Id_Case (S : String; Quotes : Boolean := True);
-- Given a string S, case it according to current identifier casing,
- -- and store in Error_Msg_String. Then append `~` to the message buffer
- -- to output the string unchanged surrounded in quotes. The quotes are
- -- suppressed if Quotes = False.
+ -- except for SPARK (an acronym) which is set all upper case, and store
+ -- in Error_Msg_String. Then append `~` to the message buffer to output
+ -- the string unchanged surrounded in quotes. The quotes are suppressed
+ -- if Quotes = False.
--------------
-- Add_Char --
begin
Name_Buffer (1 .. S'Last) := S;
Name_Len := S'Length;
- Set_Casing (Identifier_Casing (Get_Source_File_Index (Sloc (N))));
+
+ if R = SPARK then
+ Set_All_Upper_Case;
+ else
+ Set_Casing (Identifier_Casing (Get_Source_File_Index (Sloc (N))));
+ end if;
+
Error_Msg_Strlen := Name_Len;
Error_Msg_String (1 .. Name_Len) := Name_Buffer (1 .. Name_Len);
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 --
------------------------------
begin
-- Loop to check for duplicate entry
- for J in No_Dependence.First .. No_Dependence.Last loop
+ for J in No_Dependences.First .. No_Dependences.Last loop
-- Case of entry already in table
- if Same_Unit (Unit, No_Dependence.Table (J).Unit) then
+ if Same_Unit (Unit, No_Dependences.Table (J).Unit) then
-- Error has precedence over warning
if not Warn then
- No_Dependence.Table (J).Warn := False;
+ No_Dependences.Table (J).Warn := False;
end if;
return;
-- Entry is not currently in table
- No_Dependence.Append ((Unit, Warn, Profile));
+ No_Dependences.Append ((Unit, Warn, Profile));
end Set_Restriction_No_Dependence;
+ ------------------------------------------------
+ -- Set_Restriction_No_Specification_Of_Aspect --
+ ------------------------------------------------
+
+ procedure Set_Restriction_No_Specification_Of_Aspect
+ (N : Node_Id;
+ Warning : Boolean)
+ is
+ A_Id : constant Aspect_Id := Get_Aspect_Id (Chars (N));
+ pragma Assert (A_Id /= No_Aspect);
+
+ begin
+ No_Specification_Of_Aspects (A_Id) := Sloc (N);
+
+ if Warning = False then
+ No_Specification_Of_Aspect_Warning (A_Id) := False;
+ end if;
+
+ No_Specification_Of_Aspect_Set := True;
+ end Set_Restriction_No_Specification_Of_Aspect;
+
----------------------------------
-- Suppress_Restriction_Message --
----------------------------------
OSDN Git Service
