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 <kirtc...@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.
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;