7.2.7.4. Errors Related To Annotations

The following table shows all annotation types and the corresponding error messages.

Error Tag	Annotation	Description
incorrect-use-of-gnatprove	GNATprove	incorrect use of pragma Annotate (GNATprove, …)
incorrect-use-of-false_positive	False_Positive	incorrect use of pragma Annotate (GNATprove, False_Positive, …)
incorrect-use-of-intentional	Intentional	incorrect use of pragma Annotate (GNATprove, Intentional, …)
incorrect-use-of-at_end_borrow	At_End_Borrow	incorrect use of pragma Annotate (GNATprove, At_End_Borrow, …)
incorrect-use-of-automatic_instantiation	Automatic_Instantiation	incorrect use of pragma Annotate (GNATprove, Automatic_Instantiation, …)
incorrect-use-of-container_aggregates	Container_Aggregates	incorrect use of pragma Annotate (GNATprove, Container_Aggregates, …)
incorrect-use-of-handler	Handler	incorrect use of pragma Annotate (GNATprove, Handler, …)
incorrect-use-of-hide_info	Hide_Info	incorrect use of pragma Annotate (GNATprove, Hide_Info, …)
incorrect-use-of-higher_order_specialization	Higher_Order_Specialization	incorrect use of pragma Annotate (GNATprove, Higher_Order_Specialization, …)
incorrect-use-of-inline_for_proof	Inline_For_Proof	incorrect use of pragma Annotate (GNATprove, Inline_For_Proof, …)
incorrect-use-of-iterable_for_proof	Iterable_For_Proof	incorrect use of pragma Annotate (GNATprove, Iterable_For_Proof, …)
incorrect-use-of-logical_equal	Logical_Equal	incorrect use of pragma Annotate (GNATprove, Logical_Equal, …)
incorrect-use-of-mutable_in_parameters	Mutable_In_Parameters	incorrect use of pragma Annotate (GNATprove, Mutable_In_Parameters, …)
incorrect-use-of-no_bitwise_operations	No_Bitwise_Operations	incorrect use of pragma Annotate (GNATprove, No_Bitwise_Operations, …)
incorrect-use-of-no_wrap_around	No_Wrap_Around	incorrect use of pragma Annotate (GNATprove, No_Wrap_Around, …)
incorrect-use-of-ownership	Ownership	incorrect use of pragma Annotate (GNATprove, Ownership, …)
incorrect-use-of-predefined_equality	Predefined_Equality	incorrect use of pragma Annotate (GNATprove, Predefined_Equality, …)
incorrect-use-of-skip_flow_and_proof	Skip_Flow_And_Proof	incorrect use of pragma Annotate (GNATprove, Skip_Flow_And_Proof, …)
incorrect-use-of-skip_proof	Skip_Proof	incorrect use of pragma Annotate (GNATprove, Skip_Proof, …)
incorrect-use-of-unhide_info	Unhide_Info	incorrect use of pragma Annotate (GNATprove, Unhide_Info, …)
incorrect-use-of-always_return	Always_Return	incorrect use of pragma Annotate (GNATprove, Always_Return, …)
incorrect-use-of-external_axiomatization	External_Axiomatization	incorrect use of pragma Annotate (GNATprove, External_Axiomatization, …)
incorrect-use-of-might_not_return	Might_Not_Return	incorrect use of pragma Annotate (GNATprove, Might_Not_Return, …)
incorrect-use-of-terminating	Terminating	incorrect use of pragma Annotate (GNATprove, Terminating, …)