+2011-08-04 Yannick Moy <moy@adacore.com>
+
+ * gnat_rm.texi: Document new pragma and aspect.
+ * aspects.adb, aspects.ads (Aspect_Id): new value Aspect_Test_Case
+ (No_Duplicates_Allowed): new constant array defining whether duplicates
+ aspects of each kind can appear on the same declaration.
+ * einfo.adb, einfo.ads (Spec_PPC_List): replace field with Contract
+ field, which points to a node holding the previous Spec_PPC_List.
+ * exp_ch9.adb, sem_ch6.adb, sem_prag.adb: Reach to Spec_PPC_List
+ through the indirection with Contract.
+ * exp_util.adb (Insert_Actions): raise Program_Error on N_Contract node
+ * par-prag.adb (Prag): do nothing on Test_Case pragma
+ * sem.adb (Analyze): abort on N_Contract, on which Analyze should not
+ be called directly.
+ * sem_attr.adb (Analyze_Attribute): allow attribute 'Result in
+ component Ensures of Test_Case.
+ * sem_ch12.adb, sem_ch6.adb, sem_ch9.adb
+ (Analyze_Generic_Subprogram_Declaration,
+ Analyze_Subprogram_Instantiation,
+ Analyze_Abstract_Subprogram_Declaration,
+ Analyze_Subprogram_Body_Helper,
+ Analyze_Subprogram_Specification, Analyze_Entry_Declaration):
+ insert contract in subprogram node at point of definition
+ * sem_ch13.adb
+ (Aspect_Loop): do not raise error on duplicate Test_Case aspect
+ (Analyze_Aspect_Specifications): analyze Test_Case aspect and create
+ corresponding pragma
+ (Check_Aspect_At_Freeze_Point): raise Program_Error on Test_Case aspect
+ * sem_ch3.adb (Analyze_Declarations): insert analysis of test-cases,
+ similar to the analysis of pre/post
+ (Derive_Subprogram): insert contract in subprogram node at point of
+ derivation.
+ * sem_prag.adb, sem_prag.ads
+ (Check_Arg_Is_String_Literal, Check_Identifier):
+ new checking procedures to be called in treatment of pragmas
+ (Check_Test_Case): new procedure to check that a Test_Case aspect or
+ pragma is well-formed. This does not check currently that 'Result is
+ used only in the Ensures component of a Test_Case.
+ (Analyze_Pragma): add case for Test_Case
+ (Analyze_TC_In_Decl_Part): pre-analyze the Requires and Ensures
+ components of a Test_Case.
+ (Preanalyze_TC_Args): new procedure to preanalyze the boolean
+ expressions in the 3rd (and 4th if present) arguments of a Test_Case
+ pragma, treated as spec expressions.
+ (Sig_Flags): add value -1 for Test_Case.
+ * sem_util.adb, sem_util.ads (Get_Ensures_From_Test_Case_Pragma,
+ Get_Requires_From_Test_Case_Pragma): getters for both expression
+ components of a Test_Case.
+ * sinfo.adb, sinfo.ads (N_Contract): new kind of node used as
+ indirection between an entry or [generic] subprogram entity and its
+ pre/post + test-cases.
+ (Spec_PPC_List, Spec_TC_List, Set_Spec_PPC_List, Set_Spec_TC_List):
+ get/set for fields of an N_Contract node.
+ * snames.ads-tmpl (Name_Test_Case, Name_Ensures, Name_Mode,
+ Name_Normal, Name_Requires, Name_Robustness, Pragma_Test_Case): new
+ names and pragma for Test_Case.
+ * sprint.adb (Sprint_Node): raise Program_Error on N_Contract node
+
2011-08-04 Vincent Celier <celier@adacore.com>
* gnat_ugn.texi: Improve documentation of gnatmake switch
-- --
-- B o d y --
-- --
--- Copyright (C) 2010, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
Aspect_Stream_Size => Aspect_Stream_Size,
Aspect_Suppress => Aspect_Suppress,
Aspect_Suppress_Debug_Info => Aspect_Suppress_Debug_Info,
+ Aspect_Test_Case => Aspect_Test_Case,
Aspect_Type_Invariant => Aspect_Invariant,
Aspect_Unchecked_Union => Aspect_Unchecked_Union,
Aspect_Universal_Aliasing => Aspect_Universal_Aliasing,
-- --
-- S p e c --
-- --
--- Copyright (C) 2010, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
Aspect_Storage_Size,
Aspect_Stream_Size,
Aspect_Suppress,
+ Aspect_Test_Case, -- GNAT
Aspect_Type_Invariant,
Aspect_Unsuppress,
Aspect_Value_Size, -- GNAT
Aspect_Post => True,
others => False);
+ -- The following array indicates aspects for which multiple occurrences of
+ -- the same aspect attached to the same declaration are allowed.
+
+ No_Duplicates_Allowed : constant array (Aspect_Id) of Boolean :=
+ (Aspect_Test_Case => False,
+ others => True);
+
-- The following subtype defines aspects corresponding to library unit
-- pragmas, these can only validly appear as aspects for library units,
-- and result in a corresponding pragma being inserted immediately after
Aspect_Storage_Size => Expression,
Aspect_Stream_Size => Expression,
Aspect_Suppress => Name,
+ Aspect_Test_Case => Expression,
Aspect_Type_Invariant => Expression,
Aspect_Unsuppress => Name,
Aspect_Value_Size => Expression,
Aspect_Stream_Size => Name_Stream_Size,
Aspect_Suppress => Name_Suppress,
Aspect_Suppress_Debug_Info => Name_Suppress_Debug_Info,
+ Aspect_Test_Case => Name_Test_Case,
Aspect_Type_Invariant => Name_Type_Invariant,
Aspect_Unchecked_Union => Name_Unchecked_Union,
Aspect_Universal_Aliasing => Name_Universal_Aliasing,
-- Finalizer Node24
-- Related_Expression Node24
- -- Spec_PPC_List Node24
+ -- Contract Node24
-- Interface_Alias Node25
-- Interfaces Elist25
return Node18 (Id);
end Entry_Index_Constant;
+ function Contract (Id : E) return N is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Entry, E_Entry_Family)
+ or else Is_Subprogram (Id)
+ or else Is_Generic_Subprogram (Id));
+ return Node24 (Id);
+ end Contract;
+
function Entry_Parameters_Type (Id : E) return E is
begin
return Node15 (Id);
return Node19 (Id);
end Spec_Entity;
- function Spec_PPC_List (Id : E) return N is
- begin
- pragma Assert
- (Ekind_In (Id, E_Entry, E_Entry_Family)
- or else Is_Subprogram (Id)
- or else Is_Generic_Subprogram (Id));
- return Node24 (Id);
- end Spec_PPC_List;
-
function Static_Predicate (Id : E) return S is
begin
pragma Assert (Is_Discrete_Type (Id));
Set_Node18 (Id, V);
end Set_Entry_Index_Constant;
+ procedure Set_Contract (Id : E; V : N) is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void)
+ or else Is_Subprogram (Id)
+ or else Is_Generic_Subprogram (Id));
+ Set_Node24 (Id, V);
+ end Set_Contract;
+
procedure Set_Entry_Parameters_Type (Id : E; V : E) is
begin
Set_Node15 (Id, V);
Set_Node19 (Id, V);
end Set_Spec_Entity;
- procedure Set_Spec_PPC_List (Id : E; V : N) is
- begin
- pragma Assert
- (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void)
- or else Is_Subprogram (Id)
- or else Is_Generic_Subprogram (Id));
- Set_Node24 (Id, V);
- end Set_Spec_PPC_List;
-
procedure Set_Static_Predicate (Id : E; V : S) is
begin
pragma Assert
Type_Kind =>
Write_Str ("Related_Expression");
- when Subprogram_Kind =>
- Write_Str ("Spec_PPC_List");
+ when E_Entry |
+ E_Entry_Family |
+ Subprogram_Kind |
+ Generic_Subprogram_Kind =>
+ Write_Str ("Contract");
when others =>
Write_Str ("Field24???");
-- accept statement for a member of the family, and in the prefix of
-- 'COUNT when it applies to a family member.
+-- Contract (Node24)
+-- Present in entries, and in subprogram and generic subprogram entities.
+-- Points to the contract of the entity, holding both pre- and
+-- postconditions as well as test-cases.
+
-- Entry_Parameters_Type (Node15)
-- Present in entries. Points to the access-to-record type that is
-- constructed by the expander to hold a reference to the parameter
-- case where there is a separate spec, where this field references
-- the corresponding parameter entities in the spec.
--- Spec_PPC_List (Node24)
--- Present in entries, and in subprogram and generic subprogram entities.
--- Points to a list of Precondition and Postcondition pragma nodes for
--- preconditions and postconditions declared in the spec. The last pragma
--- encountered is at the head of this list, so it is in reverse order of
--- textual appearance. Note that this includes precondition/postcondition
--- pragmas generated to correspond to Pre/Post aspects.
-
-- Static_Predicate (List25)
-- Present in discrete types/subtypes with predicates (Has_Predicates
-- set True). Points to a list of expression and N_Range nodes that
-- Accept_Address (Elist21)
-- Scope_Depth_Value (Uint22)
-- Protection_Object (Node23) (protected kind)
- -- Spec_PPC_List (Node24) (for entry only)
+ -- Contract (Node24) (for entry only)
-- PPC_Wrapper (Node25)
-- Default_Expressions_Processed (Flag108)
-- Entry_Accepted (Flag152)
-- Generic_Renamings (Elist23) (for an instance)
-- Inner_Instances (Elist23) (generic case only)
-- Protection_Object (Node23) (for concurrent kind)
- -- Spec_PPC_List (Node24)
+ -- Contract (Node24)
-- Interface_Alias (Node25)
-- Overridden_Operation (Node26)
-- Wrapped_Entity (Node27) (non-generic case only)
-- Generic_Renamings (Elist23) (for an instance)
-- Inner_Instances (Elist23) (generic case only)
-- Protection_Object (Node23) (for concurrent kind)
- -- Spec_PPC_List (Node24)
+ -- Contract (Node24)
-- Interface_Alias (Node25)
-- Static_Initialization (Node26) (init_proc only)
-- Overridden_Operation (Node26) (never for init proc)
function Entry_Formal (Id : E) return E;
function Entry_Index_Constant (Id : E) return E;
function Entry_Index_Type (Id : E) return E;
+ function Contract (Id : E) return N;
function Entry_Parameters_Type (Id : E) return E;
function Enum_Pos_To_Rep (Id : E) return E;
function Enumeration_Pos (Id : E) return U;
function Size_Depends_On_Discriminant (Id : E) return B;
function Small_Value (Id : E) return R;
function Spec_Entity (Id : E) return E;
- function Spec_PPC_List (Id : E) return N;
function Static_Predicate (Id : E) return S;
function Storage_Size_Variable (Id : E) return E;
function Static_Elaboration_Desired (Id : E) return B;
procedure Set_Entry_Component (Id : E; V : E);
procedure Set_Entry_Formal (Id : E; V : E);
procedure Set_Entry_Index_Constant (Id : E; V : E);
+ procedure Set_Contract (Id : E; V : N);
procedure Set_Entry_Parameters_Type (Id : E; V : E);
procedure Set_Enum_Pos_To_Rep (Id : E; V : E);
procedure Set_Enumeration_Pos (Id : E; V : U);
procedure Set_Size_Known_At_Compile_Time (Id : E; V : B := True);
procedure Set_Small_Value (Id : E; V : R);
procedure Set_Spec_Entity (Id : E; V : E);
- procedure Set_Spec_PPC_List (Id : E; V : N);
procedure Set_Static_Predicate (Id : E; V : S);
procedure Set_Storage_Size_Variable (Id : E; V : E);
procedure Set_Static_Elaboration_Desired (Id : E; V : B);
pragma Inline (Component_Clause);
pragma Inline (Component_Size);
pragma Inline (Component_Type);
+ pragma Inline (Contract);
pragma Inline (Corresponding_Concurrent_Type);
pragma Inline (Corresponding_Discriminant);
pragma Inline (Corresponding_Equality);
pragma Inline (Size_Known_At_Compile_Time);
pragma Inline (Small_Value);
pragma Inline (Spec_Entity);
- pragma Inline (Spec_PPC_List);
pragma Inline (Static_Predicate);
pragma Inline (Storage_Size_Variable);
pragma Inline (Static_Elaboration_Desired);
pragma Inline (Set_Component_Clause);
pragma Inline (Set_Component_Size);
pragma Inline (Set_Component_Type);
+ pragma Inline (Set_Contract);
pragma Inline (Set_Corresponding_Concurrent_Type);
pragma Inline (Set_Corresponding_Discriminant);
pragma Inline (Set_Corresponding_Equality);
pragma Inline (Set_Size_Known_At_Compile_Time);
pragma Inline (Set_Small_Value);
pragma Inline (Set_Spec_Entity);
- pragma Inline (Set_Spec_PPC_List);
pragma Inline (Set_Static_Predicate);
pragma Inline (Set_Storage_Size_Variable);
pragma Inline (Set_Static_Elaboration_Desired);
P : Node_Id;
begin
- P := Spec_PPC_List (E);
+ P := Spec_PPC_List (Contract (E));
if No (P) then
return;
end if;
Ent := First_Entity (Tasktyp);
while Present (Ent) loop
if Ekind_In (Ent, E_Entry, E_Entry_Family)
- and then Present (Spec_PPC_List (Ent))
+ and then Present (Spec_PPC_List (Contract (Ent)))
then
Build_PPC_Wrapper (Ent, N);
end if;
null;
end if;
+ -- A contract node should not belong to the tree
+
+ when N_Contract =>
+ raise Program_Error;
+
-- For all other node types, keep climbing tree
when
* Pragma Task_Info::
* Pragma Task_Name::
* Pragma Task_Storage::
+* Pragma Test_Case::
* Pragma Thread_Local_Storage::
* Pragma Time_Slice::
* Pragma Title::
* Pragma Task_Info::
* Pragma Task_Name::
* Pragma Task_Storage::
+* Pragma Test_Case::
* Pragma Thread_Local_Storage::
* Pragma Time_Slice::
* Pragma Title::
must be true may contain references to function'Result in the case
of a function to refer to the returned value.
-@code{Postcondition} pragmas may appear either immediate following the
+@code{Postcondition} pragmas may appear either immediately following the
(separate) declaration of a subprogram, or at the start of the
declarations of a subprogram body. Only other pragmas may intervene
(that is appear between the subprogram declaration and its
@end smallexample
@noindent
-@code{Precondition} pragmas may appear either immediate following the
+@code{Precondition} pragmas may appear either immediately following the
(separate) declaration of a subprogram, or at the start of the
declarations of a subprogram body. Only other pragmas may intervene
(that is appear between the subprogram declaration and its
@code{Storage_Size} attribute definition clause is allowed for a task
type.
+@node Pragma Test_Case
+@unnumberedsec Pragma Test_Case
+@cindex Test cases
+@findex Test_Case
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Test_Case (
+ [Name =>] String_Expression
+ ,[Mode =>] (Normal | Robustness)
+ [, Requires => Boolean_Expression]
+ [, Ensures => Boolean_Expression]);
+@end smallexample
+
+@noindent
+The @code{Test_Case} pragma applies to the same entities as pragmas
+@code{Precondition} and @code{Postcondition}. In particular, the
+placement and visibility rules are identical to those described for pre-
+and postconditions. But the presence of pragma @code{Test_Case} does not
+lead to any modification of the code generated by the compiler. Rather,
+its purpose is to document finer-grain specifications for use by testing
+and verification tools.
+
+The compiler checks that boolean expression given in @code{Requires} and
+@code{Ensures} are valid, where the rules for @code{Requires} are the
+same as the rule for an expression in @code{Precondition} and the rules
+for @code{Ensures} are the same as the rule for an expression in
+@code{Postcondition}. In particular, attributes @code{'Old} and
+@code{'Result} can only be used within the @code{Ensures}
+expression. The following is an example of use within a package spec:
+
+@smallexample @c ada
+package Math_Functions is
+ ...
+ function Sqrt (Arg : Float) return Float;
+ pragma Test_Case (Name => ``Test_1``,
+ Mode => Normal,
+ Requires => Arg < 100,
+ Ensures => Sqrt'Result < 10);
+ ...
+end Math_Functions;
+@end smallexample
+
+@noindent
+@code{Test_Case} pragmas may appear either immediately following the
+(separate) declaration of a subprogram, or at the start of the
+declarations of a subprogram body. Only other pragmas may intervene
+(that is appear between the subprogram declaration and its test cases,
+or appear before the test case in the declaration sequence in a
+subprogram body).
+
@node Pragma Thread_Local_Storage
@unnumberedsec Pragma Thread_Local_Storage
@findex Thread_Local_Storage
@item @code{Stream_Size} @tab
@item @code{Suppress} @tab
@item @code{Suppress_Debug_Info} @tab -- GNAT
+@item @code{Test_Case} @tab -- GNAT
@item @code{Unchecked_Union} @tab
@item @code{Universal_Aliasing} @tab -- GNAT
@item @code{Unmodified} @tab -- GNAT
Pragma_Task_Info |
Pragma_Task_Name |
Pragma_Task_Storage |
+ Pragma_Test_Case |
Pragma_Thread_Local_Storage |
Pragma_Time_Slice |
Pragma_Title |
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
N_Component_Definition |
N_Component_List |
N_Constrained_Array_Definition |
+ N_Contract |
N_Decimal_Fixed_Point_Definition |
N_Defining_Character_Literal |
N_Defining_Identifier |
Prag := Parent (Prag);
end loop;
- if Nkind (Prag) /= N_Pragma
- or else Get_Pragma_Id (Prag) /= Pragma_Postcondition
- then
+ if Nkind (Prag) /= N_Pragma then
+ Error_Attr
+ ("% attribute can only appear in postcondition of function",
+ P);
+
+ elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
+ declare
+ Arg_Ens : constant Node_Id :=
+ Get_Ensures_From_Test_Case_Pragma (Prag);
+ Arg : Node_Id;
+
+ begin
+ Arg := N;
+ while Arg /= Prag and Arg /= Arg_Ens loop
+ Arg := Parent (Arg);
+ end loop;
+
+ if Arg /= Arg_Ens then
+ Error_Attr ("% attribute misplaced inside Test_Case", P);
+ end if;
+ end;
+
+ elsif Get_Pragma_Id (Prag) /= Pragma_Postcondition then
Error_Attr
("% attribute can only appear in postcondition of function",
P);
Spec := Specification (N);
Id := Defining_Entity (Spec);
Generate_Definition (Id);
+ Set_Contract (Id, Make_Contract (Sloc (Id)));
if Nkind (Id) = N_Defining_Operator_Symbol then
Error_Msg_N
end if;
Generate_Definition (Act_Decl_Id);
+ Set_Contract (Anon_Id, Make_Contract (Sloc (Anon_Id))); -- ??? needed?
+ Set_Contract (Act_Decl_Id, Make_Contract (Sloc (Act_Decl_Id)));
Set_Is_Inlined (Act_Decl_Id, Is_Inlined (Gen_Unit));
Set_Is_Inlined (Anon_Id, Is_Inlined (Gen_Unit));
-- test allows duplicate Pre/Post's that we generate internally
-- to escape being flagged here.
- Anod := First (L);
- while Anod /= Aspect loop
- if Same_Aspect (A_Id, Get_Aspect_Id (Chars (Identifier (Anod))))
- and then Comes_From_Source (Aspect)
- then
- Error_Msg_Name_1 := Nam;
- Error_Msg_Sloc := Sloc (Anod);
+ if No_Duplicates_Allowed (A_Id) then
+ Anod := First (L);
+ while Anod /= Aspect loop
+ if Same_Aspect
+ (A_Id, Get_Aspect_Id (Chars (Identifier (Anod))))
+ and then Comes_From_Source (Aspect)
+ then
+ Error_Msg_Name_1 := Nam;
+ Error_Msg_Sloc := Sloc (Anod);
- -- Case of same aspect specified twice
+ -- Case of same aspect specified twice
- if Class_Present (Anod) = Class_Present (Aspect) then
- if not Class_Present (Anod) then
- Error_Msg_NE
- ("aspect% for & previously given#",
- Id, E);
- else
- Error_Msg_NE
- ("aspect `%''Class` for & previously given#",
- Id, E);
- end if;
+ if Class_Present (Anod) = Class_Present (Aspect) then
+ if not Class_Present (Anod) then
+ Error_Msg_NE
+ ("aspect% for & previously given#",
+ Id, E);
+ else
+ Error_Msg_NE
+ ("aspect `%''Class` for & previously given#",
+ Id, E);
+ end if;
- -- Case of Pre and Pre'Class both specified
+ -- Case of Pre and Pre'Class both specified
- elsif Nam = Name_Pre then
- if Class_Present (Aspect) then
- Error_Msg_NE
- ("aspect `Pre''Class` for & is not allowed here",
- Id, E);
- Error_Msg_NE
- ("\since aspect `Pre` previously given#",
- Id, E);
+ elsif Nam = Name_Pre then
+ if Class_Present (Aspect) then
+ Error_Msg_NE
+ ("aspect `Pre''Class` for & is not allowed here",
+ Id, E);
+ Error_Msg_NE
+ ("\since aspect `Pre` previously given#",
+ Id, E);
- else
- Error_Msg_NE
- ("aspect `Pre` for & is not allowed here",
- Id, E);
- Error_Msg_NE
- ("\since aspect `Pre''Class` previously given#",
- Id, E);
+ else
+ Error_Msg_NE
+ ("aspect `Pre` for & is not allowed here",
+ Id, E);
+ Error_Msg_NE
+ ("\since aspect `Pre''Class` previously given#",
+ Id, E);
+ end if;
end if;
- end if;
- -- Allowed case of X and X'Class both specified
- end if;
+ -- Allowed case of X and X'Class both specified
+ end if;
- Next (Anod);
- end loop;
+ Next (Anod);
+ end loop;
+ end if;
-- Copy expression for later processing by the procedures
-- Check_Aspect_At_[Freeze_Point | End_Of_Declarations]
Aspect_Static_Predicate =>
-- Construct the pragma (always a pragma Predicate, with
- -- flags recording whether
+ -- flags recording whether it is static/dynamic).
Aitem :=
Make_Pragma (Loc,
Ensure_Freeze_Node (E);
Set_Is_Delayed_Aspect (Aspect);
Delay_Required := True;
+
+ when Aspect_Test_Case => declare
+ Args : List_Id;
+ Comp_Expr : Node_Id;
+ Comp_Assn : Node_Id;
+
+ begin
+ Args := New_List;
+
+ if Nkind (Expr) /= N_Aggregate then
+ Error_Msg_NE
+ ("wrong syntax for aspect `Test_Case` for &", Id, E);
+ goto Continue;
+ end if;
+
+ Comp_Expr := First (Expressions (Expr));
+ while Present (Comp_Expr) loop
+ Append (Relocate_Node (Comp_Expr), Args);
+ Next (Comp_Expr);
+ end loop;
+
+ Comp_Assn := First (Component_Associations (Expr));
+ while Present (Comp_Assn) loop
+ if List_Length (Choices (Comp_Assn)) /= 1
+ or else
+ Nkind (First (Choices (Comp_Assn))) /= N_Identifier
+ then
+ Error_Msg_NE
+ ("wrong syntax for aspect `Test_Case` for &", Id, E);
+ goto Continue;
+ end if;
+
+ Append (Make_Pragma_Argument_Association (
+ Sloc => Sloc (Comp_Assn),
+ Chars => Chars (First (Choices (Comp_Assn))),
+ Expression => Relocate_Node (Expression (Comp_Assn))),
+ Args);
+ Next (Comp_Assn);
+ end loop;
+
+ -- Build the test-case pragma
+
+ Aitem :=
+ Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Sloc (Id), Name_Test_Case),
+ Pragma_Argument_Associations =>
+ Args);
+
+ Set_From_Aspect_Specification (Aitem, True);
+ Set_Is_Delayed_Aspect (Aspect);
+
+ -- Insert immediately after the entity declaration
+
+ Insert_After (N, Aitem);
+
+ goto Continue;
+ end;
end case;
-- If a delay is required, we delay the freeze (not much point in
when Boolean_Aspects =>
raise Program_Error;
+ -- Test_Case aspect applies to entries and subprograms, hence should
+ -- never be delayed.
+
+ when Aspect_Test_Case =>
+ raise Program_Error;
+
-- Default_Value is resolved with the type entity in question
when Aspect_Default_Value =>
when Aspect_Storage_Pool =>
T := Class_Wide_Type (RTE (RE_Root_Storage_Pool));
- when
- Aspect_Alignment |
+ when Aspect_Alignment |
Aspect_Component_Size |
Aspect_Machine_Radix |
Aspect_Object_Size |
Analyze (Expression (ASN));
return;
- -- Suppress/Unsupress/Warnings should never be delayed
+ -- Suppress/Unsuppress/Warnings should never be delayed
when Aspect_Suppress |
Aspect_Unsuppress |
if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then
Spec := Specification (Original_Node (Decl));
Sent := Defining_Unit_Name (Spec);
- Prag := Spec_PPC_List (Sent);
+
+ Prag := Spec_PPC_List (Contract (Sent));
while Present (Prag) loop
Analyze_PPC_In_Decl_Part (Prag, Sent);
Prag := Next_Pragma (Prag);
end loop;
+
+ Prag := Spec_TC_List (Contract (Sent));
+ while Present (Prag) loop
+ Analyze_TC_In_Decl_Part (Prag, Sent);
+ Prag := Next_Pragma (Prag);
+ end loop;
end if;
Next (Decl);
New_Subp :=
New_Entity (Nkind (Parent_Subp), Sloc (Derived_Type));
Set_Ekind (New_Subp, Ekind (Parent_Subp));
+ Set_Contract (New_Subp, Make_Contract (Sloc (New_Subp)));
-- Check whether the inherited subprogram is a private operation that
-- should be inherited but not yet made visible. Such subprograms can
Check_SPARK_Restriction ("abstract subprogram is not allowed", N);
Generate_Definition (Designator);
+ Set_Contract (Designator, Make_Contract (Sloc (Designator)));
Set_Is_Abstract_Subprogram (Designator);
New_Overloaded_Entity (Designator);
Check_Delayed_Subprogram (Designator);
if Nkind (N) /= N_Subprogram_Body_Stub then
Set_Acts_As_Spec (N);
Generate_Definition (Body_Id);
+ Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
Generate_Reference
(Body_Id, Body_Id, 'b', Set_Ref => False, Force => True);
Generate_Reference_To_Formals (Body_Id);
Designator := Analyze_Subprogram_Specification (Specification (N));
Generate_Definition (Designator);
+ -- ??? why this call, already in Analyze_Subprogram_Specification
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
-- Proceed with analysis
Generate_Definition (Designator);
+ Set_Contract (Designator, Make_Contract (Sloc (Designator)));
if Nkind (N) = N_Function_Specification then
Set_Ekind (Designator, E_Function);
begin
for J in Inherited'Range loop
- P := Spec_PPC_List (Inherited (J));
+ P := Spec_PPC_List (Contract (Inherited (J)));
+
while Present (P) loop
Error_Msg_Sloc := Sloc (P);
-- the body will be analyzed and converted when we scan the body
-- declarations below.
- Prag := Spec_PPC_List (Spec_Id);
+ Prag := Spec_PPC_List (Contract (Spec_Id));
while Present (Prag) loop
if Pragma_Name (Prag) = Name_Precondition then
-- Now deal with inherited preconditions
for J in Inherited'Range loop
- Prag := Spec_PPC_List (Inherited (J));
+ Prag := Spec_PPC_List (Contract (Inherited (J)));
while Present (Prag) loop
if Pragma_Name (Prag) = Name_Precondition
-- Loop through PPC pragmas from spec
- Prag := Spec_PPC_List (Spec);
+ Prag := Spec_PPC_List (Contract (Spec));
loop
if Pragma_Name (Prag) = Name_Postcondition
and then (not Class or else Class_Present (Prag))
-- Start of processing for Spec_Postconditions
begin
- if Present (Spec_PPC_List (Spec_Id)) then
+ if Present (Spec_PPC_List (Contract (Spec_Id))) then
Process_Post_Conditions (Spec_Id, Class => False);
end if;
-- Process inherited postconditions
for J in Inherited'Range loop
- if Present (Spec_PPC_List (Inherited (J))) then
+ if Present (Spec_PPC_List (Contract (Inherited (J)))) then
Process_Post_Conditions (Inherited (J), Class => True);
end if;
end loop;
begin
Generate_Definition (Def_Id);
+ Set_Contract (Def_Id, Make_Contract (Sloc (Def_Id)));
Tasking_Used := True;
-- Case of no discrete subtype definition
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
+ procedure Preanalyze_TC_Args (Arg_Req, Arg_Ens : Node_Id);
+ -- Preanalyze the boolean expressions in the Requires and Ensures arguments
+ -- of a Test_Case pragma if present (possibly Empty). We treat these as
+ -- spec expressions (i.e. similar to a default expression).
+
procedure rv;
-- This is a dummy function called by the processing for pragma Reviewable.
-- It is there for assisting front end debugging. By placing a Reviewable
-- Check the specified argument Arg to make sure that it is an integer
-- literal. If not give error and raise Pragma_Exit.
+ procedure Check_Arg_Is_String_Literal (Arg : Node_Id);
+ -- Check the specified argument Arg to make sure that it is a string
+ -- literal. If not give error and raise Pragma_Exit.
+
procedure Check_Arg_Is_Library_Level_Local_Name (Arg : Node_Id);
-- Check the specified argument Arg to make sure that it has the proper
-- syntactic form for a local name and meets the semantic requirements
-- Checks that Arg, whose expression is an entity name, references a
-- first subtype.
+ procedure Check_Identifier (Arg : Node_Id; Id : Name_Id);
+ -- Checks that the given argument has an identifier, and if so, requires
+ -- it to match the given identifier name. If there is no identifier, or
+ -- a non-matching identifier, then an error message is given and
+ -- Error_Pragmas raised.
+
procedure Check_In_Main_Program;
-- Common checks for pragmas that appear within a main program
-- (Priority, Main_Storage, Time_Slice, Relative_Deadline, CPU).
-- that the constraint is static as required by the restrictions for
-- Unchecked_Union.
+ procedure Check_Test_Case;
+ -- Called to process a test-case pragma. The treatment is similar to the
+ -- one for pre- and postcondition in Check_Precondition_Postcondition.
+ -- There are three cases:
+ --
+ -- The pragma appears after a subprogram spec
+ --
+ -- The first step is to analyze the pragma, but this is skipped if
+ -- the subprogram spec appears within a package specification
+ -- (because this is the case where we delay analysis till the end of
+ -- the spec). Then (whether or not it was analyzed), the pragma is
+ -- chained to the subprogram in question (using Spec_TC_List and
+ -- Next_Pragma).
+ --
+ -- The pragma appears at the start of subprogram body declarations
+ --
+ -- In this case an immediate return to the caller is made, and the
+ -- pragma is NOT analyzed.
+ --
+ -- In all other cases, an error message for bad placement is given
+
procedure Check_Valid_Configuration_Pragma;
-- Legality checks for placement of a configuration pragma
end if;
end Check_Arg_Is_Integer_Literal;
+ ---------------------------------
+ -- Check_Arg_Is_String_Literal --
+ ---------------------------------
+
+ procedure Check_Arg_Is_String_Literal (Arg : Node_Id) is
+ Argx : constant Node_Id := Get_Pragma_Arg (Arg);
+ begin
+ if Nkind (Argx) /= N_String_Literal then
+ Error_Pragma_Arg
+ ("argument for pragma% must be string literal", Argx);
+ end if;
+ end Check_Arg_Is_String_Literal;
+
-------------------------------------------
-- Check_Arg_Is_Library_Level_Local_Name --
-------------------------------------------
Error_Pragma_Arg ("invalid argument for pragma%", Argx);
end if;
end Check_Arg_Is_One_Of;
+
---------------------------------
-- Check_Arg_Is_Queuing_Policy --
---------------------------------
end if;
end Check_First_Subtype;
+ ----------------------
+ -- Check_Identifier --
+ ----------------------
+
+ procedure Check_Identifier (Arg : Node_Id; Id : Name_Id) is
+ begin
+ if Present (Arg)
+ and then Nkind (Arg) = N_Pragma_Argument_Association
+ then
+ if Chars (Arg) = No_Name or else Chars (Arg) /= Id then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_Name_2 := Id;
+ Error_Msg_N ("pragma% argument expects identifier%", Arg);
+ raise Pragma_Exit;
+ end if;
+ end if;
+ end Check_Identifier;
+
---------------------------
-- Check_In_Main_Program --
---------------------------
PO : Node_Id;
procedure Chain_PPC (PO : Node_Id);
- -- If PO is a subprogram declaration node (or a generic subprogram
- -- declaration node), then the precondition/postcondition applies
- -- to this subprogram and the processing for the pragma is completed.
- -- Otherwise the pragma is misplaced.
+ -- If PO is an entry or a [generic] subprogram declaration node, then
+ -- the precondition/postcondition applies to this subprogram and the
+ -- processing for the pragma is completed. Otherwise the pragma is
+ -- misplaced.
---------------
-- Chain_PPC --
if Pragma_Name (N) = Name_Precondition then
if not From_Aspect_Specification (N) then
- P := Spec_PPC_List (S);
+ P := Spec_PPC_List (Contract (S));
while Present (P) loop
if Pragma_Name (P) = Name_Precondition
and then From_Aspect_Specification (P)
begin
for J in Inherited'Range loop
- P := Spec_PPC_List (Inherited (J));
+ P := Spec_PPC_List (Contract (Inherited (J)));
while Present (P) loop
if Pragma_Name (P) = Name_Precondition
and then Class_Present (P)
-- Chain spec PPC pragma to list for subprogram
- Set_Next_Pragma (N, Spec_PPC_List (S));
- Set_Spec_PPC_List (S, N);
+ Set_Next_Pragma (N, Spec_PPC_List (Contract (S)));
+ Set_Spec_PPC_List (Contract (S), N);
-- Return indicating spec case
end case;
end Check_Static_Constraint;
+ ---------------------
+ -- Check_Test_Case --
+ ---------------------
+
+ procedure Check_Test_Case is
+ P : Node_Id;
+ PO : Node_Id;
+
+ procedure Chain_TC (PO : Node_Id);
+ -- If PO is an entry or a [generic] subprogram declaration node, then
+ -- the test-case applies to this subprogram and the processing for
+ -- the pragma is completed. Otherwise the pragma is misplaced.
+
+ --------------
+ -- Chain_TC --
+ --------------
+
+ procedure Chain_TC (PO : Node_Id) is
+ S : Entity_Id;
+
+ begin
+ if Nkind (PO) = N_Abstract_Subprogram_Declaration then
+ if From_Aspect_Specification (N) then
+ Error_Pragma
+ ("aspect% cannot be applied to abstract subprogram");
+ else
+ Error_Pragma
+ ("pragma% cannot be applied to abstract subprogram");
+ end if;
+
+ elsif not Nkind_In (PO, N_Subprogram_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Entry_Declaration)
+ then
+ Pragma_Misplaced;
+ end if;
+
+ -- Here if we have [generic] subprogram or entry declaration
+
+ if Nkind (PO) = N_Entry_Declaration then
+ S := Defining_Entity (PO);
+ else
+ S := Defining_Unit_Name (Specification (PO));
+ end if;
+
+ -- Note: we do not analyze the pragma at this point. Instead we
+ -- delay this analysis until the end of the declarative part in
+ -- which the pragma appears. This implements the required delay
+ -- in this analysis, allowing forward references. The analysis
+ -- happens at the end of Analyze_Declarations.
+
+ -- Chain spec TC pragma to list for subprogram
+
+ Set_Next_Pragma (N, Spec_TC_List (Contract (S)));
+ Set_Spec_TC_List (Contract (S), N);
+ end Chain_TC;
+
+ -- Start of processing for Check_Test_Case
+
+ begin
+ if not Is_List_Member (N) then
+ Pragma_Misplaced;
+ end if;
+
+ -- Search prior declarations
+
+ P := N;
+ while Present (Prev (P)) loop
+ P := Prev (P);
+
+ -- 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 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);
+ else
+ PO := P;
+ end if;
+
+ -- Skip past prior pragma
+
+ if Nkind (PO) = N_Pragma then
+ null;
+
+ -- Skip stuff not coming from source
+
+ elsif not Comes_From_Source (PO) then
+ null;
+
+ -- Only remaining possibility is subprogram declaration
+
+ else
+ Chain_TC (PO);
+ return;
+ end if;
+ end loop;
+
+ -- If we fall through loop, pragma is at start of list, so see if it
+ -- is at the start of declarations of a subprogram body.
+
+ if Nkind (Parent (N)) = N_Subprogram_Body
+ and then List_Containing (N) = Declarations (Parent (N))
+ then
+ if Operating_Mode /= Generate_Code
+ or else Inside_A_Generic
+ then
+ -- Analyze pragma expressions for correctness and for ASIS use
+
+ Preanalyze_TC_Args (Get_Requires_From_Test_Case_Pragma (N),
+ Get_Ensures_From_Test_Case_Pragma (N));
+ end if;
+
+ return;
+
+ -- See if it is in the pragmas after a library level subprogram
+
+ elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then
+ Chain_TC (Unit (Parent (Parent (N))));
+ return;
+ end if;
+
+ -- If we fall through, pragma was misplaced
+
+ Pragma_Misplaced;
+ end Check_Test_Case;
+
--------------------------------------
-- Check_Valid_Configuration_Pragma --
--------------------------------------
end if;
end;
- --------------
+ ---------------
-- Task_Info --
- --------------
+ ---------------
-- pragma Task_Info (EXPRESSION);
end if;
end Task_Storage;
+ ---------------
+ -- Test_Case --
+ ---------------
+
+ -- pragma Test_Case ([Name =>] String_Expression
+ -- ,[Mode =>] (Normal | Robustness)
+ -- [, Requires => Boolean_Expression]
+ -- [, Ensures => Boolean_Expression]);
+
+ when Pragma_Test_Case => Test_Case : declare
+
+ begin
+ GNAT_Pragma;
+ Check_At_Least_N_Arguments (3);
+ Check_At_Most_N_Arguments (4);
+ Check_Arg_Order
+ ((Name_Name, Name_Mode, Name_Requires, Name_Ensures));
+
+ Check_Optional_Identifier (Arg1, Name_Name);
+ Check_Arg_Is_String_Literal (Arg1);
+ Check_Optional_Identifier (Arg2, Name_Mode);
+ Check_Arg_Is_One_Of (Arg2, Name_Normal, Name_Robustness);
+ if Arg_Count = 4 then
+ Check_Identifier (Arg3, Name_Requires);
+ Check_Identifier (Arg4, Name_Ensures);
+ else
+ Check_Arg_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
+ end if;
+
+ Check_Test_Case;
+ end Test_Case;
+
--------------------------
-- Thread_Local_Storage --
--------------------------
when Pragma_Exit => null;
end Analyze_Pragma;
+ -----------------------------
+ -- Analyze_TC_In_Decl_Part --
+ -----------------------------
+
+ procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
+ begin
+ -- Install formals and push subprogram spec onto scope stack so that we
+ -- can see the formals from the pragma.
+
+ Install_Formals (S);
+ Push_Scope (S);
+
+ -- Preanalyze the boolean expressions, we treat these as spec
+ -- expressions (i.e. similar to a default expression).
+
+ Preanalyze_TC_Args (Get_Requires_From_Test_Case_Pragma (N),
+ Get_Ensures_From_Test_Case_Pragma (N));
+
+ -- Remove the subprogram from the scope stack now that the pre-analysis
+ -- of the expressions in the test-case is done.
+
+ End_Scope;
+ end Analyze_TC_In_Decl_Part;
+
-------------------
-- Check_Enabled --
-------------------
Pragma_Task_Info => -1,
Pragma_Task_Name => -1,
Pragma_Task_Storage => 0,
+ Pragma_Test_Case => -1,
Pragma_Thread_Local_Storage => 0,
Pragma_Time_Slice => -1,
Pragma_Title => -1,
end if;
end Is_Pragma_String_Literal;
+ ------------------------
+ -- Preanalyze_TC_Args --
+ ------------------------
+
+ procedure Preanalyze_TC_Args (Arg_Req, Arg_Ens : Node_Id) is
+ begin
+ -- Preanalyze the boolean expressions, we treat these as spec
+ -- expressions (i.e. similar to a default expression).
+
+ if Present (Arg_Req) then
+ Preanalyze_Spec_Expression
+ (Get_Pragma_Arg (Arg_Req), Standard_Boolean);
+ end if;
+
+ if Present (Arg_Ens) then
+ Preanalyze_Spec_Expression
+ (Get_Pragma_Arg (Arg_Ens), Standard_Boolean);
+ end if;
+ end Preanalyze_TC_Args;
+
--------------------------------------
-- Process_Compilation_Unit_Pragmas --
--------------------------------------
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Analyze_Pragma (N : Node_Id);
-- Analyze procedure for pragma reference node N
+ procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id);
+ -- Special analyze routine for test-case pragma that appears within a
+ -- declarative part where the pragma is associated with a subprogram
+ -- specification. N is the pragma node, and S is the entity for the related
+ -- subprogram. This procedure does a preanalysis of the expressions in the
+ -- pragma as "spec expressions" (see section in Sem "Handling of Default
+ -- and Per-Object Expressions...").
+
function Check_Enabled (Nam : Name_Id) return Boolean;
-- This function is used in connection with pragmas Assertion, Check,
-- Precondition, and Postcondition to determine if Check pragmas (or
end if;
end Get_Enum_Lit_From_Pos;
+ ---------------------------------------
+ -- Get_Ensures_From_Test_Case_Pragma --
+ ---------------------------------------
+
+ function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
+ Args : constant List_Id := Pragma_Argument_Associations (N);
+ Res : Node_Id;
+
+ begin
+ if List_Length (Args) = 4 then
+ Res := Pick (Args, 4);
+
+ else
+ Res := Pick (Args, 3);
+ if Chars (Res) /= Name_Ensures then
+ Res := Empty;
+ end if;
+ end if;
+
+ return Res;
+ end Get_Ensures_From_Test_Case_Pragma;
+
------------------------
-- Get_Generic_Entity --
------------------------
return R;
end Get_Renamed_Entity;
+ ----------------------------------------
+ -- Get_Requires_From_Test_Case_Pragma --
+ ----------------------------------------
+
+ function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
+ Args : constant List_Id := Pragma_Argument_Associations (N);
+ Res : Node_Id;
+
+ begin
+ Res := Pick (Args, 3);
+ if Chars (Res) /= Name_Requires then
+ Res := Empty;
+ end if;
+
+ return Res;
+ end Get_Requires_From_Test_Case_Pragma;
+
-------------------------
-- Get_Subprogram_Body --
-------------------------
-- If expression N references a part of an object, return this object.
-- Otherwise return Empty. Expression N should have been resolved already.
+ function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id;
+ -- Return the Ensures components 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
-- instantiation is a renaming, the function returns the renamed generic.
-- not a renamed entity, returns its argument. It is an error to call this
-- with any other kind of entity.
+ function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id;
+ -- Return the Requires components 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
-- accept statement node. This procedure finds the Entity_Id of the related
return Node1 (N);
end Source_Type;
+ function Spec_PPC_List
+ (N : Node_Id) return Node_Id is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Contract);
+ return Node1 (N);
+ end Spec_PPC_List;
+
+ function Spec_TC_List
+ (N : Node_Id) return Node_Id is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Contract);
+ return Node2 (N);
+ end Spec_TC_List;
+
function Specification
(N : Node_Id) return Node_Id is
begin
Set_Node1 (N, Val); -- semantic field, no parent set
end Set_Source_Type;
+ procedure Set_Spec_PPC_List
+ (N : Node_Id; Val : Node_Id) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Contract);
+ Set_Node1 (N, Val); -- semantic field, no parent set
+ end Set_Spec_PPC_List;
+
+ procedure Set_Spec_TC_List
+ (N : Node_Id; Val : Node_Id) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Contract);
+ Set_Node2 (N, Val); -- semantic field, no parent set
+ end Set_Spec_TC_List;
+
procedure Set_Specification
(N : Node_Id; Val : Node_Id) is
begin
-- which gigi must do size validation for.
-- Split_PPC (Flag17)
- -- When a Pre or Postaspect specification is processed, it is broken
- -- into AND THEN sections. The left most section has Split_PPC set to
- -- False, indicating that it is the original specification (e.g. for
- -- posting errors). For other sections, Split_PPC is set to True.
- -- This flag is set in both the N_Aspect_Specification node itself,
- -- and in the pragma which is generated from this node.
+ -- When a Pre or Post aspect specification is processed, it is broken
+ -- into AND THEN sections. The left most section has Split_PPC set to
+ -- False, indicating that it is the original specification (e.g. for
+ -- posting errors). For other sections, Split_PPC is set to True.
+ -- This flag is set in both the N_Aspect_Specification node itself,
+ -- and in the pragma which is generated from this node.
-- Static_Processing_OK (Flag4-Sem)
-- Present in N_Aggregate nodes. When the Compile_Time_Known_Aggregate
-- Is_Elsif (Flag13) (set if comes from ELSIF)
-- plus fields for expression
+ --------------
+ -- Contract --
+ --------------
+
+ -- This node is used to hold the various parts of an entry or subprogram
+ -- contract, consisting in pre- and postconditions on the one hand, and
+ -- test-cases on the other hand.
+
+ -- It is referenced from an entry, a subprogram or a generic subprogram
+ -- entity.
+
+ -- Sprint syntax: <none> as the node should not appear in the tree, but
+ -- only attached to an entry or [generic] subprogram
+ -- entity.
+
+ -- N_Contract
+ -- Sloc points to the subprogram's name
+ -- Spec_PPC_List (Node1) (set to Empty if none)
+ -- Spec_TC_List (Node2) (set to Empty if none)
+
+ -- Spec_PPC_List points to a list of Precondition and Postcondition
+ -- pragma nodes for preconditions and postconditions 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 precondition/postcondition pragmas generated
+ -- to correspond to Pre/Post aspects.
+
+ -- Spec_TC_List points to a list of Test_Case pragma nodes for
+ -- 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 test-case
+ -- pragmas generated to correspond to Test_Case aspects.
+
-------------------
-- Expanded_Name --
-------------------
N_Component_Association,
N_Component_Definition,
N_Component_List,
+ N_Contract,
N_Derived_Type_Definition,
N_Decimal_Fixed_Point_Definition,
N_Defining_Program_Unit_Name,
function Source_Type
(N : Node_Id) return Entity_Id; -- Node1
+ function Spec_PPC_List
+ (N : Node_Id) return Node_Id; -- Node1
+
+ function Spec_TC_List
+ (N : Node_Id) return Node_Id; -- Node2
+
function Specification
(N : Node_Id) return Node_Id; -- Node1
procedure Set_Source_Type
(N : Node_Id; Val : Entity_Id); -- Node1
+ procedure Set_Spec_PPC_List
+ (N : Node_Id; Val : Node_Id); -- Node1
+
+ procedure Set_Spec_TC_List
+ (N : Node_Id; Val : Node_Id); -- Node2
+
procedure Set_Specification
(N : Node_Id; Val : Node_Id); -- Node1
4 => False, -- unused
5 => False), -- Etype (Node5-Sem)
+ N_Contract =>
+ (1 => False, -- Spec_PPC_List (Node1)
+ 2 => False, -- Spec_TC_List (Node2)
+ 3 => False, -- unused
+ 4 => False, -- unused
+ 5 => False), -- unused
+
N_Expanded_Name =>
(1 => True, -- Chars (Name1)
2 => True, -- Selector_Name (Node2)
pragma Inline (Selector_Names);
pragma Inline (Shift_Count_OK);
pragma Inline (Source_Type);
+ pragma Inline (Spec_PPC_List);
+ pragma Inline (Spec_TC_List);
pragma Inline (Specification);
pragma Inline (Split_PPC);
pragma Inline (Statements);
pragma Inline (Set_Selector_Names);
pragma Inline (Set_Shift_Count_OK);
pragma Inline (Set_Source_Type);
+ pragma Inline (Set_Spec_PPC_List);
+ pragma Inline (Set_Spec_TC_List);
pragma Inline (Set_Specification);
pragma Inline (Set_Split_PPC);
pragma Inline (Set_Statements);
Name_Suppress_Debug_Info : constant Name_Id := N + $; -- GNAT
Name_Suppress_Initialization : constant Name_Id := N + $; -- GNAT
Name_System_Name : constant Name_Id := N + $; -- Ada 83
+ Name_Test_Case : constant Name_Id := N + $; -- GNAT
Name_Task_Info : constant Name_Id := N + $; -- GNAT
Name_Task_Name : constant Name_Id := N + $; -- GNAT
Name_Task_Storage : constant Name_Id := N + $; -- VMS
Name_Descriptor : constant Name_Id := N + $;
Name_Dot_Replacement : constant Name_Id := N + $;
Name_Dynamic : constant Name_Id := N + $;
+ Name_Ensures : constant Name_Id := N + $;
Name_Entity : constant Name_Id := N + $;
Name_Entry_Count : constant Name_Id := N + $;
Name_External_Name : constant Name_Id := N + $;
Name_Mechanism : constant Name_Id := N + $;
Name_Message : constant Name_Id := N + $;
Name_Mixedcase : constant Name_Id := N + $;
+ Name_Mode : constant Name_Id := N + $;
Name_Modified_GPL : constant Name_Id := N + $;
Name_Name : constant Name_Id := N + $;
Name_NCA : constant Name_Id := N + $;
Name_No_Requeue_Statements : constant Name_Id := N + $;
Name_No_Task_Attributes : constant Name_Id := N + $;
Name_No_Task_Attributes_Package : constant Name_Id := N + $;
+ Name_Normal : constant Name_Id := N + $;
Name_On : constant Name_Id := N + $;
Name_Policy : constant Name_Id := N + $;
Name_Parameter_Types : constant Name_Id := N + $;
Name_Reference : constant Name_Id := N + $;
+ Name_Requires : constant Name_Id := N + $;
Name_Restricted : constant Name_Id := N + $;
Name_Result_Mechanism : constant Name_Id := N + $;
Name_Result_Type : constant Name_Id := N + $;
+ Name_Robustness : constant Name_Id := N + $;
Name_Runtime : constant Name_Id := N + $;
Name_SB : constant Name_Id := N + $;
Name_Secondary_Stack_Size : constant Name_Id := N + $;
Pragma_Suppress_Debug_Info,
Pragma_Suppress_Initialization,
Pragma_System_Name,
+ Pragma_Test_Case,
Pragma_Task_Info,
Pragma_Task_Name,
Pragma_Task_Storage,
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
Sprint_Node (Component_Definition (Node));
+ -- A contract node should not appear in the tree. It is a semantic
+ -- node attached to entry and [generic] subprogram entities.
+
+ when N_Contract =>
+ raise Program_Error;
+
when N_Decimal_Fixed_Point_Definition =>
Write_Str_With_Col_Check_Sloc (" delta ");
Sprint_Node (Delta_Expression (Node));
projects / gcc.git / commitdiff