[multiple changes]

2012-05-15  Tristan Gingold  <gingold@adacore.com>

	* exp_ch7.adb (Build_Exception_Handler): Save current
	occurrence only if -gnateE.
	(Build_Object_Declaration): Declare E_Id only if -gnateE.
	(Build_Raise_Statement): Call Raise_From_Controlled_Operation only if
	-gnateE (else raise PE).
	* s-soflin.adb (Save_Library_Occurrence): Handle null occurrence
	access.
	* a-except-2005.adb (Reraise_Library_Exception_If_Any): Call
	Raise_From_Controlled_Operation only if the saved occurrence is
	not null, otherwise raise PE.

2012-05-15  Yannick Moy  <moy@adacore.com>

	* exp_alfa.ads: Add comments describing the Alfa mode.

From-SVN: r187514

gcc/ada/ChangeLog

@@ -1,3 +1,20 @@
+2012-05-15  Tristan Gingold  <gingold@adacore.com>
+
+	* exp_ch7.adb (Build_Exception_Handler): Save current
+	occurrence only if -gnateE.
+	(Build_Object_Declaration): Declare E_Id only if -gnateE.
+	(Build_Raise_Statement): Call Raise_From_Controlled_Operation only if
+	-gnateE (else raise PE).
+	* s-soflin.adb (Save_Library_Occurrence): Handle null occurrence
+	access.
+	* a-except-2005.adb (Reraise_Library_Exception_If_Any): Call
+	Raise_From_Controlled_Operation only if the saved occurrence is
+	not null, otherwise raise PE.
+
+2012-05-15  Yannick Moy  <moy@adacore.com>
+
+	* exp_alfa.ads: Add comments describing the Alfa mode.
+
 2012-05-15  Tristan Gingold  <gingold@adacore.com>
 
 	* s-soflin.ads, s-soflin.adb (Save_Library_Occurrence): Parameter

gcc/ada/a-except-2005.adb

@@ -1296,7 +1296,13 @@ package body Ada.Exceptions is
    begin
       if Library_Exception_Set then
          LE := Library_Exception;
-         Raise_From_Controlled_Operation (LE);
+         if LE.Id = Null_Id then
+            Raise_Exception_No_Defer
+              (E       => Program_Error'Identity,
+               Message => "finalize/adjust raised exception");
+         else
+            Raise_From_Controlled_Operation (LE);
+         end if;
       end if;
    end Reraise_Library_Exception_If_Any;
 

gcc/ada/exp_alfa.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---             Copyright (C) 2011, Free Software Foundation, Inc.           --
+--          Copyright (C) 2011-2012, 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- --
@@ -24,9 +24,9 @@
 ------------------------------------------------------------------------------
 
 --  This package implements a light expansion which is used in formal
---  verification mode. Instead of a complete expansion of nodes for code
+--  verification mode (Alfa_Mode = True). Instead of a complete expansion
---  generation, this Alfa expansion targets generation of intermediate code
+--  of nodes for code generation, this Alfa expansion targets generation
---  for formal verification.
+--  of intermediate code for formal verification.
 
 --  Expand_Alfa is called directly by Expander.Expand.
 
@@ -34,15 +34,49 @@
 
 --    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)
+--        conversions, expand actuals in calls to introduce temporaries, expand
+--        generics instantiations)
 
 --    2. Facilitate treatment for the formal verification back-end (fully
---       qualify names, set membership)
+--       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_Alfa selectively expands some constructs.
+
+--  To fulfill objective 2, the tree after Alfa 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)
+
+--  Alfa 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 Alfa
+--  cross-references are output in a separate section of ALI files, as
+--  described in alfa.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_Alfa 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_Alfa is

gcc/ada/exp_ch7.adb

@@ -717,63 +717,95 @@ package body Exp_Ch7 is
       Actuals      : List_Id;
       Proc_To_Call : Entity_Id;
       Except       : Node_Id;
+      Stmts        : List_Id;
 
    begin
-      pragma Assert (Present (Data.E_Id));
       pragma Assert (Present (Data.Raised_Id));
 
-      --  Generate:
+      if Exception_Extra_Info
+        or else (For_Library and then not Restricted_Profile)
+      then
+         if Exception_Extra_Info then
+            --  Generate:
 
-      --    Get_Current_Excep.all
+            --    Get_Current_Excep.all
 
-      Except :=
+            Except :=
-        Make_Function_Call (Data.Loc,
+              Make_Function_Call (Data.Loc,
-          Name =>
+                Name =>
-            Make_Explicit_Dereference (Data.Loc,
+                  Make_Explicit_Dereference (Data.Loc,
-              Prefix =>
+                    Prefix =>
-                New_Reference_To (RTE (RE_Get_Current_Excep), Data.Loc)));
+                      New_Reference_To (RTE (RE_Get_Current_Excep),
+                                        Data.Loc)));
+         else
+            --  Generate:
 
-      if For_Library and not Restricted_Profile then
+            --    null
-         Proc_To_Call := RTE (RE_Save_Library_Occurrence);
+
-         Actuals := New_List (Except);
+            Except := Make_Null (Data.Loc);
-      else
+         end if;
-         Proc_To_Call := RTE (RE_Save_Occurrence);
+
-         Actuals :=
+         if For_Library and then not Restricted_Profile then
-           New_List
+            Proc_To_Call := RTE (RE_Save_Library_Occurrence);
-             (New_Reference_To (Data.E_Id, Data.Loc),
+            Actuals := New_List (Except);
+         else
+            Proc_To_Call := RTE (RE_Save_Occurrence);
+
+            --  The dereference occurs only when Exception_Extra_Info is true,
+            --  and therefore Except is not null.
+
+            Actuals := New_List (
+              New_Reference_To (Data.E_Id, Data.Loc),
               Make_Explicit_Dereference (Data.Loc, Except));
+         end if;
+
+         --  Generate:
+
+         --    when others =>
+         --       if not Raised_Id then
+         --          Raised_Id := True;
+
+         --          Save_Occurrence (E_Id, Get_Current_Excep.all.all);
+         --            or
+         --          Save_Library_Occurrence (Get_Current_Excep.all);
+         --       end if;
+
+         Stmts :=
+           New_List (
+             Make_If_Statement (Data.Loc,
+               Condition       =>
+                 Make_Op_Not (Data.Loc,
+                   Right_Opnd => New_Reference_To (Data.Raised_Id, Data.Loc)),
+
+               Then_Statements => New_List (
+                 Make_Assignment_Statement (Data.Loc,
+                   Name       => New_Reference_To (Data.Raised_Id, Data.Loc),
+                   Expression => New_Reference_To (Standard_True, Data.Loc)),
+
+                 Make_Procedure_Call_Statement (Data.Loc,
+                   Name                   =>
+                     New_Reference_To (Proc_To_Call, Data.Loc),
+                   Parameter_Associations => Actuals))));
+
+      else
+         --  Generate:
+
+         --    Raised_Id := True;
+
+         Stmts := New_List (
+           Make_Assignment_Statement (Data.Loc,
+             Name       => New_Reference_To (Data.Raised_Id, Data.Loc),
+             Expression => New_Reference_To (Standard_True, Data.Loc)));
       end if;
 
       --  Generate:
 
       --    when others =>
-      --       if not Raised_Id then
-      --          Raised_Id := True;
-
-      --          Save_Occurrence (E_Id, Get_Current_Excep.all.all);
-      --            or
-      --          Save_Library_Occurrence (Get_Current_Excep.all);
-      --       end if;
 
       return
         Make_Exception_Handler (Data.Loc,
-          Exception_Choices =>
+          Exception_Choices => New_List (Make_Others_Choice (Data.Loc)),
-            New_List (Make_Others_Choice (Data.Loc)),
+          Statements        => Stmts);
-          Statements => New_List (
-            Make_If_Statement (Data.Loc,
-              Condition       =>
-                Make_Op_Not (Data.Loc,
-                  Right_Opnd => New_Reference_To (Data.Raised_Id, Data.Loc)),
-
-              Then_Statements => New_List (
-                Make_Assignment_Statement (Data.Loc,
-                  Name       => New_Reference_To (Data.Raised_Id, Data.Loc),
-                  Expression => New_Reference_To (Standard_True, Data.Loc)),
-
-                Make_Procedure_Call_Statement (Data.Loc,
-                  Name                   =>
-                    New_Reference_To (Proc_To_Call, Data.Loc),
-                  Parameter_Associations => Actuals)))));
    end Build_Exception_Handler;
 
    -------------------------------
@@ -2998,8 +3030,6 @@ package body Exp_Ch7 is
          return;
       end if;
 
-      Data.Abort_Id  := Make_Temporary (Loc, 'A');
-      Data.E_Id      := Make_Temporary (Loc, 'E');
       Data.Raised_Id := Make_Temporary (Loc, 'R');
 
       --  In certain scenarios, finalization can be triggered by an abort. If
@@ -3019,35 +3049,44 @@ package body Exp_Ch7 is
         and then VM_Target = No_VM
         and then not For_Package
       then
+         Data.Abort_Id  := Make_Temporary (Loc, 'A');
+
          A_Expr := New_Reference_To (RTE (RE_Triggered_By_Abort), Loc);
 
-      --  No abort, .NET/JVM or library-level finalizers
+         --  Generate:
+         --    Abort_Id : constant Boolean := <A_Expr>;
+
+         Append_To (Decls,
+           Make_Object_Declaration (Loc,
+             Defining_Identifier => Data.Abort_Id,
+             Constant_Present    => True,
+             Object_Definition   => New_Reference_To (Standard_Boolean, Loc),
+             Expression          => A_Expr));
 
       else
-         A_Expr := New_Reference_To (Standard_False, Loc);
+         --  No abort, .NET/JVM or library-level finalizers
+
+         Data.Abort_Id  := Empty;
       end if;
 
-      --  Generate:
+      if Exception_Extra_Info then
-      --    Abort_Id : constant Boolean := <A_Expr>;
+         Data.E_Id      := Make_Temporary (Loc, 'E');
 
-      Append_To (Decls,
+         --  Generate:
-        Make_Object_Declaration (Loc,
+         --    E_Id : Exception_Occurrence;
-          Defining_Identifier => Data.Abort_Id,
-          Constant_Present    => True,
-          Object_Definition   => New_Reference_To (Standard_Boolean, Loc),
-          Expression          => A_Expr));
 
-      --  Generate:
+         E_Decl :=
-      --    E_Id : Exception_Occurrence;
+           Make_Object_Declaration (Loc,
+             Defining_Identifier => Data.E_Id,
+             Object_Definition   =>
+               New_Reference_To (RTE (RE_Exception_Occurrence), Loc));
+         Set_No_Initialization (E_Decl);
 
-      E_Decl :=
+         Append_To (Decls, E_Decl);
-        Make_Object_Declaration (Loc,
-          Defining_Identifier => Data.E_Id,
-          Object_Definition   =>
-            New_Reference_To (RTE (RE_Exception_Occurrence), Loc));
-      Set_No_Initialization (E_Decl);
 
-      Append_To (Decls, E_Decl);
+      else
+         Data.E_Id      := Empty;
+      end if;
 
       --  Generate:
       --    Raised_Id : Boolean := False;
@@ -3067,12 +3106,15 @@ package body Exp_Ch7 is
      (Data : Finalization_Exception_Data) return Node_Id
    is
       Stmt : Node_Id;
+      Expr : Node_Id;
 
    begin
       --  Standard run-time and .NET/JVM targets use the specialized routine
       --  Raise_From_Controlled_Operation.
 
-      if RTE_Available (RE_Raise_From_Controlled_Operation) then
+      if Exception_Extra_Info
+        and then RTE_Available (RE_Raise_From_Controlled_Operation)
+      then
          Stmt :=
            Make_Procedure_Call_Statement (Data.Loc,
               Name                   =>
@@ -3091,6 +3133,21 @@ package body Exp_Ch7 is
              Reason => PE_Finalize_Raised_Exception);
       end if;
 
+      --  Generate:
+      --    Raised_Id and then not Abort_Id
+      --      <or>
+      --    Raised_Id
+
+      Expr := New_Reference_To (Data.Raised_Id, Data.Loc);
+
+      if Present (Data.Abort_Id) then
+         Expr := Make_And_Then (Data.Loc,
+           Left_Opnd  => Expr,
+           Right_Opnd =>
+             Make_Op_Not (Data.Loc,
+               Right_Opnd => New_Reference_To (Data.Abort_Id, Data.Loc)));
+      end if;
+
       --  Generate:
       --    if Raised_Id and then not Abort_Id then
       --       Raise_From_Controlled_Operation (E_Id);
@@ -3100,13 +3157,7 @@ package body Exp_Ch7 is
 
       return
         Make_If_Statement (Data.Loc,
-          Condition       =>
+          Condition       => Expr,
-            Make_And_Then (Data.Loc,
-              Left_Opnd  => New_Reference_To (Data.Raised_Id, Data.Loc),
-              Right_Opnd =>
-                Make_Op_Not (Data.Loc,
-                  Right_Opnd => New_Reference_To (Data.Abort_Id, Data.Loc))),
-
           Then_Statements => New_List (Stmt));
    end Build_Raise_Statement;
 

gcc/ada/s-soflin.adb

@@ -224,10 +224,13 @@ package body System.Soft_Links is
    -----------------------------
 
    procedure Save_Library_Occurrence (E : EOA) is
+      use Ada.Exceptions;
    begin
       if not Library_Exception_Set then
          Library_Exception_Set := True;
-         Ada.Exceptions.Save_Occurrence (Library_Exception, E.all);
+         if E /= null then
+            Ada.Exceptions.Save_Occurrence (Library_Exception, E.all);
+         end if;
       end if;
    end Save_Library_Occurrence;