+2014-01-20 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_attr.adb: Code and comments cleanup.
+
+2014-01-20 Yannick Moy <moy@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.
+
2014-01-20 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Analyze_Pragma): Ensure that
-- 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
-- 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
-- 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.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.F Sets GNATprove_Mode to True. This allows debugging the frontend in
+ -- the special mode used by GNATprove.
-- d.I Do not ignore enum representation clauses in CodePeer mode.
-- The default of ignoring representation clauses for enumeration
-- 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.
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;
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
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.
Implementation Defined Pragmas
* Pragma Abort_Defer::
+* Pragma Abstract_State::
* Pragma Ada_83::
* Pragma Ada_95::
* Pragma Ada_05::
* Pragma Debug::
* Pragma Debug_Policy::
* Pragma Default_Storage_Pool::
+* Pragma Depends::
* Pragma Detect_Blocking::
* Pragma Disable_Atomic_Synchronization::
* Pragma Dispatching_Domain::
* Pragma Favor_Top_Level::
* Pragma Finalize_Storage_Only::
* Pragma Float_Representation::
+* Pragma Global::
* Pragma Ident::
* Pragma Implementation_Defined::
* Pragma Implemented::
* 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::
* Pragma Pure_12::
* Pragma Pure_Function::
* Pragma Ravenscar::
+* Pragma Refined_State::
* Pragma Relative_Deadline::
* Pragma Remote_Access_Type::
* Pragma Restricted_Run_Time::
* Aspect Abstract_State::
* Aspect Ada_2005::
* Aspect Ada_2012::
-* Pragma Allow_Integer_Address::
* Aspect Compiler_Unit::
* Aspect Contract_Cases::
* Aspect Depends::
* Aspect Dimension_System::
* Aspect Favor_Top_Level::
* Aspect Global::
+* Aspect Initial_Condition::
+* Aspect Initializes::
* Aspect Inline_Always::
* Aspect Invariant::
* Aspect Object_Size::
* Aspect Pure_05::
* Aspect Pure_12::
* Aspect Pure_Function::
+* Aspect Refined_State::
* Aspect Remote_Access_Type::
* Aspect Scalar_Storage_Order::
* Aspect Shared::
@menu
* Pragma Abort_Defer::
+* Pragma Abstract_State::
* Pragma Ada_83::
* Pragma Ada_95::
* Pragma Ada_05::
* Pragma Debug::
* Pragma Debug_Policy::
* Pragma Default_Storage_Pool::
+* Pragma Depends::
* Pragma Detect_Blocking::
* Pragma Disable_Atomic_Synchronization::
* Pragma Dispatching_Domain::
* Pragma Favor_Top_Level::
* Pragma Finalize_Storage_Only::
* Pragma Float_Representation::
+* Pragma Global::
* Pragma Ident::
* Pragma Implementation_Defined::
* Pragma Implemented::
* 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::
* Pragma Pure_12::
* Pragma Pure_Function::
* Pragma Ravenscar::
+* Pragma Refined_State::
* Pragma Relative_Deadline::
* Pragma Remote_Access_Type::
* Pragma Restricted_Run_Time::
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
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
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
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
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
@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
* Aspect Dimension_System::
* Aspect Favor_Top_Level::
* Aspect Global::
+* Aspect Initial_Condition::
+* Aspect Initializes::
* Aspect Inline_Always::
* Aspect Invariant::
* Aspect Lock_Free::
* Aspect Pure_05::
* Aspect Pure_12::
* Aspect Pure_Function::
+* Aspect Refined_State::
* Aspect Remote_Access_Type::
* Aspect Scalar_Storage_Order::
* Aspect Shared::
@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
@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
-- 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.
-- 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
return;
-- For compatibility with Declib code, treat all prefixes as
- -- legal, including non-discriminated types.
+ -- legal, including non-discriminated types. This is because
+ -- DECLIB uses the obsolescent interpretation of the attribute,
+ -- and applies it to types as well as to objects, while the
+ -- current definition applies to objects of a discriminated type.
- -- ??? this non-conforming language extension needs documenting
- -- ??? anyway it should not depend on Extend_System!
-
- elsif Present (System_Extend_Unit) then
+ elsif OpenVMS_On_Target then
return;
end if;
end if;
-- 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;
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.
-
- 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_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
Set_Size_Info (T, (Implicit_Base));
Set_First_Rep_Item (T, First_Rep_Item (Implicit_Base));
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;
-- 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;
-- 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);
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
-- 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
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
Ensure_Aggregate_Form (Arg1);
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
Ensure_Aggregate_Form (Arg1);
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
Ensure_Aggregate_Form (Arg1);
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
-- Ensure the proper placement of the pragma. Initial_Condition
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
Ensure_Aggregate_Form (Arg1);
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
-- Ensure the proper placement of the pragma. Refined states must
projects / platform / upstream / gcc.git / commitdiff