This is the mail archive of the
gcc-cvs@gcc.gnu.org
mailing list for the GCC project.
r235113 - in /trunk/gcc/ada: ChangeLog a-calend...
- From: charlet at gcc dot gnu dot org
- To: gcc-cvs at gcc dot gnu dot org
- Date: Mon, 18 Apr 2016 10:17:17 -0000
- Subject: r235113 - in /trunk/gcc/ada: ChangeLog a-calend...
Author: charlet
Date: Mon Apr 18 10:17:17 2016
New Revision: 235113
URL: https://gcc.gnu.org/viewcvs?rev=235113&root=gcc&view=rev
Log:
2016-04-18 Ed Schonberg <schonberg@adacore.com>
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): In GNATprove
mode, collect inherited class-wide conditions to generate the
corresponding pragmas.
* sem_prag.ads (Build_Pragma_Check_Equivalent): Moved from contracts
* contracts.adb (Collect_Inherited_Class_Wide_Conditions): New
procedure for overriding subprograms, used to generate the pragmas
corresponding to an inherited class- wide pre- or postcondition.
* sem_prag.adb (Build_Pragma_Check_Equivalent): moved here
from contracts.adb (Replace_Condition_Entities): Subsidiary
Build_Pragma_Check_Equivalent, to implement the proper semantics
of inherited class-wide conditions, as given in AI12-0113.
(Process_Class_Wide_Condition): Removed.
(Collect_Inherited_Class_Wide_Conditions): Iterate over pragmas
in contract of subprogram, to collect inherited class-wide
conditions.
(Build_Pragma_Check_Equivalent): Moved to sem_prag.adb
2016-04-18 Yannick Moy <moy@adacore.com>
* a-calend.adb (Ada.Calendar): Mark package body as SPARK_Mode Off.
* a-calend.ads (Ada.Calendar): Mark package spec as
SPARK_Mode and add synchronous external abstract state Clock_Time.
Modified:
trunk/gcc/ada/ChangeLog
trunk/gcc/ada/a-calend.adb
trunk/gcc/ada/a-calend.ads
trunk/gcc/ada/contracts.adb
trunk/gcc/ada/sem_ch6.adb
trunk/gcc/ada/sem_prag.adb
trunk/gcc/ada/sem_prag.ads