[multiple changes]

2013-10-17  Yannick Moy  <moy@adacore.com>

	* sem_ch8.adb (Find_Direct_Name): Keep track of assignments for
	renamings in SPARK mode.

2013-10-17  Yannick Moy  <moy@adacore.com>

	* exp_spark.adb (Expand_SPARK): Remove special case for NOT IN
	operation.
	* sinfo.ads: Add special comment section to describe SPARK mode
	effect on tree.
	* exp_spark.ads: Remove comments, moved to sinfo.ads.

2013-10-17  Yannick Moy  <moy@adacore.com>

	* exp_ch3.adb (Expand_Freeze_Class_Wide_Type,
	Expand_Freeze_Class_Wide_Type, Expand_Freeze_Class_Wide_Type):
	Remove useless special cases.
	* exp_ch4.adb (Expand_Allocator_Expression, Expand_N_Allocator,
	Expand_N_Op_Expon): Remove useless special cases.
	* exp_ch6.adb (Is_Build_In_Place_Function_Call): Disable build-in-place
	in SPARK mode by testing Full_Expander_Active instead of
	Expander_Active.
	(Make_Build_In_Place_Call_In_Allocator): Remove useless special case.
	* exp_util.adb (Build_Allocate_Deallocate_Proc): Remove
	useless special case.
	* sem_eval.adb (Compile_Time_Known_Value): Remove special handling of
	deferred constant.

2013-10-17  Yannick Moy  <moy@adacore.com>

	* gnat_ugn.texi: Document -gnateT and target file format.

2013-10-17  Vincent Celier  <celier@adacore.com>

	* prep.adb (Check_Command_Line_Symbol_Definition): Is_A_String is
	always False, even when the value starts and ends with double quotes.

From-SVN: r203747

1 files changed, 0 insertions, 48 deletions

diff --git a/gcc/ada/exp_spark.ads b/gcc/ada/exp_spark.ads
index 726b69a..c422bc7 100644
--- a/gcc/ada/exp_spark.ads
+++ b/gcc/ada/exp_spark.ads
@@ -30,54 +30,6 @@
 
 --  Expand_SPARK is called directly by Expander.Expand.
 
---  SPARK expansion has three main objectives:
-
---    1. Perform limited expansion to explicit some Ada rules and constructs
---       (translate 'Old and 'Result, replace renamings by renamed, insert
---        conversions, expand actuals in calls to introduce temporaries, expand
---        generics instantiations)
-
---    2. Facilitate treatment for the formal verification back-end (fully
---       qualify names, expand set membership, compute data dependences)
-
---    3. Avoid the introduction of low-level code that is difficult to analyze
---       formally, as typically done in the full expansion for high-level
---       constructs (tasking, dispatching)
-
---  To fulfill objective 1, Expand_SPARK selectively expands some constructs.
-
---  To fulfill objective 2, the tree after SPARK expansion should be fully
---  analyzed semantically. In particular, all expression must have their proper
---  type, and semantic links should be set between tree nodes (partial to full
---  view, etc.) Some kinds of nodes should be either absent, or can be ignored
---  by the formal verification backend:
-
---      N_Object_Renaming_Declaration: can be ignored safely
---      N_Expression_Function:         absent (rewitten)
---      N_Expression_With_Actions:     absent (not generated)
-
---  SPARK cross-references are generated from the regular cross-references
---  (used for browsing and code understanding) and additional references
---  collected during semantic analysis, in particular on all
---  dereferences. These SPARK cross-references are output in a separate section
---  of ALI files, as described in spark_xrefs.adb. They are the basis for the
---  computation of data dependences in the formal verification backend. This
---  implies that all cross-references should be generated in this mode, even
---  those that would not make sense from a user point-of-view, and that
---  cross-references that do not lead to data dependences for subprograms can
---  be safely ignored.
-
---  To support the formal verification of units parameterized by data, the
---  value of deferred constants should not be considered as a compile-time
---  constant at program locations where the full view is not visible.
-
---  To fulfill objective 3, Expand_SPARK does not expand features that are not
---  formally analyzed (tasking), or for which formal analysis relies on the
---  source level representation (dispatching, aspects, pragmas). However, these
---  should be semantically analyzed, which sometimes requires the insertion of
---  semantic pre-analysis, for example for subprogram contracts and pragma
---  check/assert.
-
 with Types; use Types;
 
 package Exp_SPARK is