Expr : Node_Id;
begin
- if Attr_Id = Attribute_To_Address then
+ case Attr_Id is
+ when Attribute_To_Address =>
- -- Extract and convert argument to expected type for call
+ -- Extract and convert argument to expected type for call
- Expr :=
- Make_Type_Conversion (Loc,
- Subtype_Mark =>
- New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
- Expression => Relocate_Node (First (Expressions (N))));
+ Expr :=
+ Make_Type_Conversion (Loc,
+ Subtype_Mark =>
+ New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
+ Expression => Relocate_Node (First (Expressions (N))));
- -- Replace attribute reference with call
+ -- Replace attribute reference with call
- Rewrite (N,
- Make_Function_Call (Loc,
- Name =>
- New_Occurrence_Of (RTE (RE_To_Address), Loc),
- Parameter_Associations => New_List (Expr)));
- Analyze_And_Resolve (N, Typ);
-
- elsif Attr_Id = Attribute_Object_Size
- or else Attr_Id = Attribute_Size
- or else Attr_Id = Attribute_Value_Size
- or else Attr_Id = Attribute_VADS_Size
- then
- Exp_Attr.Expand_Size_Attribute (N);
-
- -- For attributes which return Universal_Integer, introduce a conversion
- -- to the expected type with the appropriate check flags set.
-
- elsif Attr_Id = Attribute_Alignment
- or else Attr_Id = Attribute_Bit
- or else Attr_Id = Attribute_Bit_Position
- or else Attr_Id = Attribute_Descriptor_Size
- or else Attr_Id = Attribute_First_Bit
- or else Attr_Id = Attribute_Last_Bit
- or else Attr_Id = Attribute_Length
- or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
- or else Attr_Id = Attribute_Pos
- or else Attr_Id = Attribute_Position
- or else Attr_Id = Attribute_Range_Length
- or else Attr_Id = Attribute_Aft
- or else Attr_Id = Attribute_Max_Alignment_For_Allocation
- then
- -- If the expected type is Long_Long_Integer, there will be no check
- -- flag as the compiler assumes attributes always fit in this type.
- -- Since in SPARK_Mode we do not take Storage_Error into account, we
- -- cannot make this assumption and need to produce a check.
- -- ??? It should be enough to add this check for attributes
- -- 'Length, 'Range_Length and 'Pos when the type is as big
- -- as Long_Long_Integer.
-
- declare
- Typ : Entity_Id;
- begin
- if Attr_Id = Attribute_Range_Length
- or else Attr_Id = Attribute_Pos
- then
- Typ := Etype (Prefix (N));
+ Rewrite
+ (N,
+ Make_Function_Call (Loc,
+ Name =>
+ New_Occurrence_Of (RTE (RE_To_Address), Loc),
+ Parameter_Associations => New_List (Expr)));
+ Analyze_And_Resolve (N, Typ);
- elsif Attr_Id = Attribute_Length then
- Typ := Get_Index_Subtype (N);
+ when Attribute_Object_Size
+ | Attribute_Size
+ | Attribute_Value_Size
+ | Attribute_VADS_Size
+ =>
+ Exp_Attr.Expand_Size_Attribute (N);
+
+ -- For attributes which return Universal_Integer, introduce a
+ -- conversion to the expected type with the appropriate check flags
+ -- set.
+
+ when Attribute_Aft
+ | Attribute_Alignment
+ | Attribute_Bit
+ | Attribute_Bit_Position
+ | Attribute_Descriptor_Size
+ | Attribute_First_Bit
+ | Attribute_Last_Bit
+ | Attribute_Length
+ | Attribute_Max_Alignment_For_Allocation
+ | Attribute_Max_Size_In_Storage_Elements
+ | Attribute_Pos
+ | Attribute_Position
+ | Attribute_Range_Length
+ =>
+ -- If the expected type is Long_Long_Integer, there will be no
+ -- check flag as the compiler assumes attributes always fit in
+ -- this type. Since in SPARK_Mode we do not take Storage_Error
+ -- into account, we cannot make this assumption and need to
+ -- produce a check. ??? It should be enough to add this check for
+ -- attributes 'Length, 'Range_Length and 'Pos when the type is as
+ -- big as Long_Long_Integer.
+
+ declare
+ Typ : Entity_Id;
+ begin
+ if Attr_Id in Attribute_Pos | Attribute_Range_Length then
+ Typ := Etype (Prefix (N));
+
+ elsif Attr_Id = Attribute_Length then
+ Typ := Get_Index_Subtype (N);
+
+ else
+ Typ := Empty;
+ end if;
- else
- Typ := Empty;
- end if;
+ Apply_Universal_Integer_Attribute_Checks (N);
- Apply_Universal_Integer_Attribute_Checks (N);
+ if Present (Typ)
+ and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
+ then
+ -- ??? This should rather be a range check, but this would
+ -- crash GNATprove which somehow recovers the proper kind
+ -- of check anyway.
+ Set_Do_Overflow_Check (N);
+ end if;
+ end;
- if Present (Typ)
- and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
- then
- -- ??? This should rather be a range check, but this would
- -- crash GNATprove which somehow recovers the proper kind
- -- of check anyway.
- Set_Do_Overflow_Check (N);
- end if;
- end;
+ when Attribute_Constrained =>
- elsif Attr_Id = Attribute_Constrained then
+ -- If the prefix is an access to object, the attribute applies to
+ -- the designated object, so rewrite with an explicit dereference.
- -- If the prefix is an access to object, the attribute applies to
- -- the designated object, so rewrite with an explicit dereference.
+ if Is_Access_Type (Etype (Pref))
+ and then
+ (not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref)))
+ then
+ Rewrite (Pref,
+ Make_Explicit_Dereference (Loc, Relocate_Node (Pref)));
+ Analyze_And_Resolve (N, Standard_Boolean);
+ end if;
- if Is_Access_Type (Etype (Pref))
- and then
- (not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref)))
- then
- Rewrite (Pref,
- Make_Explicit_Dereference (Loc, Relocate_Node (Pref)));
- Analyze_And_Resolve (N, Standard_Boolean);
- end if;
+ when Attribute_Update =>
+ Expand_SPARK_Delta_Or_Update (Typ, First (Expressions (N)));
- elsif Attr_Id = Attribute_Update then
- Expand_SPARK_Delta_Or_Update (Typ, First (Expressions (N)));
- end if;
+ when others =>
+ null;
+ end case;
end Expand_SPARK_N_Attribute_Reference;
------------------------------------