projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8467449) | patch
[Ada] Sync code for external properties with SPARK RM
authorPiotr Trojanek <trojanek@adacore.com>
Wed, 26 Aug 2020 12:20:20 +0000 (14:20 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Fri, 23 Oct 2020 08:24:41 +0000 (04:24 -0400)
commit4d4ba374a73b226dc16af7190c688728f3e5d2c5
tree5f0402385166b88a2884786830ae69c5e04f47fdtree
parent846744902e122804242af2cb9f6c6828e887cdf9commit | diff
[Ada] Sync code for external properties with SPARK RM

gcc/ada/

* sem_prag.adb (Check_External_Properties): Rewrite to match the
SPARK RM description.
gcc/ada/sem_prag.adb diff | blob | history