[Ada] Improve error message for missing dependency item

[Arnaud Charlet <charlet at adacore dot com>]

This patch modifies the analysis of pragma Depends to emit a clearer message
concerning a missing dependency item.

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

--  message.ads

package Message
  with Abstract_State => State,
       Initializes    => State,
       SPARK_Mode
is
   procedure Proc (X : in Integer; Y : out Integer)
     with Global  => (In_Out => State),
          Depends => (State => State,
                      Y     => X);
end Message;

--  message.adb

package body Message
  with Refined_State => (State => N),
       SPARK_Mode
is
   N : Natural := 0;

   procedure Proc(X : in Integer; Y : out Integer)
     with Refined_Global  => (In_Out => N),
          Refined_Depends => (N => N) 
   is
   begin
      N := N + 1;
      Y := X;
   end Proc;
end Message;

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

$ gcc -c message.adb
message.adb:9:11: parameter "X" is missing from input dependence list

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

2015-10-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Check_Usage): Update the calls to Usage_Error.
	(Usage_Error): Remove formal parameter Item. Emit a clearer message
	concerning a missing dependency item and place it on the related pragma.

Attachment: difs
Description: Text document