diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ea3417e9e1b..e983e4c7f5c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,90 @@ +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);". + 2015-10-20 Steve Baird * pprint.adb: Code clean up. diff --git a/gcc/ada/a-conhel.adb b/gcc/ada/a-conhel.adb index f433250000a..de66a50397c 100644 --- a/gcc/ada/a-conhel.adb +++ b/gcc/ada/a-conhel.adb @@ -29,6 +29,8 @@ package body Ada.Containers.Helpers is package body Generic_Implementation is + pragma Annotate (CodePeer, Skip_Analysis); + use type SAC.Atomic_Unsigned; ------------ diff --git a/gcc/ada/a-disedf.ads b/gcc/ada/a-disedf.ads index f1a5f3c505b..4b28a6db333 100644 --- a/gcc/ada/a-disedf.ads +++ b/gcc/ada/a-disedf.ads @@ -45,6 +45,10 @@ package Ada.Dispatching.EDF is function Get_Deadline (T : Ada.Task_Identification.Task_Id := Ada.Task_Identification.Current_Task) - return Deadline; + return Deadline + with + SPARK_Mode, + Volatile_Function, + Global => Ada.Task_Identification.Tasking_State; end Ada.Dispatching.EDF; diff --git a/gcc/ada/a-exetim-default.ads b/gcc/ada/a-exetim-default.ads index 56429af4654..c1ccda5a694 100644 --- a/gcc/ada/a-exetim-default.ads +++ b/gcc/ada/a-exetim-default.ads @@ -36,7 +36,9 @@ with Ada.Task_Identification; with Ada.Real_Time; -package Ada.Execution_Time is +package Ada.Execution_Time with + SPARK_Mode +is type CPU_Time is private; @@ -48,7 +50,10 @@ package Ada.Execution_Time is function Clock (T : Ada.Task_Identification.Task_Id := Ada.Task_Identification.Current_Task) - return CPU_Time; + return CPU_Time + with + Volatile_Function, + Global => Ada.Real_Time.Clock_Time; function "+" (Left : CPU_Time; @@ -84,9 +89,12 @@ package Ada.Execution_Time is Interrupt_Clocks_Supported : constant Boolean := False; Separate_Interrupt_Clocks_Supported : constant Boolean := False; - function Clock_For_Interrupts return CPU_Time; + function Clock_For_Interrupts return CPU_Time with + Volatile_Function, + Global => Ada.Real_Time.Clock_Time; private + pragma SPARK_Mode (Off); type CPU_Time is new Ada.Real_Time.Time; diff --git a/gcc/ada/a-exetim-mingw.adb b/gcc/ada/a-exetim-mingw.adb index b6919f26875..44f4ac3b37c 100644 --- a/gcc/ada/a-exetim-mingw.adb +++ b/gcc/ada/a-exetim-mingw.adb @@ -39,7 +39,9 @@ with System.Task_Primitives.Operations; use System.Task_Primitives.Operations; with System.Tasking; use System.Tasking; with System.Win32; use System.Win32; -package body Ada.Execution_Time is +package body Ada.Execution_Time with + SPARK_Mode => Off +is --------- -- "+" -- diff --git a/gcc/ada/a-exetim-mingw.ads b/gcc/ada/a-exetim-mingw.ads index bc458f6700e..8dcd32018b3 100644 --- a/gcc/ada/a-exetim-mingw.ads +++ b/gcc/ada/a-exetim-mingw.ads @@ -38,7 +38,9 @@ with Ada.Task_Identification; with Ada.Real_Time; -package Ada.Execution_Time is +package Ada.Execution_Time with + SPARK_Mode +is type CPU_Time is private; @@ -50,7 +52,10 @@ package Ada.Execution_Time is function Clock (T : Ada.Task_Identification.Task_Id := Ada.Task_Identification.Current_Task) - return CPU_Time; + return CPU_Time + with + Volatile_Function, + Global => Ada.Real_Time.Clock_Time; function "+" (Left : CPU_Time; @@ -86,9 +91,12 @@ package Ada.Execution_Time is Interrupt_Clocks_Supported : constant Boolean := False; Separate_Interrupt_Clocks_Supported : constant Boolean := False; - function Clock_For_Interrupts return CPU_Time; + function Clock_For_Interrupts return CPU_Time with + Volatile_Function, + Global => Ada.Real_Time.Clock_Time; private + pragma SPARK_Mode (Off); type CPU_Time is new Ada.Real_Time.Time; diff --git a/gcc/ada/a-exetim.ads b/gcc/ada/a-exetim.ads index 2b0725058c6..54a9b41fe85 100644 --- a/gcc/ada/a-exetim.ads +++ b/gcc/ada/a-exetim.ads @@ -24,7 +24,9 @@ with Ada.Task_Identification; with Ada.Real_Time; -package Ada.Execution_Time is +package Ada.Execution_Time with + SPARK_Mode +is pragma Preelaborate; pragma Unimplemented_Unit; @@ -39,7 +41,10 @@ package Ada.Execution_Time is function Clock (T : Ada.Task_Identification.Task_Id := Ada.Task_Identification.Current_Task) - return CPU_Time; + return CPU_Time + with + Volatile_Function, + Global => Ada.Real_Time.Clock_Time; function "+" (Left : CPU_Time; @@ -75,9 +80,12 @@ package Ada.Execution_Time is Interrupt_Clocks_Supported : constant Boolean := False; Separate_Interrupt_Clocks_Supported : constant Boolean := False; - function Clock_For_Interrupts return CPU_Time; + function Clock_For_Interrupts return CPU_Time with + Volatile_Function, + Global => Ada.Real_Time.Clock_Time; private + pragma SPARK_Mode (Off); type CPU_Time is new Ada.Real_Time.Time; diff --git a/gcc/ada/a-extiin.ads b/gcc/ada/a-extiin.ads index 0105a4c88ff..8e8563dcdf1 100644 --- a/gcc/ada/a-extiin.ads +++ b/gcc/ada/a-extiin.ads @@ -14,12 +14,18 @@ ------------------------------------------------------------------------------ with Ada.Interrupts; +with Ada.Real_Time; -package Ada.Execution_Time.Interrupts is +package Ada.Execution_Time.Interrupts with + SPARK_Mode +is pragma Unimplemented_Unit; - function Clock (Interrupt : Ada.Interrupts.Interrupt_ID) return CPU_Time; + function Clock (Interrupt : Ada.Interrupts.Interrupt_ID) return CPU_Time + with + Volatile_Function, + Global => Ada.Real_Time.Clock_Time; function Supported (Interrupt : Ada.Interrupts.Interrupt_ID) return Boolean; diff --git a/gcc/ada/a-interr.ads b/gcc/ada/a-interr.ads index fede3bd8542..09a58687a32 100644 --- a/gcc/ada/a-interr.ads +++ b/gcc/ada/a-interr.ads @@ -34,6 +34,7 @@ ------------------------------------------------------------------------------ with System.Interrupts; +with Ada.Task_Identification; package Ada.Interrupts is @@ -41,25 +42,40 @@ package Ada.Interrupts is type Parameterless_Handler is access protected procedure; - function Is_Reserved (Interrupt : Interrupt_ID) return Boolean; + function Is_Reserved (Interrupt : Interrupt_ID) return Boolean with + SPARK_Mode, + Volatile_Function, + Global => Ada.Task_Identification.Tasking_State; - function Is_Attached (Interrupt : Interrupt_ID) return Boolean; + function Is_Attached (Interrupt : Interrupt_ID) return Boolean with + SPARK_Mode, + Volatile_Function, + Global => Ada.Task_Identification.Tasking_State; function Current_Handler - (Interrupt : Interrupt_ID) return Parameterless_Handler; + (Interrupt : Interrupt_ID) return Parameterless_Handler + with + SPARK_Mode => Off; procedure Attach_Handler (New_Handler : Parameterless_Handler; - Interrupt : Interrupt_ID); + Interrupt : Interrupt_ID) + with + SPARK_Mode => Off; procedure Exchange_Handler (Old_Handler : out Parameterless_Handler; New_Handler : Parameterless_Handler; - Interrupt : Interrupt_ID); + Interrupt : Interrupt_ID) + with + SPARK_Mode => Off; - procedure Detach_Handler (Interrupt : Interrupt_ID); + procedure Detach_Handler (Interrupt : Interrupt_ID) with + SPARK_Mode, + Global => (In_Out => Ada.Task_Identification.Tasking_State); - function Reference (Interrupt : Interrupt_ID) return System.Address; + function Reference (Interrupt : Interrupt_ID) return System.Address with + SPARK_Mode => Off; private pragma Inline (Is_Reserved); diff --git a/gcc/ada/a-reatim.adb b/gcc/ada/a-reatim.adb index 1b4d4d8605c..4bac97b889b 100644 --- a/gcc/ada/a-reatim.adb +++ b/gcc/ada/a-reatim.adb @@ -32,7 +32,9 @@ with System.Tasking; -package body Ada.Real_Time is +package body Ada.Real_Time with + SPARK_Mode => Off +is --------- -- "*" -- diff --git a/gcc/ada/a-reatim.ads b/gcc/ada/a-reatim.ads index 7abbeb843d2..ff73167d95d 100644 --- a/gcc/ada/a-reatim.ads +++ b/gcc/ada/a-reatim.ads @@ -36,7 +36,11 @@ with System.Task_Primitives.Operations; pragma Elaborate_All (System.Task_Primitives.Operations); -package Ada.Real_Time is +package Ada.Real_Time with + SPARK_Mode, + Abstract_State => (Clock_Time with External => (Async_Readers, + Async_Writers)) +is pragma Compile_Time_Error (Duration'Size /= 64, @@ -54,7 +58,9 @@ package Ada.Real_Time is Time_Span_Unit : constant Time_Span; Tick : constant Time_Span; - function Clock return Time; + function Clock return Time with + Volatile_Function, + Global => Clock_Time; function "+" (Left : Time; Right : Time_Span) return Time; function "+" (Left : Time_Span; Right : Time) return Time; @@ -107,6 +113,8 @@ package Ada.Real_Time is function Time_Of (SC : Seconds_Count; TS : Time_Span) return Time; private + pragma SPARK_Mode (Off); + -- Time and Time_Span are represented in 64-bit Duration value in -- nanoseconds. For example, 1 second and 1 nanosecond is represented -- as the stored integer 1_000_000_001. This is for the 64-bit Duration diff --git a/gcc/ada/a-sytaco.adb b/gcc/ada/a-sytaco.adb index 62bced2adec..ab7c9ad1629 100644 --- a/gcc/ada/a-sytaco.adb +++ b/gcc/ada/a-sytaco.adb @@ -34,7 +34,9 @@ with Ada.Exceptions; with System.Tasking; with System.Task_Primitives.Operations; -package body Ada.Synchronous_Task_Control is +package body Ada.Synchronous_Task_Control with + SPARK_Mode => Off +is ---------------- -- Initialize -- diff --git a/gcc/ada/a-sytaco.ads b/gcc/ada/a-sytaco.ads index a6bd84e1a2b..bf1ab8720c9 100644 --- a/gcc/ada/a-sytaco.ads +++ b/gcc/ada/a-sytaco.ads @@ -36,22 +36,37 @@ with System.Task_Primitives; with Ada.Finalization; +with Ada.Task_Identification; -package Ada.Synchronous_Task_Control is +package Ada.Synchronous_Task_Control with + SPARK_Mode +is pragma Preelaborate; -- In accordance with Ada 2005 AI-362 type Suspension_Object is limited private; - procedure Set_True (S : in out Suspension_Object); + procedure Set_True (S : in out Suspension_Object) with + Global => null, + Depends => (S => null, + null => S); - procedure Set_False (S : in out Suspension_Object); + procedure Set_False (S : in out Suspension_Object) with + Global => null, + Depends => (S => null, + null => S); - function Current_State (S : Suspension_Object) return Boolean; + function Current_State (S : Suspension_Object) return Boolean with + Volatile_Function, + Global => Ada.Task_Identification.Tasking_State; - procedure Suspend_Until_True (S : in out Suspension_Object); + procedure Suspend_Until_True (S : in out Suspension_Object) with + Global => null, + Depends => (S => null, + null => S); private + pragma SPARK_Mode (Off); procedure Initialize (S : in out Suspension_Object); -- Initialization for Suspension_Object diff --git a/gcc/ada/a-taside.adb b/gcc/ada/a-taside.adb index ac4473e4c1a..b916c7609a1 100644 --- a/gcc/ada/a-taside.adb +++ b/gcc/ada/a-taside.adb @@ -45,7 +45,9 @@ with System.Tasking.Utilities; pragma Warnings (On); -package body Ada.Task_Identification is +package body Ada.Task_Identification with + SPARK_Mode => Off +is use System.Parameters; diff --git a/gcc/ada/a-taside.ads b/gcc/ada/a-taside.ads index d736b0317d0..3a3df7c0d2d 100644 --- a/gcc/ada/a-taside.ads +++ b/gcc/ada/a-taside.ads @@ -36,7 +36,11 @@ with System; with System.Tasking; -package Ada.Task_Identification is +package Ada.Task_Identification with + SPARK_Mode, + Abstract_State => (Tasking_State with External => (Async_Readers, + Async_Writers)) +is pragma Preelaborate; -- In accordance with Ada 2005 AI-362 @@ -50,25 +54,35 @@ package Ada.Task_Identification is function Image (T : Task_Id) return String; - function Current_Task return Task_Id; + function Current_Task return Task_Id with + Volatile_Function, + Global => Tasking_State; pragma Inline (Current_Task); - function Environment_Task return Task_Id; + function Environment_Task return Task_Id with + SPARK_Mode => Off; pragma Inline (Environment_Task); procedure Abort_Task (T : Task_Id); pragma Inline (Abort_Task); -- Note: parameter is mode IN, not IN OUT, per AI-00101 - function Is_Terminated (T : Task_Id) return Boolean; + function Is_Terminated (T : Task_Id) return Boolean with + Volatile_Function, + Global => Tasking_State; pragma Inline (Is_Terminated); - function Is_Callable (T : Task_Id) return Boolean; + function Is_Callable (T : Task_Id) return Boolean with + Volatile_Function, + Global => Tasking_State; pragma Inline (Is_Callable); - function Activation_Is_Complete (T : Task_Id) return Boolean; + function Activation_Is_Complete (T : Task_Id) return Boolean with + Volatile_Function, + Global => Tasking_State; private + pragma SPARK_Mode (Off); type Task_Id is new System.Tasking.Task_Id; diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 870d7ffa79e..973bdde80f8 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -828,6 +828,7 @@ package body Atree is end case; Set_Chars (New_Ent, Chars (E)); + -- Set_Comes_From_Source (New_Ent, Comes_From_Source (E)); return New_Ent; end Copy_Entity; @@ -2905,6 +2906,16 @@ package body Atree is return List_Id (Nodes.Table (N + 4).Field7); end List25; + function List38 (N : Node_Id) return List_Id is + begin + return List_Id (Nodes.Table (N + 6).Field8); + end List38; + + function List39 (N : Node_Id) return List_Id is + begin + return List_Id (Nodes.Table (N + 6).Field9); + end List39; + function Elist1 (N : Node_Id) return Elist_Id is pragma Assert (N <= Nodes.Last); Value : constant Union_Id := Nodes.Table (N).Field1; @@ -5758,6 +5769,18 @@ package body Atree is Nodes.Table (N + 4).Field7 := Union_Id (Val); end Set_List25; + procedure Set_List38 (N : Node_Id; Val : List_Id) is + begin + pragma Assert (Nkind (N) in N_Entity); + Nodes.Table (N + 6).Field8 := Union_Id (Val); + end Set_List38; + + procedure Set_List39 (N : Node_Id; Val : List_Id) is + begin + pragma Assert (Nkind (N) in N_Entity); + Nodes.Table (N + 6).Field9 := Union_Id (Val); + end Set_List39; + procedure Set_Elist1 (N : Node_Id; Val : Elist_Id) is begin Nodes.Table (N).Field1 := Union_Id (Val); diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads index 155cde3d947..0b4d24531c7 100644 --- a/gcc/ada/atree.ads +++ b/gcc/ada/atree.ads @@ -1355,6 +1355,12 @@ package Atree is function List25 (N : Node_Id) return List_Id; pragma Inline (List25); + function List38 (N : Node_Id) return List_Id; + pragma Inline (List38); + + function List39 (N : Node_Id) return List_Id; + pragma Inline (List39); + function Elist1 (N : Node_Id) return Elist_Id; pragma Inline (Elist1); @@ -2706,6 +2712,12 @@ package Atree is procedure Set_List25 (N : Node_Id; Val : List_Id); pragma Inline (Set_List25); + procedure Set_List38 (N : Node_Id; Val : List_Id); + pragma Inline (Set_List38); + + procedure Set_List39 (N : Node_Id; Val : List_Id); + pragma Inline (Set_List39); + procedure Set_Elist1 (N : Node_Id; Val : Elist_Id); pragma Inline (Set_Elist1); diff --git a/gcc/ada/atree.h b/gcc/ada/atree.h index e296b8adb69..adb636a82e8 100644 --- a/gcc/ada/atree.h +++ b/gcc/ada/atree.h @@ -505,6 +505,8 @@ extern Node_Id Current_Error_Node; #define List10(N) Field10 (N) #define List14(N) Field14 (N) #define List25(N) Field25 (N) +#define List38(N) Field38 (N) +#define List39(N) Field39 (N) #define Elist1(N) Field1 (N) #define Elist2(N) Field2 (N) 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)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 58d3ba866f3..bea9dacf502 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -607,6 +607,17 @@ package Einfo is -- tables must be consulted to determine if there actually is an active -- Suppress or Unsuppress pragma that applies to the entity. +-- Class_Wide_Preconds (List38) +-- 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 (List39) +-- Ditto for class-wide postconditions. + -- Class_Wide_Type (Node9) -- Defined in all type entities. For a tagged type or subtype, returns -- the corresponding implicitly declared class-wide type. For a @@ -5844,6 +5855,8 @@ package Einfo is -- Contract (Node34) -- Import_Pragma (Node35) (non-generic case only) -- Anonymous_Master (Node36) (non-generic case only) + -- Class_Wide_Preconds (List38) + -- Class_Wide_Postconds (List39) -- Body_Needed_For_SAL (Flag40) -- Contains_Ignored_Ghost_Code (Flag279) -- Default_Expressions_Processed (Flag108) @@ -6151,6 +6164,8 @@ package Einfo is -- Contract (Node34) -- Import_Pragma (Node35) (non-generic case only) -- Anonymous_Master (Node36) (non-generic case only) + -- Class_Wide_Preconds (List38) + -- Class_Wide_Postconds (List39) -- Body_Needed_For_SAL (Flag40) -- Contains_Ignored_Ghost_Code (Flag279) -- Delay_Cleanups (Flag114) @@ -6675,6 +6690,8 @@ package Einfo is function Can_Never_Be_Null (Id : E) return B; function Can_Use_Internal_Rep (Id : E) return B; function Checks_May_Be_Suppressed (Id : E) return B; + function Class_Wide_Postconds (Id : E) return S; + function Class_Wide_Preconds (Id : E) return S; function Class_Wide_Type (Id : E) return E; function Cloned_Subtype (Id : E) return E; function Component_Alignment (Id : E) return C; @@ -7334,6 +7351,8 @@ package Einfo is procedure Set_Can_Never_Be_Null (Id : E; V : B := True); procedure Set_Can_Use_Internal_Rep (Id : E; V : B := True); procedure Set_Checks_May_Be_Suppressed (Id : E; V : B := True); + procedure Set_Class_Wide_Postconds (Id : E; V : S); + procedure Set_Class_Wide_Preconds (Id : E; V : S); procedure Set_Class_Wide_Type (Id : E; V : E); procedure Set_Cloned_Subtype (Id : E; V : E); procedure Set_Component_Alignment (Id : E; V : C); @@ -8111,6 +8130,8 @@ package Einfo is pragma Inline (Can_Never_Be_Null); pragma Inline (Can_Use_Internal_Rep); pragma Inline (Checks_May_Be_Suppressed); + pragma Inline (Class_Wide_Preconds); + pragma Inline (Class_Wide_Postconds); pragma Inline (Class_Wide_Type); pragma Inline (Cloned_Subtype); pragma Inline (Component_Bit_Offset); @@ -8615,6 +8636,8 @@ package Einfo is pragma Inline (Set_Can_Never_Be_Null); pragma Inline (Set_Can_Use_Internal_Rep); pragma Inline (Set_Checks_May_Be_Suppressed); + pragma Inline (Set_Class_Wide_Postconds); + pragma Inline (Set_Class_Wide_Preconds); pragma Inline (Set_Class_Wide_Type); pragma Inline (Set_Cloned_Subtype); pragma Inline (Set_Component_Bit_Offset); diff --git a/gcc/ada/prj-attr.adb b/gcc/ada/prj-attr.adb index 66de7c71601..791fe2113f9 100644 --- a/gcc/ada/prj-attr.adb +++ b/gcc/ada/prj-attr.adb @@ -389,6 +389,14 @@ package body Prj.Attr is "LVswitches#" & "LVexcluded_source_files#" & + -- package Prove + + "Pprove#" & + + -- package GnatTest + + "Pgnattest#" & + "#"; Initialized : Boolean := False;