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 | |
| 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
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 11 |
2 files changed, 16 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 76000d2..cef561e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,10 @@ 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. (Build_Record_VS_Func): Reimplemented. (Expand_N_Attribute): Reimplement the handling of attribute diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 8dae23d..1c067ba 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 |