sem_aux.adb, [...] (Get_Called_Entity): New function to return the entity associated...
authorYannick Moy <moy@adacore.com>
Fri, 8 Sep 2017 14:36:54 +0000 (14:36 +0000)
committerArnaud Charlet <charlet@gcc.gnu.org>
Fri, 8 Sep 2017 14:36:54 +0000 (16:36 +0200)
commit8437edb4c28091d5f863dee1d9a0ffd7cfe3e595
tree122a15be5c7b06e888641abfa05a1c93d0750b1d
parent139e8d2aacb2d4221ca94d8c413acd824820040e
sem_aux.adb, [...] (Get_Called_Entity): New function to return the entity associated with the call.

2017-09-08  Yannick Moy  <moy@adacore.com>

* sem_aux.adb, sem_aux.ads (Get_Called_Entity): New function to
return the entity associated with the call.
* sem_util.adb, sem_util.ads (Check_Function_Writable_Actuals):
Replace the internal Get_Function_Id with the new
Sem_Aux.Get_Called_Entity.
(Iterate_Call_Parameters): New
procedure to iterate on formals and actuals at the same time.
* sem_ch12.adb (Analyze_Subprogram_Instantiation):
Set SPARK_Mode from spec when set, for analysis
of instance. Restore after analysis of instance.
(Instantiate_Subprogram_Body): Set SPARK_Mode from body when
set, for analysis of body instance. Restored automatically at
the end of the subprogram.
* gnat1drv.adb (Adjust_Global_Switches): Set
Check_Validity_Of_Parameters to False in GNATprove mode.
* opt.ads (Check_Validity_Of_Parameters): Document switch to
set option.

From-SVN: r251900
gcc/ada/ChangeLog
gcc/ada/sem_aux.adb
gcc/ada/sem_aux.ads
gcc/ada/sem_ch12.adb
gcc/ada/sem_util.adb
gcc/ada/sem_util.ads