In SPARK loop and subprogram variants we now allow expressions of any
discrete type or of Ada.Numerics.Big_Numbers.Big_Integers.Big_Integer
type. This requires a variant of Preanalyze_Assert_Expression that
doesn't force the expression to be of a particular type, similar to the
existing variant of Analyze_And_Resolve.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_ch3.ads, sem_ch3.adb (Preanalyze_Assert_Expression): Add a
variant that doesn't force preanalysis to yield a specific type.diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -40,6 +40,7 @@ with Exp_Disp; use Exp_Disp;
with Exp_Dist; use Exp_Dist;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
+with Expander; use Expander;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Itypes; use Itypes;
@@ -20387,6 +20388,40 @@ package body Sem_Ch3 is
In_Assertion_Expr := In_Assertion_Expr - 1;
end Preanalyze_Assert_Expression;
+ -- ??? The variant below explicitly saves and restores all the flags,
+ -- because it is impossible to compose the existing variety of
+ -- Analyze/Resolve (and their wrappers, e.g. Preanalyze_Spec_Expression)
+ -- to achieve the desired semantics.
+
+ procedure Preanalyze_Assert_Expression (N : Node_Id) is
+ Save_In_Spec_Expression : constant Boolean := In_Spec_Expression;
+ Save_Must_Not_Freeze : constant Boolean := Must_Not_Freeze (N);
+ Save_Full_Analysis : constant Boolean := Full_Analysis;
+
+ begin
+ In_Assertion_Expr := In_Assertion_Expr + 1;
+ In_Spec_Expression := True;
+ Set_Must_Not_Freeze (N);
+ Inside_Preanalysis_Without_Freezing :=
+ Inside_Preanalysis_Without_Freezing + 1;
+ Full_Analysis := False;
+ Expander_Mode_Save_And_Set (False);
+
+ if GNATprove_Mode then
+ Analyze_And_Resolve (N);
+ else
+ Analyze_And_Resolve (N, Suppress => All_Checks);
+ end if;
+
+ Expander_Mode_Restore;
+ Full_Analysis := Save_Full_Analysis;
+ Inside_Preanalysis_Without_Freezing :=
+ Inside_Preanalysis_Without_Freezing - 1;
+ Set_Must_Not_Freeze (N, Save_Must_Not_Freeze);
+ In_Spec_Expression := Save_In_Spec_Expression;
+ In_Assertion_Expr := In_Assertion_Expr - 1;
+ end Preanalyze_Assert_Expression;
+
-----------------------------------
-- Preanalyze_Default_Expression --
-----------------------------------
diff --git a/gcc/ada/sem_ch3.ads b/gcc/ada/sem_ch3.ads
--- a/gcc/ada/sem_ch3.ads
+++ b/gcc/ada/sem_ch3.ads
@@ -235,6 +235,9 @@ package Sem_Ch3 is
-- Wrapper on Preanalyze_Spec_Expression for assertion expressions, so that
-- In_Assertion_Expr can be properly adjusted.
+ procedure Preanalyze_Assert_Expression (N : Node_Id);
+ -- Similar to the above, but without forcing N to be of a particular type
+
procedure Preanalyze_Spec_Expression (N : Node_Id; T : Entity_Id);
-- Default and per object expressions do not freeze their components, and
-- must be analyzed and resolved accordingly. The analysis is done by
