* [Ada] Extended syntax for Check_Policy
@ 2013-04-12 17:03 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2013-04-12 17:03 UTC (permalink / raw)
To: gcc-patches; +Cc: Robert Dewar
[-- Attachment #1: Type: text/plain, Size: 3397 bytes --]
With this patch, Check_Policy can optionally use the same syntax as
Assertion_Policy (the old syntax is still allowed).
This test shows error detection
1. package BadCpol is
2. pragma Check_Policy
3. (Junk, Ignore); -- OK
4. pragma Check_Policy
5. (Junk => Ignore); -- OK
6. pragma Check_Policy
7. (Name => Junk, Policy => Ignore); -- OK
8. pragma Check_Policy
9. (Name => Name, Policy => Policy); -- Error
|
>>> pragma "Check_Policy" does not allow "Name" as check name
10. pragma Check_Policy
11. (Name => Name1, Policy => Ignore); -- OK
12. pragma Check_Policy
13. (Policy, Ignore); -- Error
|
>>> pragma "Check_Policy" does not allow "Policy" as check name
14. pragma Check_Policy
15. (Policy => Ignore); -- Error
|
>>> pragma "Check_Policy" does not allow "Policy" as check name
16. pragma Check_Policy
17. (Pre'Class, Ignore); -- OK
18. pragma Check_Policy
19. (Pre'Class => Check); -- OK
20. pragma Check_Policy
21. (Pre => Check, Post); -- Error
|
>>> pragma argument identifier required here
>>> since previous argument had identifier (RM 2.8(4))
>>> missing assertion kind for pragma "Check_Policy"
22. end;
The following test compiled and run without -gnata generates
the output:
OK 1
OK 2
OK 3
1. with Text_IO; use Text_IO;
2. with System.Assertions;
3. use System.Assertions;
4.
5. procedure GoodCpol is
6. X, Y : Integer;
7.
8. begin
9. X := 23;
10. Y := 24;
11.
12. declare
13. pragma Check_Policy (Grumble, Check);
14. begin
15. pragma Check (Grumble, Y < X);
|
>>> warning: check will fail at run time
16. Put_Line ("Not OK 1");
17. exception
18. when Assert_Failure =>
19. Put_Line ("OK 1");
20. end;
21.
22. declare
23. pragma Check_Policy (Mumble => Ignore, Grumble => Check);
24. begin
25. pragma Check (Mumble, Y = 100, "Not OK 2");
26. pragma Check (Grumble, Y < X);
27. Put_Line ("Not OK 3");
28. exception
29. when Assert_Failure =>
30. Put_Line ("OK 2");
31.
32. end;
33. declare
34. pragma Check_Policy (Mumble => Disable);
35. begin
36. pragma Check (Mumble, "Not OK 4");
37. Put_Line ("OK 3");
38. exception
39. when Assert_Failure =>
40. Put_Line ("Not OK 5");
41. end;
42. end GoodCpol;
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-04-12 Robert Dewar <dewar@adacore.com>
* exp_util.adb (Make_Invariant_Call): Use Check_Kind instead
of Check_Enabled.
* gnat_rm.texi (Check_Policy): Update documentation for new
Check_Policy syntax.
* sem_prag.adb (Check_Kind): Replaces Check_Enabled
(Analyze_Pragma, case Check_Policy): Rework to accomodate new
syntax (like Assertion_Policy).
* sem_prag.ads (Check_Kind): Replaces Check_Enabled.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 15599 bytes --]
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi (revision 197915)
+++ gnat_rm.texi (working copy)
@@ -1557,15 +1557,27 @@
([Name =>] CHECK_KIND,
[Policy =>] POLICY_IDENTIFIER);
-CHECK_KIND ::= IDENTIFIER |
- Pre'Class | Post'Class | Type_Invariant'Class
+Pragma Check_Policy (
+ CHECK_KIND => POLICY_IDENTIFIER
+ @{, CHECK_KIND => POLICY_IDENTIFIER@});
+ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND
+
+CHECK_KIND ::= IDENTIFIER |
+ Pre'Class |
+ Post'Class |
+ Type_Invariant'Class |
+ Invariant'Class
+
+The identifiers Name and Policy are not allowed as CHECK_KIND values. This
+avoids confusion between the two possible syntax forms for this pragma.
+
POLICY_IDENTIFIER ::= ON | OFF | CHECK | DISABLE | IGNORE
@end smallexample
@noindent
This pragma is used to set the checking policy for assertions (specified
-by aspects of pragmas), the @code{Debug} pragma, or additional checks
+by aspects or pragmas), the @code{Debug} pragma, or additional checks
to be checked using the @code{Check} pragma. It may appear either as
a configuration pragma, or within a declarative part of package. In the
latter case, it applies from the point where it appears to the end of
@@ -1573,10 +1585,8 @@
The @code{Check_Policy} pragma is similar to the
predefined @code{Assertion_Policy} pragma,
-and if the first argument corresponds to one of the assertion kinds that
+and if the check kind corresponds to one of the assertion kinds that
are allowed by @code{Assertion_Policy}, then the effect is identical.
-The identifiers @code{Precondition} and @code{Postcondition} are allowed
-synonyms for @code{Pre} and @code{Post}.
If the first argument is Debug, then the policy applies to Debug pragmas,
disabling their effect if the policy is @code{Off}, @code{Disable}, or
@@ -1605,9 +1615,8 @@
The check policy settings @code{CHECK} and @code{IGNORE} are recognized
as synonyms for @code{ON} and @code{OFF}. These synonyms are provided for
compatibility with the standard @code{Assertion_Policy} pragma. The check
-policy setting @code{DISABLE} is also synonymous with @code{OFF} in this
-context, but does not have any other significance for check
-names other than assertion kinds.
+policy setting @code{DISABLE} causes the second argument of a corresponding
+@code{Check} pragma to be completely ignored and not analyzed.
@node Pragma Comment
@unnumberedsec Pragma Comment
Index: exp_util.adb
===================================================================
--- exp_util.adb (revision 197917)
+++ exp_util.adb (working copy)
@@ -5456,7 +5456,7 @@
pragma Assert
(Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)));
- if Check_Enabled (Name_Invariant) then
+ if Check_Kind (Name_Invariant) = Name_Check then
return
Make_Procedure_Call_Statement (Loc,
Name =>
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 197917)
+++ sem_prag.adb (working copy)
@@ -2320,12 +2320,12 @@
-- For a pragma PPC in the extended main source unit, record enabled
-- status in SCO.
- -- This may seem redundant with the call to Check_Enabled occurring
- -- later on when the pragma is rewritten into a pragma Check but
- -- is actually required in the case of a postcondition within a
+ -- This may seem redundant with the call to Check_Kind test that
+ -- occurs later on when the pragma is rewritten into a pragma Check
+ -- but is actually required in the case of a postcondition within a
-- generic.
- if Check_Enabled (Pname) and then not Split_PPC (N) then
+ if Check_Kind (Pname) = Name_Check and then not Split_PPC (N) then
Set_SCO_Pragma_Enabled (Loc);
end if;
@@ -6763,7 +6763,11 @@
Check_Applicable_Policy (N);
+ -- If pragma is disable, rewrite as Null statement and skip analysis
+
if Is_Disabled (N) then
+ Rewrite (N, Make_Null_Statement (Loc));
+ Analyze (N);
raise Pragma_Exit;
end if;
@@ -7612,6 +7616,7 @@
-- now inserted all the equivalent Check pragmas.
Rewrite (N, Make_Null_Statement (Loc));
+ Analyze (N);
end if;
end Assertion_Policy;
@@ -8096,7 +8101,32 @@
Rewrite_Assertion_Kind (Get_Pragma_Arg (Arg1));
Check_Arg_Is_Identifier (Arg1);
Cname := Chars (Get_Pragma_Arg (Arg1));
- Check_On := Check_Enabled (Cname);
+
+ -- Set Check_On to indicate check status
+
+ case Check_Kind (Cname) is
+ when Name_Ignore =>
+ Check_On := False;
+
+ when Name_Check =>
+ Check_On := True;
+
+ -- For disable, rewrite pragma as null statement and skip
+ -- rest of the analysis of the pragma.
+
+ when Name_Disable =>
+ Rewrite (N, Make_Null_Statement (Loc));
+ Analyze (N);
+ raise Pragma_Exit;
+
+ -- No other possibilities
+
+ when others =>
+ raise Program_Error;
+ end case;
+
+ -- If check kind was not Disable, then continue pragma analysis
+
Expr := Get_Pragma_Arg (Arg2);
-- Deal with SCO generation
@@ -8233,24 +8263,36 @@
-- Check_Policy --
------------------
+ -- This is the old style syntax, which is still allowed in all modes:
+
-- pragma Check_Policy ([Name =>] CHECK_KIND
-- [Policy =>] POLICY_IDENTIFIER);
-- POLICY_IDENTIFIER ::= On | Off | Check | Disable | Ignore
- -- CHECK_KIND ::= IDENTIFIER |
- -- Pre'Class | Post'Class | Identifier'Class
+ -- CHECK_KIND ::= IDENTIFIER |
+ -- Pre'Class |
+ -- Post'Class |
+ -- Type_Invariant'Class |
+ -- Invariant'Class
- when Pragma_Check_Policy => Check_Policy :
+ -- This is the new style syntax, compatible with Assertion_Policy
+ -- and also allowed in all modes.
+
+ -- Pragma Check_Policy (
+ -- CHECK_KIND => POLICY_IDENTIFIER
+ -- {, CHECK_KIND => POLICY_IDENTIFIER});
+
+ -- Note: the identifiers Name and Policy are not allowed as
+ -- Check_Kind values. This avoids ambiguities between the old and
+ -- new form syntax.
+
+ when Pragma_Check_Policy => Check_Policy : declare
+ Kind : Node_Id;
+
begin
GNAT_Pragma;
- Check_Arg_Count (2);
- Check_Optional_Identifier (Arg1, Name_Name);
- Rewrite_Assertion_Kind (Get_Pragma_Arg (Arg1));
- Check_Arg_Is_Identifier (Arg1);
- Check_Optional_Identifier (Arg2, Name_Policy);
- Check_Arg_Is_One_Of
- (Arg2, Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
+ Check_At_Least_N_Arguments (1);
-- A Check_Policy pragma can appear either as a configuration
-- pragma, or in a declarative part or a package spec (see RM
@@ -8261,8 +8303,90 @@
Check_Is_In_Decl_Part_Or_Package_Spec;
end if;
- Set_Next_Pragma (N, Opt.Check_Policy_List);
- Opt.Check_Policy_List := N;
+ -- Figure out if we have the old or new syntax. We have the
+ -- old syntax if the first argument has no identifier, or the
+ -- identifier is Name.
+
+ if Nkind (Arg1) /= N_Pragma_Argument_Association
+ or else Nam_In (Chars (Arg1), No_Name, Name_Name)
+ then
+ -- Old syntax
+
+ Check_Arg_Count (2);
+ Check_Optional_Identifier (Arg1, Name_Name);
+ Kind := Get_Pragma_Arg (Arg1);
+ Rewrite_Assertion_Kind (Kind);
+ Check_Arg_Is_Identifier (Arg1);
+
+ -- Check forbidden check kind
+
+ if Nam_In (Chars (Kind), Name_Name, Name_Policy) then
+ Error_Msg_Name_2 := Chars (Kind);
+ Error_Pragma_Arg
+ ("pragma% does not allow% as check name", Arg1);
+ end if;
+
+ -- Check policy
+
+ Check_Optional_Identifier (Arg2, Name_Policy);
+ Check_Arg_Is_One_Of
+ (Arg2,
+ Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
+
+ -- And chain pragma on the Check_Policy_List for search
+
+ Set_Next_Pragma (N, Opt.Check_Policy_List);
+ Opt.Check_Policy_List := N;
+
+ -- For the new syntax, what we do is to convert each argument to
+ -- an old syntax equivalent. We do that because we want to chain
+ -- old style Check_Pragmas for the search (we don't wnat to have
+ -- to deal with multiple arguments in the search)
+
+ else
+ declare
+ Arg : Node_Id;
+ Argx : Node_Id;
+ LocP : Source_Ptr;
+
+ begin
+ Arg := Arg1;
+ while Present (Arg) loop
+ LocP := Sloc (Arg);
+ Argx := Get_Pragma_Arg (Arg);
+
+ -- Kind must be specified
+
+ if Nkind (Arg) /= N_Pragma_Argument_Association
+ or else Chars (Arg) = No_Name
+ then
+ Error_Pragma_Arg
+ ("missing assertion kind for pragma%", Arg);
+ end if;
+
+ -- Construct equivalent old form syntax Check_Policy
+ -- pragma and insert it to get remaining checks.
+
+ Insert_Action (N,
+ Make_Pragma (LocP,
+ Chars => Name_Check_Policy,
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (LocP,
+ Expression =>
+ Make_Identifier (LocP, Chars (Arg))),
+ Make_Pragma_Argument_Association (Sloc (Argx),
+ Expression => Argx))));
+
+ Arg := Next (Arg);
+ end loop;
+
+ -- Rewrite original Check_Policy pragma to null, since we
+ -- have converted it into a series of old syntax pragmas.
+
+ Rewrite (N, Make_Null_Statement (Loc));
+ Analyze (N);
+ end;
+ end if;
end Check_Policy;
---------------------
@@ -17734,11 +17858,11 @@
when Pragma_Exit => null;
end Analyze_Pragma;
- -------------------
- -- Check_Enabled --
- -------------------
+ ----------------
+ -- Check_Kind --
+ ----------------
- function Check_Enabled (Nam : Name_Id) return Boolean is
+ function Check_Kind (Nam : Name_Id) return Name_Id is
PP : Node_Id;
begin
@@ -17757,9 +17881,11 @@
then
case (Chars (Get_Pragma_Arg (Last (PPA)))) is
when Name_On | Name_Check =>
- return True;
- when Name_Off | Name_Disable | Name_Ignore =>
- return False;
+ return Name_Check;
+ when Name_Off | Name_Ignore =>
+ return Name_Ignore;
+ when Name_Disable =>
+ return Name_Disable;
when others =>
raise Program_Error;
end case;
@@ -17775,8 +17901,12 @@
-- compatibility with the RM for the cases of assertion, invariant,
-- precondition, predicate, and postcondition.
- return Assertions_Enabled;
- end Check_Enabled;
+ if Assertions_Enabled then
+ return Name_Check;
+ else
+ return Name_Ignore;
+ end if;
+ end Check_Kind;
-----------------------------
-- Check_Applicable_Policy --
Index: sem_prag.ads
===================================================================
--- sem_prag.ads (revision 197915)
+++ sem_prag.ads (working copy)
@@ -54,7 +54,7 @@
-- of the expressions in the pragma as "spec expressions" (see section
-- in Sem "Handling of Default and Per-Object Expressions...").
- function Check_Enabled (Nam : Name_Id) return Boolean;
+ function Check_Kind (Nam : Name_Id) return Name_Id;
-- This function is used in connection with pragmas Assertion, Check,
-- and assertion aspects and pragmas, to determine if Check pragmas
-- (or corresponding assertion aspects or pragmas) are currently active
@@ -63,17 +63,15 @@
-- Assertion_Policy as configuration pragmas either in a configuration
-- pragma file, or at the start of the current unit, or locally given
-- Check_Policy and Assertion_Policy pragmas that are currently active.
- -- True is returned if the specified check is enabled.
--
- -- This function knows about all relevant synonyms (e.g. Precondition or
- -- Pre can be used to refer to the Pre aspect or Precondition pragma, and
- -- Predicate refers to both static and dynamic predicates, and Assertion
- -- applies to all assertion aspects and pragmas).
+ -- The value returned is one of the names Check, Ignore, Disable (On
+ -- returns Check, and Off returns Ignore).
--
- -- Note: for assertion kinds Pre'Class, Post'Class, Type_Invariant'Class,
- -- the name passed is Name_uPre, Name_uPost, Name_uType_Invariant, which
- -- corresponds to _Pre, _Post, _Type_Invariant, which are special names
- -- used in identifiers to represent these attribute references.
+ -- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
+ -- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
+ -- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
+ -- _Post, _Invariant, or _Type_Invariant, which are special names used
+ -- in identifiers to represent these attribute references.
procedure Check_Applicable_Policy (N : Node_Id);
-- N is either an N_Aspect or an N_Pragma node. There are two cases. If
@@ -83,9 +81,9 @@
-- we use for the purpose of this procedure is the aspect name, which may
-- be different from the pragma name (e.g. Precondition for Pre aspect).
-- In addition, 'Class aspects are recognized (and the corresponding
- -- special names used in the processing.
+ -- special names used in the processing).
--
- -- If the name is valid assertion_Kind name, then the Check_Policy pragma
+ -- If the name is valid ASSERTION_KIND name, then the Check_Policy pragma
-- chain is checked for a matching entry (or for an Assertion entry which
-- matches all possibilities). If a matching entry is found then the policy
-- is checked. If it is Off, Ignore, or Disable, then the Is_Ignored flag
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2013-04-12 13:46 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2013-04-12 17:03 [Ada] Extended syntax for Check_Policy Arnaud Charlet
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).