+2012-03-15 Yannick Moy <moy@adacore.com>
+
+ * aspects.adb, aspects.ads (Aspect_Id): New GNAT aspect
+ Aspect_Contract_Case.
+ * gnat_rm.texi Document the new pragma/aspect
+ Contract_Case. Correct the documentation of the existing
+ pragma/aspect Test_Case with the new semantics.
+ * sem_attr.adb (Analyze_Attribute): Allow use of 'Result in the
+ Ensures component of a Contract_Case pragma.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Check new aspect
+ and translate it into a pragma.
+ (Check_Aspect_At_Freeze_Point): Take into account the new aspect.
+ * sem_ch3.adb, sinfo.adb, sinfo.ads Renaming of TC (for test case)
+ into CTC (for contract and test case).
+ * sem_ch6.adb (Process_PPCs): Generate Check pragmas from
+ Contract_Case pragmas, similarly to what is done already for
+ postconditions.
+ * sem_prag.adb, sem_prag.ads (Check_Contract_Or_Test_Case):
+ Renaming of Check_Test_Case.
+ (Analyze_Pragma, Sig_Flags): Take into account the new pragma.
+ * sem_util.adb, sem_util.ads Renaming to take into account the
+ new pragma, so that functions which applied only to Test_Case
+ now apply to both Test_Case and Contract_Case.
+ * par-prag.adb, sem_warn.adb, snames.ads-tmpl Take into account
+ the new pragma.
+
2012-03-15 Robert Dewar <dewar@adacore.com>
* sem_ch6.ads: Minor comment updates.
Aspect_Bit_Order => Aspect_Bit_Order,
Aspect_Component_Size => Aspect_Component_Size,
Aspect_Constant_Indexing => Aspect_Constant_Indexing,
+ Aspect_Contract_Case => Aspect_Contract_Case,
Aspect_CPU => Aspect_CPU,
Aspect_Default_Component_Value => Aspect_Default_Component_Value,
Aspect_Default_Iterator => Aspect_Default_Iterator,
Aspect_Bit_Order,
Aspect_Component_Size,
Aspect_Constant_Indexing,
+ Aspect_Contract_Case, -- GNAT
Aspect_CPU,
Aspect_Default_Component_Value,
Aspect_Default_Iterator,
(Aspect_Ada_2005 => True,
Aspect_Ada_2012 => True,
Aspect_Compiler_Unit => True,
+ Aspect_Contract_Case => True,
Aspect_Dimension => True,
Aspect_Dimension_System => True,
Aspect_Favor_Top_Level => True,
-- 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);
+ (Aspect_Contract_Case => False,
+ Aspect_Test_Case => False,
+ others => True);
-- The following array indicates type aspects that are inherited and apply
-- to the class-wide type as well.
Aspect_Bit_Order => Expression,
Aspect_Component_Size => Expression,
Aspect_Constant_Indexing => Name,
+ Aspect_Contract_Case => Expression,
Aspect_CPU => Expression,
Aspect_Default_Component_Value => Expression,
Aspect_Default_Iterator => Name,
Aspect_Compiler_Unit => Name_Compiler_Unit,
Aspect_Component_Size => Name_Component_Size,
Aspect_Constant_Indexing => Name_Constant_Indexing,
+ Aspect_Contract_Case => Name_Contract_Case,
Aspect_CPU => Name_CPU,
Aspect_Default_Iterator => Name_Default_Iterator,
Aspect_Default_Value => Name_Default_Value,
* Pragma Complete_Representation::
* Pragma Complex_Representation::
* Pragma Component_Alignment::
+* Pragma Contract_Case::
* Pragma Convention_Identifier::
* Pragma CPP_Class::
* Pragma CPP_Constructor::
* Pragma Complete_Representation::
* Pragma Complex_Representation::
* Pragma Component_Alignment::
+* Pragma Contract_Case::
* Pragma Convention_Identifier::
* Pragma CPP_Class::
* Pragma CPP_Constructor::
pragma @code{Pack}, pragma @code{Component_Alignment}, or a record rep
clause), the GNAT uses the default alignment as described previously.
+@node Pragma Contract_Case
+@unnumberedsec Pragma Contract_Case
+@cindex Contract cases
+@findex Contract_Case
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Contract_Case (
+ [Name =>] static_string_Expression
+ ,[Mode =>] (Nominal | Robustness)
+ [, Requires => Boolean_Expression]
+ [, Ensures => Boolean_Expression]);
+@end smallexample
+
+@noindent
+The @code{Contract_Case} pragma allows defining fine-grain specifications
+that can complement or replace the contract given by a precondition and a
+postcondition. Additionally, the @code{Contract_Case} pragma can be used
+by testing and formal verification tools. The compiler checks its validity and,
+depending on the assertion policy at the point of declaration of the pragma,
+it may insert a check in the executable. For code generation, the contract
+case
+
+@smallexample @c ada
+pragma Contract_Case (
+ Name => ...
+ Mode => ...
+ Requires => R,
+ Ensures => E);
+@end smallexample
+
+@noindent
+is equivalent to
+
+@smallexample @c ada
+pragma Postcondition (not R'Old or else E);
+@end smallexample
+
+@noindent
+which is also equivalent to (in Ada 2012)
+
+@smallexample @c ada
+pragma Postcondition (if R'Old then E);
+@end smallexample
+
+@noindent
+expressing that, whenever condition @code{R} is satisfied on entry to the
+subprogram, condition @code{E} should be fulfilled on exit to the subprogram.
+
+A precondition @code{P} and postcondition @code{Q} can also be
+expressed as contract cases:
+
+@smallexample @c ada
+pragma Contract_Case (
+ Name => "Replace precondition",
+ Mode => Nominal,
+ Requires => not P,
+ Ensures => False);
+pragma Contract_Case (
+ Name => "Replace postcondition",
+ Mode => Nominal,
+ Requires => P,
+ Ensures => Q);
+@end smallexample
+
+@code{Contract_Case} pragmas may only appear immediately following the
+(separate) declaration of a subprogram in a package declaration, inside
+a package spec unit. Only other pragmas may intervene (that is appear
+between the subprogram declaration and a contract case).
+
+The compiler checks that boolean expressions 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 Contract_Case (Name => "Small argument",
+ Mode => Nominal,
+ Requires => Arg < 100,
+ Ensures => Sqrt'Result < 10);
+ ...
+end Math_Functions;
+@end smallexample
+
+@noindent
+The meaning of a contract case is that, whenever the associated subprogram is
+executed in a context where @code{Requires} holds, then @code{Ensures}
+should hold when the subprogram returns. Mode @code{Nominal} indicates
+that the input context should also satisfy the precondition of the
+subprogram, and the output context should also satisfy its
+postcondition. More @code{Robustness} indicates that the precondition and
+postcondition of the subprogram should be ignored for this contract case,
+which is mostly useful when testing such a contract using a testing tool
+that understands contract cases.
+
@node Pragma Convention_Identifier
@unnumberedsec Pragma Convention_Identifier
@findex Convention_Identifier
@noindent
The @code{Test_Case} pragma allows defining fine-grain specifications
-for use by testing and verification tools. The compiler checks its
-validity but the presence of pragma @code{Test_Case} does not lead to
-any modification of the code generated by the compiler.
+for use by testing tools. Its syntax is similar to the syntax of the
+@code{Contract_Case} pragma, which is used for both testing and
+formal verification.
+The compiler checks the validity of the @code{Test_Case} pragma, but its
+presence does not lead to any modification of the code generated by the
+compiler, contrary to the treatment of the @code{Contract_Case} pragma.
@code{Test_Case} pragmas may only appear immediately following the
(separate) declaration of a subprogram in a package declaration, inside
function Sqrt (Arg : Float) return Float;
pragma Test_Case (Name => "Test 1",
Mode => Nominal,
- Requires => Arg < 100,
+ Requires => Arg < 10000,
Ensures => Sqrt'Result < 10);
...
end Math_Functions;
@end smallexample
@noindent
-The meaning of a test case is that, if the associated subprogram is
-executed in a context where @code{Requires} holds, then @code{Ensures}
-should hold when the subprogram returns. Mode @code{Nominal} indicates
-that the input context should satisfy the precondition of the
-subprogram, and the output context should then satisfy its
-postcondition. More @code{Robustness} indicates that the pre- and
+The meaning of a test case is that there is at least one context where
+@code{Requires} holds such that, if the associated subprogram is executed in
+that context, then @code{Ensures} holds when the subprogram returns.
+Mode @code{Nominal} indicates that the input context should also satisfy the
+precondition of the subprogram, and the output context should also satisfy its
+postcondition. More @code{Robustness} indicates that the precondition and
postcondition of the subprogram should be ignored for this test case.
@node Pragma Thread_Local_Storage
@item @code{Atomic_Components} @tab
@item @code{Bit_Order} @tab
@item @code{Component_Size} @tab
+@item @code{Contract_Case} @tab -- GNAT
@item @code{Discard_Names} @tab
@item @code{External_Tag} @tab
@item @code{Favor_Top_Level} @tab -- GNAT
Pragma_Compile_Time_Error |
Pragma_Compile_Time_Warning |
Pragma_Compiler_Unit |
+ Pragma_Contract_Case |
Pragma_Convention_Identifier |
Pragma_CPP_Class |
Pragma_CPP_Constructor |
("% attribute can only appear in postcondition of function",
P);
- elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
+ elsif Get_Pragma_Id (Prag) = Pragma_Contract_Case
+ or else Get_Pragma_Id (Prag) = Pragma_Test_Case
+ then
declare
Arg_Ens : constant Node_Id :=
- Get_Ensures_From_Test_Case_Pragma (Prag);
+ Get_Ensures_From_Case_Pragma (Prag);
Arg : Node_Id;
begin
end loop;
if Arg /= Arg_Ens then
- Error_Attr ("% attribute misplaced inside Test_Case", P);
+ 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;
end if;
end;
Set_Is_Delayed_Aspect (Aspect);
Delay_Required := True;
- when Aspect_Test_Case => declare
- Args : List_Id;
- Comp_Expr : Node_Id;
- Comp_Assn : Node_Id;
- New_Expr : Node_Id;
-
- begin
- Args := New_List;
-
- if Nkind (Parent (N)) = N_Compilation_Unit then
- Error_Msg_N
- ("incorrect placement of aspect `Test_Case`", E);
- goto Continue;
- end if;
+ when Aspect_Contract_Case |
+ Aspect_Test_Case =>
+ declare
+ Args : List_Id;
+ Comp_Expr : Node_Id;
+ Comp_Assn : Node_Id;
+ New_Expr : Node_Id;
- if Nkind (Expr) /= N_Aggregate then
- Error_Msg_NE
- ("wrong syntax for aspect `Test_Case` for &", Id, E);
- goto Continue;
- end if;
+ begin
+ Args := New_List;
- -- Make pragma expressions refer to the original aspect
- -- expressions through the Original_Node link. This is used
- -- in semantic analysis for ASIS mode, so that the original
- -- expression also gets analyzed.
-
- Comp_Expr := First (Expressions (Expr));
- while Present (Comp_Expr) loop
- New_Expr := Relocate_Node (Comp_Expr);
- Set_Original_Node (New_Expr, Comp_Expr);
- Append
- (Make_Pragma_Argument_Association (Sloc (Comp_Expr),
- Expression => New_Expr),
- Args);
- Next (Comp_Expr);
- end loop;
+ if Nkind (Parent (N)) = N_Compilation_Unit then
+ Error_Msg_Name_1 := Nam;
+ Error_Msg_N ("incorrect placement of aspect `%`", E);
+ goto Continue;
+ end if;
- 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
+ if Nkind (Expr) /= N_Aggregate then
+ Error_Msg_Name_1 := Nam;
Error_Msg_NE
- ("wrong syntax for aspect `Test_Case` for &", Id, E);
+ ("wrong syntax for aspect `%` for &", Id, E);
goto Continue;
end if;
- New_Expr := Relocate_Node (Expression (Comp_Assn));
- Set_Original_Node (New_Expr, Expression (Comp_Assn));
- Append (Make_Pragma_Argument_Association (
- Sloc => Sloc (Comp_Assn),
- Chars => Chars (First (Choices (Comp_Assn))),
- Expression => New_Expr),
- Args);
- Next (Comp_Assn);
- end loop;
+ -- Make pragma expressions refer to the original aspect
+ -- expressions through the Original_Node link. This is
+ -- used in semantic analysis for ASIS mode, so that the
+ -- original expression also gets analyzed.
+
+ Comp_Expr := First (Expressions (Expr));
+ while Present (Comp_Expr) loop
+ New_Expr := Relocate_Node (Comp_Expr);
+ Set_Original_Node (New_Expr, Comp_Expr);
+ Append
+ (Make_Pragma_Argument_Association (Sloc (Comp_Expr),
+ Expression => New_Expr),
+ Args);
+ Next (Comp_Expr);
+ end loop;
- -- Build the test-case pragma
+ 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_Name_1 := Nam;
+ Error_Msg_NE
+ ("wrong syntax for aspect `%` for &", Id, E);
+ goto Continue;
+ end if;
- Aitem :=
- Make_Pragma (Loc,
- Pragma_Identifier =>
- Make_Identifier (Sloc (Id), Name_Test_Case),
- Pragma_Argument_Associations =>
- Args);
+ New_Expr := Relocate_Node (Expression (Comp_Assn));
+ Set_Original_Node (New_Expr, Expression (Comp_Assn));
+ Append (Make_Pragma_Argument_Association (
+ Sloc => Sloc (Comp_Assn),
+ Chars => Chars (First (Choices (Comp_Assn))),
+ Expression => New_Expr),
+ Args);
+ Next (Comp_Assn);
+ end loop;
- Set_From_Aspect_Specification (Aitem, True);
- Set_Corresponding_Aspect (Aitem, Aspect);
- Set_Is_Delayed_Aspect (Aspect);
+ -- Build the contract-case or test-case pragma
- -- Insert immediately after the entity declaration
+ Aitem :=
+ Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Sloc (Id), Nam),
+ Pragma_Argument_Associations =>
+ Args);
- Insert_After (N, Aitem);
+ Set_From_Aspect_Specification (Aitem, True);
+ Set_Corresponding_Aspect (Aitem, Aspect);
+ Set_Is_Delayed_Aspect (Aspect);
- goto Continue;
- end;
+ -- Insert immediately after the entity declaration
+
+ Insert_After (N, Aitem);
+
+ goto Continue;
+ end;
when Aspect_Dimension =>
Analyze_Aspect_Dimension (N, Id, Expr);
when Boolean_Aspects =>
raise Program_Error;
- -- Test_Case aspect applies to entries and subprograms, hence should
+ -- Contract_Case aspects apply to subprograms, hence should never be
+ -- delayed.
+
+ when Aspect_Contract_Case =>
+ raise Program_Error;
+
+ -- Test_Case aspects apply to entries and subprograms, hence should
-- never be delayed.
when Aspect_Test_Case =>
Check_Subprogram_Contract (Sent);
- Prag := Spec_TC_List (Contract (Sent));
+ Prag := Spec_CTC_List (Contract (Sent));
while Present (Prag) loop
- Analyze_TC_In_Decl_Part (Prag, Sent);
+ Analyze_CTC_In_Decl_Part (Prag, Sent);
Prag := Next_Pragma (Prag);
end loop;
end if;
Plist : List_Id := No_List;
-- List of generated postconditions
+ 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
-- that an invariant check is required (for an IN OUT parameter, or
-- the returned value of a function.
+ -------------
+ -- Grab_CC --
+ -------------
+
+ function Grab_CC return Node_Id is
+ CP : Node_Id;
+ Req : Node_Id;
+ Ens : Node_Id;
+ Post : Node_Id;
+ Loc : constant Source_Ptr := Sloc (Prag);
+
+ -- Similarly to 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_Case_Pragma (Prag)),
+ New_Scope => Current_Scope);
+
+ Ens := New_Copy_Tree (
+ Expression (Get_Ensures_From_Case_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 --
--------------
Set_Comes_From_Source (CP, False);
-- For a postcondition pragma within a generic, preserve the pragma
- -- for later expansion.
+ -- for later expansion. This is also used when an error was detected,
+ -- thus setting Expander_Active to False.
if Nam = Name_Postcondition
and then not Expander_Active
if Present (Spec_Id) then
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
+ -- Spec_CTC_List is non-Empty.
+
procedure Process_Post_Conditions
(Spec : Node_Id;
Class : Boolean);
-- postconditions marked with Class_Present are considered.
-- The caller has checked that Spec_PPC_List is non-Empty.
+ ----------------------------
+ -- Process_Contract_Cases --
+ ----------------------------
+
+ procedure Process_Contract_Cases (Spec : Node_Id) is
+ begin
+ -- Loop through Contract_Case 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;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ exit when No (Prag);
+ end loop;
+
+ end Process_Contract_Cases;
+
-----------------------------
-- Process_Post_Conditions --
-----------------------------
-- Start of processing for Spec_Postconditions
begin
+ -- Process postconditions expressed as contract-cases
+
+ if Present (Spec_CTC_List (Contract (Spec_Id))) then
+ Process_Contract_Cases (Spec_Id);
+ end if;
+
+ -- Process spec postconditions
+
if Present (Spec_PPC_List (Contract (Spec_Id))) then
Process_Post_Conditions (Spec_Id, Class => False);
end if;
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
- procedure Preanalyze_TC_Args (N, Arg_Req, Arg_Ens : Node_Id);
+ procedure Preanalyze_CTC_Args (N, 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).
+ -- 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).
procedure rv;
-- This is a dummy function called by the processing for pragma Reviewable.
-- 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,
- -- except the placement rules for the test-case pragma are stricter.
- -- This pragma 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_TC_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_Contract_Or_Test_Case;
+ -- Called to process a contract-case or test-case pragma. 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_Valid_Configuration_Pragma;
-- Legality checks for placement of a configuration pragma
end case;
end Check_Static_Constraint;
- ---------------------
- -- Check_Test_Case --
- ---------------------
+ ---------------------------------
+ -- Check_Contract_Or_Test_Case --
+ ---------------------------------
- procedure Check_Test_Case is
+ procedure Check_Contract_Or_Test_Case is
P : Node_Id;
PO : Node_Id;
- procedure Chain_TC (PO : Node_Id);
+ procedure Chain_CTC (PO : Node_Id);
-- If PO is 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.
+ -- contract-case or test-case applies to this subprogram and the
+ -- processing for the pragma is completed. Otherwise the pragma
+ -- is misplaced.
- --------------
- -- Chain_TC --
- --------------
+ ---------------
+ -- Chain_CTC --
+ ---------------
- procedure Chain_TC (PO : Node_Id) is
+ procedure Chain_CTC (PO : Node_Id) is
S : Entity_Id;
begin
-- in this analysis, allowing forward references. The analysis
-- happens at the end of Analyze_Declarations.
- -- There should not be another test case with the same name
- -- associated to this subprogram.
+ -- There should not be another contract-case or test-case with the
+ -- same name associated to this subprogram.
declare
- Name : constant String_Id := Get_Name_From_Test_Case_Pragma (N);
- TC : Node_Id;
+ Name : constant String_Id := Get_Name_From_Case_Pragma (N);
+ CTC : Node_Id;
begin
- TC := Spec_TC_List (Contract (S));
- while Present (TC) loop
+ CTC := Spec_CTC_List (Contract (S));
+ while Present (CTC) loop
if String_Equal
- (Name, Get_Name_From_Test_Case_Pragma (TC))
+ (Name, Get_Name_From_Case_Pragma (CTC))
then
- Error_Msg_Sloc := Sloc (TC);
+ Error_Msg_Sloc := Sloc (CTC);
if From_Aspect_Specification (N) then
Error_Pragma ("name for aspect% is already used#");
end if;
end if;
- TC := Next_Pragma (TC);
+ CTC := Next_Pragma (CTC);
end loop;
end;
- -- Chain spec TC pragma to list for subprogram
+ -- Chain spec CTC pragma to list for subprogram
- Set_Next_Pragma (N, Spec_TC_List (Contract (S)));
- Set_Spec_TC_List (Contract (S), N);
- end Chain_TC;
+ Set_Next_Pragma (N, Spec_CTC_List (Contract (S)));
+ Set_Spec_CTC_List (Contract (S), N);
+ end Chain_CTC;
- -- Start of processing for Check_Test_Case
+ -- Start of processing for Check_Contract_Or_Test_Case
begin
if not Is_List_Member (N) then
Pragma_Misplaced;
end if;
- -- Test cases should only appear in package spec unit
+ -- Contract-case or 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 test-case to the analyzed version at this point.
- -- They get propagated to the original tree when analyzing the
- -- corresponding body.
+ -- 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.
if Nkind (P) not in N_Generic_Declaration then
PO := Original_Node (P);
Pragma_Misplaced;
else
- Chain_TC (PO);
+ Chain_CTC (PO);
return;
end if;
end loop;
-- If we fall through, pragma was misplaced
Pragma_Misplaced;
- end Check_Test_Case;
+ end Check_Contract_Or_Test_Case;
--------------------------------------
-- Check_Valid_Configuration_Pragma --
end if;
end Task_Storage;
- ---------------
- -- Test_Case --
- ---------------
+ -------------------------------
+ -- Contract_Case | Test_Case --
+ -------------------------------
- -- pragma Test_Case ([Name =>] Static_String_EXPRESSION
+ -- pragma (Contract_Case | Test_Case)
+ -- ([Name =>] Static_String_EXPRESSION
-- ,[Mode =>] MODE_TYPE
-- [, Requires => Boolean_EXPRESSION]
-- [, Ensures => Boolean_EXPRESSION]);
-- MODE_TYPE ::= Nominal | Robustness
- when Pragma_Test_Case => Test_Case : declare
+ when Pragma_Contract_Case |
+ Pragma_Test_Case =>
+ Contract_Or_Test_Case : declare
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
Check_Identifier_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
end if;
- Check_Test_Case;
- end Test_Case;
+ Check_Contract_Or_Test_Case;
+ end Contract_Or_Test_Case;
--------------------------
-- Thread_Local_Storage --
when Pragma_Exit => null;
end Analyze_Pragma;
- -----------------------------
- -- Analyze_TC_In_Decl_Part --
- -----------------------------
+ ------------------------------
+ -- Analyze_CTC_In_Decl_Part --
+ ------------------------------
- procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
+ procedure Analyze_CTC_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.
-- Preanalyze the boolean expressions, we treat these as spec
-- expressions (i.e. similar to a default expression).
- Preanalyze_TC_Args (N,
- Get_Requires_From_Test_Case_Pragma (N),
- Get_Ensures_From_Test_Case_Pragma (N));
+ Preanalyze_CTC_Args (N,
+ Get_Requires_From_Case_Pragma (N),
+ Get_Ensures_From_Case_Pragma (N));
-- Remove the subprogram from the scope stack now that the pre-analysis
- -- of the expressions in the test-case is done.
+ -- of the expressions in the contract-case or test-case is done.
End_Scope;
- end Analyze_TC_In_Decl_Part;
+ end Analyze_CTC_In_Decl_Part;
--------------------
-- Check_Disabled --
Pragma_Complete_Representation => 0,
Pragma_Complex_Representation => 0,
Pragma_Component_Alignment => -1,
+ Pragma_Contract_Case => -1,
Pragma_Controlled => 0,
Pragma_Convention => 0,
Pragma_Convention_Identifier => 0,
end if;
end Make_Aspect_For_PPC_In_Gen_Sub_Decl;
- ------------------------
- -- Preanalyze_TC_Args --
- ------------------------
+ -------------------------
+ -- Preanalyze_CTC_Args --
+ -------------------------
- procedure Preanalyze_TC_Args (N, Arg_Req, Arg_Ens : Node_Id) is
+ procedure Preanalyze_CTC_Args (N, 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).
(Original_Node (Get_Pragma_Arg (Arg_Ens)), Standard_Boolean);
end if;
end if;
- end Preanalyze_TC_Args;
+ end Preanalyze_CTC_Args;
--------------------------------------
-- Process_Compilation_Unit_Pragmas --
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...").
+ procedure Analyze_CTC_In_Decl_Part (N : Node_Id; S : Entity_Id);
+ -- Special analyze routine for contract-case and test-case pragmas 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_Disabled (Nam : Name_Id) return Boolean;
-- This function is used in connection with pragmas Assertion, Check,
end if;
end Get_Enum_Lit_From_Pos;
- ---------------------------------------
- -- Get_Ensures_From_Test_Case_Pragma --
- ---------------------------------------
+ ----------------------------------
+ -- Get_Ensures_From_Case_Pragma --
+ ----------------------------------
- function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
+ function Get_Ensures_From_Case_Pragma (N : Node_Id) return Node_Id is
Args : constant List_Id := Pragma_Argument_Associations (N);
Res : Node_Id;
end if;
return Res;
- end Get_Ensures_From_Test_Case_Pragma;
+ end Get_Ensures_From_Case_Pragma;
------------------------
-- Get_Generic_Entity --
return Entity_Id (Get_Name_Table_Info (Id));
end Get_Name_Entity_Id;
- ------------------------------------
- -- Get_Name_From_Test_Case_Pragma --
- ------------------------------------
+ -------------------------------
+ -- Get_Name_From_Case_Pragma --
+ -------------------------------
- function Get_Name_From_Test_Case_Pragma (N : Node_Id) return String_Id is
+ function Get_Name_From_Case_Pragma (N : Node_Id) return String_Id is
Arg : constant Node_Id :=
Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
begin
return Strval (Expr_Value_S (Arg));
- end Get_Name_From_Test_Case_Pragma;
+ end Get_Name_From_Case_Pragma;
-------------------
-- Get_Pragma_Id --
return R;
end Get_Renamed_Entity;
- ----------------------------------------
- -- Get_Requires_From_Test_Case_Pragma --
- ----------------------------------------
+ -----------------------------------
+ -- Get_Requires_From_Case_Pragma --
+ -----------------------------------
- function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
+ function Get_Requires_From_Case_Pragma (N : Node_Id) return Node_Id is
Args : constant List_Id := Pragma_Argument_Associations (N);
Res : Node_Id;
end if;
return Res;
- end Get_Requires_From_Test_Case_Pragma;
+ end Get_Requires_From_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 component of Test_Case pragma N, or Empty otherwise
+ function Get_Ensures_From_Case_Pragma (N : Node_Id) return Node_Id;
+ -- Return the Ensures component of Contract_Case or 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
-- is the innermost visible entity with the given name. See the body of
-- Sem_Ch8 for further details on handling of entity visibility.
- function Get_Name_From_Test_Case_Pragma (N : Node_Id) return String_Id;
- -- Return the Name component of Test_Case pragma N
+ function Get_Name_From_Case_Pragma (N : Node_Id) return String_Id;
+ -- Return the Name component of Contract_Case or Test_Case pragma N
function Get_Pragma_Id (N : Node_Id) return Pragma_Id;
pragma Inline (Get_Pragma_Id);
-- 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 component of Test_Case pragma N, or Empty otherwise
+ function Get_Requires_From_Case_Pragma (N : Node_Id) return Node_Id;
+ -- Return the Requires component of Contract_Case or 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
-- --
-- B o d y --
-- --
--- Copyright (C) 1999-2011, Free Software Foundation, Inc. --
+-- Copyright (C) 1999-2012, 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- --
function Within_Postcondition return Boolean;
-- Returns True iff N is within a Postcondition or
- -- Ensures component in a Test_Case.
+ -- Ensures component in a Contract_Case or Test_Case.
--------------------------
-- Within_Postcondition --
P := Parent (Nod);
if Nkind (P) = N_Pragma
- and then Pragma_Name (P) = Name_Test_Case
and then
- Nod = Get_Ensures_From_Test_Case_Pragma (P)
+ (Pragma_Name (P) = Name_Contract_Case
+ or else Pragma_Name (P) = Name_Test_Case)
+ and then
+ Nod = Get_Ensures_From_Case_Pragma (P)
then
return True;
end if;
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2012, 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- --
return Node1 (N);
end Spec_PPC_List;
- function Spec_TC_List
+ function Spec_CTC_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;
+ end Spec_CTC_List;
function Specification
(N : Node_Id) return Node_Id is
Set_Node1 (N, Val); -- semantic field, no parent set
end Set_Spec_PPC_List;
- procedure Set_Spec_TC_List
+ procedure Set_Spec_CTC_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;
+ end Set_Spec_CTC_List;
procedure Set_Specification
(N : Node_Id; Val : Node_Id) is
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2012, 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_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_CTC_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
-- 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.
+ -- Spec_CTC_List points to a list of Contract_Case 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.
-------------------
-- Expanded_Name --
function Spec_PPC_List
(N : Node_Id) return Node_Id; -- Node1
- function Spec_TC_List
+ function Spec_CTC_List
(N : Node_Id) return Node_Id; -- Node2
function Specification
procedure Set_Spec_PPC_List
(N : Node_Id; Val : Node_Id); -- Node1
- procedure Set_Spec_TC_List
+ procedure Set_Spec_CTC_List
(N : Node_Id; Val : Node_Id); -- Node2
procedure Set_Specification
N_Contract =>
(1 => False, -- Spec_PPC_List (Node1)
- 2 => False, -- Spec_TC_List (Node2)
+ 2 => False, -- Spec_CTC_List (Node2)
3 => False, -- unused
4 => False, -- unused
5 => False), -- unused
pragma Inline (Shift_Count_OK);
pragma Inline (Source_Type);
pragma Inline (Spec_PPC_List);
- pragma Inline (Spec_TC_List);
+ pragma Inline (Spec_CTC_List);
pragma Inline (Specification);
pragma Inline (Split_PPC);
pragma Inline (Statements);
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_Spec_CTC_List);
pragma Inline (Set_Specification);
pragma Inline (Set_Split_PPC);
pragma Inline (Set_Statements);
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_Controlled : constant Name_Id := N + $;
Name_Convention : constant Name_Id := N + $;
Name_CPP_Class : constant Name_Id := N + $; -- GNAT
Pragma_Common_Object,
Pragma_Complete_Representation,
Pragma_Complex_Representation,
+ Pragma_Contract_Case,
Pragma_Controlled,
Pragma_Convention,
Pragma_CPP_Class,
projects / gcc.git / commitdiff