adabkend.adb, [...]: Everything with name 'Alfa' renamed in 'SPARK'.

2013-04-24  Yannick Moy  <moy@adacore.com>

	* adabkend.adb, ali-util.adb, ali.adb, debug.adb,
	errout.adb, errout.ads, erroutc.adb, exp_ch3.adb, exp_ch4.adb,
	exp_ch6.adb, exp_ch7.adb, exp_dbug.adb, exp_util.adb,
	expander.adb, freeze.adb, gnat1drv.adb, lib-writ.adb,
	lib-writ.ads, lib-xref.adb, lib-xref.ads, opt.adb, opt.ads,
	restrict.adb, sem_aggr.adb, sem_attr.adb, sem_ch3.adb,
	sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_eval.adb, sem_prag.adb,
	sem_res.adb, sem_util.adb: Everything with name
	'Alfa' renamed in 'SPARK'. Update comments.
	Renaming of units with name 'Alfa', renamed with 'SPARK' instead.
	* exp_alfa.adb: renamed exp_spark.adb.
	* exp_alfa.ads: renamed exp_spark.ads.
	* get_alfa.adb: renamed get_spark_xrefs.adb.
	* get_alfa.ads: renamed get_spark_xrefs.ads.
	* lib-xref-alfa.adb: renamed lib-xref-spark_specific.adb.
	* put_alfa.adb: renamed put_spark_xrefs.adb.
	* put_alfa.ads: renamed put_spark_xrefs.ads.
	* alfa.adb: renamed spark_xrefs.adb.
	* alfa.ads: renamed spark_xrefs.ads.
	* alfa_test.adb: renamed spark_xrefs_test.adb.

From-SVN: r198234

1 files changed, 87 insertions, 0 deletions

diff --git a/gcc/ada/exp_spark.ads b/gcc/ada/exp_spark.ads
new file mode 100644
index 0000000..726b69a
--- /dev/null
+++ b/gcc/ada/exp_spark.ads
@@ -0,0 +1,87 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                            E X P _ S P A R K                             --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2011-2013, Free Software Foundation, Inc.         --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
+-- for  more details.  You should have  received  a copy of the GNU General --
+-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license.          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package implements a light expansion which is used in formal
+--  verification mode (SPARK_Mode = True). Instead of a complete expansion
+--  of nodes for code generation, this SPARK expansion targets generation
+--  of intermediate code for formal verification.
+
+--  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
+
+   procedure Expand_SPARK (N : Node_Id);
+
+end Exp_SPARK;