From 964cf38cb37e4766837b284a566cabe0fc737f26 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Thu, 21 May 2020 15:42:32 +0200 Subject: [PATCH] [Ada] Fix expansion of 'Update with multiple choices in GNATprove gcc/ada/ * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Fix expansion of attribute Update. --- gcc/ada/exp_spark.adb | 66 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 57 insertions(+), 9 deletions(-) diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 6ef03c3180e..a02c0c882ef 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -258,10 +258,12 @@ package body Exp_SPARK is Assoc : Node_Id; Comp : Node_Id; + Comp_Id : Entity_Id; Comp_Type : Entity_Id; Expr : Node_Id; Index : Node_Id; Index_Typ : Entity_Id; + New_Assoc : Node_Id; begin -- Apply scalar range checks on the updated components, if needed @@ -346,19 +348,65 @@ package body Exp_SPARK is else pragma Assert (Is_Record_Type (Typ)); + -- If the aggregate has multiple component choices, e.g. + -- + -- X'Update (A | B | C => 123) + -- + -- then each component might be of a different type and might + -- or might not require a range check. We first rewrite + -- associations into single-component choices, e.g.: + -- + -- X'Update (A => 123, B => 123, C => 123) + -- + -- and then apply range checks to individual copies of the + -- expressions. + + -- Iterate over associations of the original aggregate + Assoc := First (Component_Associations (Aggr)); + + -- Rewrite into a new aggregate and decorate + + Rewrite + (Aggr, + Make_Aggregate + (Sloc => Sloc (Aggr), + Component_Associations => New_List)); + + Set_Etype (Aggr, Typ); + + -- Populate the new aggregate with component associations + while Present (Assoc) loop - Expr := Expression (Assoc); - Comp := First (Choices (Assoc)); - Comp_Type := Etype (Entity (Comp)); + Expr := Expression (Assoc); + Comp := First (Choices (Assoc)); + + while Present (Comp) loop + Comp_Id := Entity (Comp); + Comp_Type := Etype (Comp_Id); - -- 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. + New_Assoc := + Make_Component_Association + (Sloc => Sloc (Assoc), + Choices => + New_List + (New_Occurrence_Of (Comp_Id, Sloc (Comp))), + Expression => New_Copy_Tree (Expr)); - if Is_Scalar_Type (Comp_Type) then - Apply_Scalar_Range_Check (Expr, Comp_Type); - end if; + -- New association must be attached as a child of the + -- aggregate before we analyze it. + + Append (New_Assoc, Component_Associations (Aggr)); + + Analyze_And_Resolve (Expression (New_Assoc), Comp_Type); + + if Is_Scalar_Type (Comp_Type) then + Apply_Scalar_Range_Check + (Expression (New_Assoc), Comp_Type); + end if; + + Next (Comp); + end loop; Next (Assoc); end loop; -- 2.30.2