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
