2013-04-22 Yannick Moy <moy@adacore.com>
+ * par-prag.adb, sem_attr.adb, sem_ch6.adb, sem_prag.adb, sem_warn.adb,
+ snames.ads-tmpl, sinfo.ads, sem_util.ads: Remove all references to
+ Pragma_Contract_Case and Name_Contract_Case.
+
+2013-04-22 Yannick Moy <moy@adacore.com>
+
* aspects.ads, aspects.adb, sem_ch13.adb: Removal of references to
Contract_Case.
* gnat_ugn.texi, gnat_rm.texi Description of Contract_Case replaced by
Pragma_Compile_Time_Error |
Pragma_Compile_Time_Warning |
Pragma_Compiler_Unit |
- Pragma_Contract_Case |
Pragma_Contract_Cases |
Pragma_Convention_Identifier |
Pragma_CPP_Class |
if Nkind (Prag) /= N_Pragma then
Error_Attr ("% attribute can only appear in postcondition", P);
- elsif Get_Pragma_Id (Prag) = Pragma_Contract_Case
- or else
- Get_Pragma_Id (Prag) = Pragma_Test_Case
- then
+ elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
declare
Arg_Ens : constant Node_Id :=
Get_Ensures_From_CTC_Pragma (Prag);
end loop;
if Arg /= Arg_Ens then
- if Get_Pragma_Id (Prag) = Pragma_Contract_Case then
- Error_Attr
- ("% attribute misplaced inside contract case", P);
- else
- Error_Attr
- ("% attribute misplaced inside test case", P);
- end if;
+ Error_Attr ("% attribute misplaced inside test case", P);
end if;
end;
("% attribute can only appear in postcondition of function",
P);
- elsif Get_Pragma_Id (Prag) = Pragma_Contract_Case
- or else
- Get_Pragma_Id (Prag) = Pragma_Test_Case
- then
+ elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
declare
Arg_Ens : constant Node_Id :=
Get_Ensures_From_CTC_Pragma (Prag);
end loop;
if Arg /= Arg_Ens then
- if Get_Pragma_Id (Prag) = Pragma_Contract_Case then
- Error_Attr
- ("% attribute misplaced inside contract case", P);
- else
- Error_Attr
- ("% attribute misplaced inside test case", P);
- end if;
+ Error_Attr ("% attribute misplaced inside test case", P);
end if;
end;
-- -- List of subprograms inherited by this subprogram
-- We ignore postconditions "True" or "False" and contract-cases which
- -- have similar Ensures components, which we call "trivial", when
+ -- have similar consequence expressions, which we call "trivial", when
-- issuing warnings, since these postconditions and contract-cases
-- purposedly ignore the post-state.
Attribute_Result_Mentioned : Boolean := False;
-- Whether attribute 'Result is mentioned in a non-trivial postcondition
- -- or contract-case.
+ -- or contract-cases.
No_Warning_On_Some_Postcondition : Boolean := False;
- -- Whether there exists a non-trivial postcondition or contract-case
+ -- Whether there exists a non-trivial postcondition or contract-cases
-- without a corresponding warning.
Post_State_Mentioned : Boolean := False;
- -- Whether some expression mentioned in a postcondition or contract-case
- -- can have a different value in the post-state than in the pre-state.
+ -- Whether some expression mentioned in a postcondition or
+ -- contract-cases can have a different value in the post-state than
+ -- in the pre-state.
function Check_Attr_Result (N : Node_Id) return Traverse_Result;
-- Check if N is a reference to the attribute 'Result, and if so set
while Present (Post_Case) loop
Conseq := Expression (Post_Case);
- -- Ignore trivial contract-case when consequence is "True"
+ -- Ignore trivial contract-cases when consequence is "True"
-- or "False".
if not Is_Trivial_Post_Or_Ensures (Conseq) then
-- evaluate case guards and trigger consequence expressions. Subp_Id
-- denotes the related subprogram.
- function Grab_CC return Node_Id;
- -- Prag contains an analyzed contract case pragma. This function copies
- -- relevant components of the pragma, creates the corresponding Check
- -- pragma and returns the Check pragma as the result.
-
function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
-- Prag contains an analyzed precondition or postcondition pragma. This
-- function copies the pragma, changes it to the corresponding Check
Append_To (Plist, Conseq_Checks);
end Expand_Contract_Cases;
- -------------
- -- Grab_CC --
- -------------
-
- function Grab_CC return Node_Id is
- Loc : constant Source_Ptr := Sloc (Prag);
- CP : Node_Id;
- Req : Node_Id;
- Ens : Node_Id;
- Post : Node_Id;
-
- -- As with postcondition, the string is "failed xx from yy" where
- -- xx is in all lower case. The reason for this different wording
- -- compared to other Check cases is that the failure is not at the
- -- point of occurrence of the pragma, unlike the other Check cases.
-
- Msg : constant String :=
- "failed contract case from " & Build_Location_String (Loc);
-
- begin
- -- Copy the Requires and Ensures expressions
-
- Req := New_Copy_Tree
- (Expression (Get_Requires_From_CTC_Pragma (Prag)),
- New_Scope => Current_Scope);
-
- Ens := New_Copy_Tree
- (Expression (Get_Ensures_From_CTC_Pragma (Prag)),
- New_Scope => Current_Scope);
-
- -- Build the postcondition (not Requires'Old or else Ensures)
-
- Post :=
- Make_Or_Else (Loc,
- Left_Opnd =>
- Make_Op_Not (Loc,
- Make_Attribute_Reference (Loc,
- Prefix => Req,
- Attribute_Name => Name_Old)),
- Right_Opnd => Ens);
-
- -- For a contract case pragma within a generic, generate a
- -- postcondition pragma for later expansion. This is also used
- -- when an error was detected, thus setting Expander_Active to False.
-
- if not Expander_Active then
- CP :=
- Make_Pragma (Loc,
- Chars => Name_Postcondition,
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Chars => Name_Check,
- Expression => Post),
-
- Make_Pragma_Argument_Association (Loc,
- Chars => Name_Message,
- Expression => Make_String_Literal (Loc, Msg))));
-
- -- Otherwise, create the Check pragma
-
- else
- CP :=
- Make_Pragma (Loc,
- Chars => Name_Check,
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Chars => Name_Name,
- Expression => Make_Identifier (Loc, Name_Postcondition)),
-
- Make_Pragma_Argument_Association (Loc,
- Chars => Name_Check,
- Expression => Post),
-
- Make_Pragma_Argument_Association (Loc,
- Chars => Name_Message,
- Expression => Make_String_Literal (Loc, Msg))));
- end if;
-
- -- Return the Postcondition or Check pragma
-
- return CP;
- end Grab_CC;
-
--------------
-- Grab_PPC --
--------------
Spec_Postconditions : declare
procedure Process_Contract_Cases (Spec : Node_Id);
-- This processes the Spec_CTC_List from Spec, processing any
- -- contract-case from the list. The caller has checked that
+ -- contract-cases from the list. The caller has checked that
-- Spec_CTC_List is non-Empty.
procedure Process_Post_Conditions
procedure Process_Contract_Cases (Spec : Node_Id) is
begin
- -- Loop through Contract_Case pragmas from spec
+ -- Loop through Contract_Cases pragmas from spec
Prag := Spec_CTC_List (Contract (Spec));
loop
- if Pragma_Name (Prag) = Name_Contract_Case then
- if Plist = No_List then
- Plist := Empty_List;
- end if;
-
- if not Expander_Active then
- Prepend (Grab_CC, Declarations (N));
- else
- Append (Grab_CC, Plist);
- end if;
-
- elsif Pragma_Name (Prag) = Name_Contract_Cases then
+ if Pragma_Name (Prag) = Name_Contract_Cases then
Expand_Contract_Cases (Prag, Spec_Id);
end if;
procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id);
-- Preanalyze the boolean expressions in the Requires and Ensures arguments
- -- of a Contract_Case or Test_Case pragma if present (possibly Empty). We
- -- treat these as spec expressions (i.e. similar to a default expression).
+ -- of a Test_Case pragma if present (possibly Empty). We treat these as
+ -- spec expressions (i.e. similar to a default expression).
procedure Rewrite_Assertion_Kind (N : Node_Id);
-- If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
-- Preanalyze the boolean expressions, we treat these as spec
-- expressions (i.e. similar to a default expression).
- if Nam_In (Pragma_Name (N), Name_Test_Case, Name_Contract_Case) then
+ if Pragma_Name (N) = Name_Test_Case then
Preanalyze_CTC_Args
(N,
Get_Requires_From_CTC_Pragma (N),
-- UU_Typ is the related Unchecked_Union type. Flag In_Variant_Part
-- should be set when Comp comes from a record variant.
- procedure Check_Contract_Or_Test_Case;
- -- Called to process a contract-case or test-case pragma. It
- -- starts with checking pragma arguments, and the rest of the
- -- treatment is similar to the one for pre- and postcondition in
- -- Check_Precondition_Postcondition, except the placement rules for the
- -- contract-case and test-case pragmas are stricter. These pragmas may
- -- only occur after a subprogram spec declared directly in a package
- -- spec unit. In this case, the pragma is chained to the subprogram in
- -- question (using Spec_CTC_List and Next_Pragma) and analysis of the
- -- pragma is delayed till the end of the spec. In all other cases, an
- -- error message for bad placement is given.
+ procedure Check_Test_Case;
+ -- Called to process a test-case pragma. It starts with checking pragma
+ -- arguments, and the rest of the treatment is similar to the one for
+ -- pre- and postcondition in Check_Precondition_Postcondition, except
+ -- the placement rules for the test-case pragma are stricter. These
+ -- pragmas may only occur after a subprogram spec declared directly
+ -- in a package spec unit. In this case, the pragma is chained to the
+ -- subprogram in question (using Spec_CTC_List and Next_Pragma) and
+ -- analysis of the pragma is delayed till the end of the spec. In all
+ -- other cases, an error message for bad placement is given.
procedure Check_Duplicate_Pragma (E : Entity_Id);
-- Check if a rep item of the same name as the current pragma is already
end if;
end Check_Component;
- ---------------------------------
- -- Check_Contract_Or_Test_Case --
- ---------------------------------
+ ---------------------
+ -- Check_Test_Case --
+ ---------------------
- procedure Check_Contract_Or_Test_Case is
+ procedure Check_Test_Case is
P : Node_Id;
PO : Node_Id;
procedure Chain_CTC (PO : Node_Id);
-- If PO is a [generic] subprogram declaration node, then the
- -- contract-case or test-case applies to this subprogram and the
- -- processing for the pragma is completed. Otherwise the pragma
- -- is misplaced.
+ -- test-case applies to this subprogram and the processing for
+ -- the pragma is completed. Otherwise the pragma is misplaced.
---------------
-- Chain_CTC --
-- in this analysis, allowing forward references. The analysis
-- happens at the end of Analyze_Declarations.
- -- There should not be another contract-case or test-case with the
- -- same name associated to this subprogram.
+ -- There should not be another test-case with the same name
+ -- associated to this subprogram.
declare
Name : constant String_Id := Get_Name_From_CTC_Pragma (N);
-- Omit pragma Contract_Cases because it does not introduce
-- a unique case name and it does not follow the syntax of
- -- Contract_Case and Test_Case.
+ -- Test_Case.
if Pragma_Name (CTC) = Name_Contract_Cases then
null;
Set_Spec_CTC_List (Contract (S), N);
end Chain_CTC;
- -- Start of processing for Check_Contract_Or_Test_Case
+ -- Start of processing for Check_Test_Case
begin
-- First check pragma arguments
Pragma_Misplaced;
end if;
- -- Contract-case or test-case should only appear in package spec unit
+ -- Test-case should only appear in package spec unit
if Get_Source_Unit (N) = No_Unit
or else not Nkind_In (Sinfo.Unit (Cunit (Get_Source_Unit (N))),
-- If the previous node is a generic subprogram, do not go to to
-- the original node, which is the unanalyzed tree: we need to
- -- attach the contract-case or test-case to the analyzed version
- -- at this point. They get propagated to the original tree when
- -- analyzing the corresponding body.
+ -- attach the test-case to the analyzed version at this point.
+ -- They get propagated to the original tree when analyzing the
+ -- corresponding body.
if Nkind (P) not in N_Generic_Declaration then
PO := Original_Node (P);
-- If we fall through, pragma was misplaced
Pragma_Misplaced;
- end Check_Contract_Or_Test_Case;
+ end Check_Test_Case;
----------------------------
-- Check_Duplicate_Pragma --
end if;
end Component_AlignmentP;
- -------------------
- -- Contract_Case --
- -------------------
-
- -- pragma Contract_Case
- -- ([Name =>] Static_String_EXPRESSION
- -- ,[Mode =>] MODE_TYPE
- -- [, Requires => Boolean_EXPRESSION]
- -- [, Ensures => Boolean_EXPRESSION]);
-
- -- MODE_TYPE ::= Nominal | Robustness
-
- when Pragma_Contract_Case =>
- Check_Contract_Or_Test_Case;
-
--------------------
-- Contract_Cases --
--------------------
-- MODE_TYPE ::= Nominal | Robustness
when Pragma_Test_Case =>
- Check_Contract_Or_Test_Case;
+ Check_Test_Case;
--------------------------
-- Thread_Local_Storage --
Pragma_Complete_Representation => 0,
Pragma_Complex_Representation => 0,
Pragma_Component_Alignment => -1,
- Pragma_Contract_Case => -1,
Pragma_Contract_Cases => -1,
Pragma_Controlled => 0,
Pragma_Convention => 0,
-- Otherwise return Empty. Expression N should have been resolved already.
function Get_Ensures_From_CTC_Pragma (N : Node_Id) return Node_Id;
- -- Return the Ensures component of Contract_Case or Test_Case pragma N, or
- -- Empty otherwise.
+ -- Return the Ensures component of Test_Case pragma N, or Empty otherwise
function Get_Generic_Entity (N : Node_Id) return Entity_Id;
-- Returns the true generic entity in an instantiation. If the name in the
-- Sem_Ch8 for further details on handling of entity visibility.
function Get_Name_From_CTC_Pragma (N : Node_Id) return String_Id;
- -- Return the Name component of Contract_Case or Test_Case pragma N
+ -- Return the Name component of Test_Case pragma N
function Get_Pragma_Id (N : Node_Id) return Pragma_Id;
pragma Inline (Get_Pragma_Id);
-- with any other kind of entity.
function Get_Requires_From_CTC_Pragma (N : Node_Id) return Node_Id;
- -- Return the Requires component of Contract_Case or Test_Case pragma N, or
- -- Empty otherwise.
+ -- Return the Requires component of Test_Case pragma N, or Empty otherwise
function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id;
-- Nod is either a procedure call statement, or a function call, or an
SE : constant Entity_Id := Scope (E);
function Within_Postcondition return Boolean;
- -- Returns True iff N is within a Postcondition or
- -- Ensures component in a Contract_Case or Test_Case.
+ -- Returns True iff N is within a Postcondition, an
+ -- Ensures component in a Test_Case, or a Contract_Cases.
--------------------------
-- Within_Postcondition --
Nod := Parent (N);
while Present (Nod) loop
if Nkind (Nod) = N_Pragma
- and then Pragma_Name (Nod) = Name_Postcondition
+ and then Nam_In (Pragma_Name (Nod),
+ Name_Postcondition,
+ Name_Contract_Cases)
then
return True;
if Nkind (P) = N_Pragma
and then
- Nam_In (Pragma_Name (P), Name_Contract_Case,
- Name_Test_Case)
+ Pragma_Name (P) = Name_Test_Case
and then
Nod = Get_Ensures_From_CTC_Pragma (P)
then
-- Note that this includes precondition/postcondition pragmas generated
-- to correspond to Pre/Post aspects.
- -- Spec_CTC_List points to a list of Contract_Case and Test_Case pragma
+ -- Spec_CTC_List points to a list of Contract_Cases and Test_Case pragma
-- nodes for contract-cases and test-cases declared in the spec of the
-- entry/subprogram. The last pragma encountered is at the head of this
-- list, so it is in reverse order of textual appearance. Note that
- -- this includes contract-case and test-case pragmas generated from
- -- Contract_Case and Test_Case aspects.
+ -- this includes contract-cases and test-case pragmas generated from
+ -- Contract_Cases and Test_Case aspects.
-------------------
-- Expanded_Name --
Name_Common_Object : constant Name_Id := N + $; -- GNAT
Name_Complete_Representation : constant Name_Id := N + $; -- GNAT
Name_Complex_Representation : constant Name_Id := N + $; -- GNAT
- Name_Contract_Case : constant Name_Id := N + $; -- GNAT
Name_Contract_Cases : constant Name_Id := N + $; -- GNAT
Name_Controlled : constant Name_Id := N + $;
Name_Convention : constant Name_Id := N + $;
Pragma_Common_Object,
Pragma_Complete_Representation,
Pragma_Complex_Representation,
- Pragma_Contract_Case,
Pragma_Contract_Cases,
Pragma_Controlled,
Pragma_Convention,
projects / platform / upstream / linaro-gcc.git / commitdiff