The following unsupported constructs are detected by GNATprove and reported through an error message:

* an abstract state marked as Part_Of a concurrent object,

* a reference to the "Access" attribute of an ownership type which does not occur directly inside an assignment statement, an object declaration, or a simple return statement,

* a conversion between access types with different designated types,

* a formal parameter of an access-to-subprogram type which is annotated with a type invariant,

* an access-to-subprogram type designating a protected subprogram,

* an access-to-subprogram type whose return type is annotated with a type invariant,

* an access-to-subprogram type designating a borrowing traversal function,

* an access-to-subprogram type designating a dispatching operation,

* an access-to-subprogram type designating a No_Return procedure,

* an access-to-subprogram type designating a subprogram annotated with Relaxed_Initialization,

* access attribute on a procedure which might raise exceptions,

* access to procedure which might exit the program,

* a reference to the "Address" attribute occuring within a subtype indication, a range constraint, or a quantified expression,

* an uninitialized allocator whose subtype indication has a type constraint,

* a conversion between array types if some matching index types are modular types of different sizes,

* a conversion between array types if some matching index types are not both signed or both modular,

* a pragma Assert_And_Cut occurring immediately within a sequence of statements containing a Loop_Invariant,

* a borrowing traversal function whose first formal parameter does not have an anonymous access-to-variable type,

* a borrowing traversal function marked as a volatile function,

* a reference to the "Class" attribute on a constrained type,

* a representation attribute on an object of classwide type,

* a subtype predicate on a classwide type,

* a raise expression occurring in a precondition, unless it is only used to change the reported error and can safely be interpreted as False,

* a type constraint on a classwide subtype declaration,

* a continue statement preceding loop-invariant,

* a type contract (subtype predicate, default initial condition, or type invariant) on a private type whose full view is another private type,

* a conversion between a fixed-point type and a floating-point type,

* a conversion between a fixed-point type and an integer type when the small of the fixed-point type is neither an integer nor the reciprocal of an integer,

* a conversion between a floating point type and a modular type of size 128,

* a conversion between fixed point types whose smalls are not "compatible" according to Ada RM G.2.3(21-24): the division of smalls is not an integer or the reciprocal of an integer,

* an object with subcomponents of an access-to-variable type annotated with an address clause whose value is the address of another object,

* delta aggregate with possible aliasing of component associations of an ownership type,

* interface derived from other interfaces,

* entry families,

* aspect "Exceptional_Cases" on dispatching operations,

* procedure which might propagate exceptions with parameters of mode "in out" or "out" subjected to ownership which might not be passed by reference,

* aspect "Exit_Cases" on dispatching operations,

* an extension aggregate whose ancestor part is a subtype mark,

* GNAT extension for case pattern matching,

* GNAT extension for embedded binary resources,

* instance of a generic unit declared in a package whose private part is hidden outside of this package,

* instance of a generic unit declared in a package containing a type with an invariant outside of this package,

* a goto statement occuring in a loop before the invariant which refers to a label occuring inside the loop but after the invariant,

* private type whose full view contains only subcomponents whose type is annotated with Relaxed_Initialization in a package whose private part is hidden for proof,

* a reference to the "Image" or "Img" attribute on a type or an object of a type which is not a scalar type,

* usage of incomplete type completed in package body outside of an access type declaration,

* a subprogram with dispatching result which is inherited, not overriden, by a private extension completed in a hidden private part,

* a subprogram with dispatching result which is inherited, not overriden, by a private extension completed in a private part with SPARK_Mode Off,

* a subprogram which is inherited, not overriden, from an ancestor declared in a hidden private part,

* a subprogram which is inherited, not overriden, from an ancestor declared in the private part of a package with SPARK_Mode Off,

* GNAT extension for interpolated string literals,

* container aggregates,

* an iterated component associations with an iterator specification ("for ... of") in an array aggregate,

* the use of an incomplete view of a type coming from a limited with,

* a loop invariant in a list of statements with an exception handler,

* a loop invariant in a list of statements with a finally section,

* a loop with an iterator filter in its parameter specification,

* an array type with more than 4 dimensions,

* a modular type with a modulus greater than 2 ** 128,

* a move operation occuring as part of  an allocator or a conversion to an access-to-constant type which does not occur directly inside an assignment statement, an object declaration, or a simple return statement,

* a function annotated as No_Return,

* a reference to a non-static attribute,

* a primitive operation which is inherited from several interfaces in a tagged derivation,

* a primitive operation which is implicitly inherited from several progenitor types in a tagged derivation, and for which two of these progenitors provide incompatible values for the SPARK  mode of the inherited subprogram,

* a primitive operation which is inherited both from the parent type and from an interface in a tagged derivation,

* an iterator specification on a multidimensional array,

* a delta aggregate on a multidimensional array,

* a null aggregate which is a subaggregate of a multidimensional  array  aggregate with multiple associations,

* a non-scalar object or an object with an address clause declared before the loop-invariant,

* a multiplication or division between a fixed-point and a floating-point value,

* a multiplication or division between different fixed-point types if the result is not in the "perfect result set" according to Ada RM G.2.3(21),

* a reference to the "Address" attribute in an address clause whose prefix has subcomponents of an access-to-variable type,

* a dispatching primitive subprogram overriding with class-wide precondition inherited from a potentially hidden ancestor,

* a dispatching primitive subprogram overriding declared for a private untagged type with no specific precondition and a class-wide precondition inherited from ancestor,

* a declaration of an object of an ownership type outside a block for declarations,

* a package declaration occurring in a loop before the loop invariant,

* a Potentially_Invalid aspect on a function associated to the aspect Iterable,

* a part of potentially invalid object with mutable discriminants,

* a potentially invalid object with a part subject to predicates,

* a potentially invalid object with a part whose full view is not in SPARK,

* a potentially invalid object with a part annotated with relaxed initialization,

* an access to a subprogram annotated with Potentially_Invalid,

* a private type whose full view is not in SPARK annotated with two subtype predicates, one on the full view and one on the private view,

* a private type declared in a package whose private part is hidden for proof annotated with two subtype predicates, one on the  full view and one on the private view,

* a call to a primitive operation of a tagged type T occurring in the default initial condition of T with the type instance as a parameter,

* aspect "Program_Exit" on dispatching operations,

* call which might exit the program and leave outputs mentioned in the exit postcondition of its enclosing subprogram in an inconsistent state,

* a call to a protected operation of a protected component inside a protected object,

* a call to a protected operation of the formal parameter of a subprogram,

* a protected entry annotated with a Refined_Post,

* an access-to-subprogram type used as a subcomponent of a type or an object annotated with Relaxed_Initialization,

* an object annotated with Relaxed_Initialization is part of an overlay,

* a type annotated with an invariant used as a subcomponent of a type or an object annotated with Relaxed_Initialization,

* a subtype with a discriminant constraint containing only subcomponents whose type is annotated with Relaxed_Initialization,

* a subprogram declaration occurring in a loop before the loop invariant,

* a call to a suspend operation on a suspension formal parameter,

* an occurrence of the target name @ in an assignment to an object of an anonymous access-to-variable type,

* an occurrence of the target name @ in an assignment to an object containing subcomponents of a named access-to-variable type,

* an access type designating an incomplete or private type with a subcomponent annotated with a type invariant,

* a protected type annotated with a type invariant,

* a tagged type with a subcomponent annotated with a type invariant,

* a tagged type annotated with a type invariant,

* a volatile object with asynchronous writers or readers and a type invariant,

* an uninitialized allocator inside an expression function,

* a reference to the "Alignment" attribute on a prefix which is not a type with an alignment clause,

* a reference to the "Size" attribute on a prefix which is not a standalone object, a formal parameter, a component, or a slice with no padding,

* a component of an unconstrained unchecked union type in a tagged extension.

