Fedora 15 Update: why-2.29-2.fc15

[updates at fedoraproject.org]

--------------------------------------------------------------------------------
Fedora Update Notification
FEDORA-2011-9339
2011-07-15 00:42:01
--------------------------------------------------------------------------------

Name        : why
Product     : Fedora 15
Version     : 2.29
Release     : 2.fc15
URL         : http://why.lri.fr/
Summary     : Software verification platform
Description :
Why is a software verification platform that applies formal proving
tools to annotated programs.  It is currently capable of analysis of C
(through the included tool "Caduceus"), Java (through the included tool
"Krakatoa"), and potentially ML programs with some modification into
Why's own ML-like language.  Furthermore, Why is capable of analysis of
any program that is mapped onto its own internal language.  It uses a
weakest precondition involving calculus to generate potential theorems
necessary for the proof of a program's correctness.  It translates these
theorems into formats that can be used by external proof assistants
(without any extra work Coq, PVS, HOL Light, and Mizar are supported -
having one is recommended and both Coq and PVS are packaged for Fedora)
and automated theorem provers (without any extra work Simplify,
Alt-Ergo, Yices, Z3, CVC3, and Zenon are supported and Alt-Ergo, CVC3,
and Zenon are packaged for Fedora) so that these results can be
externally proven, resulting in a proof of program correctness.

Note: Each user account must be set up by running "why-config" at the
command line (to set up a configuration file).

--------------------------------------------------------------------------------
Update Information:

See http://ocamlgraph.lri.fr/download/CHANGES for the bugs fixed in this version of ocaml-ocamlgraph.

See http://frama-c.com/Changelog.html for the numerous bug fixes and new features in this version of frama-c.

See http://why.lri.fr/download/CHANGES for the bugs fixed and enhancements made to this version of why.

--------------------------------------------------------------------------------
ChangeLog:

* Thu Jul 14 2011 Jerry James <loganjerry at gmail.com> - 2.29-2
- Fix broken conditionals
* Mon Jul 11 2011 Jerry James <loganjerry at gmail.com> - 2.29-1
- New upstream release (fixes FTBFS: bz 715902)
- Remove unnecessary spec file elements (BuildRoot, etc.)
- Update approach to filtering provides and requires
- Add has_pvs analogously to has_coq, and simplify macro usage
- Add (X)Emacs support packages
- New subpackage for the jessie plugin to avoid unowned directories and
  permit a direct dependency on frama-c
- Prepare for the eventual availability of APRON
* Thu Apr 14 2011 Karsten Hopp <karsten at redhat.com> 2.28-2.2
- add ppc to excludearch, too. No pvs-sbcl available there
* Wed Apr 13 2011 Karsten Hopp <karsten at redhat.com> 2.28-2.1
- add ppc64 to excludearch, no sbcl available there
--------------------------------------------------------------------------------
References:

  [ 1 ] Bug #715902 - FTBFS why-2.28-2.fc15
        https://bugzilla.redhat.com/show_bug.cgi?id=715902
--------------------------------------------------------------------------------

This update can be installed with the "yum" update program.  Use 
su -c 'yum update why' at the command line.
For more information, refer to "Managing Software with yum",
available at http://docs.fedoraproject.org/yum/.

All packages are signed with the Fedora Project GPG key.  More details on the
GPG keys used by the Fedora Project can be found at
https://fedoraproject.org/keys
--------------------------------------------------------------------------------