From 579847c27262b011e96575c8ac74d0aa118152f0 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 21 Jan 2014 13:02:54 +0100 Subject: [multiple changes] 2014-01-21 Robert Dewar * exp_aggr.adb: Minor reformatting. 2014-01-21 Johannes Kanig * gnat1drv.adb (Gnat1drv) remove obsolete reference to -gnatd.H. 2014-01-21 Bob Duff * gnat_ugn.texi: Document the "checks" attribute in gnat2xml. 2014-01-21 Steve Baird * gnat_rm.texi: Improve description of SPARK_Mode pragma. 2014-01-21 Vincent Celier * prj-part.adb (Parse_Single_Project): Accept to extend a project if it has only be imported by an project being extended. When a project that has only been imported by a project being extended is imported by another project that is not being extended, reset the previous indication, so that it will be an error if this project is extended later. * prj-tree.adb (Create_Project): Include component From_Extended in table Projects_HT * prj-tree.ads (Project_Name_And_Node): New Boolean component From_Extended 2014-01-21 Robert Dewar * atree.ads, atree.adb: Add Node33 and Set_Node33. * einfo.ads, einfo.adb (SPARK_Pragma): New field (SPARK_Aux_Pragma): New field (SPARK_Pragma_Inherited): New flag (SPARK_Aux_Pragma_Inherited): New flag (SPARK_Mode_Pragmas): Removed. * lib.ads, lib.adb: Remove SPARK_Mode_Pragma, no longer used. * opt.ads (SPARK_Mode_Pragma): New global variable. * sem.ads: Add Save_SPARK_Mode_Pragma field to Scope_Stack_Entry. * sem_ch3.adb: Use new SPARK_Mode data structures. * sem_ch6.adb: Set SPARK_Mode fields in subprogram specs and bodies. * sem_ch7.adb: Set SPARK_Mode fields in package spec and body entities. * sem_ch8.adb (Push_Scope): Save SPARK_Mode_Pragma. (Pop_Scope): Restore SPARK_Mode_Pragma. * sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Rewrite for new data structures. 2014-01-21 Arnaud Charlet * back_end.adb: Undo previous change, not needed. Minor reformatting. From-SVN: r206879 --- gcc/ada/lib.ads | 8 -------- 1 file changed, 8 deletions(-) (limited to 'gcc/ada/lib.ads') diff --git a/gcc/ada/lib.ads b/gcc/ada/lib.ads index 5370e4a..00959cd 100644 --- a/gcc/ada/lib.ads +++ b/gcc/ada/lib.ads @@ -371,10 +371,6 @@ package Lib is -- Set when the entry is created by a call to Lib.Load and then cannot -- be changed. - -- SPARK_Mode_Pragma - -- Pointer to the configuration pragma SPARK_Mode that applies to the - -- whole unit. Add note of what this is used for ??? - -- Unit_File_Name -- The name of the source file containing the unit. Set when the entry -- is created by a call to Lib.Load, and then cannot be changed. @@ -426,7 +422,6 @@ package Lib is function Munit_Index (U : Unit_Number_Type) return Nat; function OA_Setting (U : Unit_Number_Type) return Character; function Source_Index (U : Unit_Number_Type) return Source_File_Index; - function SPARK_Mode_Pragma (U : Unit_Number_Type) return Node_Id; function Unit_File_Name (U : Unit_Number_Type) return File_Name_Type; function Unit_Name (U : Unit_Number_Type) return Unit_Name_Type; -- Get value of named field from given units table entry @@ -445,7 +440,6 @@ package Lib is procedure Set_Main_CPU (U : Unit_Number_Type; P : Int); procedure Set_Main_Priority (U : Unit_Number_Type; P : Int); procedure Set_OA_Setting (U : Unit_Number_Type; C : Character); - procedure Set_SPARK_Mode_Pragma (U : Unit_Number_Type; N : Node_Id); procedure Set_Unit_Name (U : Unit_Number_Type; N : Unit_Name_Type); -- Set value of named field for given units table entry. Note that we -- do not have an entry for each possible field, since some of the fields @@ -749,10 +743,8 @@ private pragma Inline (Set_Main_CPU); pragma Inline (Set_Main_Priority); pragma Inline (Set_OA_Setting); - pragma Inline (Set_SPARK_Mode_Pragma); pragma Inline (Set_Unit_Name); pragma Inline (Source_Index); - pragma Inline (SPARK_Mode_Pragma); pragma Inline (Unit_File_Name); pragma Inline (Unit_Name); -- cgit v1.1