The following Fedora 27 Security updates need testing: Age URL 17 https://bodhi.fedoraproject.org/updates/FEDORA-2017-d270e932a3 nagios-4.3.4-3.fc27 7 https://bodhi.fedoraproject.org/updates/FEDORA-2017-ff17e19bae weechat-1.9.1-1.fc27 6 https://bodhi.fedoraproject.org/updates/FEDORA-2017-d05a50dce6 mingw-poppler-0.57.0-2.fc27 2 https://bodhi.fedoraproject.org/updates/FEDORA-2017-7106a157f5 dnsmasq-2.77-9.fc27 2 https://bodhi.fedoraproject.org/updates/FEDORA-2017-523f6a613d botan-1.10.17-1.fc27 2 https://bodhi.fedoraproject.org/updates/FEDORA-2017-b4329d6ee5 xen-4.9.0-11.fc27 2 https://bodhi.fedoraproject.org/updates/FEDORA-2017-cf6bb19709 recode-3.6-46.fc27 2 https://bodhi.fedoraproject.org/updates/FEDORA-2017-e8179c06fd curl-7.55.1-6.fc27 2 https://bodhi.fedoraproject.org/updates/FEDORA-2017-b2c714515b tor-0.3.1.7-1.fc27 2 https://bodhi.fedoraproject.org/updates/FEDORA-2017-67f13dd1e1 mingw-taglib-1.11.1-4.fc27 0 https://bodhi.fedoraproject.org/updates/FEDORA-2017-79b7fd1b4d check-mk-1.2.8p26-1.fc27 0 https://bodhi.fedoraproject.org/updates/FEDORA-2017-f4fc897e8f golang-1.9.1-1.fc27 0 https://bodhi.fedoraproject.org/updates/FEDORA-2017-6d59576860 poppler-0.57.0-3.fc27 The following builds have been pushed to Fedora 27 updates-testing appstream-generator-0.6.7-1.fc27 erfa-1.4.0-1.fc27 flocq-2.6.0-1.fc27 frama-c-15.0-3.fc27 gappalib-coq-1.3.2-10.fc27 glibc-2.26-12.fc27 golang-github-asaskevich-govalidator-7-1.fc27 libmatroska-1.4.8-1.fc27 libnitrokey-3.0-0.2.20171007git.fa871ec.fc27 mingw-binutils-2.29.1-1.fc27 mingw-openjpeg2-2.3.0-1.fc27 mkvtoolnix-16.0.0-1.fc27 openjpeg2-2.3.0-1.fc27 poppler-0.57.0-3.fc27 prelude-lml-4.0.0-1.fc27 purple-libsteam-1.6.1-17.20170929gitab6d446.fc27 python-astropy-2.0.2-1.fc27 python-astropy-helpers-2.0.1-1.fc27 python-healpy-1.11.0-1.fc27 qcad-3.18.1.0-2.fc27 qt-creator-4.4.1-1.fc27 qtractor-0.8.4-1.fc27 radicale-2.1.8-2.fc27 snapd-2.28.1-1.fc27 snapd-glib-1.23-1.fc27 vid.stab-1.1-3.20170830gitafc8ea9.fc27 why-2.39-2.fc27 why3-0.88.0-1.fc27 Details about builds: ================================================================================ appstream-generator-0.6.7-1.fc27 (FEDORA-2017-5b15c20527) Fast AppStream metadata generator -------------------------------------------------------------------------------- Update Information: Initial packaging for Fedora (#1498468) -------------------------------------------------------------------------------- References: [ 1 ] Bug #1498468 - None https://bugzilla.redhat.com/show_bug.cgi?id=1498468 -------------------------------------------------------------------------------- ================================================================================ erfa-1.4.0-1.fc27 (FEDORA-2017-5e692a4b1c) Essential Routines for Fundamental Astronomy -------------------------------------------------------------------------------- Update Information: Updated erfa and astropy to latest upstream releases. -------------------------------------------------------------------------------- References: [ 1 ] Bug #1433636 - python-astropy-helpers-2.0.1 is available https://bugzilla.redhat.com/show_bug.cgi?id=1433636 [ 2 ] Bug #1465690 - python-astropy-2.0.2 is available https://bugzilla.redhat.com/show_bug.cgi?id=1465690 -------------------------------------------------------------------------------- ================================================================================ flocq-2.6.0-1.fc27 (FEDORA-2017-93d7fb97b0) Formalization of floating point numbers for Coq -------------------------------------------------------------------------------- Update Information: Changes in flocq 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Changes in why3 0.88.0: - two new forms of type declarations: integer range types and floating-point types. To denote constants in such types, integer constants and real constants can be cast to such types. This support is exploited in drivers for provers that support bitvector theories (CVC4, Z3) and floating-point theory (Z3). More details in the manual, section 7.2.4 "Theories". - a quote character (') inside an identifier must either be at the end, or be followed by either a digit, the underscore character (_) or another quote. Identifiers with a quote followed by a letter are reserved. - new theory ieee_float formalizing floating-point arithmetic, compliant to IEEE-754, mapped to SMT-LIB FP theory. - proof strategies: why3 config now generates default proof strategies using the installed provers. These are available under name "Auto level 0", "Auto level 1", and "Auto level 2" in why3 ide. More details in the manual, section 10.6 "Proof Strategies". - counterexamples: better support for array values, support for floating-point values, support for Z3 in addition to CVC4. More details in the manual, section 6.3.5 "Displaying Counterexamples". - support for Isabelle 2017 - discarded support for Isabelle 2016 (2016-1 still supported) - support for Coq 8.6.1 (released Jul 25, 2017) - tentative support for Coq 8.7 - discarded tactic support for Coq 8.4 (proofs still supported) - support for CVC4 1.5 (released Jul 10, 2017) - support for E 2.0 (released Jul 4, 2017) - support for E 1.9.1 (release Aug 31, 2016) The gappalib-coq, frama-c, and why builds are just rebuilds due to the new versions of flocq and why3. -------------------------------------------------------------------------------- ================================================================================ frama-c-15.0-3.fc27 (FEDORA-2017-93d7fb97b0) Framework for source code analysis of C software -------------------------------------------------------------------------------- Update Information: Changes in flocq 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Changes in why3 0.88.0: - two new forms of type declarations: integer range types and floating-point types. To denote constants in such types, integer constants and real constants can be cast to such types. This support is exploited in drivers for provers that support bitvector theories (CVC4, Z3) and floating-point theory (Z3). More details in the manual, section 7.2.4 "Theories". - a quote character (') inside an identifier must either be at the end, or be followed by either a digit, the underscore character (_) or another quote. Identifiers with a quote followed by a letter are reserved. - new theory ieee_float formalizing floating-point arithmetic, compliant to IEEE-754, mapped to SMT-LIB FP theory. - proof strategies: why3 config now generates default proof strategies using the installed provers. These are available under name "Auto level 0", "Auto level 1", and "Auto level 2" in why3 ide. More details in the manual, section 10.6 "Proof Strategies". - counterexamples: better support for array values, support for floating-point values, support for Z3 in addition to CVC4. More details in the manual, section 6.3.5 "Displaying Counterexamples". - support for Isabelle 2017 - discarded support for Isabelle 2016 (2016-1 still supported) - support for Coq 8.6.1 (released Jul 25, 2017) - tentative support for Coq 8.7 - discarded tactic support for Coq 8.4 (proofs still supported) - support for CVC4 1.5 (released Jul 10, 2017) - support for E 2.0 (released Jul 4, 2017) - support for E 1.9.1 (release Aug 31, 2016) The gappalib-coq, frama-c, and why builds are just rebuilds due to the new versions of flocq and why3. -------------------------------------------------------------------------------- ================================================================================ gappalib-coq-1.3.2-10.fc27 (FEDORA-2017-93d7fb97b0) Coq support library for gappa -------------------------------------------------------------------------------- Update Information: Changes in flocq 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Changes in why3 0.88.0: - two new forms of type declarations: integer range types and floating-point types. To denote constants in such types, integer constants and real constants can be cast to such types. This support is exploited in drivers for provers that support bitvector theories (CVC4, Z3) and floating-point theory (Z3). More details in the manual, section 7.2.4 "Theories". - a quote character (') inside an identifier must either be at the end, or be followed by either a digit, the underscore character (_) or another quote. Identifiers with a quote followed by a letter are reserved. - new theory ieee_float formalizing floating-point arithmetic, compliant to IEEE-754, mapped to SMT-LIB FP theory. - proof strategies: why3 config now generates default proof strategies using the installed provers. These are available under name "Auto level 0", "Auto level 1", and "Auto level 2" in why3 ide. More details in the manual, section 10.6 "Proof Strategies". - counterexamples: better support for array values, support for floating-point values, support for Z3 in addition to CVC4. More details in the manual, section 6.3.5 "Displaying Counterexamples". - support for Isabelle 2017 - discarded support for Isabelle 2016 (2016-1 still supported) - support for Coq 8.6.1 (released Jul 25, 2017) - tentative support for Coq 8.7 - discarded tactic support for Coq 8.4 (proofs still supported) - support for CVC4 1.5 (released Jul 10, 2017) - support for E 2.0 (released Jul 4, 2017) - support for E 1.9.1 (release Aug 31, 2016) The gappalib-coq, frama-c, and why builds are just rebuilds due to the new versions of flocq and why3. -------------------------------------------------------------------------------- ================================================================================ glibc-2.26-12.fc27 (FEDORA-2017-0d3fdd3d1f) The GNU libc libraries -------------------------------------------------------------------------------- Update Information: This update adds support for the IBM858 codepage (RHBZ#1416405). It moves the `nss_compat` NSS service module to the main glibc package (RHBZ#1400538). As a security hardening measure, stdio streams are no longer flushed on process abort/assertion failure (RHBZ#1498880). The included upstream update from the glibc 2.26 stable branch improves C++ compatibility for ` <math.h>` functions and fixes a memory leak in malloc when thread local caches are in use. -------------------------------------------------------------------------------- References: [ 1 ] Bug #1498880 - glibc: Do not flush stdio streams on abort, assertion failure https://bugzilla.redhat.com/show_bug.cgi?id=1498880 [ 2 ] Bug #1400538 - glibc: nss_compat should be shipped in the glibc package https://bugzilla.redhat.com/show_bug.cgi?id=1400538 [ 3 ] Bug #1416405 - glibc: add ibm-858 to list of charsets for iconv https://bugzilla.redhat.com/show_bug.cgi?id=1416405 -------------------------------------------------------------------------------- ================================================================================ golang-github-asaskevich-govalidator-7-1.fc27 (FEDORA-2017-607bd90b58) Validators and sanitizers for strings, numerics, slices and structs -------------------------------------------------------------------------------- Update Information: Update to latest upstream release. -------------------------------------------------------------------------------- References: [ 1 ] Bug #1489421 - None https://bugzilla.redhat.com/show_bug.cgi?id=1489421 -------------------------------------------------------------------------------- ================================================================================ libmatroska-1.4.8-1.fc27 (FEDORA-2017-0b5e62b2f7) Open audio/video container format library -------------------------------------------------------------------------------- Update Information: # Version 16.0.0 "Protest" 2017-09-30 ## New features and enhancements * mkvmerge: MP4 reader: added support for Vorbis. Implements #2093. ## Bug fixes * configure: the checks for libEBML and libMatroska have been fixed to require libEBML 1.3.5 and libMatroska 1.4.7 as intended. * mkvmerge: AAC reader: mkvmerge will now emit an error message for AAC files whose header fields imply a sampling frequency or number of channels of 0. See #2107. * mkvmerge: AVC/h.264 ES parser: fixed the calculation of reference information for P and B frames. This also fixes some P frames being marked as B frames and vice versa. * mkvmerge: AVC/h.264 ES parser: only non-key frames that have the NALU header field `nal_ref_idc` set to 0 will be marked as "discardable" in `SimpleBlock` elements. Other half of the fix for #2047. * mkvmerge: HEVC/h.265: the generation of the HEVCC structure stored in `CodecPrivate` was wrong in two places: 1. the position of the number of sub-layers was swapped with reserved bits and 2. the VPS/SPS/PPS/SEI lists did not start with a reserved 1 bit. * mkvmerge: output: the `doc type version` will be set at least to 2 if certain elements are written (`CodecState`, `CueCodecState`, `FlagInterlaced`). * mkvmerge: output: the track header attributes `MinCache` and `MaxCache` will not be written anymore. Fixes #2079. * mkvmerge: Matroska reader: the "key" and "discardable" flags of SimpleBlock elements will be kept as they are. Partial fix for #2047. * mkvmerge: Matroska reader: if present in the file, the "white colour coordinate x" track header attribute was written to both "white colour coordinate x" and "white colour coordinate y" in the output file. * mkvmerge: Opus output: mkvmerge will now put all frames with discard padding into their own block group. Fixes #2100. * MKVToolNix GUI: header editor: removed the check for external modification when saving the file. Fixes #2097. * MKVToolNix GUI: job queue: fixed calculation of total progress when automatic removal of completed is enabled. Fixes #2105. ## Build system changes * libEBML v1.3.5 and libMatroska v1.4.8 are now required. In fact v15.0.0 already requires libEBML v1.3.5 and libMatroska v1.4.7 but did not include proper version checks for them (nor was there a NEWS.md entry for the new libMatroska requirement). New is the requirement for libMatroska v1.4.8 due to it fixing writing block groups for tracks with the track number 128 (see #2103). -------------------------------------------------------------------------------- References: [ 1 ] Bug #1495383 - libmatroska-1.4.8 is available https://bugzilla.redhat.com/show_bug.cgi?id=1495383 [ 2 ] Bug #1497489 - mkvtoolnix-16.0.0 is available https://bugzilla.redhat.com/show_bug.cgi?id=1497489 -------------------------------------------------------------------------------- ================================================================================ libnitrokey-3.0-0.2.20171007git.fa871ec.fc27 (FEDORA-2017-8ad2a60bfc) Communicate with Nitrokey stick devices in a clean and easy manner -------------------------------------------------------------------------------- Update Information: New package -------------------------------------------------------------------------------- References: [ 1 ] Bug #1499408 - Review Request: libnitrokey - Communicate with Nitrokey stick devices in a clean and easy manner https://bugzilla.redhat.com/show_bug.cgi?id=1499408 -------------------------------------------------------------------------------- ================================================================================ mingw-binutils-2.29.1-1.fc27 (FEDORA-2017-c040f0498a) Cross-compiled version of binutils for Win32 and Win64 environments -------------------------------------------------------------------------------- Update Information: MinGW binutils 2.29.1 release. -------------------------------------------------------------------------------- ================================================================================ mingw-openjpeg2-2.3.0-1.fc27 (FEDORA-2017-713916caef) MinGW Windows openjpeg2 library -------------------------------------------------------------------------------- Update Information: Update to version 2.3.0, see https://github.com/uclouvain/openjpeg/blob/v2.3.0/NEWS.md for details. -------------------------------------------------------------------------------- ================================================================================ mkvtoolnix-16.0.0-1.fc27 (FEDORA-2017-0b5e62b2f7) Matroska container manipulation utilities -------------------------------------------------------------------------------- Update Information: # Version 16.0.0 "Protest" 2017-09-30 ## New features and enhancements * mkvmerge: MP4 reader: added support for Vorbis. Implements #2093. ## Bug fixes * configure: the checks for libEBML and libMatroska have been fixed to require libEBML 1.3.5 and libMatroska 1.4.7 as intended. * mkvmerge: AAC reader: mkvmerge will now emit an error message for AAC files whose header fields imply a sampling frequency or number of channels of 0. See #2107. * mkvmerge: AVC/h.264 ES parser: fixed the calculation of reference information for P and B frames. This also fixes some P frames being marked as B frames and vice versa. * mkvmerge: AVC/h.264 ES parser: only non-key frames that have the NALU header field `nal_ref_idc` set to 0 will be marked as "discardable" in `SimpleBlock` elements. Other half of the fix for #2047. * mkvmerge: HEVC/h.265: the generation of the HEVCC structure stored in `CodecPrivate` was wrong in two places: 1. the position of the number of sub-layers was swapped with reserved bits and 2. the VPS/SPS/PPS/SEI lists did not start with a reserved 1 bit. * mkvmerge: output: the `doc type version` will be set at least to 2 if certain elements are written (`CodecState`, `CueCodecState`, `FlagInterlaced`). * mkvmerge: output: the track header attributes `MinCache` and `MaxCache` will not be written anymore. Fixes #2079. * mkvmerge: Matroska reader: the "key" and "discardable" flags of SimpleBlock elements will be kept as they are. Partial fix for #2047. * mkvmerge: Matroska reader: if present in the file, the "white colour coordinate x" track header attribute was written to both "white colour coordinate x" and "white colour coordinate y" in the output file. * mkvmerge: Opus output: mkvmerge will now put all frames with discard padding into their own block group. Fixes #2100. * MKVToolNix GUI: header editor: removed the check for external modification when saving the file. Fixes #2097. * MKVToolNix GUI: job queue: fixed calculation of total progress when automatic removal of completed is enabled. Fixes #2105. ## Build system changes * libEBML v1.3.5 and libMatroska v1.4.8 are now required. In fact v15.0.0 already requires libEBML v1.3.5 and libMatroska v1.4.7 but did not include proper version checks for them (nor was there a NEWS.md entry for the new libMatroska requirement). New is the requirement for libMatroska v1.4.8 due to it fixing writing block groups for tracks with the track number 128 (see #2103). -------------------------------------------------------------------------------- References: [ 1 ] Bug #1495383 - libmatroska-1.4.8 is available https://bugzilla.redhat.com/show_bug.cgi?id=1495383 [ 2 ] Bug #1497489 - mkvtoolnix-16.0.0 is available https://bugzilla.redhat.com/show_bug.cgi?id=1497489 -------------------------------------------------------------------------------- ================================================================================ openjpeg2-2.3.0-1.fc27 (FEDORA-2017-713916caef) C-Library for JPEG 2000 -------------------------------------------------------------------------------- Update Information: Update to version 2.3.0, see https://github.com/uclouvain/openjpeg/blob/v2.3.0/NEWS.md for details. -------------------------------------------------------------------------------- ================================================================================ poppler-0.57.0-3.fc27 (FEDORA-2017-6d59576860) PDF rendering library -------------------------------------------------------------------------------- Update Information: Security fix for CVE-2017-14517, CVE-2017-14518, CVE-2017-14519 and CVE-2017-14929. -------------------------------------------------------------------------------- References: [ 1 ] Bug #1499162 - CVE-2017-14517 poppler: NULL pointer dereference in the XRef::parseEntry() function https://bugzilla.redhat.com/show_bug.cgi?id=1499162 [ 2 ] Bug #1499163 - CVE-2017-14518 poppler: Floating point exception in the isImageInterpolationRequired() function https://bugzilla.redhat.com/show_bug.cgi?id=1499163 [ 3 ] Bug #1499165 - CVE-2017-14519 poppler: Memory corruption via Gfx.cc infinite loop https://bugzilla.redhat.com/show_bug.cgi?id=1499165 [ 4 ] Bug #1499167 - CVE-2017-14929 poppler: Memory corruption via Gfx.cc infinite loop https://bugzilla.redhat.com/show_bug.cgi?id=1499167 -------------------------------------------------------------------------------- ================================================================================ prelude-lml-4.0.0-1.fc27 (FEDORA-2017-5e187b355a) Log analyzer sensor with IDMEF output -------------------------------------------------------------------------------- Update Information: Bump version 4.0.0 -------------------------------------------------------------------------------- ================================================================================ purple-libsteam-1.6.1-17.20170929gitab6d446.fc27 (FEDORA-2017-74be108bbc) Steam plugin for Pidgin/Adium/libpurple -------------------------------------------------------------------------------- Update Information: Upstream changelog: * Added option to redeem Steam game keys to the accounts menu. -------------------------------------------------------------------------------- ================================================================================ python-astropy-2.0.2-1.fc27 (FEDORA-2017-5e692a4b1c) A Community Python Library for Astronomy -------------------------------------------------------------------------------- Update Information: Updated erfa and astropy to latest upstream releases. -------------------------------------------------------------------------------- References: [ 1 ] Bug #1433636 - python-astropy-helpers-2.0.1 is available https://bugzilla.redhat.com/show_bug.cgi?id=1433636 [ 2 ] Bug #1465690 - python-astropy-2.0.2 is available https://bugzilla.redhat.com/show_bug.cgi?id=1465690 -------------------------------------------------------------------------------- ================================================================================ python-astropy-helpers-2.0.1-1.fc27 (FEDORA-2017-5e692a4b1c) Utilities for building and installing Astropy and Astropy affiliated packages -------------------------------------------------------------------------------- Update Information: Updated erfa and astropy to latest upstream releases. -------------------------------------------------------------------------------- References: [ 1 ] Bug #1433636 - python-astropy-helpers-2.0.1 is available https://bugzilla.redhat.com/show_bug.cgi?id=1433636 [ 2 ] Bug #1465690 - python-astropy-2.0.2 is available https://bugzilla.redhat.com/show_bug.cgi?id=1465690 -------------------------------------------------------------------------------- ================================================================================ python-healpy-1.11.0-1.fc27 (FEDORA-2017-3f01936a8b) Python healpix maps tools -------------------------------------------------------------------------------- Update Information: Update to 1.11.0 -------------------------------------------------------------------------------- ================================================================================ qcad-3.18.1.0-2.fc27 (FEDORA-2017-14f4c8d290) Powerful 2D CAD system -------------------------------------------------------------------------------- Update Information: - printsupport/libcupsprintersupport file symlinked (bz#1499418) ---- - Update to 3.18.1.0 -------------------------------------------------------------------------------- References: [ 1 ] Bug #1499418 - Build-id conflicts between qcad and qt5-qtbase-gui packages https://bugzilla.redhat.com/show_bug.cgi?id=1499418 -------------------------------------------------------------------------------- ================================================================================ qt-creator-4.4.1-1.fc27 (FEDORA-2017-d5c7e5705b) Cross-platform IDE for Qt -------------------------------------------------------------------------------- Update Information: Update to version 4.4.1, see http://blog.qt.io/blog/2017/10/06/qt- creator-4-4-1-released/ for details. -------------------------------------------------------------------------------- ================================================================================ qtractor-0.8.4-1.fc27 (FEDORA-2017-02c3eeb617) Audio/MIDI multi-track sequencer -------------------------------------------------------------------------------- Update Information: Update to 0.8.4. Details: https://qtractor.sourceforge.io/qtractor- downloads.html -------------------------------------------------------------------------------- References: [ 1 ] Bug #1492852 - New release (0.8.4) available https://bugzilla.redhat.com/show_bug.cgi?id=1492852 -------------------------------------------------------------------------------- ================================================================================ radicale-2.1.8-2.fc27 (FEDORA-2017-634216e756) A simple CalDAV (calendar) and CardDAV (contact) server -------------------------------------------------------------------------------- Update Information: Run in daemon mode so it creates the PID file -------------------------------------------------------------------------------- ================================================================================ snapd-2.28.1-1.fc27 (FEDORA-2017-85251c9cb1) A transactional software package manager -------------------------------------------------------------------------------- Update Information: Release 2.28.1 to Fedora (RH#1495852) -------------------------------------------------------------------------------- References: [ 1 ] Bug #1495852 - snapd-2.28.1 is available https://bugzilla.redhat.com/show_bug.cgi?id=1495852 [ 2 ] Bug #1492087 - snapd-glib-1.23 is available https://bugzilla.redhat.com/show_bug.cgi?id=1492087 -------------------------------------------------------------------------------- ================================================================================ snapd-glib-1.23-1.fc27 (FEDORA-2017-85251c9cb1) Library providing a GLib interface to snapd -------------------------------------------------------------------------------- Update Information: Release 2.28.1 to Fedora (RH#1495852) -------------------------------------------------------------------------------- References: [ 1 ] Bug #1495852 - snapd-2.28.1 is available https://bugzilla.redhat.com/show_bug.cgi?id=1495852 [ 2 ] Bug #1492087 - snapd-glib-1.23 is available https://bugzilla.redhat.com/show_bug.cgi?id=1492087 -------------------------------------------------------------------------------- ================================================================================ vid.stab-1.1-3.20170830gitafc8ea9.fc27 (FEDORA-2017-e4b6fae7e4) Video stabilize library for fmpeg, mlt or transcode -------------------------------------------------------------------------------- Update Information: - change license tag to GPLv2 - fix warning _FORTIFY_SOURCE requires compiling with optimization (-O) -------------------------------------------------------------------------------- ================================================================================ why-2.39-2.fc27 (FEDORA-2017-93d7fb97b0) Software verification platform -------------------------------------------------------------------------------- Update Information: Changes in flocq 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Changes in why3 0.88.0: - two new forms of type declarations: integer range types and floating-point types. To denote constants in such types, integer constants and real constants can be cast to such types. This support is exploited in drivers for provers that support bitvector theories (CVC4, Z3) and floating-point theory (Z3). More details in the manual, section 7.2.4 "Theories". - a quote character (') inside an identifier must either be at the end, or be followed by either a digit, the underscore character (_) or another quote. Identifiers with a quote followed by a letter are reserved. - new theory ieee_float formalizing floating-point arithmetic, compliant to IEEE-754, mapped to SMT-LIB FP theory. - proof strategies: why3 config now generates default proof strategies using the installed provers. These are available under name "Auto level 0", "Auto level 1", and "Auto level 2" in why3 ide. More details in the manual, section 10.6 "Proof Strategies". - counterexamples: better support for array values, support for floating-point values, support for Z3 in addition to CVC4. More details in the manual, section 6.3.5 "Displaying Counterexamples". - support for Isabelle 2017 - discarded support for Isabelle 2016 (2016-1 still supported) - support for Coq 8.6.1 (released Jul 25, 2017) - tentative support for Coq 8.7 - discarded tactic support for Coq 8.4 (proofs still supported) - support for CVC4 1.5 (released Jul 10, 2017) - support for E 2.0 (released Jul 4, 2017) - support for E 1.9.1 (release Aug 31, 2016) The gappalib-coq, frama-c, and why builds are just rebuilds due to the new versions of flocq and why3. -------------------------------------------------------------------------------- ================================================================================ why3-0.88.0-1.fc27 (FEDORA-2017-93d7fb97b0) Software verification platform -------------------------------------------------------------------------------- Update Information: Changes in flocq 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Changes in why3 0.88.0: - two new forms of type declarations: integer range types and floating-point types. To denote constants in such types, integer constants and real constants can be cast to such types. This support is exploited in drivers for provers that support bitvector theories (CVC4, Z3) and floating-point theory (Z3). More details in the manual, section 7.2.4 "Theories". - a quote character (') inside an identifier must either be at the end, or be followed by either a digit, the underscore character (_) or another quote. Identifiers with a quote followed by a letter are reserved. - new theory ieee_float formalizing floating-point arithmetic, compliant to IEEE-754, mapped to SMT-LIB FP theory. - proof strategies: why3 config now generates default proof strategies using the installed provers. These are available under name "Auto level 0", "Auto level 1", and "Auto level 2" in why3 ide. More details in the manual, section 10.6 "Proof Strategies". - counterexamples: better support for array values, support for floating-point values, support for Z3 in addition to CVC4. More details in the manual, section 6.3.5 "Displaying Counterexamples". - support for Isabelle 2017 - discarded support for Isabelle 2016 (2016-1 still supported) - support for Coq 8.6.1 (released Jul 25, 2017) - tentative support for Coq 8.7 - discarded tactic support for Coq 8.4 (proofs still supported) - support for CVC4 1.5 (released Jul 10, 2017) - support for E 2.0 (released Jul 4, 2017) - support for E 1.9.1 (release Aug 31, 2016) The gappalib-coq, frama-c, and why builds are just rebuilds due to the new versions of flocq and why3. -------------------------------------------------------------------------------- _______________________________________________ test mailing list -- test@xxxxxxxxxxxxxxxxxxxxxxx To unsubscribe send an email to test-leave@xxxxxxxxxxxxxxxxxxxxxxx
