GNATprove Limitations
Tool Limitations Leading to an Error Message
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 declared in a loop 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 component of an unconstrained unchecked union type in a tagged extension.
Other Tool Limitations
The following constructs are incompletely supported. They can be used safely but might lead to unexpected behavior. Warnings for these constructs can be enabled individually using the -W switch and the tag between parentheses, or collectively using the --info switch.
If all components of a given type are annotated with Relaxed_Initialization, the containing type is treated as if it had the same annotation (component-relaxed-init),
The full view of an incomplete type deferred to the body of a withed unit might be visible by GNATprove (full-view-visible).
Flow Limitations
The following constructs are imprecisely supported in flow analysis. They can be used safely but might lead to unprovable checks. Warnings can be emitted by GNATprove if the --info switch is used:
Aliasing checks might be spurious for actual parameters that are array components,
Global generation might wrongly classify an Output item as an In_Out for subprograms that call other subprograms with no Global contract,
Initialization of arrays inside FOR loops is only recognized when assignments to array element are directly indexed by the loopparameter,
Initialization of multi-dimensional array inside FOR loops is only recognized when array bounds are static,
Assignments to record objects might cause spurious data dependencies in some components of the assigned object.
Flow Analysis Limitations
These limitations in the flow analysis part of GNATprove may result in a less precise (but sound) analysis.
Flow dependencies caused by record assignments is not captured with perfect accuracy. This means that the value of one field might incorrectly be considered to participate in the derivation of another field that it does not really participate in.
Initialization of multi-dimensional arrays with nested FOR loops can be only detected if the array bounds are given by static expressions. A possible solution is to use Aspect Relaxed_Initialization and Ghost Attribute Initialized instead in such a case and to prove that only initialized data is read.
Proof Limitations
The following constructs are imprecisely supported in proof. They can be used safely but might lead to unexpected behavior. Warnings for these constructs can be enabled individually using the -W switch and the tag between parentheses, or collectively using the --info switch.
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 (contracts-recursive),
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 (dic-ignored),
The adress of objects is not precisely known if it is not supplied through an address clause (imprecise-address),
The alignment of an object might not be known for proof if it is not supplied through an attribute definition clause (imprecise-align),
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-call),
the value of attribute Component_Size might not be known for proof if it is not supplied through an attribute definition clause (imprecise-component-size),
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-record-component-attribute),
The attributes Size, Object_Size or Value_Size might not be handled precisely, nothing will be known about their evaluation (imprecise-size),
Unchecked conversion might not be handled precisely by SPARK, nothing will be known about their result (imprecise-unchecked-conversion),
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-value),
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 (imprecise-image),
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 (constants-in-loops),
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 (no-reclamation-function),
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 (numeric-variant),
The tool enforces that mutable discriminants of standalone objects and parameters with relaxed initialization are always initialized (relaxed-mutable-discriminants),
A type with predefined map aggregates doesn’t have a Length function; the length of aggregates will not be known for this type (map-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 (set-length-aggregates).