GNATprove Limitations

Tool Limitations

  1. The Global contracts generated automatically by GNATprove for subprograms without an explicit one do not take into account indirect calls (through access-to-subprogram and dynamic binding) and indirect reads/writes to global variables (through access variables).

  2. A subset of all Ada conversions between array types is supported:

    • element types must be exactly the same
    • matching index types must either be both modular with a base type of the same size, or both non modular
  3. A subset of all Ada fixed-point types and fixed-point operations is supported:

    • fixed-point types must have a small that is a negative power of 2 or 10
    • multiplication and division between different fixed-point types and universal real are rejected
    • multiplication and division whose result type is not the same fixed-point type as its fixed-point argument(s) are rejected, except for the special case of dividing a fixed-point value by the small of its type (T’Small) to yield an integer result which is always exact.
    • conversions from fixed-point types to floating-point types are rejected

    These restrictions ensure that the result of fixed-point operations always belongs to the perfect result set as defined in Ada RM G.2.3.

  4. Multidimensional array types are supported up to 4 dimensions.

  5. Loop_Invariant and Loop_Variant pragmas must appear before any non-scalar object declaration.

  6. Inheriting the same subprogram from multiple interfaces is not supported.

  7. Formal object parameters of generics of an unconstrained record type with per-object constrained fields are badly supported by the tool and may result in crashes in some cases.

  8. Quantified expressions with an iterator over a multi dimensional array (for example for all Elem of Arr where Arr is a multi dimensional array) are not supported.

  9. Constrained subtypes of class-wide types and ‘Class attributes of constrained record types are not supported.

  10. Abstract states cannot be marked Part_Of a single concurrent object (see SPARK RM 9(3)). An error is raised instead in such cases.

  11. Classwide Global and Depends contracts as defined in SPARK RM 6.1.6 are not supported.

  12. Task attributes Identity and Storage_Size are not supported.

  13. Type_Invariant and Invariant aspects are not supported:

    • on private types declared in nested packages or child packages
    • on protected types
    • on tagged types
    • on components of tagged types if the tagged type is visble from inside the scope of the invariant bearing type.
  14. Calls to protected subprograms and protected entries whose prefix denotes a formal subprogram parameter are not supported. Similarly, suspension on suspension objects given as formal subprogram parameters is not supported.

Legality Rules

  1. SPARK Reference Manual rule 4.3(1), concerning use of the box symbol “<>” in aggregates, is not currently checked.
  2. The elaboration order rules described in the SPARK Reference Manual 7.7 are not currently checked.
  3. The rule concerned with asserting that all child packages which have state denoted as being Part_Of a more visible state abstraction are given as constituents in the refinement of the more visible state is not checked (SPARK Reference Manual rule 7.2.6(6)).
  4. GNATprove does not permit formal parameters to be mentioned in the input_list of an Initializes Aspect, contrary to SPARK Reference Manual 7.1.5(4). This limitation is only relevant for packages that are nested inside subprograms. This limitation is corrected in versions of the toolset based on GNAT Pro 7.2.2, GPL 2014, or later.
  5. The case of a state abstraction whose Part_Of aspect denotes a task or protected unit is not currently supported.
  6. The case of a Refined_Post specification for a (protected) entry is not currently supported.
  7. The use Ada.Synchronous_Barriers.Synchronous_Barrier type is not currently allowed in SPARK.
  8. Entry families are not currently allowed in SPARK.

Flow Analysis Limitations

  1. 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.
  2. The Depends and Refined_Depends aspect of a task unit T must explicitly mention T, which is an implicit parameter (despite SPARK Reference Manual rule 6.1.4 which says that a “T => T” specification is assumed).

Proof Limitations

  1. Postconditions of recursive functions called in contracts and assertion pragmas are not available, possibly leading to unproved checks. The current workaround is to use a non-recursive wrapper around those functions.

  2. Attribute ‘Valid is currently assumed to always return True.

  3. Values read from an external source are assumed to be valid values. Currently there is no model of invalidity or undefinedness. The onus is on the user to ensure that all values read from an external source are valid. The use of an invalid value invalidates any proofs associated with the value.

  4. 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.

  5. The ‘Update attribute on multidimensional unconstrained arrays is not yet fully supported in proof. Checks might be missing so currently an error is emitted for any use of the ‘Update attribute on multidimensional unconstrained arrays.

  6. The difference between the floating-point values +0 and -0 (as defined in IEEE-754 standard) is ignored in proof. This is correct for all programs that do not exploit the difference in bit-pattern between +0 and -0. For example, the following specially crafted program is proved by GNATprove but fails at run time due to a division by zero, because function Magic exploits the difference of bit-pattern between +0 and -0 by using Unchecked_Conversion to return a different integer value for arguments +0 and -0.

    pragma SPARK_Mode;
    
    with Ada.Unchecked_Conversion;
    
    procedure Zero_And_Unchecked is
       procedure Crash (A, B : Float) is
          function Magic is new Ada.Unchecked_Conversion (Float, Integer);
          X : Integer;
       begin
          if A = B then
             if Magic (B) /= 0 then
                X := 100 / Magic (A);
             end if;
          end if;
       end Crash;
    
       type UInt32 is mod 2 ** 32;
       function Convert is new Ada.Unchecked_Conversion (UInt32, Float);
    
       Zero_Plus : constant Float := Convert (16#0000_0000#);
       Zero_Neg  : constant Float := Convert (16#8000_0000#);
    begin
       Crash (Zero_Plus, Zero_Neg);
    end Zero_And_Unchecked;
    
  7. GNATprove does not follow the value of tags for tagged objects. As a consequence, tag checks are currently unprovable in most cases.

  8. 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.

  9. Preconditions on arithmetic and conversion operators (including Time_Of) in Ada.Execution_Time and Ada.Real_Time packages described in SPARK Reference Manual 9.19 are not yet implemented.

  10. Preconditions on arithmetic and conversion operators (including Time_Of) in Ada.Calendar package are not yet implemented.