From 41ff70d9a5c91c3540d3fdb08ddc58d1e1d00eab Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Tue, 22 May 2018 13:23:40 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_prag.adb | 11 +++++++++++ 2 files changed, 16 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 76000d253f2..cef561e87fc 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-05-22 Hristian Kirtchev + + * sem_prag.adb (Analyze_Input_Output): Emit an error when a non-null, + non-'Result output appears in the output list of a function. + 2018-05-22 Hristian Kirtchev * exp_attr.adb (Build_Array_VS_Func): Reimplemented. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 8dae23dc5d6..1c067ba3504 100644 --- a/gcc/ada/sem_prag.adb +++ b/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 -- 2.30.2