[Ada] Ignore pragmas Compile_Time_Error/Warning in GNATprove mode
authorYannick Moy <moy@adacore.com>
Tue, 9 Oct 2018 15:06:41 +0000 (15:06 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 9 Oct 2018 15:06:41 +0000 (15:06 +0000)
commitea891b439e876000d139e45f44c49b9436d195a4
tree2611d4d339ccb513378562a60cfa3e28d72cad21
parente693ddbec3e38aeff2e229785b9037ba0caa17c8
[Ada] Ignore pragmas Compile_Time_Error/Warning in GNATprove mode

GNATprove does not have sometimes the precise information of the
compiler about size of types and objects, so that it cannot evaluate the
expressions in pragma Compile_Time_Error/Warning the same way the
compiler does.  Thus, these pragmas should be ignored in GNATprove mode,
as it can neither verify them nor assume them (if the expression cannot
be evaluated at compile time, then the semantics for GNAT is to ignore
them).

2018-10-09  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_prag.adb (Process_Compile_Time_Warning_Or_Error): Rewrite
pragmas as null statements in GNATprove mode.

From-SVN: r264981
gcc/ada/ChangeLog
gcc/ada/sem_prag.adb