[Ada] Define a light expansion mode for formal verification
Instead of the full expansion targetting code generation, a light expansion is
now used in formal verification mode. Light expansion has three main objectives:
1. Perform limited expansion to explicit some Ada rules and constructs
2. Facilitate treatment for the formal verification back-end
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)
Also remove special exits from full expansion that were previously needed.
Note that this is an intermediate step/change. A better/cleaner approach
will follow using exp_alfa.ad{s,b} files.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-30 Yannick Moy m...@adacore.com
* exp_aggr.adb, exp_ch11.adb, exp_prag.adb: Remove early exit during
expansion in Alfa mode.
* exp_ch6.adb, exp_ch6.ads (Expand_Actuals): Make subprogram public.
* exp_light.adb, exp_light.ads: New package defining light expansion.
* expander.adb (Expand): Call light expansion in Alfa mode
* exp_ch6_light.adb, exp_ch6_light.ads: Light expansion of chapter 6
constructs.
* exp_ch7_light.adb, exp_ch7_light.ads: Light expansion of chapter 7
constructs.
* exp_attr_light.adb, exp_attr_light.ads: Light expansion of attributes
* gnat1drv.adb (Adjust_Global_Switches): Comment
Index: exp_prag.adb
===
--- exp_prag.adb(revision 178293)
+++ exp_prag.adb(working copy)
@@ -321,15 +321,6 @@
-- be an explicit conditional in the source, not an implicit if, so we
-- do not call Make_Implicit_If_Statement.
- -- In formal verification mode, we keep the pragma check in the code,
- -- and its enclosed expression is not expanded. This requires that no
- -- transient scope is introduced for pragma check in this mode in
- -- Exp_Ch7.Establish_Transient_Scope.
-
- if ALFA_Mode then
- return;
- end if;
-
-- Case where we generate a direct raise
if ((Debug_Flag_Dot_G
Index: exp_ch6_light.adb
===
--- exp_ch6_light.adb (revision 0)
+++ exp_ch6_light.adb (revision 0)
@@ -0,0 +1,193 @@
+--
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- E X P _ C H 6 _ L I G H T--
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2011, 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. --
+-- --
+--
+
+with Atree;use Atree;
+with Einfo;use Einfo;
+with Exp_Ch6; use Exp_Ch6;
+with Exp_Dbug; use Exp_Dbug;
+with Rtsfind; use Rtsfind;
+with Sem_Aux; use Sem_Aux;
+with Sem_Res; use Sem_Res;
+with Sinfo;use Sinfo;
+with Stand;use Stand;
+with Tbuild; use Tbuild;
+
+package body Exp_Ch6_Light is
+
+ ---
+ -- Local Subprograms --
+ ---
+
+ procedure Expand_Simple_Function_Return (N : Node_Id);
+ -- Expand simple return from function
+
+ ---
+ -- Expand_Light_Call --
+ ---
+
+ procedure Expand_Light_Call (N : Node_Id) is
+ Call_Node : constant Node_Id := N;
+ Parent_Subp : Entity_Id;
+ Subp
[Ada] Define a light expansion mode for formal verification (2)
Following up on the previous change, we now move all the formal verification expansion in a separate exp_alfa.ad? file. Previous exp_*_light change is reverted/canceled at the same time (not shown here for convenience). Instead of the full expansion targetting code generation, a light expansion now used in formal verification mode. Light expansion has three main objectives: 1. Perform limited expansion to explicit some Ada rules and constructs 2. Facilitate treatment for the formal verification back-end 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) Also remove special exits from full expansion that were previously needed. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-30 Yannick Moy m...@adacore.com * exp_aggr.adb, exp_ch11.adb, exp_prag.adb: Remove early exit during expansion in Alfa mode. * exp_ch6.adb, exp_ch6.ads (Expand_Actuals): Make subprogram public * exp_alfa.adb, exp_alfa.ads: New package defining light expansion for Alfa mode. * gnat1drv.adb (Adjust_Global_Switches): Update Comment. * sem_res.adb: Ditto. Index: exp_prag.adb === --- exp_prag.adb(revision 178316) +++ exp_prag.adb(working copy) @@ -321,15 +321,6 @@ -- be an explicit conditional in the source, not an implicit if, so we -- do not call Make_Implicit_If_Statement. - -- In formal verification mode, we keep the pragma check in the code, - -- and its enclosed expression is not expanded. This requires that no - -- transient scope is introduced for pragma check in this mode in - -- Exp_Ch7.Establish_Transient_Scope. - - if ALFA_Mode then - return; - end if; - -- Case where we generate a direct raise if ((Debug_Flag_Dot_G Index: exp_alfa.adb === --- exp_alfa.adb(revision 0) +++ exp_alfa.adb(revision 0) @@ -0,0 +1,270 @@ +-- +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- E X P _ A L F A -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2011, 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. -- +-- -- +-- + +with Atree;use Atree; +with Einfo;use Einfo; +with Exp_Attr; use Exp_Attr; +with Exp_Ch6; use Exp_Ch6; +with Exp_Dbug; use Exp_Dbug; +with Rtsfind; use Rtsfind; +with Sem_Aux; use Sem_Aux; +with Sem_Res; use Sem_Res; +with Sinfo;use Sinfo; +with Snames; use Snames; +with Stand;use Stand; +with Tbuild; use Tbuild; + +package body Exp_Alfa is + + --- + -- Local Subprograms -- + --- + + procedure Expand_Alfa_Call (N : Node_Id); + -- This procedure contains common processing for function and procedure + -- calls: + -- * expansion of actuals to introduce necessary temporaries + -- * replacement of renaming by subprogram renamed + + procedure Expand_Alfa_N_Attribute_Reference (N : Node_Id); + -- Expand attributes 'Old and 'Result only + + procedure Expand_Alfa_N_Package_Declaration (N : Node_Id); + -- Fully qualify
