]> git.ipfire.org Git - thirdparty/gcc.git/commit
[Ada] SPARK: update borrowing effects for IN parameters
authorpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Wed, 26 Sep 2018 09:16:23 +0000 (09:16 +0000)
committerpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Wed, 26 Sep 2018 09:16:23 +0000 (09:16 +0000)
commit72b189b6a82262f7a4fe69185db3824e230ffd8c
tree26ac838f00f0d5e2e8254bd60e42f6eabc0ece9b
parentc41dad83c22241ab782f7eee7debefaf39d75f9e
[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.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@264601 138bc75d-0d04-0410-961f-82ee72b054a4
gcc/ada/ChangeLog
gcc/ada/sem_spark.adb