[Bug 456398] Review Request: why - Why software verification platform

Thu Jul 31 03:26:31 UTC 2008

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug report.

Summary: Review Request: why - Why software verification platform

https://bugzilla.redhat.com/show_bug.cgi?id=456398

------- Additional Comments From dwheeler at dwheeler.com  2008-07-30 23:26 EST -------
Okay, I've looked this over, installed on my own system and tested it, etc.
It's generally quite good, but there are a few issues... but I think they'll be
really easy to fix.

* rpmls of each binary package looks fine (permissions reasonable)

- MUST: rpmlint must be run on every package. The output should be posted in the
review.
Ok. No errors, and the warning is a well-known one
that is the fault of the ocaml compiler.  See:
 https://bugzilla.redhat.com/show_bug.cgi?id=450551
 http://caml.inria.fr/mantis/view.php?id=4564
 http://groups.google.com/group/fa.caml/browse_thread/thread/2d247a192eb92826

 But you could do better; apply "execstack -c" to ELF files in /usr/bin,
 and the programs will run without an executable stack.
 That's a better idea; OCaml doesn't actually require an executable stack,
 and the noexec stack will protect the low-level C routines it calls.

$ rpmlint SPECS/why.spec SRPMS/why-2.14-1.fc9.src.rpm \
          RPMS/i386/why-2.14-1.fc9.i386.rpm 
why.i386: W: executable-stack /usr/bin/why-stat
why.i386: W: executable-stack /usr/bin/why2html
why.i386: W: executable-stack /usr/bin/why-dp
why.i386: W: executable-stack /usr/bin/caduceus
why.i386: W: executable-stack /usr/bin/rv_merge
why.i386: W: executable-stack /usr/bin/why
why.i386: W: executable-stack /usr/bin/jessie
why.i386: W: executable-stack /usr/bin/simplify2why
why.i386: W: executable-stack /usr/bin/why-obfuscator
why.i386: W: executable-stack /usr/bin/krakatoa
2 packages and 1 specfiles checked; 0 errors, 10 warnings.

- MUST: The package must be named according to the Package Naming Guidelines
OK.

- MUST: The spec file name must match the base package %{name}, in the format
%{name}.spec unless your package has an exemption on Package Naming Guidelines.
OK

- MUST: The package must meet the Packaging Guidelines.
OK (I didn't see any errors)

- MUST: The package must be licensed with a Fedora approved license and meet the
Licensing Guidelines.
OK (GPLv2)

- MUST: The License field in the package spec file must match the actual license.
Yes; README, INSTALL, and COPYING all quite explicit that it is GPLv2.

- MUST: If (and only if) the source package includes the text of the license(s)
in its own file, then that file, containing the text of the license(s) for the
package must be included in %doc.

FAIL.  At _least_ install file "COPYING" in %doc, and go ahead and include "GPL"
too.

- MUST: The spec file must be written in American English.
OK

- MUST: The spec file for the package MUST be legible. If the reviewer is unable
to read the spec file, it will be impossible to perform a review. Fedora is not
the place for entries into the Obfuscated Code Contest (http://www.ioccc.org/).
OK

- MUST: The sources used to build the package must match the upstream source, as
provided in the spec URL. Reviewers should use md5sum for this task. If no
upstream URL can be specified for this package, please see the Source URL
Guidelines for how to deal with this.
OK

- MUST: The package must successfully compile and build into binary rpms on at
least one supported architecture.
OK

- MUST: If the package does not successfully compile, build or work on an
architecture, then those architectures should be listed in the spec in
ExcludeArch. Each architecture listed in ExcludeArch needs to have a bug filed
in bugzilla, describing the reason that the package does not compile/build/work
on that architecture. The bug number should then be placed in a comment, next to
the corresponding ExcludeArch line. New packages will not have bugzilla entries
during the review process, so they should put this description in the comment
until the package is approved, then file the bugzilla entry, and replace the
long explanation with the bug number. The bug should be marked as blocking one
(or more) of the following bugs to simplify tracking such issues:
FE-ExcludeArch-x86 , FE-ExcludeArch-x64 , FE-ExcludeArch-ppc , FE-ExcludeArch-ppc64
OK

- MUST: All build dependencies must be listed in BuildRequires, except for any
that are listed in the [wiki:Self:Packaging/Guidelines#Exceptions exceptions
section of Packaging Guidelines] ; inclusion of those as BuildRequires is
optional. Apply common sense.
OK (builds in mock)

- MUST: The spec file MUST handle locales properly. This is done by using the
%find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.
OK (No locale issue).

- MUST: Every binary RPM package which stores shared library files (not just
symlinks) in any of the dynamic linker's default paths, must call ldconfig in
%post and %postun....
OK (N/A)

- MUST: If the package is designed to be relocatable...
OK (N/A)

- MUST: A package must own all directories that it creates. If it does not
create a directory that it uses, then it should require a package which does
create that directory. Refer to the Guidelines for examples.
OK

- MUST: A package must not contain any duplicate files in the %files listing.
OK

- MUST: Permissions on files must be set properly. Executables should be set
with executable permissions, for example. Every %files section must include a
%defattr(...) line.
OK.  I checked the permissions on the binary RPMs using rpmls, looks okay.

- MUST: Each package must have a %clean section, which contains rm -rf
%{buildroot} ([wiki:Self:Packaging/Guidelines#UsingBuildRootOptFlags or
$RPM_BUILD_ROOT] ).
OK

- MUST: Each package must consistently use macros, as described in the
[wiki:Self:Packaging/Guidelines#macros macros section of Packaging Guidelines].
OK

- MUST: The package must contain code, or permissable content. This is described
in detail in the [wiki:Self:Packaging/Guidelines#CodeVsContent code vs. content
section of Packaging Guidelines] .
OK

- MUST: Large documentation files should go in a -doc subpackage. (The
definition of large is left up to the packager's best judgement, but is not
restricted to size. Large can refer to either size or quantity)
OK (N/A)

- MUST: If a package includes something as %doc, it must not affect the runtime
of the application. To summarize: If it is in %doc, the program must run
properly if it is not present.
OK

- MUST: Header files must be in a -devel package.
OK (N/A)

- MUST: Static libraries must be in a -static package.
OK (N/A)

- MUST: Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig' (for
directory ownership and usability).
OK (N/A)

- MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1),
then library files that end in .so (without suffix) must go in a -devel package.
OK (N/A)

- MUST: In the vast majority of cases, devel packages must require the base
package using a fully versioned dependency: Requires: %{name} =
%{version}-%{release}
OK (N/A)

- MUST: Packages must NOT contain any .la libtool archives, these should be
removed in the spec.
OK (N/A)

- MUST: Packages containing GUI applications must include a %{name}.desktop
file, and that file must be properly installed with desktop-file-install in the
%install section.
OK (Verified on desktop)

- MUST: Packages must not own files or directories already owned by other
packages. The rule of thumb here is that the first package to be installed
should own the files or directories that other packages may rely upon. This
means, for example, that no package in Fedora should ever share ownership with
any of the files or directories owned by the filesystem or man package. If you
feel that you have a good reason to own a file or directory that another package
owns, then please present that at package review time.
OK.  I don't know how to check that automatically, but a look using rpmls at the
binary files looks okay.

- MUST: At the beginning of %install, each package MUST run rm -rf %{buildroot}
([wiki:Self:Packaging/Guidelines#UsingBuildRootOptFlags or $RPM_BUILD_ROOT] ).
See [wiki:Self:Packaging/Guidelines#PreppingBuildRootForInstall Prepping
BuildRoot For %install] for details.
OK

- MUST: All filenames in rpm packages must be valid UTF-8.
OK.

Serious problems:
* gwhy fails if the .c file isn't in the current directory (home directory if
invoked from the GUI).
* In the Zenity patch, use --file-selection not --entry to get the filename.
That way, people can use a GUI to traverse the directory structure and click on
the right file.

Strongly recommend fixing:
* apply "execstack -c" to ELF files in /usr/bin, as noted above. (But only if
they're ELF, don't do that to bytecode).  That will enable the exec-stack
protection, there's no reason it should be disabled.
* In the description, change "Furthermore, in theory," to just "Furthermore". 
To a lot of people, "in theory" means "not really". Since they've demonstrated
the truth of the claim for 2 rather different languages, I think they've proved
that claim.
* By default gwhy gives a HUGE list of potential provers, even when they aren't
installed.  That's a big pain - you want beginning users to have a reasonable
view when they start!! In the long term, I think upstream should modify gwhy so
that at start-up it detects which provers exist, and only shows the ones that
are installed.  For the short term, can you modify the defaults so that by
default, if the user hasn't made any selections, only Zenon, Ergo, and CVC3 are
shown?

Other suggestions:
* Simplify this comment:
 # Native ocaml builds do not seem to work on ppc64 (not the first
 # package for which this has been true)
 to something shorter like this:
 # Native ocaml builds don't work on ppc64 (many packages have this problem)

* I think you should modify the %files list to use wildcards and %exclude,
instead of (for example) listing every file in /usr/bin.  It would simplify the
%files list greatly.  It would also make updates much easier; if a future
version of the package installs some new files (e.g., in /usr/bin), the spec
file would be more likely to "just work" if it used wildcards.  E.G., I suggest
something like this:
%files
%{_bindir}/*
%exclude %{_bindir}/gwhy*
...
 You must _not_ say "%{bindir}/" (that tries to grab /usr/bin itself), but
%{bindir}/* is fine... and in this case, I think it's preferable.

Zenon doesn't manage to solve many of them, but it at least manages some,
so clearly the basic bug in invoking Zenon has been fixed.

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug, or are watching someone who is.