@@ -10337,8 +10337,30 @@ package body Exp_Ch4 is
Flag : Entity_Id;
Scheme : Node_Id;
Stmts : List_Id;
+ Var : Entity_Id;
begin
+ -- Ensure that the bound variable is properly frozen. We must do
+ -- this before expansion because the expression is about to be
+ -- converted into a loop, and resulting freeze nodes may end up
+ -- in the wrong place in the tree.
+
+ if Present (Iter_Spec) then
+ Var := Defining_Identifier (Iter_Spec);
+ else
+ Var := Defining_Identifier (Loop_Spec);
+ end if;
+
+ declare
+ P : Node_Id := Parent (N);
+ begin
+ while Nkind (P) in N_Subexpr loop
+ P := Parent (P);
+ end loop;
+
+ Freeze_Before (P, Etype (Var));
+ end;
+
-- Create the declaration of the flag which tracks the status of the
-- quantified expression. Generate:
new file mode 100644
@@ -0,0 +1,5 @@
+-- { dg-do compile }
+
+package body Assert2 is
+ procedure Dummy is null;
+end Assert2;
new file mode 100644
@@ -0,0 +1,15 @@
+package Assert2
+ with SPARK_Mode
+is
+ type Living is new Integer;
+ function Is_Martian (Unused : Living) return Boolean is (False);
+
+ function Is_Green (Unused : Living) return Boolean is (True);
+
+ pragma Assert
+ (for all M in Living => (if Is_Martian (M) then Is_Green (M)));
+ pragma Assert
+ (for all M in Living => (if Is_Martian (M) then not Is_Green (M)));
+
+ procedure Dummy;
+end Assert2;