Outside of the scope of their full view, deferred constants are not anymore
considered as compile time known values in Alfa mode. This allows parameterized
formal verification, in which a deferred constant value if not known from
client units.
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-05-15 Yannick Moy <m...@adacore.com>
* sem_aux.ads: Correct typo.
* sem_eval.adb (Compile_Time_Known_Value): Return False in Alfa
mode for a deferred constant when outside of the scope of its
full view.
Index: sem_aux.ads
===================================================================
--- sem_aux.ads (revision 187501)
+++ sem_aux.ads (working copy)
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2012, 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- --
@@ -99,7 +99,7 @@
function Constant_Value (Ent : Entity_Id) return Node_Id;
-- Ent is a variable, constant, named integer, or named real entity. This
-- call obtains the initialization expression for the entity. Will return
- -- Empty for for a deferred constant whose full view is not available or
+ -- Empty for a deferred constant whose full view is not available or
-- in some other cases of internal entities, which cannot be treated as
-- constants from the point of view of constant folding. Empty is also
-- returned for variables with no initialization expression.
Index: sem_eval.adb
===================================================================
--- sem_eval.adb (revision 187501)
+++ sem_eval.adb (working copy)
@@ -1302,7 +1302,16 @@
if Ekind (E) = E_Enumeration_Literal then
return True;
- elsif Ekind (E) = E_Constant then
+ -- In Alfa mode, the value of deferred constants should be ignored
+ -- outside the scope of their full view. This allows parameterized
+ -- formal verification, in which a deferred constant value if not
+ -- known from client units.
+
+ elsif Ekind (E) = E_Constant
+ and then not (Alfa_Mode
+ and then Present (Full_View (E))
+ and then not In_Open_Scopes (Scope (E)))
+ then
V := Constant_Value (E);
return Present (V) and then Compile_Time_Known_Value (V);
end if;
