public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc/devel/autopar_devel] [Ada] Set range checks flag on 'Update for GNATprove in expansion
@ 2020-08-22 23:17 Giuliano Belinassi
0 siblings, 0 replies; only message in thread
From: Giuliano Belinassi @ 2020-08-22 23:17 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:a317e46b6a3cb28fdb9d5a4ce1629337b5754a74
commit a317e46b6a3cb28fdb9d5a4ce1629337b5754a74
Author: Piotr Trojanek <trojanek@adacore.com>
Date: Wed Apr 29 22:15:16 2020 +0200
[Ada] Set range checks flag on 'Update for GNATprove in expansion
gcc/ada/
* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Apply
scalar range checks.
* sem_attr.adb (Resolve_Attribute): Do not set scalar range
checks when resolving attribute Update.
Diff:
---
gcc/ada/exp_spark.adb | 47 +++++++++++++++++++++++++++++++++++++++++++++++
gcc/ada/sem_attr.adb | 28 ----------------------------
2 files changed, 47 insertions(+), 28 deletions(-)
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 207bb06d4ac..1f95aa49aa8 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -251,6 +251,53 @@ package body Exp_SPARK is
Analyze_And_Resolve (N, Standard_Boolean);
end if;
+ elsif Attr_Id = Attribute_Update then
+ declare
+ Aggr : constant Node_Id := First (Expressions (N));
+ -- The aggregate expression
+
+ Assoc : Node_Id;
+ Comp : Node_Id;
+ Comp_Type : Node_Id;
+ Expr : Node_Id;
+
+ begin
+ -- Apply scalar range checks on the updated components, if needed
+
+ if Is_Array_Type (Typ) then
+ Assoc := First (Component_Associations (Aggr));
+
+ while Present (Assoc) loop
+ Expr := Expression (Assoc);
+ Comp_Type := Component_Type (Typ);
+
+ if Is_Scalar_Type (Comp_Type) then
+ Apply_Scalar_Range_Check (Expr, Comp_Type);
+ end if;
+
+ Next (Assoc);
+ end loop;
+
+ else pragma Assert (Is_Record_Type (Typ));
+
+ Assoc := First (Component_Associations (Aggr));
+ while Present (Assoc) loop
+ Expr := Expression (Assoc);
+ Comp := First (Choices (Assoc));
+ Comp_Type := Etype (Entity (Comp));
+
+ -- Use the type of the first component from the Choices
+ -- list, as multiple components can only appear there if
+ -- they have exactly the same type.
+
+ if Is_Scalar_Type (Comp_Type) then
+ Apply_Scalar_Range_Check (Expr, Comp_Type);
+ end if;
+
+ Next (Assoc);
+ end loop;
+ end if;
+ end;
end if;
end Expand_SPARK_N_Attribute_Reference;
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index d012418c8a3..4f112065abe 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -11995,26 +11995,6 @@ package body Sem_Attr is
Expr := Expression (Assoc);
Resolve (Expr, Component_Type (Typ));
- -- For scalar array components set Do_Range_Check when
- -- needed. Constraint checking on non-scalar components
- -- is done in Aggregate_Constraint_Checks, but only if
- -- full analysis is enabled. These flags are not set in
- -- the front-end in GnatProve mode.
-
- if Is_Scalar_Type (Component_Type (Typ))
- and then not Is_OK_Static_Expression (Expr)
- and then not Range_Checks_Suppressed (Component_Type (Typ))
- then
- if Is_Entity_Name (Expr)
- and then Etype (Expr) = Component_Type (Typ)
- then
- null;
-
- else
- Set_Do_Range_Check (Expr);
- end if;
- end if;
-
-- The choices in the association are static constants,
-- or static aggregates each of whose components belongs
-- to the proper index type. However, they must also
@@ -12072,14 +12052,6 @@ package body Sem_Attr is
and then not Error_Posted (Comp)
then
Resolve (Expr, Etype (Entity (Comp)));
-
- if Is_Scalar_Type (Etype (Entity (Comp)))
- and then not Is_OK_Static_Expression (Expr)
- and then not Range_Checks_Suppressed
- (Etype (Entity (Comp)))
- then
- Set_Do_Range_Check (Expr);
- end if;
end if;
Next (Assoc);
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2020-08-22 23:17 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-08-22 23:17 [gcc/devel/autopar_devel] [Ada] Set range checks flag on 'Update for GNATprove in expansion Giuliano Belinassi
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).