From: Arnaud Charlet Date: Thu, 4 Aug 2011 13:26:25 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=483361a6819afa90d3aa85727b6ddfbe610d102c;p=gcc.git [multiple changes] 2011-08-04 Sergey Rybin * gnat_ugn.texi: Update doc on gnatcheck. 2011-08-04 Yannick Moy * lib-xref-alfa.adb (Add_ALFA_Xrefs): correct definition of ranges of xrefs in a scope. 2011-08-04 Yannick Moy * 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. From-SVN: r177382 --- 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 + + * gnat_ugn.texi: Update doc on gnatcheck. + +2011-08-04 Yannick Moy + + * lib-xref-alfa.adb (Add_ALFA_Xrefs): correct definition of ranges of + xrefs in a scope. + +2011-08-04 Yannick Moy + + * 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 * 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