aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
authorPiotr Trojanek <trojanek@adacore.com>2022-01-11 00:28:00 +0100
committerPierre-Marie de Rodat <derodat@adacore.com>2022-05-09 09:27:31 +0000
commit2fe776e2d346bcf450f40739825249cab449e567 (patch)
tree513f665e8c7bc007e2b35c2fb58f48fc22e3aecb /gcc
parenteb05097d5508618a70b279df6d10d409eb4c60ae (diff)
downloadgcc-2fe776e2d346bcf450f40739825249cab449e567.zip
gcc-2fe776e2d346bcf450f40739825249cab449e567.tar.gz
gcc-2fe776e2d346bcf450f40739825249cab449e567.tar.bz2
[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.
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/sem_ch3.adb35
-rw-r--r--gcc/ada/sem_ch3.ads3
2 files changed, 38 insertions, 0 deletions
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 2e207c1..a88f7f2 100644
--- 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 e45ed6c..62b15c0 100644
--- 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