r247299 - in /trunk/gcc/ada: ChangeLog a-cfdlli...

[charlet at gcc dot gnu dot org]

Author: charlet
Date: Thu Apr 27 09:28:25 2017
New Revision: 247299

URL: https://gcc.gnu.org/viewcvs?rev=247299&root=gcc&view=rev
Log:
2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_prag.adb, a-cofuse.adb, a-cofuse.ads, einfo.adb, sem_prag.adb,
	cstand.adb, par-prag.adb, a-cofuve.adb, a-cofuve.ads, a-cofuma.adb,
	a-cofuma.ads, a-cofuba.adb, a-cofuba.ads: Minor reformatting.

2017-04-27  Tristan Gingold  <gingold@adacore.com>

	* s-excmac-gcc.ads, s-excmac-gcc.adb,
	s-excmac-arm.ads, s-excmac-arm.adb (New_Occurrence): Rewrite it in
	Ada95.

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch7.adb (Establish_Transient_Scope): Rewrite
	the loop which detects potential enclosing transient scopes. The
	loop now terminates much earlier as transient scopes are bounded
	by packages and subprograms.

2017-04-27  Claire Dross  <dross@adacore.com>

	* a-cfdlli.adb, a-cfdlli.ads (=): Generic parameter removed to
	allow the use of regular equality over elements in contracts.
	(Cursor): Type is now public so that it can be used in
	model functions.
	(Formal_Model): Ghost package containing
	model functions that are used in subprogram contracts.
	(Current_To_Last): Removed, model functions should be used
	instead.
	(First_To_Previous): Removed, model functions should
	be used instead.
	(Strict_Equal): Removed, model functions
	should be used instead.
	(Append): Default parameter value
	replaced by new wrapper to allow more precise contracts.
	(Insert): Default parameter value replaced by new wrapper to
	allow more precise contracts.
	(Delete): Default parameter
	value replaced by new wrapper to allow more precise contracts.
	(Prepend): Default parameter value replaced by new wrapper to
	allow more precise contracts.
	(Delete_First): Default parameter
	value replaced by new wrapper to allow more precise contracts.
	(Delete_Last): Default parameter value replaced by new wrapper
	to allow more precise contracts.

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_spark.adb (Expand_SPARK): Perform specialized expansion
	for object declarations.
	(Expand_SPARK_N_Object_Declaration): New routine.
	* sem_elab.adb (Check_A_Call): Include calls to the
	Default_Initial_Condition procedure of a type under the SPARK
	elaboration checks umbrella.


Added:
    trunk/gcc/ada/s-excmac-arm.adb
    trunk/gcc/ada/s-excmac-gcc.adb
Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/a-cfdlli.adb
    trunk/gcc/ada/a-cfdlli.ads
    trunk/gcc/ada/a-cofuba.adb
    trunk/gcc/ada/a-cofuba.ads
    trunk/gcc/ada/a-cofuma.adb
    trunk/gcc/ada/a-cofuma.ads
    trunk/gcc/ada/a-cofuse.adb
    trunk/gcc/ada/a-cofuse.ads
    trunk/gcc/ada/a-cofuve.adb
    trunk/gcc/ada/a-cofuve.ads
    trunk/gcc/ada/cstand.adb
    trunk/gcc/ada/einfo.adb
    trunk/gcc/ada/exp_ch7.adb
    trunk/gcc/ada/exp_prag.adb
    trunk/gcc/ada/exp_spark.adb
    trunk/gcc/ada/par-prag.adb
    trunk/gcc/ada/s-excmac-arm.ads
    trunk/gcc/ada/s-excmac-gcc.ads
    trunk/gcc/ada/sem_elab.adb
    trunk/gcc/ada/sem_prag.adb