This patch corrects the mechanism which ensures that a package with a null
Abstract_State does not introduce hidden state, by ignoring internal states
and variables because they do not represent the "source" hidden state.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-07-16 Hristian Kirtchev <kirtc...@adacore.com>
gcc/ada/
* sem_util.adb (Check_No_Hidden_State): Ignore internally-generated
states and variables.
gcc/testsuite/
* gnat.dg/abstract_state1.adb, gnat.dg/abstract_state1.ads: New
testcase.
--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -3228,6 +3228,13 @@ package body Sem_Util is
begin
pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
+ -- Nothing to do for internally-generated abstract states and variables
+ -- because they do not represent the hidden state of the source unit.
+
+ if not Comes_From_Source (Id) then
+ return;
+ end if;
+
-- Find the proper context where the object or state appears
Scop := Scope (Id);
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/abstract_state1.adb
@@ -0,0 +1,5 @@
+-- { dg-do compile }
+
+package body Abstract_State1 is
+ procedure Foo is null;
+end Abstract_State1;
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/abstract_state1.ads
@@ -0,0 +1,24 @@
+package Abstract_State1
+ with Abstract_State => null,
+ Initializes => null
+is
+ type Complex (B : Boolean) is tagged private;
+ type No_F is tagged private;
+ X : constant No_F;
+
+ procedure Foo;
+
+private
+ type Complex (B : Boolean) is tagged record
+ G : Integer;
+ case B is
+ when True =>
+ F : Integer;
+ when False =>
+ null;
+ end case;
+ end record;
+
+ type No_F is new Complex (False) with null record;
+ X : constant No_F := (B => False, G => 7);
+end Abstract_State1;