From: Yannick Moy Date: Tue, 9 Oct 2018 15:06:41 +0000 (+0000) Subject: [Ada] Ignore pragmas Compile_Time_Error/Warning in GNATprove mode X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ea891b439e876000d139e45f44c49b9436d195a4;p=gcc.git [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 gcc/ada/ * sem_prag.adb (Process_Compile_Time_Warning_Or_Error): Rewrite pragmas as null statements in GNATprove mode. From-SVN: r264981 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 854cadddd51..03c0e46b2fa 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-10-09 Yannick Moy + + * sem_prag.adb (Process_Compile_Time_Warning_Or_Error): Rewrite + pragmas as null statements in GNATprove mode. + 2018-10-09 Eric Botcazou * exp_ch6.adb (Add_Call_By_Copy_Code): Initialize the temporary diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 7a71f533a43..2293f73cbd5 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -7570,6 +7570,17 @@ package body Sem_Prag is -- Start of processing for Process_Compile_Time_Warning_Or_Error begin + -- In GNATprove mode, pragmas Compile_Time_Error and + -- Compile_Time_Warning are ignored, as the analyzer may not have the + -- same information as the compiler (in particular regarding size of + -- objects decided in gigi) so it makes no sense to issue an error or + -- warning in GNATprove. + + if GNATprove_Mode then + Rewrite (N, Make_Null_Statement (Loc)); + return; + end if; + Check_Arg_Count (2); Check_No_Identifiers; Check_Arg_Is_OK_Static_Expression (Arg2, Standard_String);