Skip to content

0.9

Latest
Latest
Compare
Choose a tag to compare
@Gbury Gbury released this 04 Jul 16:38
· 30 commits to master since this release
v0.9
d9f5abb

CHANGES:

Doc

  • Add examples in the doc and tuto for type-checking (including
    a minimal working example in the tutorial).

UI

  • Make the unknown logic fatal by default, and simply enabled
    in non-strict mode (PR#158)
  • Add the --check-flow option to checks coherence of sequences
    of statements (PR#135)
  • Ensure stability of error codes for the dolmen binary

Parsing

  • Add attrs fields for all declarations and definition types,
    and correctly attach predicate attribute to individual definitions
    (PR#130)
  • Restore support for toplevel "and" in non-recursive predicate/function
    definitions in Alt-Ergo syntax (PR #147, fixes issue #144)
  • Add support for hexadecimal floats in Alt-Ergo syntax (PR #148, fixes
    issue #145)
  • Add local goals to the Prove statement (PR#140)
  • Add a check-sat/prove-sat statement to ae's language (PR#140)

Typing

  • Ignore arithmetic restrictions when typing model values. This
    particularly affects difference logic (PR#141)
  • Rename theory-specific configuration to config (instead of
    arith, arrays, etc..) (PR#142)
  • Add printing function for logics (PR#142)
  • Attach type definitions to type-defs (PR#157)
  • Add a proper reason for reserved builtins (PR#155)
  • Add bitvector builtins for alt-ergo's language (PR#136)

Loop

  • Add possibility for users of the loop library to choose the
    exit/return code for a Code.t (PR#134)
  • Add the Flow module for flow checking (PR#135)
  • Add the check function in typer.ml/typer_intf.ml
  • Add update and update_opt in State (PR#156)
  • Print type definitions in the printer of typed statements (PR#157)
  • Prelude statements have been removed and replaced with prelude files (PR#160)
  • Typer.additional_builtins is now a State.key and takes the current state
    and language as arguments (PR#160)

Model

  • Fix bug in bitvector implementation: negative inputs to bvsmod
    would raise an internal error (PR#138)
  • Remove the "error" keyword and statement from smtlib2
    response (model) files (PR#139)
  • Correctly compare abstract array values (PR#143)
  • Accept extensions of functions/symbols with only partially defined
    semantics, for e.g. fp.to_ubv, div, etc.. (PR#151)
  • Error out on incremental problems (PR#169)
Assets 9