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,
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 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,
entry families,
aspect “Exceptional_Cases” on dispatching operations,
procedures with exceptional contracts and parameters of mode “in out” or “out” subjected to ownership which might not be passed by reference,
an extension aggregate whose ancestor part is a subtype mark,
a goto statement occuring in a loop before the invariant which refers to a label occuring inside the loop but after the invariant,
a reference to the “Image” or “Img” attribute on a type or an object of a type which is not a scalar type,
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 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 a conversion to an access-to-constant type,
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 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 package declaration occurring in a loop before the loop invariant,
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 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,
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 concurrent type used as a subcomponent of a type or an object annotated with Relaxed_Initialization,
a type annotated with an invariant used as a subcomponent of a type or an object annotated with Relaxed_Initialization,
a variable annotated both with Relaxed_Initialization and as Part_Of a concurrent object,
a protected component annotated with Relaxed_Initialization,
a tagged type 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 private type declared in a nested package annotated with a type invariant,
a private type declared in a private child package 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 generation of Global contracts by GNATprove has limitations. When this capability is used in a certification context, the generated contracts should be verified by the user. In particular:
The Global contracts generated automatically by GNATprove for subprograms without an explicit one, whose body is not in SPARK, do not take into account indirect calls (through access-to-subprogram and dynamic binding) and indirect reads/writes to global variables (through access variables). See Coarse Generation for non-SPARK Subprograms.
Some features defined in the reference manual have not been implemented in the tool. It is the case of:
classwide Global and Depends contracts as defined in SPARK RM 6.1.6, and
the use of Ada.Synchronous_Barriers.Synchronous_Barrier type.
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
These limitations in the proof part of GNATprove may result in a less precise (but sound) analysis.
The following attributes are not yet supported in proof: Adjacent, Aft, Bit_Order, Body_Version, Copy_Sign, Definite, Denorm, First_Valid, Fore, Last_Valid, Machine, all Machine_* attributes, Model, all Model_* attributes, Partition_Id, Remainder, Round, Safe_First, Safe_Last, Scale, Scaling, Small, Unbiased_Rounding, Version, Wide_Image, Wide_Value, Wide_Width, Wide_Wide_Image, Wide_Wide_Value, Wide_Wide_Width, Width.
The attributes First_Bit, Last_Bit and Position are supported but if there is no record representation clause then we assume that their value is nonnegative.
Constants declared in loops before the loop invariant are handled as variables by the tool. This means in particular that any information about their values needed after the loop invariant must be stated explicitly in the loop invariant.