diff options
author | Hristian Kirtchev <kirtchev@adacore.com> | 2018-05-22 13:23:40 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-05-22 13:23:40 +0000 |
commit | 41ff70d9a5c91c3540d3fdb08ddc58d1e1d00eab (patch) | |
tree | f1edd4635995612146de932f874fb3cfcf1e94be /gcc/ada/atree.h | |
parent | f16cb8dfb93a424887b543015c1e0cfc73ec2fe3 (diff) | |
download | gcc-41ff70d9a5c91c3540d3fdb08ddc58d1e1d00eab.zip gcc-41ff70d9a5c91c3540d3fdb08ddc58d1e1d00eab.tar.gz gcc-41ff70d9a5c91c3540d3fdb08ddc58d1e1d00eab.tar.bz2 |
[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
Diffstat (limited to 'gcc/ada/atree.h')
0 files changed, 0 insertions, 0 deletions