* 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 <gingold@adacore.com>
* 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
+2012-10-29 Yannick Moy <moy@adacore.com>
+
+ * 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 <gingold@adacore.com>
+
+ * s-tarest.ads, s-tassta.adb: Add a pragma Partition_Elaboration_Policy.
+
2012-10-29 Robert Dewar <dewar@adacore.com>
* freeze.adb: Minor reformatting.
-- 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
-- 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;
* Pragma Ada_2012::
* Pragma Annotate::
* Pragma Assert::
-* Pragma Assert_And_Cut::
* Pragma Assertion_Policy::
* Pragma Assume_No_Invalid_Values::
* Pragma Ast_Entry::
* Pragma Ada_2012::
* Pragma Annotate::
* Pragma Assert::
-* Pragma Assert_And_Cut::
* Pragma Assertion_Policy::
* Pragma Assume_No_Invalid_Values::
* Pragma Ast_Entry::
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
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
-- 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"
-- 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;
-- 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;
-- 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;
Error_Pragma_Arg ("invalid argument for pragma%", Argx);
end if;
end Check_Arg_Is_One_Of;
+
---------------------------------
-- Check_Arg_Is_Queuing_Policy --
---------------------------------
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
Ada_2005_Pragma;
else -- Pragma_Assert_And_Cut
GNAT_Pragma;
+ S14_Pragma;
end if;
Check_At_Least_N_Arguments (1);
projects / thirdparty / gcc.git / commitdiff
