From fb261027f4a4fab38020063a605ff58cff6822a5 Mon Sep 17 00:00:00 2001 From: charlet Date: Mon, 29 Oct 2012 11:07:12 +0000 Subject: [PATCH] 2012-10-29 Yannick Moy * debug.adb Associate debug switch -gnatd.V to extensions for formal verification. * gnat1drv.adb (Adjust_Global_Switches): Set flag S14_Extensions when -gnatd.V is set. * gnat_rm.texi: Remove doc for Assert_And_Cut. * opt.ads Declare new flag S14_Extensions, to be set when new aspects/pragmas/attributes for formal verification should be accepted. * sem_prag.adb (Analyze_Pragma): Check that S14_Extensions is set when treating pragma Assert_And_Cut. 2012-10-29 Tristan Gingold * s-tarest.ads, s-tassta.adb: Add a pragma Partition_Elaboration_Policy. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@192931 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/ChangeLog | 17 +++++++++++++++++ gcc/ada/debug.adb | 2 +- gcc/ada/gnat1drv.adb | 4 ++++ gcc/ada/gnat_rm.texi | 38 +------------------------------------- gcc/ada/opt.ads | 5 +++++ gcc/ada/s-tarest.ads | 4 ++++ gcc/ada/s-tassta.adb | 4 ++++ gcc/ada/sem_prag.adb | 17 +++++++++++++++++ 8 files changed, 53 insertions(+), 38 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index cb3f6ab68629..c200a06367c0 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,20 @@ +2012-10-29 Yannick Moy + + * debug.adb Associate debug switch -gnatd.V to extensions for + formal verification. + * gnat1drv.adb (Adjust_Global_Switches): Set flag S14_Extensions + when -gnatd.V is set. + * gnat_rm.texi: Remove doc for Assert_And_Cut. + * opt.ads Declare new flag S14_Extensions, to be set when new + aspects/pragmas/attributes for formal verification should be + accepted. + * sem_prag.adb (Analyze_Pragma): Check that S14_Extensions is + set when treating pragma Assert_And_Cut. + +2012-10-29 Tristan Gingold + + * s-tarest.ads, s-tassta.adb: Add a pragma Partition_Elaboration_Policy. + 2012-10-29 Robert Dewar * freeze.adb: Minor reformatting. diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index f6f24f9c7bfa..02f04bcecdfa 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -139,7 +139,7 @@ package body Debug is -- d.S Force Optimize_Alignment (Space) -- d.T Force Optimize_Alignment (Time) -- d.U Ignore indirect calls for static elaboration - -- d.V + -- d.V Extensions for formal verification -- d.W Print out debugging information for Walk_Library_Items -- d.X Use Expression_With_Actions -- d.Y Do not use Expression_With_Actions diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index a8eb320667aa..39d008e23a75 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -418,6 +418,10 @@ procedure Gnat1drv is -- Set switches for formal verification mode + if Debug_Flag_Dot_VV then + S14_Extensions := True; + end if; + if Debug_Flag_Dot_FF then Alfa_Mode := True; diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 3561cedfb903..36202bd84d37 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -105,7 +105,6 @@ 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:: @@ -844,7 +843,6 @@ 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:: @@ -1197,40 +1195,6 @@ 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. For example, in -the procedure below, all that is needed to prove that the code using X -is free from run-time errors is that X is positive. Without the pragma, -GNATprove considers all execution paths through P, which may be -many. With the pragma, GNATprove only needs to consider the paths from -the start of the procedure to the pragma, and the paths from the pragma -to the end of the procedure, hence many fewer paths. For more details, -see the GNATprove User's Guide. - -@smallexample @c ada -procedure P is - X : Integer; -begin - -- complex computation that sets X - pragma Assert_And_Cut (X > 0); - -- complex computation that uses X -end P; -@end smallexample - @node Pragma Assertion_Policy @unnumberedsec Pragma Assertion_Policy @findex Debug_Policy @@ -7986,7 +7950,7 @@ features are used, as defined in Annex J of the Ada Reference Manual. wide types appear, and that no wide or wide wide string or character literals appear in the program (that is literals representing characters not in -type @code{Character}. +type @code{Character}). @node SPARK @unnumberedsubsec SPARK diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 17c93177704e..b832c1fd0b97 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1936,6 +1936,11 @@ package Opt is -- for integers are limited to the strict minimum with this option. Set by -- debug flag -gnatd.D. + S14_Extensions : Boolean := False; + -- When this flag is set, new aspects/pragmas/attributes are accepted, + -- whose main purpose is to facilitate formal verification. Set by debug + -- flag -gnatd.V. + function Full_Expander_Active return Boolean; pragma Inline (Full_Expander_Active); -- Returns the value of (Expander_Active and not Alfa_Mode). This "flag" diff --git a/gcc/ada/s-tarest.ads b/gcc/ada/s-tarest.ads index b6639b1f07f3..c8769754707f 100644 --- a/gcc/ada/s-tarest.ads +++ b/gcc/ada/s-tarest.ads @@ -43,6 +43,10 @@ -- The restricted GNARLI is also composed of System.Protected_Objects and -- System.Protected_Objects.Single_Entry +pragma Partition_Elaboration_Policy (Sequential); +-- This package only implements the sequential elaboration policy. This pragma +-- will enforce it (and detect conflicts with user specified policy). + with System.Task_Info; with System.Parameters; diff --git a/gcc/ada/s-tassta.adb b/gcc/ada/s-tassta.adb index 08886c157bb8..ab75b2337c54 100644 --- a/gcc/ada/s-tassta.adb +++ b/gcc/ada/s-tassta.adb @@ -33,6 +33,10 @@ pragma Polling (Off); -- Turn off polling, we do not want ATC polling to take place during tasking -- operations. It causes infinite loops and other problems. +pragma Partition_Elaboration_Policy (Concurrent); +-- This package only implements the concurrent elaboration policy. This pragma +-- will enforce it (and detect conflicts with user specified policy). + with Ada.Exceptions; with Ada.Unchecked_Deallocation; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index e5dfde99a73b..7f098abf6acf 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -782,6 +782,10 @@ package body Sem_Prag is -- Called for all GNAT defined pragmas to check the relevant restriction -- (No_Implementation_Pragmas). + procedure S14_Pragma; + -- Called for all pragmas defined for formal verification to check that + -- the S14_Extensions flag is set. + function Is_Before_First_Decl (Pragma_Node : Node_Id; Decls : List_Id) return Boolean; @@ -1280,6 +1284,7 @@ package body Sem_Prag is Error_Pragma_Arg ("invalid argument for pragma%", Argx); end if; end Check_Arg_Is_One_Of; + --------------------------------- -- Check_Arg_Is_Queuing_Policy -- --------------------------------- @@ -6419,6 +6424,17 @@ package body Sem_Prag is end if; end Set_Ravenscar_Profile; + ---------------- + -- S14_Pragma -- + ---------------- + + procedure S14_Pragma is + begin + if not S14_Extensions then + Error_Pragma ("pragma% requires the use of debug switch -gnatd.V"); + end if; + end S14_Pragma; + -- Start of processing for Analyze_Pragma begin @@ -6800,6 +6816,7 @@ package body Sem_Prag is Ada_2005_Pragma; else -- Pragma_Assert_And_Cut GNAT_Pragma; + S14_Pragma; end if; Check_At_Least_N_Arguments (1); -- 2.47.2