Development Log

  • SPARK Pro
    May 11th, 2017

    Added preconditions to standard numerical functions
    Preconditions have been added to functions from the standard numerical package Ada.Numerics.Generic_Elementary_Functions, in cases that may lead to Numerics.Argument_Error or Constraint_Error when called on actual parameters that are not suitable, like a negative input for Sqrt. This ensures that GNATprove generates corresponding precondition checks when such functions are called.