From: Viljar Indus <in...@adacore.com>
Unsuccessful preanalyze_and_resolve still marks identifiers as Any_Id.
Override that result if an identifier matched an assertion level.
gcc/ada/ChangeLog:
* ghost.adb (Assertion_Level_From_Arg): Ensure that assertion level
is stored as the entity for its reference.
(Enables_Ghostness): Derive the result from whether or not the
an argument indicated an assertion level.
* tbuild.adb (Make_Assertion_Level): ensure that assertion levels
have a standard scope.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/ghost.adb | 34 ++++++++--------------------------
gcc/ada/tbuild.adb | 1 +
2 files changed, 9 insertions(+), 26 deletions(-)
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 4af4e4be93e..574f7f2cda4 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -161,11 +161,13 @@ package body Ghost is
-- Alternatively the argument could be an Assertion_Level
- if Nkind (Expr) = N_Identifier
- and then Present (Get_Assertion_Level (Chars (Expr)))
- then
+ if Nkind (Expr) = N_Identifier then
Level := Get_Assertion_Level (Chars (Expr));
if Present (Level) then
+ -- The identifier resolved to an assertion level. Override the
+ -- Any_Id from a failed resolution in pre-analysis.
+
+ Set_Entity (Expr, Level);
return Level;
end if;
end if;
@@ -1774,31 +1776,11 @@ package body Ghost is
-----------------------
function Enables_Ghostness (Arg : Node_Id) return Boolean is
- Expr : constant Node_Id := Get_Pragma_Arg (Arg);
-
begin
- -- Aspect Ghost without an expression enables ghostness
+ -- Ghostness is enabled if the argument implies a default assertion
+ -- level or it is explicitly a reference to an assertion level.
- if No (Expr) then
- return True;
- end if;
-
- -- Check if the expression matches a static boolean expression first
-
- Preanalyze_And_Resolve_Without_Errors (Expr);
- if Is_OK_Static_Expression (Expr) then
- return Is_True (Expr_Value (Expr));
- end if;
-
- -- Alternatively the argument could be an Assertion_Level
-
- if Nkind (Expr) = N_Identifier
- and then Present (Get_Assertion_Level (Chars (Expr)))
- then
- return True;
- end if;
-
- return False;
+ return Present (Assertion_Level_From_Arg (Arg));
end Enables_Ghostness;
-- Local variables
diff --git a/gcc/ada/tbuild.adb b/gcc/ada/tbuild.adb
index 57ea93260f1..2840707f2e9 100644
--- a/gcc/ada/tbuild.adb
+++ b/gcc/ada/tbuild.adb
@@ -162,6 +162,7 @@ package body Tbuild is
begin
Mutate_Ekind (Level, E_Assertion_Level);
Set_Etype (Level, Standard_Void_Type);
+ Set_Scope (Level, Standard_Standard);
return Level;
end Make_Assertion_Level;
--
2.43.0
