[Ada] New pragma and aspect Contract_Case to refine contracts
Arnaud Charlet
charlet@adacore.com
Thu Mar 15 08:49:00 GMT 2012
A new pragma and aspect Contract_Case is defined, which allows defining
fine-grain specifications that can complement or replace the contract given
by a precondition and a postcondition. Additionally, the Contract_Case pragma
or aspect 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 or aspect, it may insert a check in the executable.
When compiled with assertions enabled (-gnata) and run, the following code
raises an exception:
$ ./main
$ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed contract case from p.ads:3
--- main.adb
1. with P; use P;
2.
3. procedure Main is
4. X : Integer;
5. begin
6. X := 10;
7. Incr (X);
8. X := -10;
9. Incr (X);
10. end Main;
--- p.adb
1. package body P is
2. procedure Incr (X : in out Integer) is
3. begin
4. if X /= -10 then
5. X := X + 1;
6. end if;
7. end Incr;
8. end P;
--- p.ads
1. package P is
2. procedure Incr (X : in out Integer) with
3. Contract_Case => (Name => "",
4. Mode => Nominal,
5. Requires => X < 0,
6. Ensures => X = X'Old + 1);
7. end P;
---
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
-------------- next part --------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 185390)
+++ sem_ch3.adb (working copy)
@@ -2204,9 +2204,9 @@
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;
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi (revision 185410)
+++ gnat_rm.texi (working copy)
@@ -120,6 +120,7 @@
* Pragma Complete_Representation::
* Pragma Complex_Representation::
* Pragma Component_Alignment::
+* Pragma Contract_Case::
* Pragma Convention_Identifier::
* Pragma CPP_Class::
* Pragma CPP_Constructor::
@@ -855,6 +856,7 @@
* Pragma Complete_Representation::
* Pragma Complex_Representation::
* Pragma Component_Alignment::
+* Pragma Contract_Case::
* Pragma Convention_Identifier::
* Pragma CPP_Class::
* Pragma CPP_Constructor::
@@ -1704,6 +1706,108 @@
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
@@ -5238,9 +5342,12 @@
@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
@@ -5261,19 +5368,19 @@
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
@@ -17375,6 +17482,7 @@
@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
Index: sinfo.adb
===================================================================
--- sinfo.adb (revision 185390)
+++ sinfo.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- 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- --
@@ -2812,13 +2812,13 @@
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
@@ -5892,13 +5892,13 @@
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
Index: sinfo.ads
===================================================================
--- sinfo.ads (revision 185390)
+++ sinfo.ads (working copy)
@@ -6,7 +6,7 @@
-- --
-- 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- --
@@ -6969,7 +6969,7 @@
-- 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
@@ -6978,11 +6978,12 @@
-- 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 --
@@ -8963,7 +8964,7 @@
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
@@ -9944,7 +9945,7 @@
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
@@ -11590,7 +11591,7 @@
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
@@ -12084,7 +12085,7 @@
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);
@@ -12407,7 +12408,7 @@
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);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 185390)
+++ sem_prag.adb (working copy)
@@ -181,10 +181,10 @@
-- 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.
@@ -637,15 +637,16 @@
-- 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
@@ -2113,24 +2114,25 @@
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
@@ -2166,21 +2168,21 @@
-- 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#");
@@ -2189,24 +2191,24 @@
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))),
@@ -2224,9 +2226,9 @@
-- 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);
@@ -2258,7 +2260,7 @@
Pragma_Misplaced;
else
- Chain_TC (PO);
+ Chain_CTC (PO);
return;
end if;
end loop;
@@ -2266,7 +2268,7 @@
-- If we fall through, pragma was misplaced
Pragma_Misplaced;
- end Check_Test_Case;
+ end Check_Contract_Or_Test_Case;
--------------------------------------
-- Check_Valid_Configuration_Pragma --
@@ -13904,18 +13906,21 @@
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);
@@ -13947,8 +13952,8 @@
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 --
@@ -14819,11 +14824,11 @@
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.
@@ -14834,15 +14839,15 @@
-- 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 --
@@ -15077,6 +15082,7 @@
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,
@@ -15431,11 +15437,11 @@
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).
@@ -15465,7 +15471,7 @@
(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 --
Index: sem_prag.ads
===================================================================
--- sem_prag.ads (revision 185390)
+++ sem_prag.ads (working copy)
@@ -46,13 +46,13 @@
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,
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 185390)
+++ sem_util.adb (working copy)
@@ -4490,11 +4490,11 @@
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;
@@ -4514,7 +4514,7 @@
end if;
return Res;
- end Get_Ensures_From_Test_Case_Pragma;
+ end Get_Ensures_From_Case_Pragma;
------------------------
-- Get_Generic_Entity --
@@ -4602,16 +4602,16 @@
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 --
@@ -4656,11 +4656,11 @@
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;
@@ -4677,7 +4677,7 @@
end if;
return Res;
- end Get_Requires_From_Test_Case_Pragma;
+ end Get_Requires_From_Case_Pragma;
-------------------------
-- Get_Subprogram_Body --
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 185390)
+++ sem_util.ads (working copy)
@@ -538,8 +538,9 @@
-- 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
@@ -572,8 +573,8 @@
-- 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);
@@ -590,8 +591,9 @@
-- 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
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 185409)
+++ sem_attr.adb (working copy)
@@ -4256,10 +4256,12 @@
("% 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
@@ -4269,7 +4271,13 @@
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;
Index: aspects.adb
===================================================================
--- aspects.adb (revision 185390)
+++ aspects.adb (working copy)
@@ -249,6 +249,7 @@
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,
Index: aspects.ads
===================================================================
--- aspects.ads (revision 185390)
+++ aspects.ads (working copy)
@@ -50,6 +50,7 @@
Aspect_Bit_Order,
Aspect_Component_Size,
Aspect_Constant_Indexing,
+ Aspect_Contract_Case, -- GNAT
Aspect_CPU,
Aspect_Default_Component_Value,
Aspect_Default_Iterator,
@@ -176,6 +177,7 @@
(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,
@@ -206,8 +208,9 @@
-- 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.
@@ -259,6 +262,7 @@
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,
@@ -325,6 +329,7 @@
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,
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 185410)
+++ sem_ch6.adb (working copy)
@@ -10932,6 +10932,11 @@
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
@@ -10954,6 +10959,87 @@
-- 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 --
--------------
@@ -11005,7 +11091,8 @@
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
@@ -11328,6 +11415,11 @@
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);
@@ -11336,6 +11428,34 @@
-- 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 --
-----------------------------
@@ -11380,6 +11500,14 @@
-- 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;
Index: par-prag.adb
===================================================================
--- par-prag.adb (revision 185390)
+++ par-prag.adb (working copy)
@@ -1109,6 +1109,7 @@
Pragma_Compile_Time_Error |
Pragma_Compile_Time_Warning |
Pragma_Compiler_Unit |
+ Pragma_Contract_Case |
Pragma_Convention_Identifier |
Pragma_CPP_Class |
Pragma_CPP_Constructor |
Index: sem_warn.adb
===================================================================
--- sem_warn.adb (revision 185390)
+++ sem_warn.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- 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- --
@@ -1749,7 +1749,7 @@
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 --
@@ -1770,9 +1770,11 @@
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;
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 185390)
+++ sem_ch13.adb (working copy)
@@ -1450,84 +1450,88 @@
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;
+ when Aspect_Contract_Case |
+ Aspect_Test_Case =>
+ declare
+ Args : List_Id;
+ Comp_Expr : Node_Id;
+ Comp_Assn : Node_Id;
+ New_Expr : Node_Id;
- begin
- Args := New_List;
+ 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;
+ 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;
- if Nkind (Expr) /= N_Aggregate then
- Error_Msg_NE
- ("wrong syntax for aspect `Test_Case` for &", Id, E);
- goto Continue;
- end if;
-
- -- 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;
-
- 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.
- -- Build the test-case pragma
+ 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;
- Aitem :=
- Make_Pragma (Loc,
- Pragma_Identifier =>
- Make_Identifier (Sloc (Id), Name_Test_Case),
- Pragma_Argument_Associations =>
- Args);
+ 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;
- Set_From_Aspect_Specification (Aitem, True);
- Set_Corresponding_Aspect (Aitem, Aspect);
- Set_Is_Delayed_Aspect (Aspect);
+ 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;
- -- Insert immediately after the entity declaration
+ -- Build the contract-case or test-case pragma
- Insert_After (N, Aitem);
+ Aitem :=
+ Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Sloc (Id), Nam),
+ Pragma_Argument_Associations =>
+ Args);
- goto Continue;
- end;
+ Set_From_Aspect_Specification (Aitem, True);
+ Set_Corresponding_Aspect (Aitem, Aspect);
+ Set_Is_Delayed_Aspect (Aspect);
+ -- Insert immediately after the entity declaration
+
+ Insert_After (N, Aitem);
+
+ goto Continue;
+ end;
+
when Aspect_Dimension =>
Analyze_Aspect_Dimension (N, Id, Expr);
goto Continue;
@@ -6158,7 +6162,13 @@
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 =>
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 185409)
+++ snames.ads-tmpl (working copy)
@@ -448,6 +448,7 @@
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
@@ -1623,6 +1624,7 @@
Pragma_Common_Object,
Pragma_Complete_Representation,
Pragma_Complex_Representation,
+ Pragma_Contract_Case,
Pragma_Controlled,
Pragma_Convention,
Pragma_CPP_Class,
More information about the Gcc-patches
mailing list