This patch implements a new assertion kind (usable in a Check_Policy
or Assertion_Policy pragma) "Statement_Assertions" which applies to
Assert, Assert_And_Cut, Assume, and Loop_Invariant.
The following program is to be compiled with the -gnatd.F switch (this
switch can be removed soon when we make the other assertion kinds first
class citizens)
1. pragma Ada_2012;
2. with Text_IO; use Text_IO;
3. with System.Assertions; use System.Assertions;
4. procedure StmAssert is
5. function Id (X : Integer) return Integer
6. is begin return X; end;
7.
8. Y : Integer := Id (10);
9.
10. begin
11. declare
12. pragma Check_Policy
13. (Statement_Assertions, Check);
14. begin
15. begin
16. pragma Assert (Y = 11);
17. Put_Line ("not OK1");
18. exception
19. when Assert_Failure =>
20. Put_Line ("OK1");
21. end;
22. begin
23. pragma Assert_And_Cut (Y = 11);
24. Put_Line ("not OK2");
25. exception
26. when Assert_Failure =>
27. Put_Line ("OK2");
28. end;
29. begin
30. pragma Assume (Y = 11);
31. Put_Line ("not OK3");
32. exception
33. when Assert_Failure =>
34. Put_Line ("OK3");
35. end;
36. begin
37. for J in 1 .. 1 loop
38. pragma Loop_Invariant (Y = 11);
39. Put_Line ("not OK4");
40. end loop;
41. exception
42. when Assert_Failure =>
43. Put_Line ("OK4");
44. end;
45. end;
46. declare
47. pragma Assertion_Policy
48. (Statement_Assertions => Ignore);
49. begin
50. pragma Assert (Y = 11);
51. pragma Assert_And_Cut (Y = 11);
52. pragma Assume (Y = 11);
53. for J in 1 .. 1 loop
54. pragma Loop_Invariant (J = 2);
55. end loop;
56. Put_Line ("OK5");
57. exception
58. when others => Put_Line ("not OK5");
59. end;
60.
61. end StmAssert;
The output is:
OK1
OK2
OK3
OK4
OK5
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-04-23 Robert Dewar <[email protected]>
* exp_prag.adb (Expand_Pragma_Check): Check for Assert rather
than Assertion.
* sem_prag.adb (Is_Valid_Assertion_Kind): Moved to spec
(Effective_Name): New function (Analyze_Pragma, case Check):
Disallow [Statement_]Assertions (Check_Kind): Implement
Statement_Assertions (Check_Applicable_Policy): Use Effective_Name
(Is_Valid_Assertion_Kind): Allow Statement_Assertions.
* sem_prag.ads (Is_Valid_Assertion_Kind): Moved here from body
(Effective_Name): New function.
* sem_res.adb: Minor reformatting.
* snames.ads-tmpl (Name_Statement_Assertions): New entry.
* gnat_rm.texi: Add documentation of new assertion kind
Statement_Assertions.
Index: exp_prag.adb
===================================================================
--- exp_prag.adb (revision 198175)
+++ exp_prag.adb (working copy)
@@ -377,7 +377,7 @@
-- For Assert, we just use the location
- if Nam = Name_Assertion then
+ if Nam = Name_Assert then
null;
-- For predicate, we generate the string "predicate failed
@@ -446,7 +446,7 @@
then
return;
- elsif Nam = Name_Assertion then
+ elsif Nam = Name_Assert then
Error_Msg_N ("?A?assertion will fail at run time", N);
else
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi (revision 198175)
+++ gnat_rm.texi (working copy)
@@ -1251,7 +1251,8 @@
Type_Invariant |
Type_Invariant'Class
-ID_ASSERTION_KIND ::= Assert_And_Cut |
+ID_ASSERTION_KIND ::= Assertions |
+ Assert_And_Cut |
Assume |
Contract_Cases |
Debug |
@@ -1262,6 +1263,7 @@
Postcondition |
Precondition |
Predicate
+ Statement_Assertions
POLICY_IDENTIFIER ::= Check | Disable | Ignore
@end smallexample
@@ -1292,6 +1294,15 @@
in a with'ed package which is replaced by a dummy package
for the final build.
+The implementation defined policy @code{Assertions} applies to all
+assertion kinds. The form with no assertion kind given implies this
+choice, so it applies to all assertion kinds (RM defined, and
+implementation defined).
+
+The implementation defined policy @code{Statement_Assertions}
+applies to @code{Assert}, @code{Assert_And_Cut},
+@code{Assume}, and @code{Loop_Invariant}.
+
@node Pragma Assume_No_Invalid_Values
@unnumberedsec Pragma Assume_No_Invalid_Values
@findex Assume_No_Invalid_Values
@@ -1460,6 +1471,11 @@
be activated either by the command line option @option{-gnata}, which turns on
all checks, or individually controlled using pragma @code{Check_Policy}.
+The identifiers @code{Assertions} and @code{Statement_Assertions} are not
+permitted as check kinds, since this would cause confusion with the use
+of these identifiers in @code{Assertion_Policy} and @code{Check_Policy}
+pragmas, where they are used to refer to sets of assertions.
+
@node Pragma Check_Float_Overflow
@unnumberedsec Pragma Check_Float_Overflow
@cindex Floating-point overflow
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 198184)
+++ sem_prag.adb (working copy)
@@ -181,13 +181,6 @@
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
- function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
- -- Returns True if Nam is one of the names recognized as a valid assertion
- -- kind by the Assertion_Policy pragma. Note that the 'Class cases are
- -- represented by the corresponding special names Name_uPre, Name_uPost,
- -- Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant,
- -- and _Type_Invariant).
-
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
@@ -352,9 +345,7 @@
-- In ASIS mode, for a pragma generated from a source aspect, also
-- analyze the original aspect expression.
- if ASIS_Mode
- and then Present (Corresponding_Aspect (N))
- then
+ if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
Preanalyze_Assert_Expression
(Expression (Corresponding_Aspect (N)), Standard_Boolean);
end if;
@@ -2222,9 +2213,7 @@
-- In ASIS mode, for a pragma generated from a source aspect,
-- also analyze the original aspect expression.
- if ASIS_Mode
- and then Present (Corresponding_Aspect (N))
- then
+ if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
Preanalyze_Assert_Expression
(Expression (Corresponding_Aspect (N)), Standard_Boolean);
end if;
@@ -2411,9 +2400,7 @@
-- In ASIS mode, for a pragma generated from a source aspect, also
-- analyze the original aspect expression.
- if ASIS_Mode
- and then Present (Corresponding_Aspect (N))
- then
+ if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
Check_Expr_Is_Static_Expression
(Original_Node (Get_Pragma_Arg (Arg1)), Standard_String);
end if;
@@ -2882,10 +2869,7 @@
-- Get name from corresponding aspect
- if Present (Corresponding_Aspect (N)) then
- Error_Msg_Name_1 :=
- Chars (Identifier (Corresponding_Aspect (N)));
- end if;
+ Error_Msg_Name_1 := Effective_Name (N);
end if;
end Fix_Error;
@@ -6765,11 +6749,8 @@
-- Here to start processing for recognized pragma
Prag_Id := Get_Pragma_Id (Pname);
+ Pname := Effective_Name (N);
- if Present (Corresponding_Aspect (N)) then
- Pname := Chars (Identifier (Corresponding_Aspect (N)));
- end if;
-
-- Check applicable policy. We skip this for a pragma that came from
-- an aspect, since we already dealt with the Disable case, and we set
-- the Is_Ignored flag at the time the aspect was analyzed.
@@ -7426,9 +7407,9 @@
Check_Arg_Order ((Name_Check, Name_Message));
Check_Optional_Identifier (Arg1, Name_Check);
- -- We treat pragma Assert as equivalent to:
+ -- We treat pragma Assert[_And_Cut] as equivalent to:
- -- pragma Check (Assertion, condition [, msg]);
+ -- pragma Check (Assert[_And_Cut], condition [, msg]);
-- So rewrite pragma in this manner, transfer the message
-- argument if present, and analyze the result
@@ -7443,8 +7424,7 @@
Expr := Get_Pragma_Arg (Arg1);
Newa := New_List (
Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Name_Assertion)),
-
+ Expression => Make_Identifier (Loc, Pname)),
Make_Pragma_Argument_Association (Sloc (Expr),
Expression => Expr));
@@ -8083,6 +8063,9 @@
-- Invariant'Class |
-- Type_Invariant'Class
+ -- The identifiers Assertions and Statement_Assertions are not
+ -- allowed, since they have special meaning for Check_Policy.
+
when Pragma_Check => Check : declare
Expr : Node_Id;
Eloc : Source_Ptr;
@@ -8108,6 +8091,23 @@
Check_Arg_Is_Identifier (Arg1);
Cname := Chars (Get_Pragma_Arg (Arg1));
+ -- Check forbidden name Assertions or Statement_Assertions
+
+ case Cname is
+ when Name_Assertions =>
+ Error_Pragma_Arg
+ ("""Assertions"" is not allowed as a check kind "
+ & "for pragma%", Arg1);
+
+ when Name_Statement_Assertions =>
+ Error_Pragma_Arg
+ ("""Statement_Assertions"" is not allowed as a check kind "
+ & "for pragma%", Arg1);
+
+ when others =>
+ null;
+ end case;
+
-- Set Check_On to indicate check status
-- If this comes from an aspect, we have already taken care of
@@ -17945,8 +17945,13 @@
begin
if Nam = Pnm
- or else (Is_Valid_Assertion_Kind (Nam)
- and then Pnm = Name_Assertion)
+ or else (Pnm = Name_Assertion
+ and then Is_Valid_Assertion_Kind (Nam))
+ or else (Pnm = Name_Statement_Assertions
+ and then Nam_In (Nam, Name_Assert,
+ Name_Assert_And_Cut,
+ Name_Assume,
+ Name_Loop_Invariant))
then
case (Chars (Get_Pragma_Arg (Last (PPA)))) is
when Name_On | Name_Check =>
@@ -17985,36 +17990,9 @@
PP : Node_Id;
Policy : Name_Id;
- Ename : Name_Id;
- -- Effective name of aspect or pragma, this is simply the name of
- -- the aspect or pragma, except in the case of a pragma derived from
- -- an aspect, in which case it is the name of the aspect (which may be
- -- different, e.g. Pre aspect generating Precondition pragma). It also
- -- deals with the 'Class cases for an aspect.
+ Ename : constant Name_Id := Effective_Name (N);
begin
- if Nkind (N) = N_Pragma then
- if Present (Corresponding_Aspect (N)) then
- Ename := Chars (Identifier (Corresponding_Aspect (N)));
- else
- Ename := Chars (Pragma_Identifier (N));
- end if;
-
- else
- pragma Assert (Nkind (N) = N_Aspect_Specification);
- Ename := Chars (Identifier (N));
-
- if Class_Present (N) then
- case Ename is
- when Name_Invariant => Ename := Name_uInvariant;
- when Name_Pre => Ename := Name_uPre;
- when Name_Post => Ename := Name_uPost;
- when Name_Type_Invariant => Ename := Name_uType_Invariant;
- when others => raise Program_Error;
- end case;
- end if;
- end if;
-
-- No effect if not valid assertion kind name
if not Is_Valid_Assertion_Kind (Ename) then
@@ -18072,6 +18050,66 @@
Name_Priority_Specific_Dispatching);
end Delay_Config_Pragma_Analyze;
+ --------------------
+ -- Effective_Name --
+ --------------------
+
+ function Effective_Name (N : Node_Id) return Name_Id is
+ Pras : Node_Id;
+ Name : Name_Id;
+
+ begin
+ pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma));
+ Pras := N;
+
+ if Is_Rewrite_Substitution (Pras)
+ and then Nkind (Original_Node (Pras)) = N_Pragma
+ then
+ Pras := Original_Node (Pras);
+ end if;
+
+ -- Case where we came from aspect specication
+
+ if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then
+ Pras := Corresponding_Aspect (Pras);
+ end if;
+
+ -- Get name from aspect or pragma
+
+ if Nkind (Pras) = N_Pragma then
+ Name := Pragma_Name (Pras);
+ else
+ Name := Chars (Identifier (Pras));
+ end if;
+
+ -- Deal with 'Class
+
+ if Class_Present (Pras) then
+ case Name is
+
+ -- Names that need converting to special _xxx form
+
+ when Name_Pre => Name := Name_uPre;
+ when Name_Post => Name := Name_uPost;
+ when Name_Invariant => Name := Name_uInvariant;
+ when Name_Type_Invariant => Name := Name_uType_Invariant;
+
+ -- Names already in special _xxx form (leave them alone)
+
+ when Name_uPre => null;
+ when Name_uPost => null;
+ when Name_uInvariant => null;
+ when Name_uType_Invariant => null;
+
+ -- Anything else is impossible with Class_Present set True
+
+ when others => raise Program_Error;
+ end case;
+ end if;
+
+ return Name;
+ end Effective_Name;
+
-------------------------
-- Get_Base_Subprogram --
-------------------------
@@ -18521,31 +18559,32 @@
when
-- RM defined
- Name_Assert |
- Name_Static_Predicate |
- Name_Dynamic_Predicate |
- Name_Pre |
- Name_uPre |
- Name_Post |
- Name_uPost |
- Name_Type_Invariant |
- Name_uType_Invariant |
+ Name_Assert |
+ Name_Static_Predicate |
+ Name_Dynamic_Predicate |
+ Name_Pre |
+ Name_uPre |
+ Name_Post |
+ Name_uPost |
+ Name_Type_Invariant |
+ Name_uType_Invariant |
-- Impl defined
- Name_Assert_And_Cut |
- Name_Assume |
- Name_Contract_Cases |
- Name_Debug |
- Name_Invariant |
- Name_uInvariant |
- Name_Loop_Invariant |
- Name_Loop_Variant |
- Name_Postcondition |
- Name_Precondition |
- Name_Predicate => return True;
+ Name_Assert_And_Cut |
+ Name_Assume |
+ Name_Contract_Cases |
+ Name_Debug |
+ Name_Invariant |
+ Name_uInvariant |
+ Name_Loop_Invariant |
+ Name_Loop_Variant |
+ Name_Postcondition |
+ Name_Precondition |
+ Name_Predicate |
+ Name_Statement_Assertions => return True;
- when others => return False;
+ when others => return False;
end case;
end Is_Valid_Assertion_Kind;
Index: sem_prag.ads
===================================================================
--- sem_prag.ads (revision 198175)
+++ sem_prag.ads (working copy)
@@ -104,10 +104,30 @@
-- True have their analysis delayed until after the main program is parsed
-- and analyzed.
+ function Effective_Name (N : Node_Id) return Name_Id;
+ -- N is a pragma node or aspect specification node. This function returns
+ -- the name of the pragma or aspect, taking into account possible rewrites,
+ -- and also cases where a pragma comes from an attribute (in such cases,
+ -- the name can be different from the pragma name, e.g. Pre generates
+ -- a Precondition pragma. This also deals with the presence of 'Class
+ -- which results in one of the special names Name_uPre, Name_uPost,
+ -- Name_uInvariant, or Name_uType_Invariant being returned to represent
+ -- the corresponding aspects with x'Class names.
+
procedure Initialize;
-- Initializes data structures used for pragma processing. Must be called
-- before analyzing each new main source program.
+ function Is_Config_Static_String (Arg : Node_Id) return Boolean;
+ -- This is called for a configuration pragma that requires either string
+ -- literal or a concatenation of string literals. We cannot use normal
+ -- static string processing because it is too early in the case of the
+ -- pragma appearing in a configuration pragmas file. If Arg is of an
+ -- appropriate form, then this call obtains the string (doing any necessary
+ -- concatenations) and places it in Name_Buffer, setting Name_Len to its
+ -- length, and then returns True. If it is not of the correct form, then an
+ -- appropriate error message is posted, and False is returned.
+
function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
-- The node N is a node for an entity and the issue is whether the
-- occurrence is a reference for the purposes of giving warnings about
@@ -124,15 +144,12 @@
-- False is returned, then the argument is treated as an entity reference
-- to the operator.
- function Is_Config_Static_String (Arg : Node_Id) return Boolean;
- -- This is called for a configuration pragma that requires either string
- -- literal or a concatenation of string literals. We cannot use normal
- -- static string processing because it is too early in the case of the
- -- pragma appearing in a configuration pragmas file. If Arg is of an
- -- appropriate form, then this call obtains the string (doing any necessary
- -- concatenations) and places it in Name_Buffer, setting Name_Len to its
- -- length, and then returns True. If it is not of the correct form, then an
- -- appropriate error message is posted, and False is returned.
+ function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
+ -- Returns True if Nam is one of the names recognized as a valid assertion
+ -- kind by the Assertion_Policy pragma. Note that the 'Class cases are
+ -- represented by the corresponding special names Name_uPre, Name_uPost,
+ -- Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant,
+ -- and _Type_Invariant).
procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id);
-- This routine makes aspects from precondition or postcondition pragmas
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 198186)
+++ sem_res.adb (working copy)
@@ -8908,27 +8908,32 @@
Orig : constant Node_Id := Original_Node (Parent (N));
begin
+ -- Special handling of Asssert pragma
+
if Nkind (Orig) = N_Pragma
and then Pragma_Name (Orig) = Name_Assert
then
- -- Don't want to warn if original condition is explicit False
-
declare
Expr : constant Node_Id :=
Original_Node
(Expression
(First (Pragma_Argument_Associations (Orig))));
+
begin
+ -- Don't warn if original condition is explicit False,
+ -- since obviously the failure is expected in this case.
+
if Is_Entity_Name (Expr)
and then Entity (Expr) = Standard_False
then
null;
+
+ -- Issue warning. We do not want the deletion of the
+ -- IF/AND-THEN to take this message with it. We achieve this
+ -- by making sure that the expanded code points to the Sloc
+ -- of the expression, not the original pragma.
+
else
- -- Issue warning. We do not want the deletion of the
- -- IF/AND-THEN to take this message with it. We achieve
- -- this by making sure that the expanded code points to
- -- the Sloc of the expression, not the original pragma.
-
-- Note: Use Error_Msg_F here rather than Error_Msg_N.
-- The source location of the expression is not usually
-- the best choice here. For example, it gets located on
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 198175)
+++ snames.ads-tmpl (working copy)
@@ -761,6 +761,7 @@
Name_Simple_Barriers : constant Name_Id := N + $;
Name_Spec_File_Name : constant Name_Id := N + $;
Name_State : constant Name_Id := N + $;
+ Name_Statement_Assertions : constant Name_Id := N + $;
Name_Static : constant Name_Id := N + $;
Name_Stack_Size : constant Name_Id := N + $;
Name_Strict : constant Name_Id := N + $;
