7.2.7.3. Miscellaneous warnings reported by GNATprove

The following table shows default warnings reported by GNATprove outside of flow analysis and proof.

Warning Tag	Explanation
address-to-access-conversion	call to conversion function is assumed to return a valid access designating a valid value
alias-volatile-atomic-mismatch	aliased objects should both be volatile or non-volatile, and both be atomic or non-atomic
alias-volatile-prop-mismatch	aliased objects should have the same volatile properties
attribute-valid-always-true	attribute Valid or Valid_Scalars is assumed to return True
auto-lemma-calls	the automatically instantiated lemma contains calls which cannot be arbitrarily specialized
auto-lemma-different	the automatically instantiated lemma contains calls to its associated function with different specializations
auto-lemma-higher-order	the automatically instantiated lemma is not annotated with Higher_Order_Specialization
auto-lemma-specializable	the automatically instantiated lemma does not contain any specializable calls to its associated function
initialization-to-alias	initialization of object is assumed to have no effects on other non-volatile objects
is-valid-returns-true	function Is_Valid is assumed to return True
generic-not-analyzed	GNATprove doesn’t analyze generics, only instances
no-possible-termination	procedure which does not return normally nor raises an exception cannot always terminate
potentially-invalid-read	invalid data might be read in the contract of a subprogram without an analyzed body; the fact that the read data is valid is not checked by SPARK
no-check-message-justified	no check message justified by this pragma
proved-check-justified	only proved check messages justified by this pragma
deprecated-terminating	Terminating, Always_Return, and Might_Not_Return annotations are ignored
deprecated-external-axiomatization	External Axiomatizations are not supported anymore, ignored
ignored-pragma	pragma is ignored (it is not yet supported)
overflow-mode-ignored	pragma Overflow_Mode in code is ignored
precondition-statically-false	precondition is statically False
restriction-ignored	restriction is ignored (it is not yet supported)
unreferenced-function	analyzing unreferenced function
unreferenced-procedure	analyzing unreferenced procedure
useless-potentially-invalid-func-result	function result annotated with Potentially_Invalid cannot have invalid values
useless-potentially-invalid-object	object annotated with Potentially_Invalid cannot have invalid values
useless-relaxed-init-func-result	function result annotated with Relaxed_Initialization cannot be partially initialized
useless-relaxed-init-object	object annotated with Relaxed_Initialization cannot be partially initialized
variant-no-recursion	no recursive call visible on subprogram with Subprogram_Variant

The following table shows warnings guaranteed to be reported by GNATprove.

Warning Tag	Explanation
assumed-always-terminates	no Always_Terminates aspect available for subprogram, subprogram is assumed to always terminate
assumed-global-null	no Global contract available for subprogram, null is assumed
imprecise-address-specification	object with an imprecisely supported address specification: non-atomic objects should not be accessed concurrently, volatile properties should be correct, indirect writes to object to and through potential aliases are ignored, and reads should be valid

The following warnings are disabled by default, and can be enabled collectively using switch --pedantic, or individually using switch -W.

Warning Tag	Explanation
image-attribute-length	string attribute has an implementation-defined length
operator-reassociation	possible operator reassociation due to missing parentheses
representation-attribute-value	representation attribute has an implementation-defined value

The following warnings are disabled by default, and can be enabled collectively using switch --info, or individually using switch -W.

Warning Tag	Explanation
component-relaxed-init	If all components of a given type are annotated with Relaxed_Initialization, the containing type is treated as if it had the same annotation
full-view-visible	The full view of an incomplete type deferred to the body of a withed unit might be visible by GNATprove
alias-array	Aliasing checks might be spurious for actual parameters that are array components
imprecise-global-generation	Global generation might wrongly classify an Output item as an In_Out for subprograms that call other subprograms with no Global contract
array-initialization	Initialization of arrays inside FOR loops is only recognized when assignments to array element are directly indexed by the loopparameter
multidimensional-array-init	Initialization of multi-dimensional array inside FOR loops is only recognized when array bounds are static
tagged-assignment	Assignments to record objects might cause spurious data dependencies in some components of the assigned object
contracts-recursive	Explicit and implicit postconditions of a recursive subprogram cannot be used on (mutually) recursive calls occurring inside assertions and contracts, but will still be available in regular code
dic-ignored	The Default_Initial_Condition of a type won’t be assumed on subcomponents initialized by default inside assertions and contracts, but will still be available in regular code
imprecise-address	The adress of objects is not precisely known if it is not supplied through an address clause
imprecise-align	The alignment of an object might not be known for proof if it is not supplied through an attribute definition clause
imprecise-call	The behavior of a call might not be known by SPARK and handled in an imprecise way; its precondition might be impossible to prove and nothing will be known about its result
imprecise-component-size	the value of attribute Component_Size might not be known for proof if it is not supplied through an attribute definition clause
imprecise-record-component-attribute	the value of attributes First_Bit, Last_Bit, and Position on record components are handled in an imprecise way if the record does not have a record representation clause
imprecise-size	The attributes Size, Object_Size or Value_Size might not be handled precisely, nothing will be known about their evaluation
imprecise-unchecked-conversion	Unchecked conversion might not be handled precisely by SPARK, nothing will be known about their result
imprecise-value	References to the attribute Value are handled in an imprecise way; its precondition is impossible to prove and nothing will be known about the evaluation of the attribute reference
imprecise-image	References to the attributes Image and Img are handled in an imprecise way; nothing will be known about the evaluation of the attribute reference apart from a bound on its length
constants-in-loops	The initial value of constants declared before the loop invariant is not visible after the invariant; it shall be restated in the invariant if necessary
no-reclamation-function	No reclamation function or reclaimed value was found for an ownership type, which may make it impossible to prove that values of this type are reclaimed
numeric-variant	For recursive expression functions with a numeric (not structural) Subprogram_Variant, the definition of the expression function might not be available for recursive calls occurring inside assertions and contracts, but will still be available in regular code
relaxed-mutable-discriminants	The tool enforces that mutable discriminants of standalone objects and parameters with relaxed initialization are always initialized
map-length-aggregates	A type with predefined map aggregates doesn’t have a Length function; the length of aggregates will not be known for this type
set-length-aggregates	A type with predefined set aggregates doesn’t have a Length function; the length of aggregates will not be known for this type
predefined-equality-null	A type is annotated with Only_Null as value for the Predefined_Equality annotation, but no constant annotated with Null_Value is found; this will result in all calls to the predefined equality being rejected
init-cond-ignored	The initial condition of a withed package might be ignored if it is not known to be true, due to elaboration order
unit-not-spark	A unit whose analysis has been requested on the command-line is not annotated with SPARK_Mode Pragma

The following info messages are issued by default, and can be disabled using switch -A.

Warning Tag	Explanation
info-unrolling-inlining	These messages are issued when the tool is unrolling loops or inlining subprograms, or unable to do so