Commit aca670a0 by Arnaud Charlet

[multiple changes]

2014-06-13  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Add local
	variable Missing_Parentheses. Emit an error when a state
	declaration with options appears without parentheses. Add a
	guard to prevent a bogus error when a state declaration may be
	interpreted as an option if a previous declaration with options
	was not parenthesized.

2014-06-13  Robert Dewar  <dewar@adacore.com>

	* checks.adb: Validate_Alignment_Check_Warnings: New procedure
	(Apply_Address_Clause_Check): Make Aligment_Warnings table entry.
	* checks.ads (Alignment_Warnings_Record): New type.
	(Alignment_Warnings): New table
	(Validate_Alignment_Check_Warnings): New procedure.
	* errout.adb (Delete_Warning_And_Continuations): New procedure
	(Error_Msg_Internal): Set Warning_Msg (Delete_Warning): Handle
	Warnings_Treated_As_Errors (Finalize): Minor reformatting
	* errout.ads (Warning_Msg): New variable
	(Delete_Warning_And_Continuations): New procedure
	* erroutc.adb (Delete_Msg): Handle Warnings_Treated_As_Errors count.
	* gnat1drv.adb (Post_Compilation_Validation_Checks): New procedure.

2014-06-13  Ed Schonberg  <schonberg@adacore.com>

	* a-coinho.adb, a-coinho.ads: Add Reference machinery.

From-SVN: r211627
parent d2adb45e
2014-06-13 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Analyze_Pragma): Add local
variable Missing_Parentheses. Emit an error when a state
declaration with options appears without parentheses. Add a
guard to prevent a bogus error when a state declaration may be
interpreted as an option if a previous declaration with options
was not parenthesized.
2014-06-13 Robert Dewar <dewar@adacore.com>
* checks.adb: Validate_Alignment_Check_Warnings: New procedure
(Apply_Address_Clause_Check): Make Aligment_Warnings table entry.
* checks.ads (Alignment_Warnings_Record): New type.
(Alignment_Warnings): New table
(Validate_Alignment_Check_Warnings): New procedure.
* errout.adb (Delete_Warning_And_Continuations): New procedure
(Error_Msg_Internal): Set Warning_Msg (Delete_Warning): Handle
Warnings_Treated_As_Errors (Finalize): Minor reformatting
* errout.ads (Warning_Msg): New variable
(Delete_Warning_And_Continuations): New procedure
* erroutc.adb (Delete_Msg): Handle Warnings_Treated_As_Errors count.
* gnat1drv.adb (Post_Compilation_Validation_Checks): New procedure.
2014-06-13 Ed Schonberg <schonberg@adacore.com>
* a-coinho.adb, a-coinho.ads: Add Reference machinery.
2014-06-13 Hristian Kirtchev <kirtchev@adacore.com>
* errout.adb (SPARK_Msg_N): New routine.
(SPARK_Msg_NE): New routine.
* errout.ads Add a section on SPARK-related error routines.
......
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2012, Free Software Foundation, Inc. --
-- Copyright (C) 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- --
......@@ -62,6 +62,13 @@ package body Ada.Containers.Indefinite_Holders is
Container.Busy := 0;
end Adjust;
overriding procedure Adjust (Control : in out Reference_Control_Type) is
begin
if Control.Container /= null then
Control.Container.Busy := Control.Container.Busy + 1;
end if;
end Adjust;
------------
-- Assign --
------------
......@@ -94,6 +101,20 @@ package body Ada.Containers.Indefinite_Holders is
Free (Container.Element);
end Clear;
------------------------
-- Constant_Reference --
------------------------
function Constant_Reference
(Container : aliased Holder) return Constant_Reference_Type
is
Ref : constant Constant_Reference_Type :=
(Element => Container.Element,
Control => (Controlled with Container'Unrestricted_Access));
begin
return Ref;
end Constant_Reference;
----------
-- Copy --
----------
......@@ -101,9 +122,9 @@ package body Ada.Containers.Indefinite_Holders is
function Copy (Source : Holder) return Holder is
begin
if Source.Element = null then
return (AF.Controlled with null, 0);
return (Controlled with null, 0);
else
return (AF.Controlled with new Element_Type'(Source.Element.all), 0);
return (Controlled with new Element_Type'(Source.Element.all), 0);
end if;
end Copy;
......@@ -133,6 +154,16 @@ package body Ada.Containers.Indefinite_Holders is
Free (Container.Element);
end Finalize;
overriding procedure Finalize (Control : in out Reference_Control_Type)
is
begin
if Control.Container /= null then
Control.Container.Busy := Control.Container.Busy - 1;
end if;
Control.Container := null;
end Finalize;
--------------
-- Is_Empty --
--------------
......@@ -207,6 +238,36 @@ package body Ada.Containers.Indefinite_Holders is
end if;
end Read;
procedure Read
(Stream : not null access Root_Stream_Type'Class;
Item : out Constant_Reference_Type)
is
begin
raise Program_Error with "attempt to stream reference";
end Read;
procedure Read
(Stream : not null access Root_Stream_Type'Class;
Item : out Reference_Type)
is
begin
raise Program_Error with "attempt to stream reference";
end Read;
---------------
-- Reference --
---------------
function Reference
(Container : aliased in out Holder) return Reference_Type
is
Ref : constant Reference_Type :=
(Element => Container.Element,
Control => (Controlled with Container'Unrestricted_Access));
begin
return Ref;
end Reference;
---------------------
-- Replace_Element --
---------------------
......@@ -247,7 +308,7 @@ package body Ada.Containers.Indefinite_Holders is
pragma Unsuppress (Accessibility_Check);
begin
return (AF.Controlled with new Element_Type'(New_Item), 0);
return (Controlled with new Element_Type'(New_Item), 0);
end To_Holder;
--------------------
......@@ -293,5 +354,20 @@ package body Ada.Containers.Indefinite_Holders is
Element_Type'Output (Stream, Container.Element.all);
end if;
end Write;
procedure Write
(Stream : not null access Root_Stream_Type'Class;
Item : Reference_Type)
is
begin
raise Program_Error with "attempt to stream reference";
end Write;
procedure Write
(Stream : not null access Root_Stream_Type'Class;
Item : Constant_Reference_Type)
is
begin
raise Program_Error with "attempt to stream reference";
end Write;
end Ada.Containers.Indefinite_Holders;
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2011, Free Software Foundation, Inc. --
-- Copyright (C) 2014, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
......@@ -62,10 +62,29 @@ package Ada.Containers.Indefinite_Holders is
procedure Query_Element
(Container : Holder;
Process : not null access procedure (Element : Element_Type));
procedure Update_Element
(Container : Holder;
Process : not null access procedure (Element : in out Element_Type));
type Constant_Reference_Type
(Element : not null access constant Element_Type) is private
with
Implicit_Dereference => Element;
type Reference_Type
(Element : not null access Element_Type) is private
with
Implicit_Dereference => Element;
function Constant_Reference
(Container : aliased Holder) return Constant_Reference_Type;
pragma Inline (Constant_Reference);
function Reference
(Container : aliased in out Holder) return Reference_Type;
pragma Inline (Reference);
procedure Assign (Target : in out Holder; Source : Holder);
function Copy (Source : Holder) return Holder;
......@@ -74,10 +93,14 @@ package Ada.Containers.Indefinite_Holders is
private
package AF renames Ada.Finalization;
use Ada.Finalization;
use Ada.Streams;
type Element_Access is access all Element_Type;
type Holder_Access is access all Holder;
for Holder_Access'Storage_Size use 0;
procedure Read
(Stream : not null access Ada.Streams.Root_Stream_Type'Class;
Container : out Holder);
......@@ -96,6 +119,53 @@ private
overriding procedure Adjust (Container : in out Holder);
overriding procedure Finalize (Container : in out Holder);
Empty_Holder : constant Holder := (AF.Controlled with null, 0);
type Reference_Control_Type is new Controlled with
record
Container : Holder_Access;
end record;
overriding procedure Adjust (Control : in out Reference_Control_Type);
pragma Inline (Adjust);
overriding procedure Finalize (Control : in out Reference_Control_Type);
pragma Inline (Finalize);
type Constant_Reference_Type
(Element : not null access constant Element_Type)
is record
Control : Reference_Control_Type;
end record;
procedure Write
(Stream : not null access Root_Stream_Type'Class;
Item : Constant_Reference_Type);
for Constant_Reference_Type'Write use Write;
procedure Read
(Stream : not null access Root_Stream_Type'Class;
Item : out Constant_Reference_Type);
for Constant_Reference_Type'Read use Read;
type Reference_Type
(Element : not null access Element_Type)
is record
Control : Reference_Control_Type;
end record;
procedure Write
(Stream : not null access Root_Stream_Type'Class;
Item : Reference_Type);
for Reference_Type'Write use Write;
procedure Read
(Stream : not null access Root_Stream_Type'Class;
Item : out Reference_Type);
for Reference_Type'Read use Read;
Empty_Holder : constant Holder := (Controlled with null, 0);
end Ada.Containers.Indefinite_Holders;
......@@ -27,15 +27,14 @@ with Atree; use Atree;
with Casing; use Casing;
with Debug; use Debug;
with Einfo; use Einfo;
with Errout; use Errout;
with Elists; use Elists;
with Eval_Fat; use Eval_Fat;
with Exp_Ch11; use Exp_Ch11;
with Exp_Ch2; use Exp_Ch2;
with Exp_Ch4; use Exp_Ch4;
with Exp_Ch11; use Exp_Ch11;
with Exp_Pakd; use Exp_Pakd;
with Exp_Util; use Exp_Util;
with Elists; use Elists;
with Expander; use Expander;
with Eval_Fat; use Eval_Fat;
with Freeze; use Freeze;
with Lib; use Lib;
with Nlists; use Nlists;
......@@ -47,9 +46,9 @@ with Rident; use Rident;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Eval; use Sem_Eval;
with Sem_Ch3; use Sem_Ch3;
with Sem_Ch8; use Sem_Ch8;
with Sem_Eval; use Sem_Eval;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sem_Warn; use Sem_Warn;
......@@ -589,7 +588,7 @@ package body Checks is
Expr : Node_Id;
-- Address expression (not necessarily the same as Aexp, for example
-- when Aexp is a reference to a constant, in which case Expr gets
-- reset to reference the value expression of the constant.
-- reset to reference the value expression of the constant).
procedure Compile_Time_Bad_Alignment;
-- Post error warnings when alignment is known to be incompatible. Note
......@@ -758,21 +757,32 @@ package body Checks is
Prefix => New_Occurrence_Of (E, Loc),
Attribute_Name => Name_Alignment)),
Right_Opnd => Make_Integer_Literal (Loc, Uint_0)),
Reason => PE_Misaligned_Address_Value));
Reason => PE_Misaligned_Address_Value));
Warning_Msg := No_Error_Msg;
Analyze (First (Actions (N)), Suppress => All_Checks);
-- If the address clause generates an alignment check and we are
-- in ZFP or some restricted run-time, add a warning to explain
-- the propagation warning that is generated by the check.
-- If the address clause generated a warning message (for example,
-- from Warn_On_Non_Local_Exception mode with the active restriction
-- No_Exception_Propagation).
if Warning_Msg /= No_Error_Msg then
-- If the expression has a known at compile time value, then
-- once we know the alignment of the type, we can check if the
-- exception will be raised or not, and if not, we don't need
-- the warning so we will kill the warning later on.
if Compile_Time_Known_Value (Expr) then
Alignment_Warnings.Append
((E => E, A => Expr_Value (Expr), W => Warning_Msg));
end if;
-- Add explanation of the warning that is generated by the check
if Nkind (First (Actions (N))) = N_Raise_Program_Error
and then not Warnings_Off (E)
and then Warn_On_Non_Local_Exception
and then Restriction_Active (No_Exception_Propagation)
then
Error_Msg_N
("address value may be incompatible with alignment of object?",
N);
("\address value may be incompatible with alignment "
& "of object?X?", AC);
end if;
return;
......@@ -9483,6 +9493,26 @@ package body Checks is
end if;
end Tag_Checks_Suppressed;
---------------------------------------
-- Validate_Alignment_Check_Warnings --
---------------------------------------
procedure Validate_Alignment_Check_Warnings is
begin
for J in Alignment_Warnings.First .. Alignment_Warnings.Last loop
declare
AWR : Alignment_Warnings_Record
renames Alignment_Warnings.Table (J);
begin
if Known_Alignment (AWR.E)
and then AWR.A mod Alignment (AWR.E) = 0
then
Delete_Warning_And_Continuations (AWR.W);
end if;
end;
end loop;
end Validate_Alignment_Check_Warnings;
--------------------------
-- Validity_Check_Range --
--------------------------
......
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- 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- --
......@@ -35,6 +35,7 @@
-- This always occurs whether checks are suppressed or not. Dynamic range
-- checks are, of course, not inserted if checks are suppressed.
with Errout; use Errout;
with Namet; use Namet;
with Table;
with Types; use Types;
......@@ -79,6 +80,53 @@ package Checks is
-- Returns current overflow checking mode, taking into account whether
-- we are inside an assertion expression.
------------------------------------------
-- Control of Alignment Check Warnings --
------------------------------------------
-- When we have address clauses, there is an issue of whether the address
-- specified is appropriate to the alignment. In the general case where the
-- address is dynamic, we generate a check and a possible warning (this
-- warning occurs for example if we have a restricted run time with the
-- restriction No_Exception_Propagation). We also issue this warning in
-- the case where the address is static, but we don't know the alignment
-- at the time we process the address clause. In such a case, we issue the
-- warning, but we may be able to find out later (after the back end has
-- annotated the actual alignment chosen) that the warning was not needed.
-- To deal with deleting these potentially annoying warnings, we save the
-- warning information in a table, and then delete the waranings in the
-- post compilation validation stage if we can tell that the check would
-- never fail (in general the back end will also optimize away the check
-- in such cases).
-- Table used to record information
type Alignment_Warnings_Record is record
E : Entity_Id;
-- Entity whose alignment possibly warrants a warning
A : Uint;
-- Compile time known value of address clause for which the alignment
-- is to be checked once we know the alignment.
W : Error_Msg_Id;
-- Id of warning message we might delete
end record;
package Alignment_Warnings is new Table.Table (
Table_Component_Type => Alignment_Warnings_Record,
Table_Index_Type => Int,
Table_Low_Bound => 0,
Table_Initial => 10,
Table_Increment => 200,
Table_Name => "Alignment_Warnings");
procedure Validate_Alignment_Check_Warnings;
-- This routine is called after back annotation of type data to delete any
-- alignment warnings that turn out to be false alarms, based on knowing
-- the actual alignment, and a compile-time known alignment value.
-------------------------------------------
-- Procedures to Activate Checking Flags --
-------------------------------------------
......
......@@ -249,6 +249,38 @@ package body Errout is
end if;
end Compilation_Errors;
--------------------------------------
-- Delete_Warning_And_Continuations --
--------------------------------------
procedure Delete_Warning_And_Continuations (Msg : Error_Msg_Id) is
Id : Error_Msg_Id;
begin
pragma Assert (not Errors.Table (Msg).Msg_Cont);
Id := Msg;
loop
declare
M : Error_Msg_Object renames Errors.Table (Id);
begin
if not M.Deleted then
M.Deleted := True;
Warnings_Detected := Warnings_Detected - 1;
if M.Warn_Err then
Warnings_Treated_As_Errors := Warnings_Treated_As_Errors + 1;
end if;
end if;
Id := M.Next;
exit when Id = No_Error_Msg;
exit when not Errors.Table (Id).Msg_Cont;
end;
end loop;
end Delete_Warning_And_Continuations;
---------------
-- Error_Msg --
---------------
......@@ -1117,6 +1149,14 @@ package body Errout is
end if;
end if;
-- Record warning message issued
if Errors.Table (Cur_Msg).Warn
and then not Errors.Table (Cur_Msg).Msg_Cont
then
Warning_Msg := Cur_Msg;
end if;
-- If too many warnings turn off warnings
if Maximum_Messages /= 0 then
......@@ -1296,7 +1336,7 @@ package body Errout is
F : Error_Msg_Id;
procedure Delete_Warning (E : Error_Msg_Id);
-- Delete a message if not already deleted and adjust warning count
-- Delete a warning msg if not already deleted and adjust warning count
--------------------
-- Delete_Warning --
......@@ -1307,10 +1347,14 @@ package body Errout is
if not Errors.Table (E).Deleted then
Errors.Table (E).Deleted := True;
Warnings_Detected := Warnings_Detected - 1;
if Errors.Table (E).Warn_Err then
Warnings_Treated_As_Errors := Warnings_Treated_As_Errors + 1;
end if;
end if;
end Delete_Warning;
-- Start of message for Finalize
-- Start of processing for Finalize
begin
-- Set Prev pointers
......@@ -1360,11 +1404,12 @@ package body Errout is
then
Delete_Warning (Cur);
-- If this is a continuation, delete previous messages
-- If this is a continuation, delete previous parts of message
F := Cur;
while Errors.Table (F).Msg_Cont loop
F := Errors.Table (F).Prev;
exit when F = No_Error_Msg;
Delete_Warning (F);
end loop;
......
......@@ -615,6 +615,16 @@ package Errout is
-- A constant which is different from any value returned by Get_Error_Id.
-- Typically used by a client to indicate absense of a saved Id value.
Warning_Msg : Error_Msg_Id := No_Error_Msg;
-- This is set if a warning message is generated to the ID of the resulting
-- message. Continuation messages have no effect. It is legitimate for the
-- client to set this to No_Error_Msg and then test it to see if a warning
-- message has been issued.
procedure Delete_Warning_And_Continuations (Msg : Error_Msg_Id);
-- Deletes the given warning message and all its continuations. This is
-- typically used in conjunction with reading the value of Warning_Msg.
function Get_Msg_Id return Error_Msg_Id renames Erroutc.Get_Msg_Id;
-- Returns the Id of the message most recently posted using one of the
-- Error_Msg routines.
......
......@@ -140,6 +140,11 @@ package body Erroutc is
if Errors.Table (D).Warn or else Errors.Table (D).Style then
Warnings_Detected := Warnings_Detected - 1;
if Errors.Table (D).Warn_Err then
Warnings_Treated_As_Errors :=
Warnings_Treated_As_Errors + 1;
end if;
else
Total_Errors_Detected := Total_Errors_Detected - 1;
......
......@@ -25,6 +25,7 @@
with Atree; use Atree;
with Back_End; use Back_End;
with Checks;
with Comperr;
with Csets; use Csets;
with Debug; use Debug;
......@@ -110,6 +111,13 @@ procedure Gnat1drv is
-- Called when we are not generating code, to check if -gnatR was requested
-- and if so, explain that we will not be honoring the request.
procedure Post_Compilation_Validation_Checks;
-- This procedure performs various validation checks that have to be left
-- to the end of the compilation process, after generating code but before
-- issuing error messages. In particular, these checks generally require
-- the information provided by the back end in back annotation of declared
-- entities (e.g. actual size and alignment values chosen by the back end).
----------------------------
-- Adjust_Global_Switches --
----------------------------
......@@ -746,6 +754,35 @@ procedure Gnat1drv is
end if;
end Check_Rep_Info;
----------------------------------------
-- Post_Compilation_Validation_Checks --
----------------------------------------
procedure Post_Compilation_Validation_Checks is
begin
-- Validate alignment check warnings. In some cases we generate warnings
-- about possible alignment errors because we don't know the alignment
-- that will be chosen by the back end. This routine is in charge of
-- getting rid of those warnings if we can tell they are not needed.
Checks.Validate_Alignment_Check_Warnings;
-- Validate unchecked conversions (using the values for size and
-- alignment annotated by the backend where possible).
Sem_Ch13.Validate_Unchecked_Conversions;
-- Validate address clauses (again using alignment values annotated
-- by the backend where possible).
Sem_Ch13.Validate_Address_Clauses;
-- Validate independence pragmas (again using values annotated by
-- the back end for component layout etc.)
Sem_Ch13.Validate_Independence;
end Post_Compilation_Validation_Checks;
-- Start of processing for Gnat1drv
begin
......@@ -897,9 +934,7 @@ begin
if Compilation_Errors then
Treepr.Tree_Dump;
Sem_Ch13.Validate_Unchecked_Conversions;
Sem_Ch13.Validate_Address_Clauses;
Sem_Ch13.Validate_Independence;
Post_Compilation_Validation_Checks;
Errout.Output_Messages;
Namet.Finalize;
......@@ -1095,9 +1130,7 @@ begin
Set_Standard_Output;
Sem_Ch13.Validate_Unchecked_Conversions;
Sem_Ch13.Validate_Address_Clauses;
Sem_Ch13.Validate_Independence;
Post_Compilation_Validation_Checks;
Errout.Finalize (Last_Call => True);
Errout.Output_Messages;
Treepr.Tree_Dump;
......@@ -1137,9 +1170,7 @@ begin
or else Targparm.Frontend_Layout_On_Target
or else Targparm.VM_Target /= No_VM)
then
Sem_Ch13.Validate_Unchecked_Conversions;
Sem_Ch13.Validate_Address_Clauses;
Sem_Ch13.Validate_Independence;
Post_Compilation_Validation_Checks;
Errout.Finalize (Last_Call => True);
Errout.Output_Messages;
Write_ALI (Object => False);
......@@ -1189,20 +1220,9 @@ begin
Exp_CG.Generate_CG_Output;
-- Validate unchecked conversions (using the values for size and
-- alignment annotated by the backend where possible).
Sem_Ch13.Validate_Unchecked_Conversions;
-- Validate address clauses (again using alignment values annotated
-- by the backend where possible).
Sem_Ch13.Validate_Address_Clauses;
-- Perform post compilation validation checks
-- Validate independence pragmas (again using values annotated by
-- the back end for component layout etc.)
Sem_Ch13.Validate_Independence;
Post_Compilation_Validation_Checks;
-- Now we complete output of errors, rep info and the tree info. These
-- are delayed till now, since it is perfectly possible for gigi to
......
......@@ -10133,6 +10133,9 @@ package body Sem_Prag is
-- ABSTRACT_STATE ::= name
when Pragma_Abstract_State => Abstract_State : declare
Missing_Parentheses : Boolean := False;
-- Flag set when a state declaration with options is not properly
-- parenthesized.
-- Flags used to verify the consistency of states
......@@ -10569,25 +10572,63 @@ package body Sem_Prag is
Opt := First (Expressions (State));
while Present (Opt) loop
if Nkind (Opt) = N_Identifier
and then Chars (Opt) = Name_External
then
Analyze_External_Option (Opt);
if Nkind (Opt) = N_Identifier then
if Chars (Opt) = Name_External then
Analyze_External_Option (Opt);
-- Option Part_Of without an encapsulating state is
-- illegal. (SPARK RM 7.1.4(9)).
-- When an illegal option Part_Of is without a parent
-- state, it appears in the list of expression of the
-- aggregate rather than the component associations
-- (SPARK RM 7.1.4(9)).
elsif Chars (Opt) = Name_Part_Of then
SPARK_Msg_N
("indicator Part_Of must denote an abstract "
& "state", Opt);
-- Do not emit an error message when a previous state
-- declaration with options was not parenthesized as
-- the option is actually another state declaration.
--
-- with Abstract_State
-- (State_1 with ..., -- missing parentheses
-- (State_2 with ...),
-- State_3) -- ok state declaration
elsif Missing_Parentheses then
null;
-- Otherwise the option is not allowed. Note that it
-- is not possible to distinguish between an option
-- and a state declaration when a previous state with
-- options not properly parentheses.
--
-- with Abstract_State
-- (State_1 with ..., -- missing parentheses
-- State_2); -- could be an option
elsif Chars (Opt) = Name_Part_Of then
else
SPARK_Msg_N
("simple option not allowed in state declaration",
Opt);
end if;
-- Catch a case where missing parentheses around a state
-- declaration with options cause a subsequent state
-- declaration with options to be treated as an option.
--
-- with Abstract_State
-- (State_1 with ..., -- missing parentheses
-- (State_2 with ...))
elsif Nkind (Opt) = N_Extension_Aggregate then
Missing_Parentheses := True;
SPARK_Msg_N
("indicator Part_Of must denote an abstract state",
Opt);
("state declaration must be parenthesized",
Ancestor_Part (State));
-- Otherwise the option is malformed
else
SPARK_Msg_N
("simple option not allowed in state declaration",
Opt);
SPARK_Msg_N ("malformed option", Opt);
end if;
Next (Opt);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment