2011-08-04 Sergey Rybin <rybin@adacore.com>

	* gnat_ugn.texi: Update doc on gnatcheck.

2011-08-04  Yannick Moy  <moy@adacore.com>

	* lib-xref-alfa.adb (Add_ALFA_Xrefs): correct definition of ranges of
	xrefs in a scope.

2011-08-04  Yannick Moy  <moy@adacore.com>

	* exp_prag.adb (Expand_Pragma_Check): in ALFA mode, return without
	performing expansion.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper,
	Analyze_Generic_Subprogram_Body): protect call to Process_PCCs so that
	it is not called in ALFA mode.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177382 138bc75d-0d04-0410-961f-82ee72b054a4

5 files changed, 50 insertions, 19 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 7112facf76d..48e9e5352ac 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,20 @@
+2011-08-04  Sergey Rybin  <rybin@adacore.com>
+
+	* gnat_ugn.texi: Update doc on gnatcheck.
+
+2011-08-04  Yannick Moy  <moy@adacore.com>
+
+	* lib-xref-alfa.adb (Add_ALFA_Xrefs): correct definition of ranges of
+	xrefs in a scope.
+
+2011-08-04  Yannick Moy  <moy@adacore.com>
+
+	* exp_prag.adb (Expand_Pragma_Check): in ALFA mode, return without
+	performing expansion.
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper,
+	Analyze_Generic_Subprogram_Body): protect call to Process_PCCs so that
+	it is not called in ALFA mode.
+
 2011-08-04  Emmanuel Briot  <briot@adacore.com>
 
 	* make.adb, osint.adb, osint.ads (Reset_Command_Line_Files): not used
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 7e1f4208b3f..b1900a9ad7d 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-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- --
@@ -321,6 +321,12 @@ package body Exp_Prag is
       --  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
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Case where we generate a direct raise
 
       if ((Debug_Flag_Dot_G
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index 1d87f4aebd9..d47d6eabd93 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -17306,9 +17306,6 @@ outside the current directory, the source search path has to be provided when
 calling @command{gnatcheck}, either through a specified project file or
 through @command{gnatcheck} switches.
 
-A number of rules are predefined in @command{gnatcheck} and are described
-later in this chapter.
-
 For full details, refer to @cite{GNATcheck Reference Manual} document.
 
 
diff --git a/gcc/ada/lib-xref-alfa.adb b/gcc/ada/lib-xref-alfa.adb
index 4f52676474f..26bd28e0f03 100644
--- a/gcc/ada/lib-xref-alfa.adb
+++ b/gcc/ada/lib-xref-alfa.adb
@@ -339,7 +339,6 @@ package body ALFA is
    --------------------
 
    procedure Add_ALFA_Xrefs is
-      Prev_Scope_Idx  : Scope_Index;
       Cur_Scope_Idx   : Scope_Index;
       From_Xref_Idx   : Xref_Index;
       Cur_Entity      : Entity_Id;
@@ -613,13 +612,12 @@ package body ALFA is
 
       --  Initialize loop
 
-      Prev_Scope_Idx := 1;
       Cur_Scope_Idx  := 1;
       From_Xref_Idx  := 1;
       Cur_Entity     := Empty;
 
-      if ALFA_Scope_Table.Last /= 0 then
-         ALFA_Scope_Table.Table (1).From_Xref := 1;
+      if ALFA_Scope_Table.Last = 0 then
+         return;
       end if;
 
       --  Loop to output references
@@ -721,9 +719,15 @@ package body ALFA is
 
             pragma Assert (Is_Future_Scope_Entity (XE.Ent_Scope));
 
+            --  Update the range of cross references to which the current scope
+            --  refers to. This may be the empty range only for the first scope
+            --  considered.
+
             if XE.Ent_Scope /= Cur_Scope then
                ALFA_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
                  From_Xref_Idx;
+               ALFA_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
+                 ALFA_Xref_Table.Last;
                From_Xref_Idx := ALFA_Xref_Table.Last + 1;
             end if;
 
@@ -732,14 +736,6 @@ package body ALFA is
                pragma Assert (Cur_Scope_Idx <= ALFA_Scope_Table.Last);
             end loop;
 
-            if Prev_Scope_Idx /= Cur_Scope_Idx
-              and then ALFA_Xref_Table.Last /= 0
-            then
-               ALFA_Scope_Table.Table (Prev_Scope_Idx).To_Xref :=
-                 ALFA_Xref_Table.Last;
-               Prev_Scope_Idx := Cur_Scope_Idx;
-            end if;
-
             if XE.Ent /= Cur_Entity then
                Cur_Entity_Name :=
                  new String'(Exact_Source_Name (Sloc (XE.Ent)));
@@ -758,6 +754,8 @@ package body ALFA is
          end Add_One_Xref;
       end loop;
 
+      --  Update the range of cross references to which the scope refers to
+
       ALFA_Scope_Table.Table (Cur_Scope_Idx).From_Xref := From_Xref_Idx;
       ALFA_Scope_Table.Table (Cur_Scope_Idx).To_Xref   := ALFA_Xref_Table.Last;
    end Add_ALFA_Xrefs;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index c11c6e83543..d0e51e51870 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -962,7 +962,15 @@ package body Sem_Ch6 is
          end if;
 
          Set_Actual_Subtypes (N, Current_Scope);
-         Process_PPCs (N, Gen_Id, Body_Id);
+
+         --  Deal with preconditions and postconditions. In formal verification
+         --  mode, we keep pre- and postconditions attached to entities rather
+         --  than inserted in the code, in order to facilitate a distinct
+         --  treatment for them.
+
+         if not ALFA_Mode then
+            Process_PPCs (N, Gen_Id, Body_Id);
+         end if;
 
          --  If the generic unit carries pre- or post-conditions, copy them
          --  to the original generic tree, so that they are properly added
@@ -2663,9 +2671,14 @@ package body Sem_Ch6 is
       HSS := Handled_Statement_Sequence (N);
       Set_Actual_Subtypes (N, Current_Scope);
 
-      --  Deal with preconditions and postconditions
+      --  Deal with preconditions and postconditions. In formal verification
+      --  mode, we keep pre- and postconditions attached to entities rather
+      --  than inserted in the code, in order to facilitate a distinct
+      --  treatment for them.
 
-      Process_PPCs (N, Spec_Id, Body_Id);
+      if not ALFA_Mode then
+         Process_PPCs (N, Spec_Id, Body_Id);
+      end if;
 
       --  Add a declaration for the Protection object, renaming declarations
       --  for discriminals and privals and finally a declaration for the entry