The new pragma Assert_And_Cut behaves exactly like pragma Assert for
compilation, but it informs formal verification tools of program points where
the tool may simpllify it treatment by using the given assertion.
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-10-29 Yannick Moy <m...@adacore.com>
* gnat_rm.texi: Describe new pragma Assert_And_Cut.
* par-prag.adb, sem_prag.adb, snames.ads-tmpl: Add new pragma
and treat it like pragma Assert.
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi (revision 192918)
+++ gnat_rm.texi (working copy)
@@ -105,6 +105,7 @@
* Pragma Ada_2012::
* Pragma Annotate::
* Pragma Assert::
+* Pragma Assert_And_Cut::
* Pragma Assertion_Policy::
* Pragma Assume_No_Invalid_Values::
* Pragma Ast_Entry::
@@ -843,6 +844,7 @@
* Pragma Ada_2012::
* Pragma Annotate::
* Pragma Assert::
+* Pragma Assert_And_Cut::
* Pragma Assertion_Policy::
* Pragma Assume_No_Invalid_Values::
* Pragma Ast_Entry::
@@ -1195,7 +1197,23 @@
of Ada, and the DISABLE policy is an implementation-defined
addition.
+@node Pragma Assert_And_Cut
+@unnumberedsec Pragma Assert_And_Cut
+@findex Assert_And_Cut
+@noindent
+Syntax:
+@smallexample @c ada
+pragma Assert_And_Cut (
+ boolean_EXPRESSION
+ [, string_EXPRESSION]);
+@end smallexample
+@noindent
+The effect of this pragma for compilation is exactly the same as the one
+of pragma @code{Assert}. This pragma is used to help formal verification
+tools by marking program points where the tool can simplify precise
+knowledge about execution based on the assertion given.
+
@node Pragma Assertion_Policy
@unnumberedsec Pragma Assertion_Policy
@findex Debug_Policy
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 192918)
+++ sem_prag.adb (working copy)
@@ -6759,14 +6759,17 @@
end if;
end Annotate;
- ------------
- -- Assert --
- ------------
+ -----------------------------
+ -- Assert & Assert_And_Cut --
+ -----------------------------
-- pragma Assert ([Check =>] Boolean_EXPRESSION
-- [, [Message =>] Static_String_EXPRESSION]);
- when Pragma_Assert => Assert : declare
+ -- pragma Assert_And_Cut ([Check =>] Boolean_EXPRESSION
+ -- [, [Message =>] Static_String_EXPRESSION]);
+
+ when Pragma_Assert | Pragma_Assert_And_Cut => Assert : declare
Expr : Node_Id;
Newa : List_Id;
@@ -6784,6 +6787,13 @@
-- So rewrite pragma in this manner, transfer the message
-- argument if present, and analyze the result
+ -- Pragma Assert_And_Cut is treated exactly like pragma Assert by
+ -- the frontend. Formal verification tools may use it to "cut" the
+ -- paths through the code, to make verification tractable. When
+ -- dealing with a semantically analyzed tree, the information that
+ -- a Check node N corresponds to a source Assert_And_Cut pragma
+ -- can be retrieved from the pragma kind of Original_Node(N).
+
Expr := Get_Pragma_Arg (Arg1);
Newa := New_List (
Make_Pragma_Argument_Association (Loc,
@@ -15185,6 +15195,7 @@
Pragma_All_Calls_Remote => -1,
Pragma_Annotate => -1,
Pragma_Assert => -1,
+ Pragma_Assert_And_Cut => -1,
Pragma_Assertion_Policy => 0,
Pragma_Assume_No_Invalid_Values => 0,
Pragma_Asynchronous => -1,
Index: par-prag.adb
===================================================================
--- par-prag.adb (revision 192918)
+++ par-prag.adb (working copy)
@@ -1098,6 +1098,7 @@
Pragma_All_Calls_Remote |
Pragma_Annotate |
Pragma_Assert |
+ Pragma_Assert_And_Cut |
Pragma_Asynchronous |
Pragma_Atomic |
Pragma_Atomic_Components |
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 192918)
+++ snames.ads-tmpl (working copy)
@@ -448,6 +448,7 @@
-- correctly recognize and process Name_AST_Entry.
Name_Assert : constant Name_Id := N + $; -- Ada 05
+ Name_Assert_And_Cut : constant Name_Id := N + $; -- GNAT
Name_Asynchronous : constant Name_Id := N + $;
Name_Atomic : constant Name_Id := N + $;
Name_Atomic_Components : constant Name_Id := N + $;
@@ -1697,6 +1698,7 @@
Pragma_Abort_Defer,
Pragma_All_Calls_Remote,
Pragma_Assert,
+ Pragma_Assert_And_Cut,
Pragma_Asynchronous,
Pragma_Atomic,
Pragma_Atomic_Components,
