Changes in flocq 3.4.1:

• ensured compatibility from Coq 8.7 to 8.14

Changes in flocq 3.4.2:

• restored compatibility with Coq 8.11

Changes in frama-c 23.0 Vanadium:

• See https://frama-c.com/html/changelog.html

Changes in why3 1.4.0, where :x: marks a backwards incompatibility

• WhyML

  • sub-namespaces are now allowed in for each loops; see Section 7.4.7 of the manual
  • function literals are now supported; see Sections 7.3.2 and 7.4.9 of the manual

• Standard library

  • added lemma permut_sub_trans to array.ArrayPermut
  • added function inter (intersection) to bag.Bag
  • added a new theory option.Map
  • added a precondition to string.OCaml.([])
  • added functions set, init, sub to mach.array.ArrayInt63
  • moved OCaml exception Invalid_argument to ocaml.Exceptions :x:
  • added function length in mach.c.String
  • added functions sdiv and srem to bv
  • added signed operations to mach.bv
  • added missing module for double-precision floats to mach.floats

• Tools

  • command-line options now follow the getopt standard; in particular, long options start with -- :x:
  • binaries why3config, why3prove, etc, no longer exist; they are now plugins that can be loaded only using the main why3 binary, e.g., why3 config :x:
  • why3 config now uses subcommands instead of options; in particular, prover detection is performed using why3 config detect and manual prover addition is performed using why3 config add-prover; see Section 6.1 of the manual :x:
  • why3 execute now provides runtime assertion checking; see Section 6.8.1 of the manual
  • runtime assertion checking is also used to validate counterexamples in why3 prove
  • loop invariants can now be inferred automatically; see Section 8.5 of the manual
  • JSON output of counterexamples was modified :x:

• IDE

  • native keyboard modifiers are now used on macOS
  • why3 ide in the Docker image can now be used through a web browser instead of an X server; see Section 5.1.2 of the manual

• Input Formats

  • a new front-end named MLCFG was added; it supports unstructured program codes, including goto statements; see Section 9.3 of the manual
  • translation of <> and not have been fixed for micro-C and Python

• Extraction

  • allowed transitive inclusion (export) of interfaces and preludes
  • added remove module for drivers to exclude modules
  • added C extraction of strings
  • improved handling of C header files
  • added support of blacklist to C extraction
  • fixed extraction of partially applied functions
  • fixed OCaml extraction of nested tuples
  • fixed OCaml extraction of OneTime integers

• Web interface TryWhy3

  • ?lang=foo can now be used to select an input format other than WhyML; the input format can also be changed dynamically using a combobox
  • ?code=foo can now be used to fill the editor with some code; the encoded string can be retrieved by clicking the "Copy URL" button
  • examples are no longer embedded; only files mentioned in examples/index.txt are considered :x:
  • Alt-Ergo workers can now be stopped without losing the session

• Provers

  • support for PVS 7.1 (released Apr 30, 2020)
  • support for Z3 4.8.7 (released Nov 19, 2019)
  • support for Z3 4.8.8 (released May 9, 2020)
  • support for Z3 4.8.9 (released Sep 11, 2020)
  • support for Z3 4.8.10 (released Jan 20, 2021)
  • support for AltErgo 2.3.3 (released Aug 19, 2020)
  • support for AltErgo 2.4.0 (released Jan 22, 2021)
  • support for Coq 8.13.0 (released Jan 7, 2021)
  • support for CVC4 1.8 (released Jun 19, 2020)

• Documentation

  • Why3 modes for editors (Section 5.3)
  • Why3-specific configuration for shells (Section 5.4)
  • detailed explanations on semantics of various WhyML statements (Section 7.4)
  • detailed explanations on WhyML module system (Section 7.5)
  • explanations on how users can customize drivers (Section 12.5)

• API

  • helpers were added to ease production of parse trees; see Section 4.9 of the manual
  • generation of counterexamples was changed; see Section 4.10 of the manual :x:

• Additional bug fixes

  • fixed why3 prove when called on a DIMACS file
  • improved detection of out-of-range values in why3 execute
  • fixed micro-Python parser when there is no newline at end of file
  • fixed SMT translation of negative floating-point literals
  • fixed set of reserved symbols for SMT solvers
  • restored hypothesis_selection transformation
  • fixed unsoundness of transformations case and destruct in presence of polymorphic formulas

The gappalib-coq build is a simple rebuild due to the flocq update.