[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

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,

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: "

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;

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.
 

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;