Skip to content

0.7.0

Choose a tag to compare

@Lucccyo Lucccyo released this 04 Jul 12:11
163def8

This new release introduces the new Ortac/Wrapper plugin, which includes extended support for projection functions, model-based specifications, and old operator support.
It also fixes some bugs for both the Ortac/Wrapper and Ortac/QCheck-STM plugins.

New introduction of the Ortac/Wrapper plugin

  • Support for old operator
    The Ortac/Wrapper plugin now supports the old operator in post-conditions,
    checking post-conditions mentionning pre-states.
    #297

  • Model-based specification support with projection function

    • Ortac/Wrapper now handles Gospel models in specifications. Generation is skipped if the required projection is missing, avoiding incorrect code.
      #305, #313, #327, #332, #331, #324
  • Improved generated output
    Generated files includes a header comment indicating that they were produced by Ortac.
    #322

  • Automatic Dune file generation
    The Ortac/Dune plugin automatically generates dune files for Ortac/Wrapper plugin.
    #314, #335

Tests

  • Test reorganization
    Tests for the Ortac/Wrapper plugin have been split into separate files to improve maintainability.
    #306

  • Extended test coverage
    Several additional tests were added to better cover the Ortac/Wrapper plugin features.
    #299

Bug Fixes

  • Ortac/QCheck-STM

    • Fixed incorrect behavior in the next-state computation for functions specialized for ints.
      #326
    • Disabled warning 34 (unused open) in generated code to reduce noise.
      #307
  • Ortac/Wrapper
    Fixed incorrect error type reporting for violated pre-conditions and post-conditions in generated tests.
    #295