OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes] 

2015-10-20  Yannick Moy  <moy@adacore.com>

	* 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  <schonberg@adacore.com>

	* 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  <celier@adacore.com>

	* prj-attr.adb: Add packages Prove and GnatTest.

2015-10-20  Steve Baird  <baird@adacore.com>

	* 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);".

From-SVN: r229070
This commit is contained in:
Arnaud Charlet 2015-10-20 14:24:52 +02:00
parent fb159eb789
commit 635ffc52d8
21 changed files with 316 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

87
gcc/ada/ChangeLog
View File

@ -1,3 +1,90 @@
2015-10-20 Yannick Moy <moy@adacore.com>
* 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 <schonberg@adacore.com>
* 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 <celier@adacore.com>
* prj-attr.adb: Add packages Prove and GnatTest.
2015-10-20 Steve Baird <baird@adacore.com>
* 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 <baird@adacore.com>
* pprint.adb: Code clean up.

2
gcc/ada/a-conhel.adb
View File

@ -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;
------------

6
gcc/ada/a-disedf.ads
View File

@ -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;

14
gcc/ada/a-exetim-default.ads
View File

@ -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;

4
gcc/ada/a-exetim-mingw.adb
View File

@ -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
---------
-- "+" --

14
gcc/ada/a-exetim-mingw.ads
View File

@ -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;

14
gcc/ada/a-exetim.ads
View File

@ -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;

10
gcc/ada/a-extiin.ads
View File

@ -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;

30
gcc/ada/a-interr.ads
View File

@ -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);

4
gcc/ada/a-reatim.adb
View File

@ -32,7 +32,9 @@
with System.Tasking;
package body Ada.Real_Time is
package body Ada.Real_Time with
SPARK_Mode => Off
is
---------
-- "*" --

12
gcc/ada/a-reatim.ads
View File

@ -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

4
gcc/ada/a-sytaco.adb
View File

@ -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 --

25
gcc/ada/a-sytaco.ads
View File

@ -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

4
gcc/ada/a-taside.adb
View File

@ -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;

26
gcc/ada/a-taside.ads
View File

@ -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;

23
gcc/ada/atree.adb
View File

@ -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);

12
gcc/ada/atree.ads
View File

@ -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);

2
gcc/ada/atree.h
View File

@ -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)

30
gcc/ada/einfo.adb
View File

@ -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));

23
gcc/ada/einfo.ads
View File

@ -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);

8
gcc/ada/prj-attr.adb
View File

@ -389,6 +389,14 @@ package body Prj.Attr is
"LVswitches#" &
"LVexcluded_source_files#" &
-- package Prove
"Pprove#" &
-- package GnatTest
"Pgnattest#" &
"#";
Initialized : Boolean := False;