7.2.6.3. Miscellaneous warnings reported by GNATprove

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

Message Kind	Explanation
address to access conversion	call to conversion function is assumed to return a valid access designating a valid value
volatile and atomic status of aliases	aliased objects should both be volatile or non-volatile, and both be atomic or non-atomic
volatile properties of aliases	aliased objects should have the same volatile properties
attribute Valid always True	attribute Valid is assumed to return True
initialization of alias	initialization of object is assumed to have no effects on other non-volatile objects
function Is_Valid always return True	function Is_Valid is assumed to return True
procedure not terminating normally nor abnormally	procedure which does not return normally nor raises an exception cannot always terminate
no check message justified	no check message justified by this pragma
proved check message justified	only proved check messages justified by this pragma
Terminating deprecated	Terminating, Always_Return, and Might_Not_Return annotations are ignored
External Axiomatizations not supported	External Axiomatizations are not supported anymore, ignored
pragma ignored	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
unreferenced function	analyzing unreferenced function
unreferenced procedure	analyzing unreferenced procedure
useless Relaxed_Initialization aspect on function result	function result annotated with Relaxed_Initialization cannot be partially initialized
useless Relaxed_Initialization aspect on object	object annotated with Relaxed_Initialization cannot be partially initialized
variant not recursive	no recursive call visible on subprogram with Subprogram_Variant

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

Message Kind	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
imprecisely supported 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 table shows warnings reported by GNATprove when using switch --pedantic.

Message Kind	Explanation
string 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