[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 76000d253f2d9ced18a0ecf0175b062644df0890..cef561e87fc21b7597755b3e900b84c35dadbbc7 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-05-22  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * 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  <kirtchev@adacore.com>
 
        * exp_attr.adb (Build_Array_VS_Func): Reimplemented.

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 8dae23dc5d6e3fbc1b47c994b248c6bc9f71b98f..1c067ba350445cc93cd24d0d2839b5d02e42db44 100644 (file)
--- 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