Development Log

  • SPARK Pro
    Mar 31st, 2016

    Always generate axiom for expression function
    Previously, no axiom was generated for an expression function in a part of code with no explicit SPARK_Mode, which prevented proofs of client code that relied on the implicit postcondition of the expression function. Now, an axiom is generated in such a case.