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.