+2014-07-16 Robert Dewar <dewar@adacore.com>
+
+ * snames.ads-tmpl, sem_attr.adb, exp_attr.adb: Same_Storage attribute
+ is renamed Has_Same_Storage.
+ * gnat_rm.texi: Document missing SPARK pragmas and attributes.
+ * sem_prag.adb: Minor comment fix (use LOCAL_NAME in syntax
+ descriptions).
+
2014-07-16 Robert Dewar <dewar@adacore.com>
* exp_util.adb, sem_attr.adb, exp_ch4.adb, a-cohase.ads,
Analyze_And_Resolve (N, P_Type);
end From_Any;
+ ----------------------
+ -- Has_Same_Storage --
+ ----------------------
+
+ when Attribute_Has_Same_Storage => Has_Same_Storage : declare
+ Loc : constant Source_Ptr := Sloc (N);
+
+ X : constant Node_Id := Prefix (N);
+ Y : constant Node_Id := First (Expressions (N));
+ -- The arguments
+
+ X_Addr, Y_Addr : Node_Id;
+ -- Rhe expressions for their addresses
+
+ X_Size, Y_Size : Node_Id;
+ -- Rhe expressions for their sizes
+
+ begin
+ -- The attribute is expanded as:
+
+ -- (X'address = Y'address)
+ -- and then (X'Size = Y'Size)
+
+ -- If both arguments have the same Etype the second conjunct can be
+ -- omitted.
+
+ X_Addr :=
+ Make_Attribute_Reference (Loc,
+ Attribute_Name => Name_Address,
+ Prefix => New_Copy_Tree (X));
+
+ Y_Addr :=
+ Make_Attribute_Reference (Loc,
+ Attribute_Name => Name_Address,
+ Prefix => New_Copy_Tree (Y));
+
+ X_Size :=
+ Make_Attribute_Reference (Loc,
+ Attribute_Name => Name_Size,
+ Prefix => New_Copy_Tree (X));
+
+ Y_Size :=
+ Make_Attribute_Reference (Loc,
+ Attribute_Name => Name_Size,
+ Prefix => New_Copy_Tree (Y));
+
+ if Etype (X) = Etype (Y) then
+ Rewrite (N,
+ (Make_Op_Eq (Loc,
+ Left_Opnd => X_Addr,
+ Right_Opnd => Y_Addr)));
+ else
+ Rewrite (N,
+ Make_Op_And (Loc,
+ Left_Opnd =>
+ Make_Op_Eq (Loc,
+ Left_Opnd => X_Addr,
+ Right_Opnd => Y_Addr),
+ Right_Opnd =>
+ Make_Op_Eq (Loc,
+ Left_Opnd => X_Size,
+ Right_Opnd => Y_Size)));
+ end if;
+
+ Analyze_And_Resolve (N, Standard_Boolean);
+ end Has_Same_Storage;
+
--------------
-- Identity --
--------------
when Attribute_Rounding =>
Expand_Fpt_Attribute_R (N);
- ------------------
- -- Same_Storage --
- ------------------
-
- when Attribute_Same_Storage => Same_Storage : declare
- Loc : constant Source_Ptr := Sloc (N);
-
- X : constant Node_Id := Prefix (N);
- Y : constant Node_Id := First (Expressions (N));
- -- The arguments
-
- X_Addr, Y_Addr : Node_Id;
- -- Rhe expressions for their addresses
-
- X_Size, Y_Size : Node_Id;
- -- Rhe expressions for their sizes
-
- begin
- -- The attribute is expanded as:
-
- -- (X'address = Y'address)
- -- and then (X'Size = Y'Size)
-
- -- If both arguments have the same Etype the second conjunct can be
- -- omitted.
-
- X_Addr :=
- Make_Attribute_Reference (Loc,
- Attribute_Name => Name_Address,
- Prefix => New_Copy_Tree (X));
-
- Y_Addr :=
- Make_Attribute_Reference (Loc,
- Attribute_Name => Name_Address,
- Prefix => New_Copy_Tree (Y));
-
- X_Size :=
- Make_Attribute_Reference (Loc,
- Attribute_Name => Name_Size,
- Prefix => New_Copy_Tree (X));
-
- Y_Size :=
- Make_Attribute_Reference (Loc,
- Attribute_Name => Name_Size,
- Prefix => New_Copy_Tree (Y));
-
- if Etype (X) = Etype (Y) then
- Rewrite (N,
- (Make_Op_Eq (Loc,
- Left_Opnd => X_Addr,
- Right_Opnd => Y_Addr)));
- else
- Rewrite (N,
- Make_Op_And (Loc,
- Left_Opnd =>
- Make_Op_Eq (Loc,
- Left_Opnd => X_Addr,
- Right_Opnd => Y_Addr),
- Right_Opnd =>
- Make_Op_Eq (Loc,
- Left_Opnd => X_Size,
- Right_Opnd => Y_Size)));
- end if;
-
- Analyze_And_Resolve (N, Standard_Boolean);
- end Same_Storage;
-
-------------
-- Scaling --
-------------
* Pragma Assertion_Policy::
* Pragma Assume::
* Pragma Assume_No_Invalid_Values::
+* Pragma Async_Readers::
+* Pragma Async_Writers::
* Pragma Attribute_Definition::
* Pragma Ast_Entry::
* Pragma C_Pass_By_Copy::
* Pragma Detect_Blocking::
* Pragma Disable_Atomic_Synchronization::
* Pragma Dispatching_Domain::
+* Pragma Effective_Reads::
+* Pragma Effective_Writes::
* Pragma Elaboration_Checks::
* Pragma Eliminate::
* Pragma Enable_Atomic_Synchronization::
* Pragma Overflow_Mode::
* Pragma Overriding_Renamings::
* Pragma Partition_Elaboration_Policy::
+* Pragma Part_Of::
* Pragma Passive::
* Pragma Persistent_BSS::
* Pragma Polling::
* Pragma Psect_Object::
* Pragma Pure_Function::
* Pragma Ravenscar::
+* Pragma Refined_Depends::
+* Pragma Refined_Global::
+* Pragma Refined_Post::
* Pragma Refined_State::
* Pragma Relative_Deadline::
* Pragma Remote_Access_Type::
Implementation Defined Aspects
* Aspect Abstract_State::
+* Aspect Async_Readers::
+* Aspect Async_Writers::
* Aspect Contract_Cases::
* Aspect Depends::
* Aspect Dimension::
* Aspect Dimension_System::
+* Aspect Effective_Reads::
+* Aspect Effective_Writes::
* Aspect Favor_Top_Level::
* Aspect Global::
* Aspect Initial_Condition::
* Aspect Invariant::
* Aspect Linker_Section::
* Aspect Object_Size::
+* Aspect Part_Of::
* Aspect Persistent_BSS::
* Aspect Predicate::
* Aspect Pure_Function::
+* Aspect Refined_Depends::
+* Aspect Refined_Global::
+* Aspect Refined_Post::
* Aspect Refined_State::
* Aspect Remote_Access_Type::
* Aspect Scalar_Storage_Order::
* Pragma Assertion_Policy::
* Pragma Assume::
* Pragma Assume_No_Invalid_Values::
+* Pragma Async_Readers::
+* Pragma Async_Writers::
* Pragma Attribute_Definition::
* Pragma Ast_Entry::
* Pragma C_Pass_By_Copy::
* Pragma Detect_Blocking::
* Pragma Disable_Atomic_Synchronization::
* Pragma Dispatching_Domain::
+* Pragma Effective_Reads::
+* Pragma Effective_Writes::
* Pragma Elaboration_Checks::
* Pragma Eliminate::
* Pragma Enable_Atomic_Synchronization::
* Pragma Overflow_Mode::
* Pragma Overriding_Renamings::
* Pragma Partition_Elaboration_Policy::
+* Pragma Part_Of::
* Pragma Passive::
* Pragma Persistent_BSS::
* Pragma Polling::
* Pragma Psect_Object::
* Pragma Pure_Function::
* Pragma Ravenscar::
+* Pragma Refined_Depends::
+* Pragma Refined_Global::
+* Pragma Refined_Post::
* Pragma Refined_State::
* Pragma Relative_Deadline::
* Pragma Remote_Access_Type::
is erroneous so there are no guarantees that this will always be the
case, and it is recommended that these two options not be used together.
+@node Pragma Async_Readers
+@unnumberedsec Pragma Async_Readers
+@findex Async_Readers
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.2.
+
+@node Pragma Async_Writers
+@unnumberedsec Pragma Async_Writers
+@findex Async_Writers
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.2.
+
@node Pragma Ast_Entry
@unnumberedsec Pragma Ast_Entry
@cindex OpenVMS
versions of Ada as an implementation-defined pragma.
See Ada 2012 Reference Manual for details.
+@node Pragma Effective_Reads
+@unnumberedsec Pragma Effective_Reads
+@findex Effective_Reads
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.2.
+
+@node Pragma Effective_Writes
+@unnumberedsec Pragma Effective_Writes
+@findex Effective_Writes
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.2.
+
@node Pragma Elaboration_Checks
@unnumberedsec Pragma Elaboration_Checks
@cindex Elaboration control
versions of Ada as an implementation-defined pragma.
See Ada 2012 Reference Manual for details.
+@node Pragma Part_Of
+@unnumberedsec Pragma Part_Of
+@findex Part_Of
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.2.6.
+
@node Pragma Passive
@unnumberedsec Pragma Passive
@findex Passive
@noindent
which is the preferred method of setting the @code{Ravenscar} profile.
+@node Pragma Refined_Depends
+@unnumberedsec Pragma Refined_Depends
+@findex Refined_Depends
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 6.1.5.
+
+@node Pragma Refined_Global
+@unnumberedsec Pragma Refined_Global
+@findex Refined_Global
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 6.1.4.
+
+@node Pragma Refined_Post
+@unnumberedsec Pragma Refined_Post
+@findex Refined_Post
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.2.7.
+
@node Pragma Refined_State
@unnumberedsec Pragma Refined_State
@findex Refined_State
@menu
* Aspect Abstract_State::
+* Aspect Async_Readers::
+* Aspect Async_Writers::
* Aspect Contract_Cases::
* Aspect Depends::
* Aspect Dimension::
* Aspect Dimension_System::
+* Aspect Effective_Reads::
+* Aspect Effective_Writes::
* Aspect Favor_Top_Level::
* Aspect Global::
* Aspect Initial_Condition::
* Aspect Linker_Section::
* Aspect Lock_Free::
* Aspect Object_Size::
+* Aspect Part_Of::
* Aspect Persistent_BSS::
* Aspect Predicate::
* Aspect Pure_Function::
+* Aspect Refined_Depends::
+* Aspect Refined_Global::
+* Aspect Refined_Post::
* Aspect Refined_State::
* Aspect Remote_Access_Type::
* Aspect Scalar_Storage_Order::
@noindent
This aspect is equivalent to pragma @code{Abstract_State}.
+@node Aspect Async_Readers
+@unnumberedsec Aspect Async_Readers
+@findex Async_Readers
+@noindent
+This aspect is equivalent to pragma @code{Async_Readers}.
+
+@node Aspect Async_Writers
+@unnumberedsec Aspect Async_Writers
+@findex Async_Writers
+@noindent
+This aspect is equivalent to pragma @code{Async_Writers}.
+
@node Aspect Contract_Cases
@unnumberedsec Aspect Contract_Cases
@findex Contract_Cases
See section ``Performing Dimensionality Analysis in GNAT'' in the GNAT Users
Guide for detailed examples of use of the dimension system.
+@node Aspect Effective_Reads
+@unnumberedsec Aspect Effective_Reads
+@findex Effective_Reads
+@noindent
+This aspect is equivalent to pragma @code{Effective_Reads}.
+
+@node Aspect Effective_Writes
+@unnumberedsec Aspect Effective_Writes
+@findex Effective_Writes
+@noindent
+This aspect is equivalent to pragma @code{Effective_Writes}.
+
@node Aspect Favor_Top_Level
@unnumberedsec Aspect Favor_Top_Level
@findex Favor_Top_Level
This aspect is equivalent to an @code{Object_Size} attribute definition
clause.
+@node Aspect Part_Of
+@unnumberedsec Aspect Part_Of
+@findex Part_Of
+@noindent
+This aspect is equivalent to pragma @code{Part_Of}.
+
@node Aspect Persistent_BSS
@unnumberedsec Aspect Persistent_BSS
@findex Persistent_BSS
@noindent
This aspect is equivalent to pragma @code{Pure_Function}.
+@node Aspect Refined_Depends
+@unnumberedsec Aspect Refined_Depends
+@findex Refined_Depends
+@noindent
+This aspect is equivalent to pragma @code{Refined_Depends}.
+
+@node Aspect Refined_Global
+@unnumberedsec Aspect Refined_Global
+@findex Refined_Global
+@noindent
+This aspect is equivalent to pragma @code{Refined_Global}.
+
+@node Aspect Refined_Post
+@unnumberedsec Aspect Refined_Post
+@findex Refined_Post
+@noindent
+This aspect is equivalent to pragma @code{Refined_Post}.
+
@node Aspect Refined_State
@unnumberedsec Aspect Refined_State
@findex Refined_State
Check_E0;
Set_Etype (N, Standard_Boolean);
+ ----------------------
+ -- Has_Same_Storage --
+ ----------------------
+
+ when Attribute_Has_Same_Storage =>
+ Check_Ada_2012_Attribute;
+ Check_E1;
+
+ -- The arguments must be objects of any type
+
+ Analyze_And_Resolve (P);
+ Analyze_And_Resolve (E1);
+ Check_Object_Reference (P);
+ Check_Object_Reference (E1);
+ Set_Etype (N, Standard_Boolean);
+
-----------------------
-- Has_Tagged_Values --
-----------------------
Check_Real_Type;
Set_Etype (N, Universal_Real);
- ------------------
- -- Same_Storage --
- ------------------
-
- when Attribute_Same_Storage =>
- Check_Ada_2012_Attribute;
- Check_E1;
-
- -- The arguments must be objects of any type
-
- Analyze_And_Resolve (P);
- Analyze_And_Resolve (E1);
- Check_Object_Reference (P);
- Check_Object_Reference (E1);
- Set_Etype (N, Standard_Boolean);
-
--------------------------
-- Scalar_Storage_Order --
--------------------------
Boolean_Literals (Has_Discriminants (P_Entity)), Loc));
Analyze_And_Resolve (N, Standard_Boolean);
+ ----------------------
+ -- Has_Same_Storage --
+ ----------------------
+
+ when Attribute_Has_Same_Storage =>
+ null;
+
-----------------------
-- Has_Tagged_Values --
-----------------------
Fold_Ureal (N, Model_Small_Value (P_Type), Static);
end if;
- ------------------
- -- Same_Storage --
- ------------------
-
- when Attribute_Same_Storage =>
- null;
-
-----------
-- Scale --
-----------
-- Async_Readers/Async_Writers/Effective_Reads/Effective_Writes --
------------------------------------------------------------------
- -- pragma Asynch_Readers ( identifier [, boolean_EXPRESSION] );
- -- pragma Asynch_Writers ( identifier [, boolean_EXPRESSION] );
- -- pragma Effective_Reads ( identifier [, boolean_EXPRESSION] );
- -- pragma Effective_Writes ( identifier [, boolean_EXPRESSION] );
+ -- pragma Asynch_Readers ( object_LOCAL_NAME [, FLAG] );
+ -- pragma Asynch_Writers ( object_LOCAL_NAME [, FLAG] );
+ -- pragma Effective_Reads ( object_LOCAL_NAME [, FLAG] );
+ -- pragma Effective_Writes ( object_LOCAL_NAME [, FLAG] );
+
+ -- FLAG ::= boolean_EXPRESSION
when Pragma_Async_Readers |
Pragma_Async_Writers |
-- CPP_Class --
---------------
- -- pragma CPP_Class ([Entity =>] local_NAME)
+ -- pragma CPP_Class ([Entity =>] LOCAL_NAME)
when Pragma_CPP_Class => CPP_Class : declare
begin
-- pragma Export (
-- [ Convention =>] convention_IDENTIFIER,
- -- [ Entity =>] local_NAME
+ -- [ Entity =>] LOCAL_NAME
-- [, [External_Name =>] static_string_EXPRESSION ]
-- [, [Link_Name =>] static_string_EXPRESSION ]);
-- pragma External (
-- [ Convention =>] convention_IDENTIFIER,
- -- [ Entity =>] local_NAME
+ -- [ Entity =>] LOCAL_NAME
-- [, [External_Name =>] static_string_EXPRESSION ]
-- [, [Link_Name =>] static_string_EXPRESSION ]);
-- Implementation_Defined --
----------------------------
- -- pragma Implementation_Defined (local_NAME);
+ -- pragma Implementation_Defined (LOCAL_NAME);
-- Marks previously declared entity as implementation defined. For
-- an overloaded entity, applies to the most recent homonym.
-- pragma Import (
-- [Convention =>] convention_IDENTIFIER,
- -- [Entity =>] local_NAME
+ -- [Entity =>] LOCAL_NAME
-- [, [External_Name =>] static_string_EXPRESSION ]
-- [, [Link_Name =>] static_string_EXPRESSION ]);
-- pragma Interface (
-- [ Convention =>] convention_IDENTIFIER,
- -- [ Entity =>] local_NAME
+ -- [ Entity =>] LOCAL_NAME
-- [, [External_Name =>] static_string_EXPRESSION ]
-- [, [Link_Name =>] static_string_EXPRESSION ]);
--------------------
-- pragma Interface_Name (
- -- [ Entity =>] local_NAME
+ -- [ Entity =>] LOCAL_NAME
-- [,[External_Name =>] static_string_EXPRESSION ]
-- [,[Link_Name =>] static_string_EXPRESSION ]);
-- Keep_Names --
----------------
- -- pragma Keep_Names ([On => ] local_NAME);
+ -- pragma Keep_Names ([On => ] LOCAL_NAME);
when Pragma_Keep_Names => Keep_Names : declare
Arg : Node_Id;
-- pragma Part_Of (ABSTRACT_STATE);
- -- ABSTRACT_STATE ::= name
+ -- ABSTRACT_STATE ::= NAME
when Pragma_Part_Of => Part_Of : declare
procedure Propagate_Part_Of
-- Unmodified --
----------------
- -- pragma Unmodified (local_Name {, local_Name});
+ -- pragma Unmodified (LOCAL_NAME {, LOCAL_NAME});
when Pragma_Unmodified => Unmodified : declare
Arg_Node : Node_Id;
-- Unreferenced --
------------------
- -- pragma Unreferenced (local_Name {, local_Name});
+ -- pragma Unreferenced (LOCAL_NAME {, LOCAL_NAME});
-- or when used in a context clause:
-- Unreferenced_Objects --
--------------------------
- -- pragma Unreferenced_Objects (local_Name {, local_Name});
+ -- pragma Unreferenced_Objects (LOCAL_NAME {, LOCAL_NAME});
when Pragma_Unreferenced_Objects => Unreferenced_Objects : declare
Arg_Node : Node_Id;
Name_Fore : constant Name_Id := N + $;
Name_Has_Access_Values : constant Name_Id := N + $; -- GNAT
Name_Has_Discriminants : constant Name_Id := N + $; -- GNAT
+ Name_Has_Same_Storage : constant Name_Id := N + $; -- Ada 12
Name_Has_Tagged_Values : constant Name_Id := N + $; -- GNAT
Name_Identity : constant Name_Id := N + $;
Name_Img : constant Name_Id := N + $; -- GNAT
Name_Safe_Large : constant Name_Id := N + $; -- Ada 83
Name_Safe_Last : constant Name_Id := N + $;
Name_Safe_Small : constant Name_Id := N + $; -- Ada 83
- Name_Same_Storage : constant Name_Id := N + $; -- Ada 12
Name_Scalar_Storage_Order : constant Name_Id := N + $; -- GNAT
Name_Scale : constant Name_Id := N + $;
Name_Scaling : constant Name_Id := N + $;
Attribute_Fore,
Attribute_Has_Access_Values,
Attribute_Has_Discriminants,
+ Attribute_Has_Same_Storage,
Attribute_Has_Tagged_Values,
Attribute_Identity,
Attribute_Img,
Attribute_Safe_Large,
Attribute_Safe_Last,
Attribute_Safe_Small,
- Attribute_Same_Storage,
Attribute_Scalar_Storage_Order,
Attribute_Scale,
Attribute_Scaling,
projects / thirdparty / gcc.git / commitdiff
