Debug flags used during initial development of GNATprove are now freed,
at the exception of -gnatd.F, which stays as a pure debug flag to emulate
the behavior of the frontend in GNATprove mode.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-20 Yannick Moy <m...@adacore.com>
* debug.adb Free debug flags -gnatd.D, -gnatd.G and -gnatd.V *
* errout.adb (Compilation_Errors): Remove special handling in
GNATprove mode.
* gnat1drv.adb (Adjust_Global_Switches): Remove handling of the
removed debug flags.
* gnat_rm.texi: Initial documentation for Abstract_State, Depends,
Global, Initial_Condition, Initializes and Refined_State pragmas and
aspects.
* opt.ads (Frame_Condition_Mode, Formal_Extensions,
SPARK_Strict_Mode): Remove global flags.
* sem_ch3.adb (Analyze_Object_Declaration): Check of no hidden state
always performed now, on packages declaring a null state.
(Signed_Integer_Type_Declaration): Remove ill-designed attempt
at providing pedantic mode for bounds of integer types.
* sem_ch4.adb (Analyze_Quantified_Expression): Warning on suspicious
"some" quantified expression now issued under control of -gnatw.t,
like the other warning on unused bound variable.
* sem_prag.adb (Check_Precondition_Postcondition): Remove useless test
on removed flag.
(Analyze_Pragma): Remove tests for SPARK 2014
pragmas, not officially allowed by GNAT.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 206822)
+++ sem_ch3.adb (working copy)
@@ -3911,7 +3911,7 @@
-- Verify whether the object declaration introduces an illegal hidden
-- state within a package subject to a null abstract state.
- if Formal_Extensions and then Ekind (Id) = E_Variable then
+ if Ekind (Id) = E_Variable then
Check_No_Hidden_State (Id);
end if;
end Analyze_Object_Declaration;
@@ -20444,66 +20444,8 @@
Set_Ekind (T, E_Signed_Integer_Subtype);
Set_Etype (T, Implicit_Base);
- -- In formal verification mode, restrict the base type's range to the
- -- minimum allowed by RM 3.5.4, namely the smallest symmetric range
- -- around zero with a possible extra negative value that contains the
- -- subtype range. Keep Size, RM_Size and First_Rep_Item info, which
- -- should not be relied upon in formal verification.
+ Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
- if SPARK_Strict_Mode then
- declare
- Sym_Hi_Val : Uint;
- Sym_Lo_Val : Uint;
- Dloc : constant Source_Ptr := Sloc (Def);
- Lbound : Node_Id;
- Ubound : Node_Id;
- Bounds : Node_Id;
-
- begin
- -- If the subtype range is empty, the smallest base type range
- -- is the symmetric range around zero containing Lo_Val and
- -- Hi_Val.
-
- if UI_Gt (Lo_Val, Hi_Val) then
- Sym_Hi_Val := UI_Max (UI_Abs (Lo_Val), UI_Abs (Hi_Val));
- Sym_Lo_Val := UI_Negate (Sym_Hi_Val);
-
- -- Otherwise, if the subtype range is not empty and Hi_Val has
- -- the largest absolute value, Hi_Val is non negative and the
- -- smallest base type range is the symmetric range around zero
- -- containing Hi_Val.
-
- elsif UI_Le (UI_Abs (Lo_Val), UI_Abs (Hi_Val)) then
- Sym_Hi_Val := Hi_Val;
- Sym_Lo_Val := UI_Negate (Hi_Val);
-
- -- Otherwise, the subtype range is not empty, Lo_Val has the
- -- strictly largest absolute value, Lo_Val is negative and the
- -- smallest base type range is the symmetric range around zero
- -- with an extra negative value Lo_Val.
-
- else
- Sym_Lo_Val := Lo_Val;
- Sym_Hi_Val := UI_Sub (UI_Negate (Lo_Val), Uint_1);
- end if;
-
- Lbound := Make_Integer_Literal (Dloc, Sym_Lo_Val);
- Ubound := Make_Integer_Literal (Dloc, Sym_Hi_Val);
- Set_Is_Static_Expression (Lbound);
- Set_Is_Static_Expression (Ubound);
- Analyze_And_Resolve (Lbound, Any_Integer);
- Analyze_And_Resolve (Ubound, Any_Integer);
-
- Bounds := Make_Range (Dloc, Lbound, Ubound);
- Set_Etype (Bounds, Base_Typ);
-
- Set_Scalar_Range (Implicit_Base, Bounds);
- end;
-
- else
- Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
- end if;
-
Set_Size_Info (T, (Implicit_Base));
Set_First_Rep_Item (T, First_Rep_Item (Implicit_Base));
Set_Scalar_Range (T, Def);
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi (revision 206833)
+++ gnat_rm.texi (working copy)
@@ -98,6 +98,7 @@
Implementation Defined Pragmas
* Pragma Abort_Defer::
+* Pragma Abstract_State::
* Pragma Ada_83::
* Pragma Ada_95::
* Pragma Ada_05::
@@ -137,6 +138,7 @@
* Pragma Debug::
* Pragma Debug_Policy::
* Pragma Default_Storage_Pool::
+* Pragma Depends::
* Pragma Detect_Blocking::
* Pragma Disable_Atomic_Synchronization::
* Pragma Dispatching_Domain::
@@ -157,6 +159,7 @@
* Pragma Favor_Top_Level::
* Pragma Finalize_Storage_Only::
* Pragma Float_Representation::
+* Pragma Global::
* Pragma Ident::
* Pragma Implementation_Defined::
* Pragma Implemented::
@@ -168,7 +171,9 @@
* Pragma Import_Valued_Procedure::
* Pragma Independent::
* Pragma Independent_Components::
+* Pragma Initial_Condition::
* Pragma Initialize_Scalars::
+* Pragma Initializes::
* Pragma Inline_Always::
* Pragma Inline_Generic::
* Pragma Interface::
@@ -225,6 +230,7 @@
* Pragma Pure_12::
* Pragma Pure_Function::
* Pragma Ravenscar::
+* Pragma Refined_State::
* Pragma Relative_Deadline::
* Pragma Remote_Access_Type::
* Pragma Restricted_Run_Time::
@@ -277,7 +283,6 @@
* Aspect Abstract_State::
* Aspect Ada_2005::
* Aspect Ada_2012::
-* Pragma Allow_Integer_Address::
* Aspect Compiler_Unit::
* Aspect Contract_Cases::
* Aspect Depends::
@@ -285,6 +290,8 @@
* Aspect Dimension_System::
* Aspect Favor_Top_Level::
* Aspect Global::
+* Aspect Initial_Condition::
+* Aspect Initializes::
* Aspect Inline_Always::
* Aspect Invariant::
* Aspect Object_Size::
@@ -294,6 +301,7 @@
* Aspect Pure_05::
* Aspect Pure_12::
* Aspect Pure_Function::
+* Aspect Refined_State::
* Aspect Remote_Access_Type::
* Aspect Scalar_Storage_Order::
* Aspect Shared::
@@ -923,6 +931,7 @@
@menu
* Pragma Abort_Defer::
+* Pragma Abstract_State::
* Pragma Ada_83::
* Pragma Ada_95::
* Pragma Ada_05::
@@ -962,6 +971,7 @@
* Pragma Debug::
* Pragma Debug_Policy::
* Pragma Default_Storage_Pool::
+* Pragma Depends::
* Pragma Detect_Blocking::
* Pragma Disable_Atomic_Synchronization::
* Pragma Dispatching_Domain::
@@ -982,6 +992,7 @@
* Pragma Favor_Top_Level::
* Pragma Finalize_Storage_Only::
* Pragma Float_Representation::
+* Pragma Global::
* Pragma Ident::
* Pragma Implementation_Defined::
* Pragma Implemented::
@@ -993,7 +1004,9 @@
* Pragma Import_Valued_Procedure::
* Pragma Independent::
* Pragma Independent_Components::
+* Pragma Initial_Condition::
* Pragma Initialize_Scalars::
+* Pragma Initializes::
* Pragma Inline_Always::
* Pragma Inline_Generic::
* Pragma Interface::
@@ -1050,6 +1063,7 @@
* Pragma Pure_12::
* Pragma Pure_Function::
* Pragma Ravenscar::
+* Pragma Refined_State::
* Pragma Relative_Deadline::
* Pragma Remote_Access_Type::
* Pragma Restricted_Run_Time::
@@ -1115,6 +1129,13 @@
for the declarations or handlers, if any, associated with this statement
sequence).
+@node Pragma Abstract_State
+@unnumberedsec Pragma Abstract_State
+@findex Abstract_State
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.4.
+
@node Pragma Ada_83
@unnumberedsec Pragma Ada_83
@findex Ada_83
@@ -2411,6 +2432,13 @@
versions of Ada as an implementation-defined pragma.
See Ada 2012 Reference Manual for details.
+@node Pragma Depends
+@unnumberedsec Pragma Depends
+@findex Depends
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 6.1.5.
+
@node Pragma Detect_Blocking
@unnumberedsec Pragma Detect_Blocking
@findex Detect_Blocking
@@ -3188,6 +3216,13 @@
Digits values above 15 are not allowed.
@end itemize
+@node Pragma Global
+@unnumberedsec Pragma Global
+@findex Global
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 6.1.4.
+
@node Pragma Ident
@unnumberedsec Pragma Ident
@findex Ident
@@ -3629,6 +3664,13 @@
constraints on the representation of the object (for instance prohibiting
tight packing).
+@node Pragma Initial_Condition
+@unnumberedsec Pragma Initial_Condition
+@findex Initial_Condition
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.6.
+
@node Pragma Initialize_Scalars
@unnumberedsec Pragma Initialize_Scalars
@findex Initialize_Scalars
@@ -3691,6 +3733,13 @@
checking (see description of stack checking in the @value{EDITION}
User's Guide) when using this pragma.
+@node Pragma Initializes
+@unnumberedsec Pragma Initializes
+@findex Initializes
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.5.
+
@node Pragma Inline_Always
@unnumberedsec Pragma Inline_Always
@findex Inline_Always
@@ -5852,6 +5901,13 @@
@noindent
which is the preferred method of setting the @code{Ravenscar} profile.
+@node Pragma Refined_State
+@unnumberedsec Pragma Refined_State
+@findex Refined_State
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.2.2.
+
@node Pragma Relative_Deadline
@unnumberedsec Pragma Relative_Deadline
@findex Relative_Deadline
@@ -7508,6 +7564,8 @@
* Aspect Dimension_System::
* Aspect Favor_Top_Level::
* Aspect Global::
+* Aspect Initial_Condition::
+* Aspect Initializes::
* Aspect Inline_Always::
* Aspect Invariant::
* Aspect Lock_Free::
@@ -7518,6 +7576,7 @@
* Aspect Pure_05::
* Aspect Pure_12::
* Aspect Pure_Function::
+* Aspect Refined_State::
* Aspect Remote_Access_Type::
* Aspect Scalar_Storage_Order::
* Aspect Shared::
@@ -7674,8 +7733,20 @@
@unnumberedsec Aspect Global
@findex Global
@noindent
-This aspect is equivalent pragma @code{Global}.
+This aspect is equivalent to pragma @code{Global}.
+@node Aspect Initial_Condition
+@unnumberedsec Aspect Initial_Condition
+@findex Initial_Condition
+@noindent
+This aspect is equivalent to pragma @code{Initial_Condition}.
+
+@node Aspect Initializes
+@unnumberedsec Aspect Initializes
+@findex Initializes
+@noindent
+This aspect is equivalent to pragma @code{Initializes}.
+
@node Aspect Inline_Always
@unnumberedsec Aspect Inline_Always
@findex Inline_Always
@@ -7744,6 +7815,12 @@
@noindent
This aspect is equivalent to pragma @code{Pure_Function}.
+@node Aspect Refined_State
+@unnumberedsec Aspect Refined_State
+@findex Refined_State
+@noindent
+This aspect is equivalent to pragma @code{Refined_State}.
+
@node Aspect Remote_Access_Type
@unnumberedsec Aspect Remote_Access_Type
@findex Remote_Access_Type
Index: debug.adb
===================================================================
--- debug.adb (revision 206809)
+++ debug.adb (working copy)
@@ -121,10 +121,10 @@
-- d.A Read/write Aspect_Specifications hash table to tree
-- d.B
-- d.C Generate concatenation call, do not generate inline code
- -- d.D SPARK strict mode
+ -- d.D
-- d.E Turn selected errors into warnings
- -- d.F SPARK mode
- -- d.G Frame condition mode for gnat2why
+ -- d.F Debug mode for GNATprove
+ -- d.G
-- d.H
-- d.I Do not ignore enum representation clauses in CodePeer mode
-- d.J Disable parallel SCIL generation mode
@@ -139,7 +139,7 @@
-- d.S Force Optimize_Alignment (Space)
-- d.T Force Optimize_Alignment (Time)
-- d.U Ignore indirect calls for static elaboration
- -- d.V Extensions for formal verification
+ -- d.V
-- d.W Print out debugging information for Walk_Library_Items
-- d.X
-- d.Y
@@ -594,22 +594,13 @@
-- d.C Generate call to System.Concat_n.Str_Concat_n routines in cases
-- where we would normally generate inline concatenation code.
- -- d.D SPARK strict mode. Interpret compiler permissions as strictly as
- -- possible in SPARK mode.
-
-- d.E Turn selected errors into warnings. This debug switch causes a
-- specific set of error messages into warnings. Setting this switch
-- causes Opt.Error_To_Warning to be set to True.
- -- d.F SPARK mode. Generate AST in a form suitable for formal
- -- verification, as well as additional cross reference information in
- -- ALI files to compute effects of subprograms. Note that ALI files
- -- are only written when option d.G is also given.
+ -- d.F Sets GNATprove_Mode to True. This allows debugging the frontend in
+ -- the special mode used by GNATprove.
- -- d.G Frame condition mode for gnat2why. In this mode, gnat2why will
- -- generate ALI files with an extra section which contains the effects
- -- of subprograms.
-
-- d.I Do not ignore enum representation clauses in CodePeer mode.
-- The default of ignoring representation clauses for enumeration
-- types in CodePeer is good for the majority of Ada code, but in some
@@ -657,10 +648,6 @@
-- reverts to the behavior of earlier compilers, which ignored
-- indirect calls.
- -- d.V Extensions for formal verification. New attributes/aspects/pragmas
- -- defined in GNAT for formal verification with the tool GNATprove are
- -- only accepted under this switch.
-
-- d.W Print out debugging information for Walk_Library_Items, including
-- the order in which units are walked. This is primarily for use in
-- debugging CodePeer mode.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 206836)
+++ sem_prag.adb (working copy)
@@ -2998,12 +2998,6 @@
-- 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.
- -- This name needs fixing ??? There is no such thing as an
- -- "S14_Extensions" flag ???
-
function Is_Before_First_Decl
(Pragma_Node : Node_Id;
Decls : List_Id) return Boolean;
@@ -4651,7 +4645,7 @@
-- N_Contract node.
if Acts_As_Spec (PO)
- and then (GNATprove_Mode or Formal_Extensions)
+ and then GNATprove_Mode
then
declare
Prag : constant Node_Id := New_Copy_Tree (N);
@@ -9302,17 +9296,6 @@
end if;
end Set_Ravenscar_Profile;
- ----------------
- -- S14_Pragma --
- ----------------
-
- procedure S14_Pragma is
- begin
- if not Formal_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
@@ -9700,9 +9683,7 @@
-- Verify whether the state introduces an illegal hidden state
-- within a package subject to a null abstract state.
- if Formal_Extensions then
- Check_No_Hidden_State (Id);
- end if;
+ Check_No_Hidden_State (Id);
-- Associate the state with its related package
@@ -9722,7 +9703,6 @@
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
Ensure_Aggregate_Form (Arg1);
@@ -11894,7 +11874,6 @@
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
Ensure_Aggregate_Form (Arg1);
@@ -13165,7 +13144,6 @@
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
Ensure_Aggregate_Form (Arg1);
@@ -13897,7 +13875,6 @@
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
-- Ensure the proper placement of the pragma. Initial_Condition
@@ -14009,7 +13986,6 @@
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
Ensure_Aggregate_Form (Arg1);
@@ -17542,7 +17518,6 @@
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
-- Ensure the proper placement of the pragma. Refined states must
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb (revision 206825)
+++ gnat1drv.adb (working copy)
@@ -298,12 +298,6 @@
Treat_Categorization_Errors_As_Warnings := True;
end if;
- -- Set switches for formal verification mode
-
- if Debug_Flag_Dot_VV then
- Formal_Extensions := True;
- end if;
-
-- Enable GNATprove_Mode when using -gnatd.F switch
if Debug_Flag_Dot_FF then
@@ -315,24 +309,6 @@
if GNATprove_Mode then
- -- Set strict standard interpretation of compiler permissions
-
- if Debug_Flag_Dot_DD then
- SPARK_Strict_Mode := True;
- end if;
-
- -- Distinguish between the two modes of gnat2why: frame condition
- -- generation (generation of ALI files) and analysis (no ALI files
- -- generated). This is done with the switch -gnatd.G, which activates
- -- frame condition mode. The other changes in behavior depending on
- -- this switch are done in gnat2why directly.
-
- if Debug_Flag_Dot_GG then
- Frame_Condition_Mode := True;
- else
- Opt.Disable_ALI_File := True;
- end if;
-
-- Turn off inlining, which would confuse formal verification output
-- and gain nothing.
Index: errout.adb
===================================================================
--- errout.adb (revision 206809)
+++ errout.adb (working copy)
@@ -233,15 +233,6 @@
begin
if not Finalize_Called then
raise Program_Error;
-
- -- In formal verification mode, errors issued when analyzing code
- -- are not compilation errors, and should not result in exiting with
- -- an error status. These errors are handled in the driver of the
- -- verification process instead.
-
- elsif GNATprove_Mode and not Frame_Condition_Mode then
- return False;
-
else
return Erroutc.Compilation_Errors;
end if;
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb (revision 206835)
+++ sem_ch4.adb (working copy)
@@ -3690,20 +3690,21 @@
Error_Msg_N ("?T?unused variable &", Loop_Id);
end if;
- -- Diagnose a possible misuse of the "some" existential quantifier. When
+ -- Diagnose a possible misuse of the SOME existential quantifier. When
-- we have a quantified expression of the form:
-- for some X => (if P then Q [else True])
- -- the if expression will not hold and render the quantified expression
- -- trivially True.
+ -- any value for X that makes P False results in the if expression being
+ -- trivially True, and so also results in the the quantified expression
+ -- being trivially True.
- if Formal_Extensions
+ if Warn_On_Suspicious_Contract
and then not All_Present (N)
and then Nkind (Cond) = N_If_Expression
and then No_Else_Or_Trivial_True (Cond)
then
- Error_Msg_N ("?suspicious expression", N);
+ Error_Msg_N ("?T?suspicious expression", N);
Error_Msg_N ("\\did you mean (for all X ='> (if P then Q))", N);
Error_Msg_N ("\\or (for some X ='> P and then Q) instead'?", N);
end if;
Index: opt.ads
===================================================================
--- opt.ads (revision 206827)
+++ opt.ads (working copy)
@@ -2001,17 +2001,6 @@
-- Modes for Formal Verification --
-----------------------------------
- Frame_Condition_Mode : Boolean := False;
- -- Specific mode to be used in combination with GNATprove_Mode. If set to
- -- true, ALI files containing the frame conditions (global effects) are
- -- generated, and analysis is *not* performed. If not true, analysis is
- -- performed. Set by debug flag -gnatd.G.
-
- Formal_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.
-
Global_SPARK_Mode : SPARK_Mode_Id := None;
-- The mode applicable to the whole compilation. The global mode can be set
-- in a configuration file such as gnat.adc.
@@ -2023,11 +2012,6 @@
-- that this is completely separate from the SPARK restriction defined in
-- GNAT to detect violations of a subset of SPARK 2005 rules.
- SPARK_Strict_Mode : Boolean := False;
- -- Interpret compiler permissions as strictly as possible. E.g. base ranges
- -- for integers are limited to the strict minimum with this option. Set by
- -- debug flag -gnatd.D.
-
private
-- The following type is used to save and restore settings of switches in
