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