In the GNATprove mode for formal verification, side-effects are removed
from expressions when the corresponding procedure is called in the
frontend. This should only be done when not inside a generic, which is
both useless and harmful as it deactivates the mechanism for name
resolution of generic instances. Now fixed.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-19 Yannick Moy <m...@adacore.com>
* exp_util.adb (Remove_Side_Effects): Do not remove side-effects
inside a generic.
Index: exp_util.adb
===================================================================
--- exp_util.adb (revision 207892)
+++ exp_util.adb (working copy)
@@ -6638,9 +6638,12 @@
begin
-- Handle cases in which there is nothing to do. In GNATprove mode,
-- removal of side effects is useful for the light expansion of
- -- renamings.
+ -- renamings. This removal should only occur when not inside a
+ -- generic and not doing a pre-analysis.
- if not (Expander_Active or (Full_Analysis and GNATprove_Mode)) then
+ if not Expander_Active
+ and (Inside_A_Generic or not Full_Analysis or not GNATprove_Mode)
+ then
return;
end if;
