diff mbox

[Ada] Improve error message for missing dependency item

Message ID 20151020095539.GA13388@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 20, 2015, 9:55 a.m. UTC 
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.
diff mbox

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 229031)
+++ sem_prag.adb	(working copy)
@@ -1220,14 +1220,14 @@ 
          Used_Items : Elist_Id;
          Is_Input   : Boolean)
       is
-         procedure Usage_Error (Item : Node_Id; Item_Id : Entity_Id);
+         procedure Usage_Error (Item_Id : Entity_Id);
          --  Emit an error concerning the illegal usage of an item
 
          -----------------
          -- Usage_Error --
          -----------------
 
-         procedure Usage_Error (Item : Node_Id; Item_Id : Entity_Id) is
+         procedure Usage_Error (Item_Id : Entity_Id) is
             Error_Msg : Name_Id;
 
          begin
@@ -1245,10 +1245,10 @@ 
 
                   Add_Item_To_Name_Buffer (Item_Id);
                   Add_Str_To_Name_Buffer
-                    (" & must appear in at least one input dependence list");
+                    (" & is missing from input dependence list");
 
                   Error_Msg := Name_Find;
-                  SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
+                  SPARK_Msg_NE (Get_Name_String (Error_Msg), N, Item_Id);
                end if;
 
             --  Output case (SPARK RM 6.1.5(10))
@@ -1258,10 +1258,10 @@ 
 
                Add_Item_To_Name_Buffer (Item_Id);
                Add_Str_To_Name_Buffer
-                 (" & must appear in exactly one output dependence list");
+                 (" & is missing from output dependence list");
 
                Error_Msg := Name_Find;
-               SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
+               SPARK_Msg_NE (Get_Name_String (Error_Msg), N, Item_Id);
             end if;
          end Usage_Error;
 
@@ -1297,13 +1297,13 @@ 
               and then not Contains (Used_Items, Item_Id)
             then
                if Is_Formal (Item_Id) then
-                  Usage_Error (Item, Item_Id);
+                  Usage_Error (Item_Id);
 
                --  States and global objects are not used properly only when
                --  the subprogram is subject to pragma Global.
 
                elsif Global_Seen then
-                  Usage_Error (Item, Item_Id);
+                  Usage_Error (Item_Id);
                end if;
             end if;