From b5eccd0cbd46ba49b361d67597284a94a4fdd8b7 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 24 Feb 2014 18:14:40 +0100 Subject: [PATCH] [multiple changes] 2014-02-24 Thomas Quinot * g-sercom-mingw.adb (Open): Fix incorrect test for error return value. * erroutc.adb: Minor reformatting. 2014-02-24 Hristian Kirtchev * sem_prag.adb (Check_Clause_Syntax): Account for a solitary input item in a dependency list. 2014-02-24 Yannick Moy * gnat1drv.adb (Adjust_Global_Switches): Do not use validity checks at all in GNATprove_Mode. From-SVN: r208089 --- gcc/ada/ChangeLog | 16 ++++++++++++++++ gcc/ada/erroutc.adb | 4 ++-- gcc/ada/g-sercom-mingw.adb | 2 +- gcc/ada/gnat1drv.adb | 6 ++++++ gcc/ada/sem_prag.adb | 23 ++++++++++++++--------- 5 files changed, 39 insertions(+), 12 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b4ee2084caf..cc6e73bb7c0 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,19 @@ +2014-02-24 Thomas Quinot + + * g-sercom-mingw.adb (Open): Fix incorrect test for error return + value. + * erroutc.adb: Minor reformatting. + +2014-02-24 Hristian Kirtchev + + * sem_prag.adb (Check_Clause_Syntax): Account + for a solitary input item in a dependency list. + +2014-02-24 Yannick Moy + + * gnat1drv.adb (Adjust_Global_Switches): Do not + use validity checks at all in GNATprove_Mode. + 2014-02-24 Robert Dewar * g-sercom-mingw.adb, g-sercom-linux.adb, sem_prag.adb, freeze.adb, diff --git a/gcc/ada/erroutc.adb b/gcc/ada/erroutc.adb index 8604f2590db..53b80b1fd43 100644 --- a/gcc/ada/erroutc.adb +++ b/gcc/ada/erroutc.adb @@ -481,8 +481,8 @@ package body Erroutc is Max := Integer (Length - Column + 1); declare - Txt : constant String := Text.all & Warn_Tag.all; - Len : constant Natural := Txt'Length; + Txt : constant String := Text.all & Warn_Tag.all; + Len : constant Natural := Txt'Length; begin -- For warning, add "warning: " unless msg starts with "info: " diff --git a/gcc/ada/g-sercom-mingw.adb b/gcc/ada/g-sercom-mingw.adb index 0144c235697..292ca8f563e 100644 --- a/gcc/ada/g-sercom-mingw.adb +++ b/gcc/ada/g-sercom-mingw.adb @@ -129,7 +129,7 @@ package body GNAT.Serial_Communications is dwFlagsAndAttributes => 0, hTemplateFile => 0); - if Port.H.all = 0 then + if Port.H.all = Port_Data (INVALID_HANDLE_VALUE) then Raise_Error ("cannot open com port"); end if; end Open; diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index d6df2a0eeb3..d7d7d67f0f9 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -384,6 +384,12 @@ procedure Gnat1drv is Assertions_Enabled := True; + -- Disable validity checks, since it generates code raising + -- exceptions for invalid data, which confuses GNATprove. Invalid + -- data is directly detected by GNATprove's flow analysis. + + Validity_Checks_On := False; + -- Turn off style check options since we are not interested in any -- front-end warnings when we are getting SPARK output. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 9f4ce2a72a2..b7321e8637d 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -24261,17 +24261,22 @@ package body Sem_Prag is -- Input items - if Nkind (Inputs) = N_Aggregate - and then Present (Expressions (Inputs)) - then - Input := First (Expressions (Inputs)); - while Present (Input) loop - Check_Item_Syntax (Input); - Next (Input); - end loop; + if Nkind (Inputs) = N_Aggregate then + if Present (Expressions (Inputs)) then + Input := First (Expressions (Inputs)); + while Present (Input) loop + Check_Item_Syntax (Input); + Next (Input); + end loop; + + else + Error_Msg_N ("malformed input dependency list", Inputs); + end if; + + -- Single input item else - Error_Msg_N ("malformed input dependency list", Inputs); + Check_Item_Syntax (Inputs); end if; end Check_Clause_Syntax;