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
+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,
2014-02-24 Robert Dewar <dewar@adacore.com>
* g-sercom-mingw.adb, g-sercom-linux.adb, sem_prag.adb, freeze.adb,
Max := Integer (Length - Column + 1);
declare
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: "
begin
-- For warning, add "warning: " unless msg starts with "info: "
dwFlagsAndAttributes => 0,
hTemplateFile => 0);
dwFlagsAndAttributes => 0,
hTemplateFile => 0);
+ if Port.H.all = Port_Data (INVALID_HANDLE_VALUE) then
Raise_Error ("cannot open com port");
end if;
end Open;
Raise_Error ("cannot open com port");
end if;
end Open;
Assertions_Enabled := True;
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.
-- Turn off style check options since we are not interested in any
-- front-end warnings when we are getting SPARK output.
- 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
- Error_Msg_N ("malformed input dependency list", Inputs);
+ Check_Item_Syntax (Inputs);
end if;
end Check_Clause_Syntax;
end if;
end Check_Clause_Syntax;