+2013-10-17 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb, aspects.ads, sem_prag.ads: Remove all entries
+ for Refined_Pre from the various tables.
+ * par-prag.adb: Remove the entry for Refined_Pre from the list
+ of pragmas not needing special processing by the parser.
+ * sem_ch13.adb (Analyze_Aspect_Specifications):
+ Remove the processing for aspect Refined_Pre.
+ (Check_Aspect_At_Freeze_Point): Remove the entry for aspect
+ Refined_Pre.
+ * sem_prag.adb (Analyze_Pragma): Refined_Pre is no longer a
+ valid assertion kind. Remove the analysis of pragma Refined_Pre.
+ (Analyze_Refined_Pragma): Update the comment on usage.
+ (Find_Related_Subprogram_Or_Body): Update the comment on
+ usage. Pragma Refined_Pre is no longer processed by this routine.
+ (Is_Valid_Assertion_Kind): Refined_Pre is no longer a valid
+ assertion kind.
+ * snames.ads-tmpl: Remove predefined name Refined_Pre. Remove
+ the pragma id for Refined_Pre.
+
2013-10-17 Hristian Kirtchev <kirtchev@adacore.com>
* exp_util.adb, exp_util.ads (Entity_Of): Moved to Sem_Util.
Aspect_Refined_Depends => Aspect_Refined_Depends,
Aspect_Refined_Global => Aspect_Refined_Global,
Aspect_Refined_Post => Aspect_Refined_Post,
- Aspect_Refined_Pre => Aspect_Refined_Pre,
Aspect_Refined_State => Aspect_Refined_State,
Aspect_Remote_Access_Type => Aspect_Remote_Access_Type,
Aspect_Remote_Call_Interface => Aspect_Remote_Call_Interface,
Aspect_Refined_Depends, -- GNAT
Aspect_Refined_Global, -- GNAT
Aspect_Refined_Post, -- GNAT
- Aspect_Refined_Pre, -- GNAT
Aspect_Refined_State, -- GNAT
Aspect_Relative_Deadline,
Aspect_Scalar_Storage_Order, -- GNAT
Aspect_Refined_Depends => Expression,
Aspect_Refined_Global => Expression,
Aspect_Refined_Post => Expression,
- Aspect_Refined_Pre => Expression,
Aspect_Refined_State => Expression,
Aspect_Relative_Deadline => Expression,
Aspect_Scalar_Storage_Order => Expression,
Aspect_Refined_Depends => Name_Refined_Depends,
Aspect_Refined_Global => Name_Refined_Global,
Aspect_Refined_Post => Name_Refined_Post,
- Aspect_Refined_Pre => Name_Refined_Pre,
Aspect_Refined_State => Name_Refined_State,
Aspect_Relative_Deadline => Name_Relative_Deadline,
Aspect_Remote_Access_Type => Name_Remote_Access_Type,
Aspect_Dimension => Never_Delay,
Aspect_Dimension_System => Never_Delay,
Aspect_Refined_Post => Never_Delay,
- Aspect_Refined_Pre => Never_Delay,
Aspect_SPARK_Mode => Never_Delay,
Aspect_Synchronization => Never_Delay,
Aspect_Test_Case => Never_Delay,
(Aspect_Refined_Depends => True,
Aspect_Refined_Global => True,
Aspect_Refined_Post => True,
- Aspect_Refined_Pre => True,
Aspect_SPARK_Mode => True,
Aspect_Warnings => True,
others => False);
Pragma_Refined_Depends |
Pragma_Refined_Global |
Pragma_Refined_Post |
- Pragma_Refined_Pre |
Pragma_Refined_State |
Pragma_Relative_Deadline |
Pragma_Remote_Access_Type |
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Refined_Post);
- -- Refined_Pre
-
- -- Disable the support for aspect Refined_Pre as its static and
- -- runtime semantics are still under heavy design.
-
- when Aspect_Refined_Pre =>
- Error_Msg_NE ("aspect & is not supported", Aspect, Id);
- goto Continue;
-
-- Refined_State
when Aspect_Refined_State => Refined_State : declare
Aspect_Refined_Depends |
Aspect_Refined_Global |
Aspect_Refined_Post |
- Aspect_Refined_Pre |
Aspect_Refined_State |
Aspect_SPARK_Mode |
Aspect_Test_Case =>
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
-- Subsidiary to the analysis of pragmas Contract_Cases, Depends, Global,
- -- Refined_Depends, Refined_Global, Refined_Post and Refined_Pre. Find the
- -- declaration of the related subprogram [body or stub] subject to pragma
- -- Prag. If flag Do_Checks is set, the routine reports duplicate pragmas
- -- and detects improper use of refinement pragmas in stand alone expression
- -- functions. The returned value depends on the related pragma as follows:
+ -- Refined_Depends, Refined_Global and Refined_Post. Find the declaration
+ -- of the related subprogram [body or stub] subject to pragma Prag. If flag
+ -- Do_Checks is set, the routine reports duplicate pragmas and detects
+ -- improper use of refinement pragmas in stand alone expression functions.
+ -- The returned value depends on the related pragma as follows:
-- 1) Pragmas Contract_Cases, Depends and Global yield the corresponding
-- N_Subprogram_Declaration node or if the pragma applies to a stand
-- alone body, the N_Subprogram_Body node or Empty if illegal.
- -- 2) Pragmas Refined_Depends, Refined_Global, Refined_Post and
- -- Refined_Pre yield N_Subprogram_Body or N_Subprogram_Body_Stub nodes
- -- or Empty if illegal.
+ -- 2) Pragmas Refined_Depends, Refined_Global and Refined_Post yield
+ -- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if
+ -- illegal.
function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
-- If Def_Id refers to a renamed subprogram, then the base subprogram (the
Body_Id : out Entity_Id;
Legal : out Boolean);
-- Subsidiary routine to the analysis of body pragmas Refined_Depends,
- -- Refined_Global, Refined_Post and Refined_Pre. Check the placement and
- -- related context of the pragma. Spec_Id is the entity of the related
+ -- Refined_Global and Refined_Post. Check the placement and related
+ -- context of the pragma. Spec_Id is the entity of the related
-- subprogram. Body_Id is the entity of the subprogram body. Flag Legal
-- is set when the pragma is properly placed.
-- Precondition |
-- Predicate |
-- Refined_Post |
- -- Refined_Pre |
-- Statement_Assertions
-- Note: The RM_ASSERTION_KIND list is language-defined, and the
end if;
end Refined_Depends_Global;
- ------------------------------
- -- Refined_Post/Refined_Pre --
- ------------------------------
+ ------------------
+ -- Refined_Post --
+ ------------------
-- pragma Refined_Post (boolean_EXPRESSION);
- -- pragma Refined_Pre (boolean_EXPRESSION);
- when Pragma_Refined_Post |
- Pragma_Refined_Pre => Refined_Pre_Post :
- declare
+ when Pragma_Refined_Post => Refined_Post : declare
Body_Id : Entity_Id;
Legal : Boolean;
Spec_Id : Entity_Id;
begin
- -- Disable the support for pragma Refined_Pre as its static and
- -- runtime semantics are still under heavy design. The pragma is
- -- silently ignored.
-
- if Pname = Name_Refined_Pre then
- Set_Is_Ignored (N);
- end if;
-
Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal);
-- Analyze the boolean expression as a "spec expression"
if Legal then
Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id);
end if;
- end Refined_Pre_Post;
+ end Refined_Post;
-------------------
-- Refined_State --
Look_For_Body : constant Boolean :=
Nam_In (Nam, Name_Refined_Depends,
Name_Refined_Global,
- Name_Refined_Post,
- Name_Refined_Pre);
+ Name_Refined_Post);
-- Refinement pragmas must be associated with a subprogram body [stub]
begin
Pragma_Refined_Depends => -1,
Pragma_Refined_Global => -1,
Pragma_Refined_Post => -1,
- Pragma_Refined_Pre => -1,
Pragma_Refined_State => -1,
Pragma_Relative_Deadline => -1,
Pragma_Remote_Access_Type => -1,
Name_Precondition |
Name_Predicate |
Name_Refined_Post |
- Name_Refined_Pre |
Name_Statement_Assertions => return True;
when others => return False;
(Pragma_Refined_Depends => True,
Pragma_Refined_Global => True,
Pragma_Refined_Post => True,
- Pragma_Refined_Pre => True,
Pragma_SPARK_Mode => True,
Pragma_Warnings => True,
others => False);
Name_Refined_Depends : constant Name_Id := N + $; -- GNAT
Name_Refined_Global : constant Name_Id := N + $; -- GNAT
Name_Refined_Post : constant Name_Id := N + $; -- GNAT
- Name_Refined_Pre : constant Name_Id := N + $; -- GNAT
Name_Refined_State : constant Name_Id := N + $; -- GNAT
Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05
Name_Remote_Access_Type : constant Name_Id := N + $; -- GNAT
Pragma_Refined_Depends,
Pragma_Refined_Global,
Pragma_Refined_Post,
- Pragma_Refined_Pre,
Pragma_Refined_State,
Pragma_Relative_Deadline,
Pragma_Remote_Access_Type,
projects / thirdparty / gcc.git / commitdiff
