SPAT v1.3.0

CHANGELOG

• No functional changes
• Full Alire integration
  • Once the crates are incorporated in the index, you should be able to build SPAT directly from an Alire environment.
• Switched to SI_Units v0.2.0

KNOWN ISSUES

• I noticed too late that this change also broke the CI builds, that means the files in .github/workflow are technically that one commit d922439 behind the officially signed tag.
  Oh well.

SPAT v1.2.1

No functional changes at all, just added the alire.toml, so I could use alr publish.

SPAT v1.2.0

Official SPAT v1.2.0 release.

Except for the version number, this release is identical as the v1.2.0-pre-0 pre-release.

It's about time to make it official.

SPAT v1.2.0-pre-0

This is a pre-release version. Handle with care.

CHANGELOG:

• Added steps to all output options (both summary and report modes) (#61, #64).
• To unify steps reporting, prover steps are now immediately scaled when reading (not only for the --suggest option) (#64).
• Added sorting options per step (maximum and minimum success) (#64).
• Sorting files (summary) output implemented for all possible sorting options (including the new ones) (#64).
• Table like output, which also better adapts to the actual items printed (#64).

SPAT v1.1.4

CHANGELOG:

• Fixed defect where the number of steps for Proof_Switches given by the --suggest option picked up the wrong entry and reported the wrong (i.e. too low) number of steps needed for successful proof (#60).

SPAT v1.1.3

CHANGELOG:

• Output of --suggest option now prefers body files (related to #55).

Known Issues:

• ´--suggest´ option still broken, especially in regards to the --steps option given to the prover (#60).

SPAT v1.1.2

CHANGELOG

• Fixes a major issue with the --suggest option and the required backwards mapping from .spark files to their respective source files.
  Especially prominent when generics were used as the generics were mentioned multiple times instead of their respective instantiations which were omitted from the output.
• Also, most likely attributed to my own stupidity, the fix for #54 (which was scheduled for the 1.2.0 release) was unintentionally merged back from the main branch into the fixes-1.1 branch.

SPAT v1.1.1

CHANGELOG:

• Major fix for --suggest option (#50):
  Found and fixed a defect that renders the whole output of previous versions bogus.
  Steps are now scaled according to the GNAT model.
  File names are reported only once for a single .spark file (with preference on spec files), to conform with how gnatprove handles compilation units.

SPAT v1.1.0

Official 1.1.0 release

CHANGELOG

• GNATStudio plug-in spat.py (#1, #43, #45, #46)
• --raw option for script use. (#1, #43, #45, #46)
• --details options now also accepts an optional level argument (1, 2, f) (#35, #47)

Known issues:

• Output of suggest option is completely broken (it was considered experimental, after all).

  Not only is it invalid (there is an extraneous quote character after the steps parameter. (#48, #49)), I found a major bug when inserting the data into the returned data structure that effectively means that random proof data will be inserted for random files, rendering the whole output useless. This will be fixed in the course of doing the fix for #50.

SPAT v1.0.0

Official 1.0.0 release.

CHANGELOG:

• Documentation fixes.