1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT COMPILER COMPONENTS                         --
4--                                                                          --
5--                             E X P _ A L F A                              --
6--                                                                          --
7--                                 S p e c                                  --
8--                                                                          --
9--          Copyright (C) 2011-2012, Free Software Foundation, Inc.         --
10--                                                                          --
11-- GNAT is free software;  you can  redistribute it  and/or modify it under --
12-- terms of the  GNU General Public License as published  by the Free Soft- --
13-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
14-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
15-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
16-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
17-- for  more details.  You should have  received  a copy of the GNU General --
18-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
19-- http://www.gnu.org/licenses for a complete copy of the license.          --
20--                                                                          --
21-- GNAT was originally developed  by the GNAT team at  New York University. --
22-- Extensive contributions were provided by Ada Core Technologies Inc.      --
23--                                                                          --
24------------------------------------------------------------------------------
25
26--  This package implements a light expansion which is used in formal
27--  verification mode (Alfa_Mode = True). Instead of a complete expansion
28--  of nodes for code generation, this Alfa expansion targets generation
29--  of intermediate code for formal verification.
30
31--  Expand_Alfa is called directly by Expander.Expand.
32
33--  Alfa expansion has three main objectives:
34
35--    1. Perform limited expansion to explicit some Ada rules and constructs
36--       (translate 'Old and 'Result, replace renamings by renamed, insert
37--        conversions, expand actuals in calls to introduce temporaries, expand
38--        generics instantiations)
39
40--    2. Facilitate treatment for the formal verification back-end (fully
41--       qualify names, expand set membership, compute data dependences)
42
43--    3. Avoid the introduction of low-level code that is difficult to analyze
44--       formally, as typically done in the full expansion for high-level
45--       constructs (tasking, dispatching)
46
47--  To fulfill objective 1, Expand_Alfa selectively expands some constructs.
48
49--  To fulfill objective 2, the tree after Alfa expansion should be fully
50--  analyzed semantically. In particular, all expression must have their proper
51--  type, and semantic links should be set between tree nodes (partial to full
52--  view, etc.) Some kinds of nodes should be either absent, or can be ignored
53--  by the formal verification backend:
54
55--      N_Object_Renaming_Declaration: can be ignored safely
56--      N_Expression_Function:         absent (rewitten)
57--      N_Expression_With_Actions:     absent (not generated)
58
59--  Alfa cross-references are generated from the regular cross-references (used
60--  for browsing and code understanding) and additional references collected
61--  during semantic analysis, in particular on all dereferences. These Alfa
62--  cross-references are output in a separate section of ALI files, as
63--  described in alfa.adb. They are the basis for the computation of data
64--  dependences in the formal verification backend. This implies that all
65--  cross-references should be generated in this mode, even those that would
66--  not make sense from a user point-of-view, and that cross-references that do
67--  not lead to data dependences for subprograms can be safely ignored.
68
69--  To support the formal verification of units parameterized by data, the
70--  value of deferred constants should not be considered as a compile-time
71--  constant at program locations where the full view is not visible.
72
73--  To fulfill objective 3, Expand_Alfa does not expand features that are not
74--  formally analyzed (tasking), or for which formal analysis relies on the
75--  source level representation (dispatching, aspects, pragmas). However, these
76--  should be semantically analyzed, which sometimes requires the insertion of
77--  semantic pre-analysis, for example for subprogram contracts and pragma
78--  check/assert.
79
80with Types; use Types;
81
82package Exp_Alfa is
83
84   procedure Expand_Alfa (N : Node_Id);
85
86end Exp_Alfa;
87