From 56730418631c887e3c20f6529ed9399b80b50915 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Mon, 8 Jul 2019 08:14:15 +0000 Subject: [PATCH] [Ada] Set dummy Etype for the fake __HEAP entity in GNATprove GNATprove represents reads and writes via pointers as operations on a fake __HEAP entity. This entity already had various properties set to dummy values (e.g. Scope set to Standard_Standard), so that it can be processed like other entities without crashing and not special-cased everywhere. Now it also has a dummy Etype, so it can be processed with Is_Single_Concurrent_Object. The modified code is only executed by GNATprove; frontend is not affected. 2019-07-08 Piotr Trojanek gcc/ada/ * lib-xref-spark_specific.adb (Create_Heap): Set dummy Etype for the fake __HEAP entity. From-SVN: r273216 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/lib-xref-spark_specific.adb | 1 + 2 files changed, 6 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6ed43390ea2..afa238184db 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-08 Piotr Trojanek + + * lib-xref-spark_specific.adb (Create_Heap): Set dummy Etype for + the fake __HEAP entity. + 2019-07-08 Daniel Mercier * gnat1drv.adb: Suppress warnings on memory representation in diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 36aaefbce15..0ad704454f4 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -298,6 +298,7 @@ package body SPARK_Specific is Set_Ekind (Heap, E_Variable); Set_Is_Internal (Heap, True); + Set_Etype (Heap, Standard_Void_Type); Set_Scope (Heap, Standard_Standard); Set_Has_Fully_Qualified_Name (Heap); end Create_Heap; -- 2.30.2