From 9c79f208a3b8ba3c84f5ced0279a79f2cac0f50b Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 29 Oct 2012 11:48:00 +0100 Subject: [PATCH] [multiple changes] 2012-10-29 Arnaud Charlet * s-win32.ads: Kill potential warning. 2012-10-29 Yannick Moy * 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. From-SVN: r192923 --- gcc/ada/gnat_rm.texi | 18 ++++++++++++++++++ gcc/ada/par-prag.adb | 1 + gcc/ada/s-win32.ads | 9 +++++++-- gcc/ada/sem_prag.adb | 19 +++++++++++++++---- gcc/ada/snames.ads-tmpl | 2 ++ 5 files changed, 43 insertions(+), 6 deletions(-) diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 9e875bc9c52..7e0df9fb854 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -105,6 +105,7 @@ Implementation Defined Pragmas * 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 @@ consideration, the use of these pragmas should be minimized. * Pragma Ada_2012:: * Pragma Annotate:: * Pragma Assert:: +* Pragma Assert_And_Cut:: * Pragma Assertion_Policy:: * Pragma Assume_No_Invalid_Values:: * Pragma Ast_Entry:: @@ -1195,6 +1197,22 @@ of Ada from 2005 on. In GNAT, it is implemented in all versions 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 diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 8b071424567..79d57a3f8e2 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1098,6 +1098,7 @@ begin Pragma_All_Calls_Remote | Pragma_Annotate | Pragma_Assert | + Pragma_Assert_And_Cut | Pragma_Asynchronous | Pragma_Atomic | Pragma_Atomic_Components | diff --git a/gcc/ada/s-win32.ads b/gcc/ada/s-win32.ads index d3343252f16..ec07b820d45 100644 --- a/gcc/ada/s-win32.ads +++ b/gcc/ada/s-win32.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2008-2012, Free Software Foundation, Inc. -- +-- Copyright (C) 2008-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- -- @@ -32,7 +32,7 @@ -- This package plus its child provide the low level interface to the Win32 -- API. The core part of the Win32 API (common to RTX and Win32) is in this -- package, and an additional part of the Win32 API which is not supported by --- RTX is in package System.Win33.Ext. +-- RTX is in package System.Win32.Ext. with Interfaces.C; @@ -73,8 +73,13 @@ package System.Win32 is for Bits2'Size use 2; for Bits17'Size use 17; + -- Note that the following clashes with standard names are to stay + -- compatible with the historical choice of following the C names. + + pragma Warnings (Off); FALSE : constant := 0; TRUE : constant := 1; + pragma Warnings (On); function GetLastError return DWORD; pragma Import (Stdcall, GetLastError, "GetLastError"); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 2c9d518f670..4af9a517185 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -6759,14 +6759,17 @@ package body Sem_Prag is 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 @@ package body Sem_Prag is -- 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 @@ package body Sem_Prag is 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, diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 167d110749a..bae9c07a329 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -448,6 +448,7 @@ package Snames is -- 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 @@ package Snames is Pragma_Abort_Defer, Pragma_All_Calls_Remote, Pragma_Assert, + Pragma_Assert_And_Cut, Pragma_Asynchronous, Pragma_Atomic, Pragma_Atomic_Components, -- 2.34.1