+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.
package body Generic_Implementation is
+ pragma Annotate (CodePeer, Skip_Analysis);
+
use type SAC.Atomic_Unsigned;
------------
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;
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;
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;
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;
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
---------
-- "+" --
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;
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;
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;
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;
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;
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;
------------------------------------------------------------------------------
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;
------------------------------------------------------------------------------
with System.Interrupts;
+with Ada.Task_Identification;
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);
with System.Tasking;
-package body Ada.Real_Time is
+package body Ada.Real_Time with
+ SPARK_Mode => Off
+is
---------
-- "*" --
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,
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;
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
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 --
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
pragma Warnings (On);
-package body Ada.Task_Identification is
+package body Ada.Task_Identification with
+ SPARK_Mode => Off
+is
use System.Parameters;
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
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;
end case;
Set_Chars (New_Ent, Chars (E));
+ -- Set_Comes_From_Source (New_Ent, Comes_From_Source (E));
return New_Ent;
end Copy_Entity;
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;
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);
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);
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);
#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)
-- Anonymous_Master Node36
- -- (unused) Node38
- -- (unused) Node39
+ -- (Class_Wide_Preconds) List38
+
+ -- (Class_Wide_Postconds) List39
+
-- (unused) Node40
-- (unused) Node41
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));
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));
-- 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
-- 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)
-- 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)
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;
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);
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);
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);
"LVswitches#" &
"LVexcluded_source_files#" &
+ -- package Prove
+
+ "Pprove#" &
+
+ -- package GnatTest
+
+ "Pgnattest#" &
+
"#";
Initialized : Boolean := False;
projects / gcc.git / commitdiff