[Ada] Add utility to preanalyze assert expression without forcing its type

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.

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
index 2e207c16e23fa479997f0883fdcb754e3c20b169..a88f7f205fdc2a4dbc901d86a93772d2ee1a7dc1 100644 (file)
--- 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
index e45ed6cac1b982650f923d6723f1ff1e344ffe87..62b15c08903c870fb927e653a4122c68f107a6ac 100644 (file)
--- 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