diff options
author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2011-08-02 15:21:19 +0000 |
---|---|---|
committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2011-08-02 15:21:19 +0000 |
commit | 6cb4b97331605fe09d8f160813c344e9edcc8f99 (patch) | |
tree | cdbed559d62d3196ef10ffa5c397108b184f5e08 /gcc/ada/restrict.adb | |
parent | 3f40ab54c7204c97414c98730ee3b90c725c3f83 (diff) | |
download | gcc-6cb4b97331605fe09d8f160813c344e9edcc8f99.tar.gz |
2011-08-02 Sergey Rybin <rybin@adacore.com>
* gnat_rm.texi: Ramification of pragma Eliminate documentation
- fix bugs in the description of Source_Trace;
- get rid of UNIT_NAME;
2011-08-02 Javier Miranda <miranda@adacore.com>
* exp_ch9.adb
(Build_Dispatching_Requeue): Adding support for VM targets
since we cannot directly reference the Tag entity.
* exp_sel.adb (Build_K): Adding support for VM targets.
(Build_S_Assignment): Adding support for VM targets.
* exp_disp.adb
(Default_Prim_Op_Position): In VM targets do not restrict availability
of predefined interface primitives to compiling in Ada 2005 mode.
(Is_Predefined_Interface_Primitive): In VM targets this service is not
restricted to compiling in Ada 2005 mode.
(Make_VM_TSD): Generate code that declares and initializes the OSD
record. Needed to support dispatching calls through synchronized
interfaces.
* exp_ch3.adb
(Make_Predefined_Primitive_Specs): Enable generation of predefined
primitives associated with synchronized interfaces.
(Make_Predefined_Primitive_Bodies): Enable generation of predefined
primitives associated with synchronized interfaces.
2011-08-02 Yannick Moy <moy@adacore.com>
* par-ch11.adb (P_Handled_Sequence_Of_Statements): mark a sequence of
statements hidden in SPARK if preceded by the HIDE directive
(Parse_Exception_Handlers): mark each exception handler in a sequence of
exception handlers as hidden in SPARK if preceded by the HIDE directive
* par-ch6.adb (P_Subprogram): mark a subprogram body hidden in SPARK
if starting with the HIDE directive
* par-ch7.adb (P_Package): mark a package body hidden in SPARK if
starting with the HIDE directive; mark the declarations in a private
part as hidden in SPARK if the private part starts with the HIDE
directive
* restrict.adb, restrict.ads
(Set_Hidden_Part_In_SPARK): record a range of slocs as hidden in SPARK
(Is_In_Hidden_Part_In_SPARK): new function which returns whether its
argument node belongs to a part which is hidden in SPARK
(Check_SPARK_Restriction): do not issue violations on nodes in hidden
parts in SPARK; protect the possibly costly call to
Is_In_Hidden_Part_In_SPARK by a check that the SPARK restriction is on
* scans.ads (Token_Type): new value Tok_SPARK_Hide in enumeration
* scng.adb (Accumulate_Token_Checksum_GNAT_6_3,
Accumulate_Token_Checksum_GNAT_5_03): add case for new token
Tok_SPARK_Hide.
(Scan): recognize special comment starting with '#' and followed by
SPARK keyword "hide" as a HIDE directive.
2011-08-02 Yannick Moy <moy@adacore.com>
* types.ads, erroutc.ads: Minor reformatting.
2011-08-02 Vincent Celier <celier@adacore.com>
* link.c: Add response file support for cross platforms.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177179 138bc75d-0d04-0410-961f-82ee72b054a4
Diffstat (limited to 'gcc/ada/restrict.adb')
-rw-r--r-- | gcc/ada/restrict.adb | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index b37a593b8be..e12dd6396b5 100644 --- a/gcc/ada/restrict.adb +++ b/gcc/ada/restrict.adb @@ -119,6 +119,12 @@ package body Restrict is 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 @@ package body Restrict is 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 @@ package body Restrict is 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 @@ package body Restrict is 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 -- ------------------------------ |