In GNATprove mode for formal verification, some treatment typically only
done during expansion needs to be performed on the tree, but it should
not be applied inside generics. Otherwise, this breaks the name
resolution mechanism for genetic instances. This completes a previous
similar fix.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-19 Yannick Moy <m...@adacore.com>
* expander.adb (Expand): Do nothing inside generics.
* sem_aggr.adb (Aggregate_Constraint_Checks): Do nothing inside
generics.
Index: sem_aggr.adb
===================================================================
--- sem_aggr.adb (revision 207879)
+++ sem_aggr.adb (working copy)
@@ -459,7 +459,9 @@
-- added in the tree, so that the formal verification can rely on those
-- to be present.
- if not (Expander_Active or GNATprove_Mode) or In_Spec_Expression then
+ if not Expander_Active
+ and (Inside_A_Generic or not Full_Analysis or not GNATprove_Mode)
+ then
return;
end if;
Index: expander.adb
===================================================================
--- expander.adb (revision 207879)
+++ expander.adb (working copy)
@@ -90,7 +90,8 @@
-- analysis, in which case Full_Analysis = True or a pre-analysis in
-- which case Full_Analysis = False. See the spec of Sem for more info
-- on this. Additionally, the GNATprove_Mode flag indicates that a light
- -- expansion for formal verification should be used.
+ -- expansion for formal verification should be used. This expansion is
+ -- never done inside generics.
-- The second reason for the Expander_Active flag to be False is that
-- we are performing a pre-analysis. During pre-analysis all expansion
@@ -108,7 +109,9 @@
-- given that the expansion actions that would normally process it will
-- not take place. This prevents cascaded errors due to stack mismatch.
- 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
Set_Analyzed (N, Full_Analysis);
if Serious_Errors_Detected > 0 and then Scope_Is_Transient then
