From 79dd9ad2c6c2772f96d66ae63624b4bfbec604db Mon Sep 17 00:00:00 2001 From: charlet Date: Tue, 20 Oct 2015 12:24:52 +0000 Subject: 2015-10-20 Yannick Moy * a-sytaco.ads (Ada.Synchronous_Task_Control): Package now withs System.Task_Identification. The visible part of the spec has SPARK_Mode. The private part has pragma SPARK_Mode (Off). (Set_True): Added Global and Depends aspects (Set_False): Added Global and Depends aspects (Current_State): Added Volatile_Function aspect and added external state Ada.Task_Identification.Tasking_State as a Global input. (Suspend_Until_True): Added Global and Depends aspects * a-sytaco.adb (Ada.Synchronous_Task_Control): Package body has SPARK_Mode => Off * a-extiin.ads (Ada.Execution_Time.Interrupts): Package now withs Ada.Real_Time and has SPARK_Mode. (Clock): Added Volatile_Function aspect and added external state Ada.Real_Time.Clock_Time as a Global input. * a-reatim.ads (Ada.Real_Time): The visible part of the spec has SPARK_Mode. The private part has pragma SPARK_Mode (Off). The package declares external state Clock_Time with properties Async_Readers and Async_Writers. (Clock): Added Volatile_Function aspect and added external state Clock_Time as a Global input. * a-reatim.adb (Ada.Real_Time): Package body has SPARK_Mode => Off * a-exetim-default.ads, a-exetim-mingw.ads (Ada.Execution_Time): The visible part of the spec has SPARK_Mode. The private part has pragma SPARK_Mode (Off). (Clock): Added Volatile_Function aspect and added external state Clock_Time as a Global input. (Clock_For_Interrupts): Added Volatile_Function aspect and added external state Ada.Real_Time.Clock_Time as a Global input. * a-exetim-mingw.adb (Ada.Execution_Time): Package body has SPARK_Mode => Off * a-interr.ads (Ada.Interrupts): Package now withs Ada.Task_Identification (Is_Reserved): Added SPARK_Mode, Volatile_Function and external state Ada.Task_Identification.Tasking_State as a Global input. (Is_Attached): Added SPARK_Mode, Volatile_Function and external state Ada.Task_Identification.Tasking_State as a Global input. (Attach_Handler): Added SPARK_Mode => Off (Exchange_Handler): Added SPARK_Mode => Off (Detach_Handler): Added SPARK_Mode and external state Ada.Task_Identification.Tasking_State as a Global In_Out. (Reference): Added SPARK_Mode => Off * a-disedf.ads (Get_Deadline): Added SPARK_Mode, Volatile_Function and external state Ada.Task_Identification.Tasking_State as a Global input. * a-taside.ads (Ada.Task_Identification): The visible part of the spec has SPARK_Mode. The private part has pragma SPARK_Mode (Off). The package declares external state Tasking_State with properties Async_Readers and Async_Writers. (Current_Task): Added Volatile_Function aspect and added external state Tasking_State as a Global input. (Environment_Task): Added SPARK_Mode => Off (Is_Terminated): Added Volatile_Function aspect and added external state Tasking_State as a Global input. (Is_Callable): Added Volatile_Function aspect and added external state Tasking_State as a Global input. (Activation_Is_Complete): Added Volatile_Function aspect and added external state Tasking_State as a Global input. * a-taside.adb (Ada.Task_Identification): Package body has SPARK_Mode => Off. 2015-10-20 Ed Schonberg * atree.ads, atree.adb: Enable List38 and List39 on entities. * einfo.ads, einfo.adb (Class_Wide_Preconds) new attribute defined on subprograms. Holds the list of class-wide precondition functions inherited from ancestors. Each such function is an instantiation of the generic function generated from an explicit aspect specification for a class-wide precondition. A type is an ancestor of itself, and therefore a root type has such an instance on its own list. (Class_Wide_Postconds): ditto for postconditions. 2015-10-20 Vincent Celier * prj-attr.adb: Add packages Prove and GnatTest. 2015-10-20 Steve Baird * a-conhel.adb: Add an Annotate pragma to help suppress CodePeer's analysis of internals of container generic instances. This pragma has no other effect. * a-conhel.adb (Generic_Implementation) Add "pragma Annotate (CodePeer, Skip_Analysis);". git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@229070 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/einfo.adb | 30 ++++++++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) (limited to 'gcc/ada/einfo.adb') diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index c6a999893a8..dff2a2b7843 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -267,8 +267,10 @@ package body Einfo is -- Anonymous_Master Node36 - -- (unused) Node38 - -- (unused) Node39 + -- (Class_Wide_Preconds) List38 + + -- (Class_Wide_Postconds) List39 + -- (unused) Node40 -- (unused) Node41 @@ -842,6 +844,18 @@ package body Einfo is return Flag31 (Id); end Checks_May_Be_Suppressed; + function Class_Wide_Postconds (Id : E) return S is + begin + pragma Assert (Is_Subprogram (Id)); + return List39 (Id); + end Class_Wide_Postconds; + + function Class_Wide_Preconds (Id : E) return S is + begin + pragma Assert (Is_Subprogram (Id)); + return List38 (Id); + end Class_Wide_Preconds; + function Class_Wide_Type (Id : E) return E is begin pragma Assert (Is_Type (Id)); @@ -3732,6 +3746,18 @@ package body Einfo is Set_Flag31 (Id, V); end Set_Checks_May_Be_Suppressed; + procedure Set_Class_Wide_Preconds (Id : E; V : S) is + begin + pragma Assert (Is_Subprogram (Id)); + Set_List38 (Id, V); + end Set_Class_Wide_Preconds; + + procedure Set_Class_Wide_Postconds (Id : E; V : S) is + begin + pragma Assert (Is_Subprogram (Id)); + Set_List39 (Id, V); + end Set_Class_Wide_Postconds; + procedure Set_Class_Wide_Type (Id : E; V : E) is begin pragma Assert (Is_Type (Id)); -- cgit v1.2.1