Thu, 08 Dec 2022 00:34:42 UTC

Information for build why-2.26-1.fc13

Package Namewhy
SummarySoftware verification platform
DescriptionWhy 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, Mizar are supported - having one is recommended and Coq is packaged for Fedora) and automated theorem provers (without any extra work, Simplify, Alt-Ergo, Yices, Z3, CVC Lite, Zenon are supported and Zenon is 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). Invoke the Jessie plug-in with: frama-c -jessie FILE.c
Built bydwheeler
State complete
Volume fedora_koji_archive00
StartedMon, 11 Oct 2010 17:41:48 UTC
CompletedMon, 11 Oct 2010 17:48:46 UTC
Taskbuild (dist-f13-updates-candidate, /why:31c88ec25fd629a44737cefa586d64688fed12a0)
why-2.26-1.fc13.src.rpm (info) (download)
why-2.26-1.fc13.i686.rpm (info) (download)
why-all-2.26-1.fc13.i686.rpm (info) (download)
why-coq-2.26-1.fc13.i686.rpm (info) (download)
why-gwhy-2.26-1.fc13.i686.rpm (info) (download)
why-pvs-support-2.26-1.fc13.i686.rpm (info) (download)
why-2.26-1.fc13.x86_64.rpm (info) (download)
why-all-2.26-1.fc13.x86_64.rpm (info) (download)
why-coq-2.26-1.fc13.x86_64.rpm (info) (download)
why-gwhy-2.26-1.fc13.x86_64.rpm (info) (download)
why-pvs-support-2.26-1.fc13.x86_64.rpm (info) (download)
Changelog * Sat Oct 09 2010 David A. Wheeler + Mark Rader <> - 2.26-1 - Upgrade to upstream version 2.26 (inc. update of krakatoa.pdf) - Integrated with Frama-C and PVS (as pvs-sbcl) * Mon Jan 11 2010 Richard W.M. Jones <> - 2.23-2 - Rebuild to fix dependencies. * Fri Jan 08 2010 Alan Dunn <> - 2.23-1 - Upgrade to upstream version 2.23 - Move execstack fixing to spec file from patch - Moved patch descriptions to initial patch declaration as in examples in Fedora documentation - New Caduceus, Krakatoa documentation - Update test result from small test min.mlw - Added CVC3 interfacing capabilities - Removed patch for gwhy configuration, as there is a new mechanism for this * Tue Sep 22 2009 Dennis Gilmore <> - 2.17-5 - Exclude sparc64 s390 s390x there is no ocaml there * Fri Aug 07 2009 Alan Dunn <> - 2.17-4 - Removed now irrelevant check for no OCaml in Fedora < 9 (those distributions are EOL) - Changed ExcludeArch to proper Fedora versions - Builds coq subpackage exactly when Coq can be built, thus making build independent of whether Coq can be built - define -> global - Fixed accidental use of in tar ocamlgraph instead of one that is separately packaged * Mon Jul 27 2009 Fedora Release Engineering <> - 2.17-3 - Rebuilt for * Wed Feb 25 2009 Fedora Release Engineering <> - 2.17-2 - Rebuilt for * Wed Dec 24 2008 Alan Dunn <> 2.17-1 - Upgrade to version 2.17 (bz: 477790) - Add ownership of two directories common with Coq, but neither program requires the other (bz: 474016) - Minor filename change in 2.17 (GPL -> LICENSE) - Added back Coq .v files to match policy for Coq - Changed directory structure re: jessie and krakatoa to match new structure in 2.17 - Minor changes to patches to ensure they still work in 2.17 - Corrected package location gwhy-icon.png (should only be in gwhy) * Tue Aug 05 2008 Alan Dunn <> 2.14-2.1 - ExcludeArch ppc64 on Fedora 8 due to no ocaml. * Fri Aug 01 2008 Alan Dunn <> 2.14-2 - Fixed minor issues in response to package review: - Inclusion of COPYING, GPL license-related files - Added config.mll patch to make default config file created nicer - Changes subpackage dependencies to be fully versioned. - Makes during build allowed to be noisy (allowed to print). * Wed Jul 30 2008 Alan Dunn <> 2.14-1 - Changed to new version of why, removed previous why-cpulimit name change, zenon output format patches as the issues were fixed in why 2.14. - Moved doc subpackage back into main package. - Added example files to documentation subpackage. - Added check section with test on small why file. - Reformatted some macro names for greater readability. * Thu Jul 24 2008 Alan Dunn <> 2.13-2 - Added several patches: fixed Zenon output, completed fix of rename of cpulimit -> why-cpulimit. * Wed Jul 23 2008 Alan Dunn <> 2.13-1 - Initial Fedora RPM version.