Patchwork [Ada] Deferred constants are not always compile time known values in Alfa mode

login
register
mail settings
Submitter Arnaud Charlet
Date May 15, 2012, 9:27 a.m.
Message ID <20120515092710.GA25720@adacore.com>
Download mbox | patch
Permalink /patch/159271/
State New
Headers show

Comments

Arnaud Charlet - May 15, 2012, 9:27 a.m.
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  <moy@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.

Patch

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;