[Ada] Prohibit output dependency items on functions
authorHristian Kirtchev <kirtchev@adacore.com>
Tue, 22 May 2018 13:23:40 +0000 (13:23 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 22 May 2018 13:23:40 +0000 (13:23 +0000)
commit41ff70d9a5c91c3540d3fdb08ddc58d1e1d00eab
treef1edd4635995612146de932f874fb3cfcf1e94be
parentf16cb8dfb93a424887b543015c1e0cfc73ec2fe3
[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
gcc/ada/ChangeLog
gcc/ada/sem_prag.adb