This patch modifies the parser to catch a case where the argument of SPARK
aspect Refined_State is not properly parenthesized.
------------
-- Source --
------------
-- no_parens.ads
package No_Parens
with SPARK_Mode => On,
Abstract_State => State
is
pragma Elaborate_Body;
end No_Parens;
-- no_parens.adb
package body No_Parens
with SPARK_Mode => On,
Refined_State => State => (Speed, Status)
is
Speed : Integer := 0;
Status : Integer := 0;
end No_Parens;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c no_parens.adb
no_parens.adb:3:25: missing "("
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-07-17 Hristian Kirtchev <kirtc...@adacore.com>
* par-ch13.adb (Get_Aspect_Specifications):
Catch a case where the argument of SPARK aspect Refined_State
is not properly parenthesized.
Index: par-ch13.adb
===================================================================
--- par-ch13.adb (revision 212640)
+++ par-ch13.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -308,8 +308,8 @@
end if;
-- Detect a common error where the non-null definition of
- -- aspect Depends, Global, Refined_Depends or Refined_Global
- -- must be enclosed in parentheses.
+ -- aspect Depends, Global, Refined_Depends, Refined_Global
+ -- or Refined_State lacks enclosing parentheses.
if Token /= Tok_Left_Paren and then Token /= Tok_Null then
@@ -400,6 +400,48 @@
Restore_Scan_State (Scan_State);
end if;
end;
+
+ -- Refined_State
+
+ elsif A_Id = Aspect_Refined_State then
+ if Token = Tok_Identifier then
+ declare
+ Scan_State : Saved_Scan_State;
+
+ begin
+ Save_Scan_State (Scan_State);
+ Scan; -- past state
+
+ -- The refinement contains a constituent, the whole
+ -- argument of Refined_State must be parenthesized.
+
+ -- with Refined_State => State => Constit
+
+ if Token = Tok_Arrow then
+ Restore_Scan_State (Scan_State);
+ Error_Msg_SC -- CODEFIX
+ ("missing ""(""");
+ Resync_Past_Malformed_Aspect;
+
+ -- Return when the current aspect is the last
+ -- in the list of specifications and the list
+ -- applies to a body.
+
+ if Token = Tok_Is then
+ return Aspects;
+ end if;
+
+ -- The refinement lacks constituents. Do not flag
+ -- this case as the error would be misleading. The
+ -- diagnostic is left to the analysis.
+
+ -- with Refined_State => State
+
+ else
+ Restore_Scan_State (Scan_State);
+ end if;
+ end;
+ end if;
end if;
end if;
