Development Log

  • SPARK Pro
    Nov 22nd, 2016

    Remove trivial checks on float-to-int conversions
    Range checks on float-to-int conversions that can be proved to be always passing by trivial interval analysis of the types of subexpressions are not emitted anymore. This improves provability of programs where such conversions are used, as automatic provers sometimes had difficulty proving range checks on such conversions.