r206805 - in /trunk/gcc/ada: ChangeLog adabkend...

[charlet@gcc.gnu.org]

Author: charlet
Date: Mon Jan 20 13:44:07 2014
New Revision: 206805

URL: http://gcc.gnu.org/viewcvs?rev=206805&root=gcc&view=rev
Log:
2014-01-20  Yannick Moy  <moy@adacore.com>

	* adabkend.adb, ali-util.adb, errout.adb, exp_ch7.adb,
	* exp_dbug.adb, freeze.adb, lib-xref.adb, restrict.adb,
	* sem_attr.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb,
	* sem_prag.adb, sem_res.adb, sem_util.adb Rename SPARK_Mode into
	GNATprove_Mode.
	* sem_ch13.adb: Remove blank.
	* exp_spark.adb, exp_spark.ads (Expand_SPARK_Call): Only replace
	subprograms by alias for renamings, not for inherited primitive
	operations.
	* exp_util.adb (Expand_Subtype_From_Expr): Apply the expansion
	in GNATprove mode.
	(Remove_Side_Effects): Apply the removal in
	GNATprove mode, for the full analysis of expressions.
	* expander.adb (Expand): Call the light SPARK expansion in GNATprove
	mode.
	(Expander_Mode_Restore, Expander_Mode_Save_And_Set): Ignore
	save/restore actions for Expander_Active flag in GNATprove mode,
	similar to what is done in ASIS mode.
	* frontend.adb (Frontend): Generic bodies are instantiated in
	GNATprove mode.
	* gnat1drv.adb (Adjust_Global_Switches): Set operating
	mode to Check_Semantics in GNATprove mode, although a light
	expansion is still performed.
	(Gnat1drv): Set Back_End_Mode to
	Declarations_Only in GNATprove mode, and later on special case
	the GNATprove mode to continue analysis anyway.
	* lib-writ.adb (Write_ALI): Always generate ALI files in
	GNATprove mode.
	* opt.adb, opt.ads (Full_Expander_Active): Make it equivalent to
	Expander_Active.
	(SPARK_Mode): Renamed as GNATprove_Mode.
	* sem_aggr.adb (Aggregate_Constraint_Checks): Add checks in the
	tree in GNATprove_Mode.
	* sem_ch12.adb (Analyze_Package_Instantiation): Always instantiate
	body in GNATprove mode.
	(Need_Subprogram_Instance_Body): Always instantiate body in GNATprove
	mode.
	* sem_ch3.adb (Constrain_Index, Process_Range_Expr_In_Decl):
	Make sure side effects are removed in GNATprove mode.


Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/adabkend.adb
    trunk/gcc/ada/ali-util.adb
    trunk/gcc/ada/errout.adb
    trunk/gcc/ada/exp_ch7.adb
    trunk/gcc/ada/exp_dbug.adb
    trunk/gcc/ada/exp_spark.adb
    trunk/gcc/ada/exp_spark.ads
    trunk/gcc/ada/exp_util.adb
    trunk/gcc/ada/expander.adb
    trunk/gcc/ada/expander.ads
    trunk/gcc/ada/freeze.adb
    trunk/gcc/ada/frontend.adb
    trunk/gcc/ada/gnat1drv.adb
    trunk/gcc/ada/lib-writ.adb
    trunk/gcc/ada/lib-xref.adb
    trunk/gcc/ada/opt.adb
    trunk/gcc/ada/opt.ads
    trunk/gcc/ada/restrict.adb
    trunk/gcc/ada/sem_aggr.adb
    trunk/gcc/ada/sem_attr.adb
    trunk/gcc/ada/sem_ch12.adb
    trunk/gcc/ada/sem_ch13.adb
    trunk/gcc/ada/sem_ch3.adb
    trunk/gcc/ada/sem_ch4.adb
    trunk/gcc/ada/sem_ch5.adb
    trunk/gcc/ada/sem_ch6.adb
    trunk/gcc/ada/sem_ch8.adb
    trunk/gcc/ada/sem_prag.adb
    trunk/gcc/ada/sem_res.adb
    trunk/gcc/ada/sem_util.adb