v0.4.1

WhyR (version 0.4.1)

Changes:

• Added the option for proving goals directly to the WhyR command-line. -p turns proving on, and -P controls the prover used.
• Other minor bugfixes.

v0.4.0

WhyR (version 0.4.0)

Changes:

• Added the set logic type. Corresponds to the Why3 notion of sets.
• Added assigns clauses and frame conditions:
  • Functions can now be specified with a set of memory locations that restrict how they can write to memory.
  • Store instructions are checked to ensure they do not write to memory not in the assigns clause.
  • Call instructions must have a callee that assigns a subset of the caller's assigns clause.
  • Allocations after the function begins ("fresh" memory) is always acceptable to write to.
  • In WhyR metadata and WAR, you can specify sets of pointers, as well as simple ranges of pointers.
• RTE assertions now have a specific label when generating Why3.
• Added an option to add vacuous assertions to goals, to detect contradiction in logic.

v0.3.0

WhyR (version 0.3.0)

Changes:

• Added support for the vector data type.
• Implemented modelling for the vector-specific instructions.

v0.2.1

WhyR (version 0.2.1)

Changes:

• Minor bugfixes.

v0.2.0

WhyR (version 0.2.0)

Changes:

• Added support for modelling struct types. They have most features implemented, except for the following:
  • No recursive or mutually recursive structs.
  • No opaque structs.
  • getelementptr works, but the memory model does not yet model what you get out of the resultant pointer.

v0.1.0

WhyR (version 0.1.0)

Changes:

• Initial release.