diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2016-04-18 12:17:17 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2016-04-18 12:17:17 +0200 |
| commit | 539ca5ec98443a3140523337f1dc131fd709f17a (patch) | |
| tree | 207360cf2657a7089f40a548444d592842c182af /gcc/tree-chkp-opt.c | |
| parent | fd22e260b5d48a245411c09858fa42b1614a89c7 (diff) | |
| download | gcc-539ca5ec98443a3140523337f1dc131fd709f17a.zip gcc-539ca5ec98443a3140523337f1dc131fd709f17a.tar.gz gcc-539ca5ec98443a3140523337f1dc131fd709f17a.tar.bz2 | |
[multiple changes]
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.
From-SVN: r235113
Diffstat (limited to 'gcc/tree-chkp-opt.c')
0 files changed, 0 insertions, 0 deletions