[Ada] SPARK: update borrowing effects for IN parameters
commitf0f2d1fc033cbe56098f7261d91ef6a8130d0b27
authorMaroua Maalej <maalej@adacore.com>
Wed, 26 Sep 2018 09:16:23 +0000 (26 09:16 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Wed, 26 Sep 2018 09:16:23 +0000 (26 09:16 +0000)
tree26ac838f00f0d5e2e8254bd60e42f6eabc0ece9b
parent98f57e4ca3ee558c5a88d471019de0cf005967e9
[Ada] SPARK: update borrowing effects for IN parameters

2018-09-26  Maroua Maalej  <maalej@adacore.com>

gcc/ada/

* sem_spark.adb (Check_Param_In, Setup_Parameter_Or_Global):
Change the operation associated to assigning to an IN parameter.
In SPARK, IN access-to-variable is an observe operation for a
function, and borrow operation for a procedure.

From-SVN: r264601
gcc/ada/ChangeLog
gcc/ada/sem_spark.adb