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;