===================================================================
@@ -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
===================================================================
@@ -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,
===================================================================
@@ -1098,6 +1098,7 @@
Pragma_All_Calls_Remote |
Pragma_Annotate |
Pragma_Assert |
+ Pragma_Assert_And_Cut |
Pragma_Asynchronous |
Pragma_Atomic |
Pragma_Atomic_Components |
===================================================================
@@ -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,