Skip to content

JKind v1.5.1

Compare
Choose a tag to compare
@agacek agacek released this 20 May 15:50
· 429 commits to master since this release

Features

  • Added enumeration types, for example
type state = enum { A, B, C, Error };
  • Added Turing machine example.
  • Users of the JKind API may now pass null to AST constructors
    in place of empty lists.
  • Added -xml_to_stdout flag which prints results as an xml file
    directly to the standard output.
  • Allow types and constants to reference previous types and constants
    rather than requring declaration before use.

Changes

  • We no longer support equations with no left-hand side. Instead, one
    must at least use () as the left-hand side when an equation assigns
    no variables.
  • Constants and enumeration literals must have globally unique names
    (e.g. cannot conflict with node variables).

Fixes

  • Added support for 'unknown' result from Z3.
  • Improved parsing performance.
  • Fixed bug in tuple handling.
  • Fixed unguarded pre check with respect to node calls.
  • Fixed integer overflow error with bounds checking for arrays.