projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 49ea96b) | patch
[Ada] Correctly mark subprogram as not always inlined in GNATprove mode
authorYannick Moy <moy@adacore.com>
Mon, 16 Nov 2020 11:06:32 +0000 (12:06 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Mon, 14 Dec 2020 15:51:48 +0000 (10:51 -0500)
commit3fcb8100aac71b8a109a4f0ceaabd6cfd650b668
tree6c89c3c7377ed176bd7391c5449eb7aed51ef93dtree
parent49ea96b4d883105e44a63f304584088928732975commit | diff
[Ada] Correctly mark subprogram as not always inlined in GNATprove mode

gcc/ada/

* inline.adb (Cannot_Inline): Add No_Info parameter to disable
info message.
* inline.ads (Cannot_Inline): When No_Info is set to True, do
not issue info message in GNATprove mode, but still mark the
subprogram as not always inlined.
* sem_res.adb (Resolve_Call): Always call Cannot_Inline inside
an assertion expression.
gcc/ada/inline.adb diff | blob | history
gcc/ada/inline.ads diff | blob | history
gcc/ada/sem_res.adb diff | blob | history