@@ -941,6 +941,17 @@ package body Sem_Prag is
Ekind_In (Item_Id, E_Abstract_State, E_Variable)
then
+ -- A [generic] function is not allowed to have Output
+ -- items in its dependency relations. Note that "null"
+ -- and attribute 'Result are still valid items.
+
+ if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+ and then not Is_Input
+ then
+ SPARK_Msg_N
+ ("output item is not applicable to function", Item);
+ end if;
+
-- The item denotes a concurrent type. Note that single
-- protected/task types are not considered here because
-- they behave as objects in the context of pragma
This patch modifies the analysis of pragma [Refined_]Depends to emit an error when the pragma is asspciated with a [generic] function, and one of its clauses contains a non-null, non-'Result output item. ------------ -- Source -- ------------ -- pack.ads package Pack with SPARK_Mode is Obj_1 : Integer := 1; Obj_2 : Integer := 2; function Func_1 return Integer with Global => (In_Out => Obj_1); -- Error function Func_2 return Integer with Global => (Output => Obj_1); -- Error function Func_3 return Integer with Depends => (Func_3'Result => Obj_1, -- OK Obj_1 => Obj_1); -- Error function Func_4 return Integer with Depends => (Func_4'Result => Obj_1, -- OK null => Obj_2); -- OK end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c pack.ads pack.ads:6:22: global mode "In_Out" is not applicable to functions pack.ads:9:22: global mode "Output" is not applicable to functions pack.ads:13:23: output item is not applicable to function Tested on x86_64-pc-linux-gnu, committed on trunk 2018-05-22 Hristian Kirtchev <kirtchev@adacore.com> gcc/ada/ * sem_prag.adb (Analyze_Input_Output): Emit an error when a non-null, non-'Result output appears in the output list of a function.