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 <kirtc...@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.
--- gcc/ada/sem_prag.adb
+++ gcc/ada/sem_prag.adb
@@ -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