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;