2012-10-31 Basile Starynkevitch <basile@starynkevitch.net>

	MELT branch merged with trunk rev 193029 using svnmerge.py



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/branches/melt-branch@193030 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 13 insertions, 0 deletions

diff --git a/gcc/ada/exp_alfa.adb b/gcc/ada/exp_alfa.adb
index 2a640fd5423..69a6e2b0cec 100644
--- a/gcc/ada/exp_alfa.adb
+++ b/gcc/ada/exp_alfa.adb
@@ -81,6 +81,14 @@ package body Exp_Alfa is
          when N_Attribute_Reference =>
             Expand_Alfa_N_Attribute_Reference (N);
 
+         --  Qualification of entity names in formal verification mode
+         --  is limited to the addition of a suffix for homonyms (see
+         --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
+         --  as full expansion does, but this was removed as this prevents the
+         --  verification back-end from using a short name for debugging and
+         --  user interaction. The verification back-end already takes care
+         --  of qualifying names when needed.
+
          when N_Block_Statement     |
               N_Package_Body        |
               N_Package_Declaration |
@@ -97,6 +105,9 @@ package body Exp_Alfa is
          when N_In =>
             Expand_Alfa_N_In (N);
 
+         --  A NOT IN B gets transformed to NOT (A IN B). This is the same
+         --  expansion used in the normal case, so shared the code.
+
          when N_Not_In =>
             Expand_N_Not_In (N);
 
@@ -106,6 +117,8 @@ package body Exp_Alfa is
          when N_Simple_Return_Statement =>
             Expand_Alfa_N_Simple_Return_Statement (N);
 
+         --  In Alfa mode, no other constructs require expansion
+
          when others =>
             null;
       end case;