[Ada] Prohibit output dependency items on functions
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 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. From-SVN: r260519
Showing
Please
register
or
sign in
to comment