[multiple changes]

2014-02-24  Thomas Quinot  <quinot@adacore.com>

	* g-sercom-mingw.adb (Open): Fix incorrect test for error return
	value.
	* erroutc.adb: Minor reformatting.

2014-02-24  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Check_Clause_Syntax): Account
	for a solitary input item in a dependency list.

2014-02-24  Yannick Moy  <moy@adacore.com>

	* gnat1drv.adb (Adjust_Global_Switches): Do not
	use validity checks at all in GNATprove_Mode.

From-SVN: r208089

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b4ee2084caf767f2f753bd0303081f051c3034e3..cc6e73bb7c0fd6f8e84290d4ea09da5f1fedca49 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,19 @@
+2014-02-24  Thomas Quinot  <quinot@adacore.com>
+
+       * g-sercom-mingw.adb (Open): Fix incorrect test for error return
+       value.
+       * erroutc.adb: Minor reformatting.
+
+2014-02-24  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * sem_prag.adb (Check_Clause_Syntax): Account
+       for a solitary input item in a dependency list.
+
+2014-02-24  Yannick Moy  <moy@adacore.com>
+
+       * gnat1drv.adb (Adjust_Global_Switches): Do not
+       use validity checks at all in GNATprove_Mode.
+
 2014-02-24  Robert Dewar  <dewar@adacore.com>
 
        * 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 8604f2590db8f7e2e0f147f49f05690c8912a832..53b80b1fd439bddfb6a53c1545faffb606896c32 100644 (file)
--- 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 0144c235697f8dfae74e21fd18886bbd3f957127..292ca8f563efa4544cbb96376b37d572d638108d 100644 (file)
--- 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 d6df2a0eeb3797e867ff2201e104aba281e962a6..d7d7d67f0f925da0585749311de908a84b3af400 100644 (file)
--- 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 9f4ce2a72a2b82f1eee006e884159ff58bdb76bf..b7321e8637d58bed51953abfa03b970c66fd5550 100644 (file)
--- 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;