[Ada] Warning on unused loop variable of a quantified expression

[Arnaud Charlet]

This patch adds a check in the analysis of quantified expressions to detect an
unused loop variable and issue a warning.

------------
-- Source --
------------

--  warnings.adb

with Ada.Containers.Doubly_Linked_Lists;

procedure Warnings is
   package DLL is new Ada.Containers.Doubly_Linked_Lists (Natural, "=");

   type Test_Array is array (Natural range <>, Natural range <>) of Natural;

   function Factorial (Val : Natural) return Natural is
   begin
      if Val > 1 then
         return Val * Factorial (Val - 1);
      end if;

      return 1;
   end Factorial;

   TA   : constant Test_Array (1 .. 3, 1 .. 4) := (others => (others => 0));
   Flag : Boolean;
   L    : DLL.List;

begin
   Flag := (for all Element of TA => Element > 1);
   Flag := (for some Element of TA => Factorial (3) = 6);
   Flag := (for all Element of L => Element > 1);
   Flag := (for some Element of L => Factorial (3) = 6);
   Flag := (for all Element in 1 .. 4 => Factorial (Element) > 0);
   Flag := (for some Element in 1 .. 4 => Factorial (3) = 6);
   Flag := (for all Element in DLL.Iterate (L) => DLL.Element (Element) > 1);
   Flag := (for some Element in DLL.Iterate (L) => Factorial (3) = 6);

end Warnings;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c -gnat12 -gnatw.t warnings.adb
warnings.adb:23:22: warning: unused variable "Element"
warnings.adb:25:22: warning: unused variable "Element"
warnings.adb:27:22: warning: unused variable "Element"
warnings.adb:29:22: warning: unused variable "Element"

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch4.adb (Analyze_Quantified_Expression):
	Add local variable Loop_Id. Verify that the loop variable
	is used within the condition of the quantified expression.
	(Referenced): New routine.

-------------- next part --------------
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 198287)
+++ sem_ch4.adb	(working copy)
@@ -3510,6 +3510,9 @@
       --  Determine whether if expression If_Expr lacks an else part or if it
       --  has one, it evaluates to True.
 
+      function Referenced (Id : Entity_Id; Expr : Node_Id) return Boolean;
+      --  Determine whether entity Id is referenced within expression Expr
+
       --------------------
       -- Is_Empty_Range --
       --------------------
@@ -3561,9 +3564,44 @@
                        and then Is_True (Expr_Value (Else_Expr)));
       end No_Else_Or_Trivial_True;
 
+      ----------------
+      -- Referenced --
+      ----------------
+
+      function Referenced (Id : Entity_Id; Expr : Node_Id) return Boolean is
+         Seen : Boolean := False;
+
+         function Is_Reference (N : Node_Id) return Traverse_Result;
+         --  Determine whether node N denotes a reference to Id. If this is the
+         --  case, set global flag Seen to True and stop the traversal.
+
+         function Is_Reference (N : Node_Id) return Traverse_Result is
+         begin
+            if Is_Entity_Name (N)
+              and then Present (Entity (N))
+              and then Entity (N) = Id
+            then
+               Seen := True;
+               return Abandon;
+            else
+               return OK;
+            end if;
+         end Is_Reference;
+
+         procedure Inspect_Expression is new Traverse_Proc (Is_Reference);
+
+      --  Start of processing for Referenced
+
+      begin
+         Inspect_Expression (Expr);
+
+         return Seen;
+      end Referenced;
+
       --  Local variables
 
       Cond    : constant Node_Id := Condition (N);
+      Loop_Id : Entity_Id;
       QE_Scop : Entity_Id;
 
    --  Start of processing for Analyze_Quantified_Expression
@@ -3590,22 +3628,39 @@
       if Present (Iterator_Specification (N)) then
          Preanalyze (Iterator_Specification (N));
 
+         --  Do not proceed with the analysis when the range of iteration is
+         --  empty. The appropriate error is issued by Is_Empty_Range.
+
          if Is_Entity_Name (Name (Iterator_Specification (N)))
            and then Is_Empty_Range (Etype (Name (Iterator_Specification (N))))
          then
             return;
          end if;
 
-      else
+      else pragma Assert (Present (Loop_Parameter_Specification (N)));
          Preanalyze (Loop_Parameter_Specification (N));
       end if;
 
       Preanalyze_And_Resolve (Cond, Standard_Boolean);
 
       End_Scope;
-
       Set_Etype (N, Standard_Boolean);
 
+      --  Verify that the loop variable is used within the condition of the
+      --  quantified expression.
+
+      if Present (Iterator_Specification (N)) then
+         Loop_Id := Defining_Identifier (Iterator_Specification (N));
+      else
+         Loop_Id := Defining_Identifier (Loop_Parameter_Specification (N));
+      end if;
+
+      if Warn_On_Suspicious_Contract
+        and then not Referenced (Loop_Id, Cond)
+      then
+         Error_Msg_N ("?T?unused variable &", Loop_Id);
+      end if;
+
       --  Diagnose a possible misuse of the "some" existential quantifier. When
       --  we have a quantified expression of the form
       --